An integrated set of tools for specifying, coding, and verifying programs written in the Gypsy language, a language similar to Pascal which has both specification and programming features. This methology includes an editor, a specification processor, a verification condition generator, a user-directed theorem prover, and an information flow tool.