Article

A contextual interpretation of undefinedness for runtime assertion checking

Authors:

Gary T. LeavensAuthors Info & Claims

AADEBUG'05: Proceedings of the sixth international symposium on Automated analysis-driven debugging

Pages 149 - 158

https://doi.org/10.1145/1085130.1085150

Published: 19 September 2005 Publication History

Abstract

Runtime assertion checkers and static checking and verification tools must all cope with the well-known undefinedness problem of logic. This problem is particularly severe for runtime assertion checkers, since, in addition to the possibility of exceptions and errors, runtime assertion checkers must cope with non-executable expressions (such as certain quantified expressions). This paper describes how the runtime assertion checker of the Java Modeling Language (JML) copes with undefinedness.JML is interesting because it attempts to satisfy the needs of a wide range of tools; besides runtime assertion checking, these include static checking tools (like ESC/Java) and static verification tools. These other tools use theorem provers that are based on standard (two-valued) logic and hence use the underspecified total functions semantics for assertions. That semantics validates all the rules of standard logic by substituting an arbitrary value of the appropriate type for each undefined subexpression.JML's runtime assertion checker implements this semantics, and also deals with non-executable expressions, in a way that is both simple and practical. The technique implemented selects a value for undefined subexpressions depending on the context in which the undefinedness occurs.This technique enables JML's runtime assertion checker to be consistent with the other JML tools and to fulfill its role as a practical and effective means of debugging both code and specifications.

References

[1]

D. Bartetzko, C. Fischer, M. Moller, and H. Wehrheim. Jass - Java with assertions. In Workshop on Runtime Verification held in conjunction with the 13th Conference on Computer Aided Verification, CAV'01, 2001. Published in Electronic Notes in Theoretical Computer Science, K. Havelund and G. Rosu (eds.), 55(2), 2001.]]

[2]

J. A. Bergstra and A. Ponse. Kleene's three-valued logic and process algebra. Information Processing Letters, 67(2):95--103, 1998.]]

Digital Library

[3]

A. Blikle. Three-valued predicates for software specification and validation. Fundamenta Informaticae, XIV:387--410, 1991.]]

[4]

L. Burdy, Y. Cheon, D. Cok, M. Ernst, J. Kiniry, G. T. Leavens, K. R. M. Leino, and E. Poll. An overview of {JML tools and applications. International Journal on Software Tools for Technology Transfer (STTT), 7(3):212--232, June 2005.]]

[5]

R. Cattell. The Object Database Standard: ODMG--93. Morgan Kaufmann Publishers, San Mateo, California, 1994.]]

Digital Library

[6]

Y. Cheon. A runtime assertion checker for the {Java Modeling Language. Technical Report 03-09, Department of Computer Science, Iowa State University, Ames, IA, Apr. 2003. The author's Ph.D. dissertation.]]

[7]

Y. Cheon, M. Kim, and A. Perumendla. A complete automation of unit testing for java programs. In H. R. Arabnia and H. Reza, editors, Proceedings of the 2005 International Conference on Software Engineering Research and Practice (SERP '05), Volume I, Las Vegas, Nevada, June 27-29, 2005, pages 290--295. CSREA Press, 2005.]]

[8]

Y. Cheon and G. T. Leavens. A runtime assertion checker for the Java Modeling Language (JML). In H. R. Arabnia and Y. Mun, editors, Proceedings of the International Conference on Software Engineering Research and Practice (SERP '02), Las Vegas, Nevada, USA, June 24-27, 2002, pages 322--328. CSREA Press, June 2002.]]

[9]

Y. Cheon and G. T. Leavens. A simple and practical approach to unit testing: The JML and JUnit way. In B. Magnusson, editor, ECOOP 2002 --- Object-Oriented Programming, 16th European Conference, Máalaga, Spain, Proceedings, volume 2374 of Lecture Notes in Computer Science, pages 231--255, Berlin, June 2002. Springer-Verlag.]]

Digital Library

[10]

Y. Cheon, G. T. Leavens, M. Sitaraman, and S. Edwards. Model variables: Cleanly supporting abstraction in design by contract. Software---Practice and Experience, 35(6):583--599, May 2005.]]

Digital Library

[11]

K. Finney. Mathematical notation in formal specification: Too difficult for the masses? IEEE Transactions on Software Engineering, 22(2):158--159, Feb. 1996.]]

Digital Library

[12]

