Interfacing program construction and verification

Math¿pad is a document preparation system designed and developed by the authors and oriented towards the calculational construction of programs. PVS (Prototype Verification System) is a theorem checker developed at SRI that has been extensively used for verifying software, in particular in safety-critical applications. This paper describes how these two systems have been combined into one. We discuss the potential benefits of the combination seen from the viewpoint of someone wanting to use formal methods for the construction of computer programs, and we discuss the architecture of the combined system for the benefit of anyone wanting to investigate combining the Math¿pad system with other programming tools