No Cover Image

Conference Paper/Proceeding/Abstract 877 views 63 downloads

Physical Type Tracking through Minimal Source-Code Annotation

Dave Donaghy, Tom Crick Orcid Logo

Proceedings of 14th International Workshop on Automated Verification of Critical Systems

Swansea University Author: Tom Crick Orcid Logo

Abstract

One of many common artefacts of complex software systems that often needs to be tracked through the entirety of the software system is the underlying type to which numerical variables refer. Commonly-used languages used in industry provide complex mechanisms through which general objects are associa...

Full description

Published in: Proceedings of 14th International Workshop on Automated Verification of Critical Systems
ISSN: 0929-0672
Published: Enschede, Netherlands University of Twente 2014
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa43773
Tags: Add Tag
No Tags, Be the first to tag this record!
Abstract: One of many common artefacts of complex software systems that often needs to be tracked through the entirety of the software system is the underlying type to which numerical variables refer. Commonly-used languages used in industry provide complex mechanisms through which general objects are associated to a given type: for example, the class (and template) mechanisms in Python (and C++) are extremely rich mechanisms for the construction of types with almost entirely arbitrary associated operation sets.However, one often deals with software objects that ultimately represent numerical entities corresponding to real-world measurements, even through standardised SI units: metres per second, kilogram metres per second-squared, etc. In such situations, one can be left with insufficient and ineffective type-checking: for example, the C double type will not prevent the erroneous addition of values representing velocity (with SI units metre per second) to values representing mass (SI unit kilogram).We present an addition to the C language, defined through the existing attribute mechanism, that allows automatic control of physical types at compile-time; the only requirement is that individual variables be identified at declaration time with appropriate SI (or similar) units.
Item Description: 14th International Workshop on Automated Verification of Critical Systems (AVoCS'14)
Keywords: Verification, software engineering, type-checking, units, compilers, plug-ins
College: Faculty of Humanities and Social Sciences