“Practical” should be a word most welcome to formal methodists (out of whose way most software practitioners scurry so as not to get involved in “impractical, highfalutin math”). This paper’s authors show a way forward that renders formal verification less cumbersome, that is, more practical.
The ten-page paper begins with a correct and concise characterization of the Floyd-Hoare style of verification as “setting up a direct compliance argument between an abstract formal specification and a concrete implementation.” The authors point out that such direct compliance of implementation with specification engenders a large number of verification conditions (VCs). Such large numbers of VCs strain mechanized and human-assisted proofs of the VC collections, and can render rigorous verification out of practical reach.
The authors report success in addressing the VC explosion problem by means of moving “the major proof step to a point between two abstract specifications,” namely, the formal requirement/design specification and the implementation specification. In the following sketch of Echo’s flow, prototype verification system (PVS) denotes the specification and verification system of that name, and SPARK annotations denotes the Ada with annotations subset of the full Ada language.
- (1) PVS --> SPARK annotations --> PVS’
- (2) Proof that PVS’ ==> PVS
- (3) Verification that the Ada code (implementation) complies with the SPARK annotations.
Here, --> denotes transformation and ==> denotes implication. There is thus verification of both specification and implementation.
This well-written scientific summary of Echo will convince its readers of Echo’s soundness and promise.
