The B-method is a state-oriented formal method for software development. It provides a uniform language, 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 higher-order logic with a type system. PVS does not come with a particular built-in software construction methodology. We show how the abstract machine notation of the B-method can be supported by PVS. We advocate a shallow embedding, but rather than translate the abstract machine notation in PVS, we add the notation as a layer over the PVS language. The embedding has been fully implemented in a front-end tool called PBS.

• csl-99-1.ps