Abstract
This paper shows how classic inductive assertions can be used in conjunction with an operational semantics to prove partial correctness properties of programs. The method imposes only the proof obligations that would be produced by a verification condition generator but does not require the definition of a verification condition generation. The paper focuses on iterative programs but recursive programs are briefly discussed. Assertions are attached to the program by defining a predicate on states. This predicate is then “completed” to an alleged invariant by the definition of a partial function defined in terms of the state transition function of the operational semantics. If this alleged invariant can be proved to be an invariant under the state transition function, it follows that the assertions are true every time they are encountered in execution and thus that the post-condition is true if reached from a state satisfying the pre-condition. But because of the manner in which the alleged invariant is defined, the verification conditions are sufficient to prove invariance. Indeed, the “natural” proof generates as subgoals the classical verification conditions. The invariant function may be thought of as a state-based verification condition generator for the annotated program. The method allows standard inductive assertion style proofs to be constructed directly in an operational semantics setting. The technique is demonstrated by proving the partial correctness of a simple bytecode program with respect to a pre-existing operational model of the Java Virtual Machine.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Boyer, R.S., Moore, J.S.: A Computational Logic Handbook, 2nd edn. Academic Press, New York (1997)
Floyd, R.: Assigning meanings to programs. In: Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics, vol. XIX, pp. 19–32. American Mathematical Society, Providence (1967)
Gloess, P.Y.: Imperative program verification in PVS. Technical Report, École Nationale Supérieure Électronique, Informatique et Radiocommunications de Bordeaux (1999), http://dept-info.labri.u-bordeaux.fr/~gloess/imperative/index.html
Goldstine, H.H., von Neumann, J.: Planning and coding problems for an electronic computing instrument. In: von Neumann, J. (ed.) Collected Works, vol. V, Pergamon Press, Oxford (1961)
Hoare, C.A.R.: An axiomatic basis for computer programming. Comm. ACM 12(10), 576–583 (1969)
Homeier, P., Martin, D.: A mechanically verified verification condition generator. The Computer Journal 38(2), 131–141 (1995)
Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Press, Boston (2000)
King, J.C.: A Program Verifier. PhD thesis, Carnegie-Mellon University (1969)
Lindholm, T., Yellin, F.: The Java Virtual Machine Specification, 2nd edn. Addison-Wesley, Boston (1999)
Manolios, P., Moore, J.S.: Partial functions in ACL2. Technical Report, Computer Sciences, University of Texas at Austin (2001), http://www.cs.utexas.edu/users/moore/publications/defpun/index.html
McCarthy, J.: Towards a mathematical science of computation. In: Proceedings of the Information Processing Cong. 1962, Munich, West Germany, pp. 21–28. North-Holland, Amsterdam (1962)
Moore, J.S.: An NQTHM formalization of a small machine. Technical Report, Computational Logic, Inc. (May 1991), ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/nqthm-1992/examples/basic/smallmachine.events
Moore, J.S.: Inductive assertions and operational semantics – long version. Technical Report, Department of Computer Sciences, University of Texas at Austin (2003), http://www.cs.utexas.edu/users/moore/publications/trecia/index.html
Moore, J.S.: Proving theorems about Java and the JVM with ACL2. In: Broy, M. (ed.) Lecture Notes of the Marktoberdorf 2002 Summer School. LNCS, Springer, Heidelberg (2003), http://www.cs.utexas.edu/users/moore/publications/marktoberdorf-03
Moore, J.S., Porter, G.: The Apprentice challenge. ACM TOPLAS 24(3), 1–24 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Moore, J.S. (2003). Inductive Assertions and Operational Semantics. In: Geist, D., Tronci, E. (eds) Correct Hardware Design and Verification Methods. CHARME 2003. Lecture Notes in Computer Science, vol 2860. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39724-3_27
Download citation
DOI: https://doi.org/10.1007/978-3-540-39724-3_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20363-6
Online ISBN: 978-3-540-39724-3
eBook Packages: Springer Book Archive