C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended static checking for Java. In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI'02), volume 37, 5 of SIGPLAN, pages 234--245, New York, June 17--19 2002. ACM Press.]]

Digital Library

[13]

D. Gries and F. B. Schneider. Avoiding the undefined by underspecification. In J. van Leeuwen, editor, Computer Science Today: Recent Trends and Developments, number 1000 in Lecture Notes in Computer Science, pages 366--373. Springer-Verlag, New York, NY, 1995.]]

[14]

B. Jacobs and E. Poll. Java program verification at Nijmegen: Developments and perspective. Technical Report NIII-R0318, Computing Science Institute, University of Nijmegen, 2003.]]

[15]

C. B. Jones. Partial functions and logics: A warning. Inf. Process. Lett., 54(2):65--67, 1995.]]

Digital Library

[16]

C. B. Jones and K. Middelburg. A typed logic of partial functions reconstructed classically. Acta Informatica, 31(5):399--430, 1994.]]

Digital Library

[17]

S. Kent and I. Maung. Quantified Assertions in Eiffel. In Proceedings of TOOLS Pacific 95 (TOOLS 18), pages 349--364. Prentice Hall, November 1995.]]

[18]

B. Konikowska, A. Tarlecki, and A. Blikle. A three-valued logic for software specification and validation. Fundamenta Informaticae, XIV:411--453, 1991.]]

[19]

R. Kramer. iContract -- the Java design by contract tool. TOOLS 26: Technology of Object-Oriented Languages and Systems, Los Alamitos, California, pages 295--307, 1998.]]

Digital Library

[20]

G. T. Leavens and A. L. Baker. Enhancing the pre- and postcondition technique for more expressive specifications. In J. M. Wing, J. Woodcock, and J. Davies, editors, FM'99 --- Formal Methods: World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 1999, Proceedings, volume 1709 of Lecture Notes in Computer Science, pages 1087--1106. Springer-Verlag, 1999.]]

Digital Library

[21]

G. T. Leavens, A. L. Baker, and C. Ruby. Preliminary design of JML: A behavioral interface specification language for Java. Technical Report 98-06-rev28, Iowa State University, Department of Computer Science, July 2005. See www.jmlspecs.org.]]

[22]

G. T. Leavens, Y. Cheon, C. Clifton, C. Ruby, and D. R. Cok. How the design of JML accommodates both runtime assertion checking and formal verification. Science of Computer Programming, 55(1-3):185--208, Mar. 2005.]]

Digital Library

[23]

G. T. Leavens and J. M. Wing. Protective interface specifications. Formal Aspects of Computing, 10:59--75, 1998.]]

[24]

B. Liskov and J. Wing. A behavioral notion of subtyping. ACM Trans. Prog. Lang. Syst., 16(6):1811--1841, Nov. 1994.]]

Digital Library

[25]

B. Meyer. Applying "design by contract". Computer, 25(10):40--51, Oct. 1992.]]

Digital Library

[26]

B. Meyer. Eiffel: The Language. Object-Oriented Series. Prentice Hall, New York, NY, 1992.]]

Digital Library

[27]

B. Meyer. Object-oriented Software Construction. Prentice Hall, New York, NY, second edition, 1997.]]

Digital Library

[28]

D. S. Rosenblum. Towards a method of programming with assertions. In Proceedings of the 14th International Conference on Software Engineering, pages 92--104, May 1992.]]

Digital Library

[29]

B. Schieder and M. Broy. Adapting calculational logic to the undefined. The Computer Journal, 5(2):73--81, Feb. 1999.]]

[30]

Sun Microsystems, Inc. A simple assertion facility for the java programming language. Available from http://java.sun.com/docs/books/jls/assert-spec.html (Date retrieved: April 2, 2003).]]

Cited By

Petiot GBotella BJulliand JKosmatov NSignoles J(2014)Instrumentation of Annotated C Programs for Test GenerationProceedings of the 2014 IEEE 14th International Working Conference on Source Code Analysis and Manipulation10.1109/SCAM.2014.19(105-114)Online publication date: 28-Sep-2014
https://dl.acm.org/doi/10.1109/SCAM.2014.19
Hatcliff JLeavens GLeino KMüller PParkinson M(2012)Behavioral interface specification languagesACM Computing Surveys10.1145/2187671.218767844:3(1-58)Online publication date: 14-Jun-2012
https://dl.acm.org/doi/10.1145/2187671.2187678
Garcia ARomanovsky AIssarny V(2010)Guest Editors' Introduction to the Special Section on Exception HandlingIEEE Transactions on Software Engineering10.1109/TSE.2010.4536:2(147-149)Online publication date: 1-Mar-2010
https://dl.acm.org/doi/10.1109/TSE.2010.45
Show More Cited By

