Software Verification Research Centre
	Department of Computer Science, The University of Queensland


	The Cogito 1 Methods and Tools are available

Cogito is the generic name of the methods and tools focus of the
Software Verification Research Centre (SVRC). It encompasses and
integrates the results of numerous methods, tools and reasoning projects
carried out within the SVRC.  The first iteration of integrated methods
and tools is Cogito 1: it includes the specification language `Sum',
a Repository Manger, a theorem prover `Ergo', several analysis and
translation tools and supporting documentation and educational material.

The specification language Sum is Z-based, extended to facilitate refinement
to code. It is therefore a key component of the Cogito development
methodology.  Sum extends Z with modules, syntactically distinguishes
state and operation schemas, explicitly states operation preconditions,
and partially merges terms and formulae by including boolean as a toolkit 
type. Sum has both an ascii and a graphical syntax, and a pretty printer 
is available for the graphical version which includes mathematical notation.

Refinement from an initial abstract specification through 
more concrete versions towards implementation is performed at the
theory level within Ergo and projected to the
specification level.  The modelling used ensures that these two levels
are close and that type constraints may be imposed at the theory level. 

Sum has an `implementation' subset, known as the intermediate language,
for expressing the final refinement stage prior to translation to an
imperative language.  Translation is automatic, and in the first instance the
imperative language is an Ada subset.  The refinement environment and the
translation to Ada are designed and under construction.)

SVRC is collaborating with industry on two pilot projects
using Cogito 1 tools and methods in industrial applications. These projects
are well underway and have included a two-week course to
external participants on specification and validation using Sum and 
an introduction to the various tools and specification management 
generally. 

There are three main publications: The Cogito Methodology and System [1],
The Cogito Repository Manager [2], and Extending Z with Modules [3].

Cogito 1 currently has the following `products' (* indicates availability via 
FTP):

	A Repository Manager for development tracking and control *
	(also used as a basis for tool integration).

	A Comprehensive Front-End for the analysis of Sum specification *
	(including separate compilation and type-queries).

	A Theorem Prover (Ergo) populated with over 2000 theorems and 
	associated tactics for the analysis of Sum specifications.

	A Translator from Sum specifications to Ergo theories (in alpha test).

	A Lecture Course on Specification Using Sum (250 Slides).

	Exercises on the use of Sum (20 pages) and of solutions (50 pages).

	A Sum language reference manual (100 pages) *.

	A theory reference manual (300 pages).

	Over 80 example Sum specifications *.

The following are due by 31 May:

	A course on formal reasoning and formal validation of specifications.

	A proof obligation generator (for a pre-defined set of validation
	conditions concerning specification well-formedness).

	A fully-populated theory environment (derived theorems regarding 
	properties of the Sum language).

	Case studies on validation and formal proof.

The Ergo theorem prover populated with Sum theories, together with the
theory documentation, case studies and a translator from Sum to Ergo will
become available sometime in June '95.

The semantics of the Sum language is defined by translation to a set of
structures in Ergo based on typed ZFC set theory. All structures in Ergo's
Sum theories are constructed definitionally (and are therefore justified
with respect to the underlying set theory model) rather than axiomatically.
This relies on the ability of Ergo to interpret abstract theories usefully.

Axioms and rules for reasoning about schemas, etc. are being defined and 
justified in terms of the underlying models. This provides a secure
semantics as well as a reasoning environment guaranteed to be 
consistent with the semantics.

SVRC is enthusiastic about the potential impact of this work.
The feedback from Australian Government Organisations and
Industry is very positive.

Over the next few years we will rationalise our position and
explore additions and extensions to our framework; in particular, later
versions will address real-time, concurrency and object-orientation issues.

Feedback on any aspect is welcome.

For more information about Cogito 1, contact the SVRC at: svrc@cs.uq.oz.au.

Cogito 1.0 system and associated (selected) documentation can be
retrieved by anonymous ftp from: ftp.cs.uq.oz.au from the directory 
pub/SVRC/software.

--------
references

[1] Anthony Bloesch, Peter Kearney, Ed Kazmierczak and Owen Traynor, "The 
Cogito Methodology and System", In Proc. Asia Pacific Software Engineering 
Conf., Tokyo, IEEE Press (1994).

[2] Owen Traynor and Anthony Bloesch, "The Cogito Repository Manager", In Proc. 
Asia Pacific Software Engineering Conf., Tokyo, IEEE Press (1994).

[3] Owen Traynor, Peter Kearney, Ed Kazmierczak, Li Wang and Einar Karlsen,
"Extending Z with Modules", In Proc.  ACSC'95 (Australian Computer Science 
Communications, Vol17.1.), (1995).