Cogito Ergo Sum - providing structured theorem prover support for specification formalisms


Ray Nickson, Owen Traynor and Mark Utting
Software Varification Research Centre Department of Computer Science, The University of Queensland Qld. 4072 Australia
{nickson, owen, marku}@cs.uq.oz.au


Abstract

The Cogito 1 system provides comprehensive reasoning and development support for modular Z specifications. A key issue in the evolution of Cogito has been the provision of reasoning support for the specification language Sum. The theorem prover Ergo is used to support reasoning about Sum specifications. This paper discusses the demands that specification lan guages typically put on reasoning support systems, spe cifically with reference to specification languages that support modular specification and parameterisation. The Ergo theorem prover has evolved significantly over the past 2 years, mainly to provide more sophisticated support for reasoning about (Sum) specifications. These extensions to Ergo are summarised and it is shown how they provide generic support for reasoning about specification formalisms.
Conference Home Page