Conference presentation
Cogito Ergo Sum: providing structured theorem prover support for specification formalisms
Australasian Computer Science Conference (ACSC96), 19th (Melbourne, Australia)
University of Melbourne
1996
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.
Details
- Title
- Cogito Ergo Sum: providing structured theorem prover support for specification formalisms
- Authors
- Ray Nickson (Author) - University of QueenslandOwen Traynor (Author) - University of QueenslandMark Utting (Author) - University of Queensland
- Conference details
- Australasian Computer Science Conference (ACSC96), 19th (Melbourne, Australia)
- Publisher
- University of Melbourne
- Date published
- 1996
- Organisation Unit
- School of Science and Engineering - Legacy; University of the Sunshine Coast, Queensland
- Language
- English
- Record Identifier
- 99449921602621
- Output Type
- Conference presentation
Metrics
888 Record Views