TY - GEN
T1 - Rule-based analysis of dimensional safety
AU - Chen, Feng
AU - Roşu, Grigore
AU - Venkatesan, Ram Prasad
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2003.
PY - 2003
Y1 - 2003
N2 - Dimensional safety policy checking is an old topic in software analysis concerned with ensuring that programs do not violate basic principles of units of measurement. Scientific and/or navigation software is routinely dimensional and violations of measurement unit safety policies can hide significant domain-specific errors which are hard or impossible to find otherwise. Dimensional analysis of programs written in conventional programming languages is addressed in this paper. We draw general design principles for dimensional analysis tools and then discuss our prototypes, implemented by rewriting, which include both dynamic and static checkers. Our approach is based on assume/assert annotations of code which are properly interpreted by our tools and ignored by standard compilers/interpreters. The output of our prototypes consists of warnings that list those expressions violating the unit safety policy. These prototypes are implemented in the rewriting system Maude.
AB - Dimensional safety policy checking is an old topic in software analysis concerned with ensuring that programs do not violate basic principles of units of measurement. Scientific and/or navigation software is routinely dimensional and violations of measurement unit safety policies can hide significant domain-specific errors which are hard or impossible to find otherwise. Dimensional analysis of programs written in conventional programming languages is addressed in this paper. We draw general design principles for dimensional analysis tools and then discuss our prototypes, implemented by rewriting, which include both dynamic and static checkers. Our approach is based on assume/assert annotations of code which are properly interpreted by our tools and ignored by standard compilers/interpreters. The output of our prototypes consists of warnings that list those expressions violating the unit safety policy. These prototypes are implemented in the rewriting system Maude.
UR - http://www.scopus.com/inward/record.url?scp=84947786679&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84947786679&partnerID=8YFLogxK
U2 - 10.1007/3-540-44881-0_15
DO - 10.1007/3-540-44881-0_15
M3 - Conference contribution
AN - SCOPUS:84947786679
SN - 3540402543
SN - 9783540402541
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 197
EP - 207
BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
A2 - Nieuwenhuis, Robert
PB - Springer
T2 - 14th International Conference on Rewriting Techniques and Applications, RTA 2003
Y2 - 9 June 2003 through 11 June 2003
ER -