Inductive assertions and operational semantics |
| |
Authors: | J Strother Moore |
| |
Affiliation: | (1) Department of Computer Sciences, The University of Texas at Austin, Taylor Hall 2.124 #C0500, 1 University Station, Austin, TX 78712-0233, USA |
| |
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. |
| |
Keywords: | Software verification Theorem proving Verification condition JVM |
本文献已被 SpringerLink 等数据库收录! |
|