Procedural Axiomatization in Program Verification

The goal of the paper is to emphasize the connection between languages and program verification techniques, such as Floyd's inductive assertions and Topor's virtual programs, which are based on symbolic execution. The paper claims the opportunity of having an "executable" specification language, i.e. of having a procedural representation of both the assertions, and the simplification rules and axioms. The paper describes a predicate logic functional specification language with an efficient symbolic interpreter. The interpreter can deterministically execute axioms which express functions as well as function properties, thus reducing most of the burden of theorem proving.