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