A Formal Reasoning Environment for Sum---A Z Based Specification Language

Anthony Bloesch
Software Verification Research Center Department of Computer Science, University of Queensland, 4072 Australia.
anthonyb@cs.uq.edu.au.

Edmund Kazmierczak
Software Verification Research Center Department of Computer Science, University of Queensland, 4072 Australia.
eka@cs.uq.edu.au.

Peter Kearney
Software Verification Research Center Department of Computer Science, University of Queensland, 4072 Australia.
pk@cs.uq.edu.au.

John Staples
Software Verification Research Center Department of Computer Science, University of Queensland, 4072 Australia.
staples@cs.uq.edu.au.

Owen Traynor
Software Verification Research Center Department of Computer Science, University of Queensland, 4072 Australia.
owen@cs.uq.edu.au.

Mark Utting
Software Verification Research Center Department of Computer Science, University of Queensland, 4072 Australia.
marku@cs.uq.edu.au.

Abstract

We describe techniques and tools which have been developed to support the modular formal specification language Sum. The mathematical basis for Sum is set theory. The foundation for Sum is the well-known Z specification language with extensions which address current software engineering concerns. In particular, we describe the support available for reasoning about Sum specifications.

Conference Home Page