Program Design in PVS
Jozef Hooman
June 1996
Abstract prepared for Proceedings Workshop on Tool Support for System
Development and Verification, pp. 8.
ABSTRACT
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.
Postscript