Index Terms

A contextual interpretation of undefinedness for runtime assertion checking

Recommendations

How the design of JML accommodates both runtime assertion checking and formal verification
Formal methods for components and objects pragmatic aspects and applications

Specifications that are used in detailed design and in the documentation of existing code are primarily written and read by programmers. However, most formal specification languages either make heavy use of symbolic mathematical operators, which ...
Ortac: Runtime Assertion Checking for OCaml (Tool Paper)
Runtime Verification
Abstract
Runtime assertion checking (RAC) is a convenient set of techniques that lets developers abstract away the process of verifying the correctness of their programs by writing formal specifications and automating their verification at runtime.
In this ...
The e-ACSL perspective on runtime assertion checking
VORTEX 2021: Proceedings of the 5th ACM International Workshop on Verification and mOnitoring at Runtime EXecution

Runtime Assertion Checking (RAC) is the discipline of verifying program assertions at runtime, i.e. when executing the code. Nowadays, RAC usually relies on Behavioral Interface Specification Languages (BISL) à la Eiffel for writing powerful code ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

AADEBUG'05: Proceedings of the sixth international symposium on Automated analysis-driven debugging

September 2005

172 pages

ISBN:1595930507

DOI:10.1145/1085130

General Chair:
Clinton Jeffery
New Mexico State University, USA
,
Program Chairs:
Jong-Deok Choi
IBM T.J. Watson Research Center, USA
,
Raimondas Lencevicius
Nokia Research Center, USA

Copyright © 2005 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 19 September 2005

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

AADEBUG05

Sponsor:

AADEBUG05: AADEBUG '05 - Sixth International Symposium on Automated and Analysis Driven Debugging

September 19 - 21, 2005

California, Monterey, USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
195
Total Downloads

Downloads (Last 12 months)1
Downloads (Last 6 weeks)0

Reflects downloads up to 15 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Petiot GBotella BJulliand JKosmatov NSignoles J(2014)Instrumentation of Annotated C Programs for Test GenerationProceedings of the 2014 IEEE 14th International Working Conference on Source Code Analysis and Manipulation10.1109/SCAM.2014.19(105-114)Online publication date: 28-Sep-2014
https://dl.acm.org/doi/10.1109/SCAM.2014.19
Hatcliff JLeavens GLeino KMüller PParkinson M(2012)Behavioral interface specification languagesACM Computing Surveys10.1145/2187671.218767844:3(1-58)Online publication date: 14-Jun-2012
https://dl.acm.org/doi/10.1145/2187671.2187678
Garcia ARomanovsky AIssarny V(2010)Guest Editors' Introduction to the Special Section on Exception HandlingIEEE Transactions on Software Engineering10.1109/TSE.2010.4536:2(147-149)Online publication date: 1-Mar-2010
https://dl.acm.org/doi/10.1109/TSE.2010.45
Chalin P(2010)Engineering a Sound Assertion Semantics for the Verifying CompilerIEEE Transactions on Software Engineering10.1109/TSE.2009.5936:2(275-287)Online publication date: 1-Mar-2010
https://dl.acm.org/doi/10.1109/TSE.2009.59
Kim MCheon Y(2008)A Fitness Function to Find Feasible Sequences of Method Calls for Evolutionary Testing of Object-Oriented ProgramsProceedings of the 2008 International Conference on Software Testing, Verification, and Validation10.1109/ICST.2008.31(537-540)Online publication date: 9-Apr-2008
https://dl.acm.org/doi/10.1109/ICST.2008.31
Chalin PRioux F(2008)JML Runtime Assertion CheckingProceedings of the 15th international symposium on Formal Methods10.1007/978-3-540-68237-0_18(246-261)Online publication date: 26-May-2008
https://dl.acm.org/doi/10.1007/978-3-540-68237-0_18
Leavens GBaker ARuby C(2006)Preliminary design of JMLACM SIGSOFT Software Engineering Notes10.1145/1127878.112788431:3(1-38)Online publication date: 1-May-2006
https://dl.acm.org/doi/10.1145/1127878.1127884

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents