Supporting the B-method in PVS: An Approach to the Abstract Machine Notation in Type Theory

Machine Notation in Type Theory C'esar Mu~noz Computer Science Laboratory SRI International 333 Ravenswood Avenue Menlo Park, CA 94025, USA Email: munoz@csl.sri.com Tel: +1 (650) 859-2784, Fax: +1 (650) 859-2844 Abstract The B-method is a state-oriented formal method for software development. It provides a uniform language, namely the Abstract Machine Notation, to specify, design, and implement systems. The underlying logic of the method is a set theory with a first-order predicate calculus. On the other hand, PVS is a specification language integrated with a theorem prover. The logical framework of PVS is a higherorder logic with a type system. PVS does not come with a particular built-in software construction methodology. In this paper we show how the abstract machine notation can be embedded in PVS. The contributions of this work point in two directions. In one sense, the PVS system is enhanced with a methodology for software development and a notation for specifications (those ..