The full version of this announcement is 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.
Cogito 1 currently has the following `products':
Cogito 1.0 system and associated (selected) documentation can be retrieved by anonymous ftp .