Inductive assertions and operational semantics
Author: Moore, J.
Source: International Journal on Software Tools for Technology Transfer, Volume 8, Numbers 4-5, August 2006 , pp. 359-371(13)
Abstract:This paper shows how classic inductive assertions can be used in conjunction with a formal 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 generator. All that is required is a theorem prover, a formal operational semantics, and the object program with appropriate assertions at user-selected cut points. The verification conditions are generated in the course of the theorem-proving process by straightforward symbolic evaluation of the formal operational semantics. The technique is demonstrated by proving the partial correctness of simple bytecode programs with respect to a preexisting operational model of the Java Virtual Machine.
Document Type: Research Article
Affiliations: Email: Moore@cs.utexas.edu
Publication date: August 1, 2006