Skip to main content
SpringerLink
Log in

Rule-Based Analysis of Dimensional Safety

  • Conference paper
  • First Online:
Rewriting Techniques and Applications (RTA 2003)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2706))

Included in the following conference series:

Abstract

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.

This work is supported by joint NSF/NASA grant CCR-0234524.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. GNU BC. URL: http://www.gnu.org/software/bc/bc.html.

  2. J. Bergstra and J.V. Tucker. Equational specifications, complete rewriting systems, and computable and semicomputable algebras. JACM, 42(6):1194–1230, 1995.

    Article  MATH  MathSciNet  Google Scholar 

  3. P. Borovanský, H. Cîrstea, H. Dubois, C. Kirchner, H. Kirchner, P.-E. Moreau, C. Ringeissen, and M. Vittek. ELAN. User manual — http://www.loria.fr.

  4. M. Broy, M. Wirsing, and P. Pepper. On the algebraic definition of programming languages. ACM Trans. on Prog. Lang. and Systems, 9(1):54–99, January 1987.

    Article  MATH  Google Scholar 

  5. T. Cheatham. Handling fractions and n-tuples in algebraic languages. Presented at the 15th ACM Annual Meeting, Aug. 1960.

    Google Scholar 

  6. M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and J. Quesada. Maude: spec. and progr. in rewriting logic. J. of TCS, 285(2):187–243, 2002.

    Article  MATH  Google Scholar 

  7. Compaq. ESC for Java, 2000. URL: http://www.research.compaq.com/SRC/esc.

  8. R. Diaconescu and K. Futatsugi. CafeOBJ Report: The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification. World Scientific, 1998. AMAST Series in Computing, volume 6.

    Google Scholar 

  9. A. Dreiheller, M. Moerschbacher, and B. Mohr. Physcal — programming Pascal with physical units. ACM SIGPLAN Notices, 21(12):114–123, December 1986.

    Article  Google Scholar 

  10. N. Gehani. Units of measure as a data attribute. Comp. Lang., 2:93–111, 1977.

    Article  MATH  Google Scholar 

  11. N. H. Gehani. Ada’s derived types and units of measure. Software: Practice and Experience, 15(6):555–569, June 1985.

    Article  Google Scholar 

  12. J. Goguen and G. Malcolm. Alg. Semantics of Imperative Programs. MIT, 1996.

    Google Scholar 

  13. J. Goguen, T. Winkler, J. Meseguer, K. Futatsugi, and J.-P. Jouannaud. Introducing OBJ. In Software Eng. with OBJ: Alg. spec. in action. Kluwer, 2000.

    Google Scholar 

  14. I. J. Hayes and B. P. Mahony. Units of measurement in formal specifications. Technical report, SVR Centre, University of Queensland, November 1994.

    Google Scholar 

  15. P. N. Hilfinger. An Ada package for dimensional analysis. ACM Transactions on Programming Languages and Systems, 10(2):189–203, April 1988.

    Article  Google Scholar 

  16. R. T. House. A proposal for the extended form of type checking of expressions. The Computer Journal, 26(4):366–374, 1983.

    MATH  Google Scholar 

  17. M. Karr and D. B. Loveman III. Incorporation of units into programming languages. Communications of the ACM, 21(5):385–391, May 1978.

    Article  Google Scholar 

  18. A. J. Kennedy. Relational parametricity and units of measure. In POPL’97. ACM.

    Google Scholar 

  19. A. J. Kennedy. Programming Languages and Dimensions. PhD thesis, St. Catherine’s College, University of Cambridge, November 1995.

    Google Scholar 

  20. G. W. Macpherson. A reusable ada package for scientific dimensional integrity. ACM Ada Letters, XVI(3):56–69, 1996.

    Article  MathSciNet  Google Scholar 

  21. R. Milner. A theory of type polymorphism in programming languages. Journal of Computer and System Sciences, 17:348–375, 1978.

    Article  MATH  MathSciNet  Google Scholar 

  22. Peter G. Neumann. Letter from the editor — risks to the public. ACM SIGSOFT Software Engineering Notes, 10(3):10, July 1985.

    Google Scholar 

  23. M. Odersky and K. Läufer. Putting type annotations to work. TR, Newton Institute Workshop on Advances in Type Systems for Comp., Cambridge, 1995.

    Google Scholar 

  24. Mars Climate Orbiter. URL: http://mars.jpl.nasa.gov/msp98/orbiter.

  25. M. Rittri. Dimensional inference under polymorphic recursion. In Functional Programming Languages and Computer Architecture, 7th Conference. ACM, 1995.

    Google Scholar 

  26. M. Wand. First-order identities as a defining language. Acta Inf. (14), 1980.

    Google Scholar 

  27. Z. Yang. Encoding types in ML-like languages. In ICPF 98. ACM, 1998.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Illinois at Urbana, Champaign, USA

    Feng Chen, Grigore Roşu & Ram Prasad Venkatesan

Authors
  1. Feng Chen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Grigore Roşu
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Ram Prasad Venkatesan
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dpt. Lenguajes y Sistemas Informáticos (LSI), Technical University of Catalonia (UPC), Jordi Girona 1, 08034, Barcelona, Spain

    Robert Nieuwenhuis

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Chen, F., Roşu, G., Venkatesan, R.P. (2003). Rule-Based Analysis of Dimensional Safety. In: Nieuwenhuis, R. (eds) Rewriting Techniques and Applications. RTA 2003. Lecture Notes in Computer Science, vol 2706. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44881-0_15

Download citation

  • DOI: https://doi.org/10.1007/3-540-44881-0_15

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-40254-1

  • Online ISBN: 978-3-540-44881-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation