This Article 
 Bibliographic References 
 Add to: 
Engineering a Sound Assertion Semantics for the Verifying Compiler
March/April 2010 (vol. 36 no. 2)
pp. 275-287
Patrice Chalin, Dependable Software Research Group, Concordia University, Montreal
The Verifying Compiler (VC) project is a core component of the Dependable Systems Evolution Grand Challenge. The VC offers the promise of automatically proving that a program or component is correct, where correctness is defined by program assertions. While several VC prototypes exist, all adopt a semantics for assertions that is unsound. This paper presents a consolidation of VC requirements analysis (RA) activities that, in particular, brought us to ask targeted VC customers what kind of semantics they wanted. Taking into account both practitioners' needs and current technological factors, we offer recovery of soundness through an adjusted definition of assertion validity that matches user expectations and can be implemented practically using current prover technology. For decades, there have been debates concerning the most appropriate semantics for program assertions. Our contribution here is unique in that we have applied fundamental software engineering techniques by asking primary stakeholders what they want and, based on this, proposed a means of efficiently realizing the semantics stakeholders want using standard tools and techniques. We describe how support for the new semantics has been added to ESC/Java2, one of the most fully developed VC prototypes. Case studies demonstrate the effectiveness of the new semantics at uncovering previously indiscernible specification errors.

[1] J. Barnes, High Integrity Software: The Spark Approach to Safety and Security. Addison-Wesley, 2003.
[2] M. Barnett, K.R.M. Leino, and W. Schulte, "The Spec# Programming System: An Overview," G. Barthe, L. Burdy, M. Huisman, J.-L. Lanet, and T. Muntean, eds., Proc. Int'l Workshop the Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, Mar. 2004.
[3] C. Barrett and C. Tinelli, "CVC3," Proc. Int'l Conf. Computer Aided Verification, pp. 298-302, 2007.
[4] H. Barringer, J.H. Cheng, and C.B. Jones, "A Logic Covering Undefinedness in Program Proofs," Acta Informatica, vol. 21, no. 3, pp. 251-269, 1984.
[5] S. Berezin, C. Barrett, I. Shikanian, M. Chechik, A. Gurfinkel, and D.L. Dill, "A Practical Approach to Partial Functions in CVC Lite," Electronic Notes in Theoretical Computer Science, vol. 125, no. 3, pp. 13-23, 2005.
[6] J.C. Bicarregui, C.A.R. Hoare, and J.C.P. Woodcock, "The Verified Software Repository: A Step towards the Verifying Compiler," Formal Aspects of Computing, vol. 18, pp. 143-151, 2006.
[7] J. Bloch, Effective Java Programming Language Guide. Addison-Wesley, 2001.
[8] P. Chalin, "Are Practitioners Writing Contracts?" Proc. Rigorous Development of Complex Fault-Tolerant Systems, M. Butler, C.B. Jones, A. Romanovsky, and E. Troubitsyna, eds., pp. 100-113, 2006.
[9] P. Chalin, "Are the Logical Foundations of Verifying Compiler Prototypes Matching User Expectations?" Formal Aspects of Computing, vol. 19, no. 2, pp. 139-158, 2007.
[10] P. Chalin and P.R. James, "Non-Null References by Default in Java: Alleviating the Nullity Annotation Burden," Proc. 21st European Conf. Object-Oriented Programming, pp. 227-247, July/Aug. 2007.
[11] P. Chalin, P.R. James, and G. Karabotsos, "JML4: Towards an Industrial Grade IVE for Java and Next Generation Research Platform for JML," Proc. Int'l Conf. Verified Software: Theories, Tools, Experiments, Oct. 2008.
[12] P. Chalin, P.R. James, and F. Rioux, "Reducing the Use of Nullable Types through Non-Null by Default and Monotonic Non-Null," IET Software J., vol. 2, no. 6, pp. 515-531, 2008.
[13] P. Chalin, J. Kiniry, G.T. Leavens, and E. Poll, "Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2," Proc. Fourth Int'l Symp. Formal Methods for Components and Objects, 2005.
[14] P. Chalin and F. Rioux, "JML Runtime Assertion Checking: Improved Error Reporting and Efficiency Using Strong Validity," Proc. 15th Int'l Symp. Formal Methods, 2008.
[15] M. Chechik, A. Gurfinkel, and B. Devereux, "CChek: A Multi-Valued Model-Checker," Proc. 14th Int'l Conf. Computer Aided Verification, July 2002.
[16] Y. Cheon, "A Runtime Assertion Checker for the Java Modeling Language," PhD thesis, Iowa State Univ., also Technical Report #03-09, Apr. 2003.
[17] Y. Cheon and G.T. Leavens, "A Contextual Interpretation of Undefinedness for Runtime Assertion Checking," Proc. Sixth Int'l Symp. Automated Analysis-Driven Debugging, 2005.
[18] D.R. Cok and J.R. Kiniry, "ESC/Java2: Uniting ESC/Java and JML," Proc. Int'l Workshop the Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, G. Barthe, L. Burdy, M. Huisman, J.-L. Lanet, and T. Muntean, eds., pp. 108-128, Mar. 2004.
[19] D. Crocker, "Safe Object-Oriented Software: The Verified Design-By-Contract Paradigm," Escher Technologies Ltd., 2005.
[20] Á. Darvas, F. Mehta, and A. Rudich, "Efficient Well-Definedness Checking," Proc. Int'l Joint Conf. Automated Reasoning, pp. 100-115, 2008.
[21] K. Devlin, "Why Universities Require Computer Science Students to Take Math," Comm. ACM, vol. 46, no. 9, pp. 36-39, 2003.
[22] M.R. Fish and J.A. Turner, "Understanding the Process of Information Technology Implementation," Proc. Am. Conf. Information Systems, 2002.
[23] C. Flanagan, K.R.M. Leino, M. Lillibridge, G. Nelson, J.B. Saxe, and R. Stata, "Extended Static Checking for Java," Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation, vol. 37, no. 5, pp. 234-245, 2002.
[24] D. Gries and F.B. Schneider, "Avoiding the Undefined by Underspecification," Computer Science Today: Recent Trends and Developments, J.V. Leeuwen, ed., vol. 1000, pp. 366-373, Springer-Verlag, 1995.
[25] J. Grundy, "Predicative Programming—A Survey," Proc. Int'l Conf. Formal Methods in Programming and Their Applications, June/July, 1993.
[26] J.V. Guttag and J.J. Horning, Larch: Languages and Tools for Formal Specification. Springer-Verlag, 1993.
[27] R. Hähnle, "Many-Valued Logic, Partiality, and Abstraction in Formal Specification Languages," Logic J. Interest Group in Pure and Applied Logic, vol. 13, no. 4, pp. 415-433, 2005.
[28] E.C.R. Hehner, "Predicative Programming Part I," Comm. ACM, vol. 27, no. 2, pp. 134-143, 1984.
[29] E.C.R. Hehner, "Predicative Programming Part II," Comm. ACM, vol. 27, no. 2, pp. 144-151, 1984.
[30] Healthcare Information and Management Systems Society (HIMSS) "HealthCare CIO Results: Key Trends Index," Proc. 15th Ann. Leadership Survey, 2004.
[31] C.A.R. Hoare, "The Verifying Compiler: A Grand Challenge for Computing Research," J. ACM, vol. 50, no. 1, pp. 63-69, 2003.
[32] C.A.R. Hoare and J. He, Unifying Theories of Programming. Prentice Hall, 1998.
[33] T. Hoare and J. Misra, "Vision of a Grand Challenge Project," Proc. IFIP Working Conf. Verified Software: Theories, Tools, Experiments, July 2005.
[34] P.R. James and P. Chalin, "Extended Static Checking in JML4: Benefits of Multiple-Prover Support," Proc. ACM Symp. Applied Computing, Software Verification and Testing Track, Mar. 2009.
[35] C. Jones, Applied Software Measurement: Assuring Productivity and Quality, second ed. McGraw Hill, 1996.
[36] C. Jones, P. O'Hearn, and J. Woodcock, "Verified Software: A Grand Challenge," Computer, vol. 39, no. 4, pp. 93-95, Apr. 2006.
[37] C.B. Jones, Systematic Software Development Using VDM, second ed. Prentice Hall, 1990.
[38] C.B. Jones and C.A. Middelburg, "A Typed Logic of Partial Functions Reconstructed Classically," Acta Informatica, vol. 31, no. 5, pp. 399-430, 1994.
[39] J. Kiniry, A. Morkan, and B. Denby, "Soundness and Completeness Warnings in ESC/Java2," Proc. Workshop the Specification and Verification of Component-Based Software, Nov. 2006.
[40] B. Konikowska, "Two over Three: A Two-Valued Logic for Software Specification and Validation over a Three-Valued Predicate Calculus," J. Applied Non-Classical Logics, vol. 3, pp. 39-71, 1993.
[41] B. Konikowska, A. Tarlecki, and A. Blikle, "A Three-Valued Logic for Software Specification and Validation," Fundamenta Informaticae, vol. 14, no. 4, pp. 411-453, 1991.
[42] K.A. Kuhn and D.A. Guise, "From Hospital Information Systems to Health Information Systems: Problems, Challenges, Perspectives," Methods of Information in Medicine, vol. 40, pp. 275-287, 2001.
[43] D. Kulak and E. Guiney, Use Cases: Requirements in Context, second ed. Addison-Wesley, 2003.
[44] P.G. Larsen and N. Plat, "Introduction to Overture," Proc. First Overture Workshop, July 2005.
[45] G.T. Leavens and Y. Cheon, "Design by Contract with JML,", 2006.
[46] 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, vol. 55, nos. 1-3, pp. 185-208, 2005.
[47] G.T. Leavens, K.R.M. Leino, E. Poll, C. Ruby, and B. Jacobs, "JML: Notations and Tools Supporting Detailed Design in Java," Proc. Object-Oriented Systems, Languages and Applications Companion, pp. 105-106, 2000.
[48] G.T. Leavens, E. Poll, C. Clifton, Y. Cheon, C. Ruby, D. Cok, P. Müller, J. Kiniry, and P. Chalin, "JML Reference Manual," http:/, 2006.
[49] G.T. Leavens and J.M. Wing, "Protective Interface Specifications," Formal Aspects of Computing, vol. 10, pp. 59-75, 1998.
[50] D. Leffingwell and D. Widrig, Managing Software Requirements: A Use Case Approach, second ed. Addison-Wesley, 2003.
[51] K.R.M. Leino, "Ecstatic: An Object-Oriented Programming Language with an Axiomatic Semantics," Proc. Fourth Int'l Workshop Foundations of Object-Oriented Languages, Jan. 1997.
[52] K.R.M. Leino, J.B. Saxe, and R. Stata, "Checking Java Programs via Guarded Commands," Technical Note 1999-002, COMPAQ SRC, May 1999.
[53] B. Meyer, "Applying Design by Contract," Computer, vol. 25, no. 10, pp. 40-51, Oct. 1992.
[54] B. Meyer, Object-Oriented Software Construction, second ed. Prentice Hall, 1997.
[55] J.M. Morris, "Non-Deterministic Expressions and Predicate Transformers," Information Processing Letters, vol. 61, no. 5, pp. 241-246, 1997.
[56] P. Müller, A. Poetzsch-Heffter, and G.T. Leavens, "Modular Invariants for Layered Object Structures," Science of Computer Programming, vol. 62, no. 3, pp. 253-286, 2006.
[57] T. Nipkow, L.C. Paulson, and M. Wenzel, Isabelle/HOL—A Proof Assistant for Higher-Order Logic. Springer, 2002.
[58] "Report on the Programming Language Haskell 98, A Non-Strict Purely Functional Language," S. Peyton-Jones, ed., May 2002.
[59] M. Sagiv, T. Reps, and R. Wilhelm, "Parametric Shape Analysis via 3-Valued Logic," ACM Trans. Programming Languages and Systems, vol. 24, no. 3, pp. 217-298, 2002.
[60] C. Sauer, "Deciding the Future for IS Failures: Not the Choice You Might Think," Rethinking Management Information Systems, W. Curie and R. Galliers, eds., pp. 279-309, Oxford Univ. Press, 1999.
[61] SRI Int'l "The PVS Specification and Verification System," http:/, 2009.
[62] Standish Group "CHAOS: A Recipe for Success," The Standish Group Int'l, Inc., 1999.
[63] Standish Group "CHAOS Third Quarter Research Report," The Standish Group Int'l, Inc., 2004.
[64] D.C. Stidolph and J. Whitehead, "Managerial Issues for the Consideration and Use of Formal Methods," Proc. Int'l Symp. Formal Methods Europe, K. Araki, S. Gnesi, and D. Mandrioli, eds., pp. 170-186, 2003.
[65] A. Taylor, "IT Projects: Sink or Swim?" Computer Bull., vol. 42, no. 1, pp. 24-26, 2000.
[66] T. Wilson and S. Maharaj, "Omnibus: A Clean Language for Supporting DBC, ESC and VDBC," Proc. Third Int'l Conf. Software Eng. and Formal Methods, Sept. 2005.
[67] J.M. Wing, "A Two-Tiered Approach to Specifying Programs," Technical Report TR 299, MIT, LCS, 1983.
[68] J.M. Wing, "Writing Larch Interface Language Specifications," ACM Trans. Programming Languages and Systems, vol. 9, no. 1, pp. 1-24, 1987.
[69] G. Winskel, The Formal Semantics of Programming Languages. MIT Press, 1993.
[70] J.C.P. Woodcock, "Dependable Systems Evolution: A Grand Challenge for Computer Science," May 2003.

Index Terms:
Software verification, assertions, programming by contract, logics of programs, requirements engineering.
Patrice Chalin, "Engineering a Sound Assertion Semantics for the Verifying Compiler," IEEE Transactions on Software Engineering, vol. 36, no. 2, pp. 275-287, March-April 2010, doi:10.1109/TSE.2009.59
Usage of this product signifies your acceptance of the Terms of Use.