Conference Paper/Proceeding/Abstract 988 views 87 downloads
Physical Type Tracking through Minimal Source-Code Annotation
Proceedings of 14th International Workshop on Automated Verification of Critical Systems
Swansea University Author: Tom Crick
-
PDF | Accepted Manuscript
Download (122.23KB)
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...
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 |
2023-01-11T14:20:31Z |
id |
cronfa43773 |
recordtype |
SURis |
fullrecord |
<?xml version="1.0"?><rfc1807><datestamp>2022-12-18T17:45:21.0692887</datestamp><bib-version>v2</bib-version><id>43773</id><entry>2018-09-12</entry><title>Physical Type Tracking through Minimal Source-Code Annotation</title><swanseaauthors><author><sid>200c66ef0fc55391f736f6e926fb4b99</sid><ORCID>0000-0001-5196-9389</ORCID><firstname>Tom</firstname><surname>Crick</surname><name>Tom Crick</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><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 Paper/Proceeding/Abstract</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/><url/><notes>14th International Workshop on Automated Verification of Critical Systems (AVoCS'14)</notes><college>COLLEGE NANME</college><department>Education</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>EDUC</DepartmentCode><institution>Swansea University</institution><apcterm/><funders/><projectreference/><lastEdited>2022-12-18T17:45:21.0692887</lastEdited><Created>2018-09-12T06:00:44.0394759</Created><path><level id="1">Faculty of Humanities and Social Sciences</level><level id="2">School of Social Sciences - Education and Childhood Studies</level></path><authors><author><firstname>Dave</firstname><surname>Donaghy</surname><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:19.4970000</uploaded><type>Output</type><contentLength>90974</contentLength><contentType>application/pdf</contentType><version>Accepted Manuscript</version><cronfaStatus>true</cronfaStatus><embargoDate>2018-09-12T00:00:00.0000000</embargoDate><copyrightCorrect>true</copyrightCorrect><language>eng</language></document></documents><OutputDurs/></rfc1807> |
spelling |
2022-12-18T17:45:21.0692887 v2 43773 2018-09-12 Physical Type Tracking through Minimal Source-Code Annotation 200c66ef0fc55391f736f6e926fb4b99 0000-0001-5196-9389 Tom Crick Tom Crick true false 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 Paper/Proceeding/Abstract 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 NANME Education COLLEGE CODE EDUC Swansea University 2022-12-18T17:45:21.0692887 2018-09-12T06:00:44.0394759 Faculty of Humanities and Social Sciences School of Social Sciences - Education and Childhood Studies Dave Donaghy 1 Tom Crick 0000-0001-5196-9389 2 0043773-12092018060219.pdf type-tracking-submission31.pdf 2018-09-12T06:02:19.4970000 Output 90974 application/pdf Accepted Manuscript true 2018-09-12T00:00:00.0000000 true eng |
title |
Physical Type Tracking through Minimal Source-Code Annotation |
spellingShingle |
Physical Type Tracking through Minimal Source-Code Annotation Tom Crick |
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_***_Tom Crick |
author |
Tom Crick |
author2 |
Dave Donaghy Tom Crick |
format |
Conference Paper/Proceeding/Abstract |
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 |
Faculty of Humanities and Social Sciences |
hierarchytype |
|
hierarchy_top_id |
facultyofhumanitiesandsocialsciences |
hierarchy_top_title |
Faculty of Humanities and Social Sciences |
hierarchy_parent_id |
facultyofhumanitiesandsocialsciences |
hierarchy_parent_title |
Faculty of Humanities and Social Sciences |
department_str |
School of Social Sciences - Education and Childhood Studies{{{_:::_}}}Faculty of Humanities and Social Sciences{{{_:::_}}}School of Social Sciences - Education and Childhood Studies |
document_store_str |
1 |
active_str |
0 |
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-24T03:55:07Z |
_version_ |
1763752759429955584 |
score |
11.030209 |