Program Design in PVS

Jozef Hooman

June 1996

Abstract prepared for Proceedings Workshop on Tool Support for System Development and Verification, pp. 8.


Hoare triples (precondition, program, postcondition) have been incorporated in the verification system PVS (Prototype Verification System). Two approaches are presented: the conventional one, with a clear distinction between syntax and semantics, and another where programs are identified with their semantics. In the last approach specifications are embedded in the semantic framework, leading to a formalism where specifications and programming constructs can be mixed freely. This framework forms the basis of a formal method for the design of distributed real-time systems.