No Cover Image

Conference contribution 17 views 2 downloads

Physical Type Tracking through Minimal Source-Code Annotation / Dave Donaghy; Tom Crick

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

Swansea University Author: Crick, Tom

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!
first_indexed 2018-09-12T12:59:42Z
last_indexed 2018-10-15T19:18:02Z
id cronfa43773
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2018-10-15T14:50:05Z</datestamp><bib-version>v2</bib-version><id>43773</id><entry>2018-09-12</entry><title>Physical Type Tracking through Minimal Source-Code Annotation</title><alternativeTitle></alternativeTitle><author>Tom Crick</author><firstname>Tom</firstname><surname>Crick</surname><active>true</active><ORCID>0000-0001-5196-9389</ORCID><ethesisStudent>false</ethesisStudent><sid>200c66ef0fc55391f736f6e926fb4b99</sid><email>9971fd6d74987b78a0d7fce128f8c721</email><emailaddr>z93Ri4T5hwMLTfh+6XG11n2HZhUyFASdV1DFdgIIhKs=</emailaddr><date>2018-09-12</date><deptcode>EDUC</deptcode><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.</abstract><type>Conference contribution</type><journal>Proceedings of 14th International Workshop on Automated Verification of Critical Systems</journal><volume/><journalNumber/><paginationStart/><paginationEnd/><publisher>University of Twente</publisher><placeOfPublication>Enschede, Netherlands</placeOfPublication><isbnPrint/><isbnElectronic/><issnPrint/><issnElectronic>0929-0672</issnElectronic><keywords>Verification, software engineering, type-checking, units, compilers, plug-ins</keywords><publishedDay>24</publishedDay><publishedMonth>9</publishedMonth><publishedYear>2014</publishedYear><publishedDate>2014-09-24</publishedDate><doi></doi><url></url><notes>14th International Workshop on Automated Verification of Critical Systems (AVoCS'14)</notes><college>College of Arts and Humanities</college><department>School of Education</department><CollegeCode>CAAH</CollegeCode><DepartmentCode>EDUC</DepartmentCode><institution/><researchGroup>None</researchGroup><supervisor/><sponsorsfunders/><grantnumber/><degreelevel/><degreename>None</degreename><lastEdited>2018-10-15T14:50:05Z</lastEdited><Created>2018-09-12T06:00:44Z</Created><path><level id="1">College of Arts and Humanities</level><level id="2">College of Arts and Humanities</level></path><authors><author><firstname>Dave</firstname><surname>Donaghy</surname><orcid/><order>1</order></author><author><firstname>Tom</firstname><surname>Crick</surname><orcid>0000-0001-5196-9389</orcid><order>2</order></author></authors><documents><document><filename>0043773-12092018060219.pdf</filename><originalFilename>type-tracking-submission31.pdf</originalFilename><uploaded>2018-09-12T06:02:19Z</uploaded><type>Output</type><contentLength>90974</contentLength><contentType>application/pdf</contentType><version>AM</version><cronfaStatus>true</cronfaStatus><action>Updated Copyright</action><actionDate>15/10/2018</actionDate><embargoDate>2018-09-12T00:00:00</embargoDate><documentNotes/><copyrightCorrect>true</copyrightCorrect><language>eng</language></document></documents></rfc1807>
spelling 2018-10-15T14:50:05Z v2 43773 2018-09-12 Physical Type Tracking through Minimal Source-Code Annotation Tom Crick Tom Crick true 0000-0001-5196-9389 false 200c66ef0fc55391f736f6e926fb4b99 9971fd6d74987b78a0d7fce128f8c721 z93Ri4T5hwMLTfh+6XG11n2HZhUyFASdV1DFdgIIhKs= 2018-09-12 EDUC 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. Conference contribution Proceedings of 14th International Workshop on Automated Verification of Critical Systems University of Twente Enschede, Netherlands 0929-0672 Verification, software engineering, type-checking, units, compilers, plug-ins 24 9 2014 2014-09-24 14th International Workshop on Automated Verification of Critical Systems (AVoCS'14) College of Arts and Humanities School of Education CAAH EDUC None None 2018-10-15T14:50:05Z 2018-09-12T06:00:44Z College of Arts and Humanities College of Arts and Humanities Dave Donaghy 1 Tom Crick 0000-0001-5196-9389 2 0043773-12092018060219.pdf type-tracking-submission31.pdf 2018-09-12T06:02:19Z Output 90974 application/pdf AM true Updated Copyright 15/10/2018 2018-09-12T00:00:00 true eng
title Physical Type Tracking through Minimal Source-Code Annotation
spellingShingle Physical Type Tracking through Minimal Source-Code Annotation
Crick, Tom
title_short Physical Type Tracking through Minimal Source-Code Annotation
title_full Physical Type Tracking through Minimal Source-Code Annotation
title_fullStr Physical Type Tracking through Minimal Source-Code Annotation
title_full_unstemmed Physical Type Tracking through Minimal Source-Code Annotation
title_sort Physical Type Tracking through Minimal Source-Code Annotation
author_id_str_mv 200c66ef0fc55391f736f6e926fb4b99
author_id_fullname_str_mv 200c66ef0fc55391f736f6e926fb4b99_***_Crick, Tom
author Crick, Tom
author2 Dave Donaghy
Tom Crick
format Conference contribution
container_title Proceedings of 14th International Workshop on Automated Verification of Critical Systems
publishDate 2014
institution Swansea University
issn 0929-0672
publisher University of Twente
college_str College of Arts and Humanities
hierarchytype
hierarchy_top_id collegeofartsandhumanities
hierarchy_top_title College of Arts and Humanities
hierarchy_parent_id collegeofartsandhumanities
hierarchy_parent_title College of Arts and Humanities
department_str College of Arts and Humanities{{{_:::_}}}College of Arts and Humanities{{{_:::_}}}College of Arts and Humanities
document_store_str 1
active_str 1
description 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.
published_date 2014-09-24T12:13:08Z
_version_ 1634049236408467456
score 11.317979