Temporal Axiomatization of Program Verification Methods

Abstract

Temporal logic as a descriptive language allows us to formalize our expectations about the time during which a program runs. Since different program verification methods differ in their view of how they consider program execution we can characterize them axiomatically by using temporal logic. In this chapter we give the required characterization for the Floyd-Hoare method, for the method of intermittent assertions introduced by Burstall [1974] and subsequently propagated by Manna, Waldinger [1978], and for the method introduced by Pnueli [1977] . Sain [1986, 1991] study in detail the axiomatic characterization and interrelation of these program verification methods by means of different induction axiom schemas in the scope of her non-standard dynamic logic.