Invariant-based programming is a correct-by-construction approach to program development in which the invariants of a program are written before the actual code. Socos is an environment for graphically constructing invariant-based programs (as statechart-like diagrams) and verifying their correctness (by invoking an automatic theorem prover). It borrows the specification language, logical framework and proof tactics from the PVS system. In this paper, we describe an extension to Socos for animating invariant-based programs in the logical framework of PVS. An invariant-based program is represented as an abstract datatype encoding the program state coupled a small-step state transition function encoding the operational semantics of the program. Socos visualizes the execution, allowing the user to inspect the current state and identify invalid assertions through test cases. Since programs are executed within the theorem prover framework (rather than translated into another language or compiled to machine code), failed test cases are logically sound refutations of the verification conditions. Invariants not executable in the general (e.g., containing unbounded quantification) can be handled for bounded test cases by introducing custom evaluation functions. While such functions provide no correctness guarantees, they can increase the assurance of a correctness condition before doing the actual proof. We illustrate this workflow through a verification exercise with non-trivial verification conditions, arguing that animation of invariant diagrams serves as an important stepping stone towards a fully verified program.
原文链接
分享
引用
