Presents an overview of the Possum specification animation system and its integration into the Cogito methodology and toolset. Possum allows interpretation (or animation) of specifications written in Sum, the specification language of Cogito. We distinguish two potential uses for Possum and illustrate each of these with an example. The first is the use of Possum for specification verification, where the analysis of properties of specifications by the specification designer is emphasised. The second use is specification validation, where the specification is checked against the informal requirements of the system.

We present an overview of the Possum specification animation system, an addition to the Cogito methodology and toolset. Possum allows interpretation (or animation) of specifications written in SUM, which is the specification language used in Cogito. We give an account of the functionality of Possum, illustrated by some simple examples, and describe the way in which Possum is used in a typical Cogito development. The current capabilities and limitations of Possum are reviewed from a technical perspective and an overview of other systems that support the animation of formal specification languages is presented.

Abstract In many areas of computation and reasoning, the value of an expression may depend on an implicit parameter, which may for example represent a program state, or time, or a possible world. In this paper we describe a formal first order logic which captures a general notion of expressions which depend on an implicit parameter. Both semantics and syntax are discussed. An important application of the logic, used as a running example, is to provide a basis for unifying the Hoare logic of procedural programs with the mathematically powerful techniques of classical logic and set theory. It is, however, beyond the scope of this paper to develop this application fully.