[T1] ================================================ AMAST Links 02 06

             The Cogito 1 Methods and Tools are available
           Software Verification Research Centre, Queensland

   The full version of this announcement is available at URL:
   http://www.cs.utwente.nl/data/amast/links/v02/i06/full/AC0206T1.txt

  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.
  Cogito 1 currently has the following `products':
 o  A Repository Manager for development tracking and control.
 o  A Comprehensive Front-End for the analysis of Sum specification.
 o  A Theorem Prover (Ergo) populated with over 2000 theorems and 
    associated tactics for the analysis of Sum specifications.
 o  A Translator from Sum specifications to Ergo theories.
 o  A Lecture Course on Specification Using Sum (250 Slides).
 o  Exercises on the use of Sum (20 pages) and of solutions 
 o  A Sum language reference manual (10 pages).
 o  A theory reference manual (300 pages).
  Cogito 1.0 system and associated (selected) documentation can be
retrieved by anonymous ftp from URL:
ftp://ftp.cs.uq.oz.au/pub/SVRC/software