[Savannah-hackers] savannah.gnu.org: submission of The Ebba toolset

[gaia]

A package was submitted to savannah.gnu.org.
This mail was sent to address@hidden, address@hidden


Antti-Juhani Kaijanaho <address@hidden> described the package as follows:
License: gpl
Other License: 
Package: The Ebba toolset
System name: ebba
This package does NOT want to apply for inclusion in the GNU project

This project is building a toolset for a formal method which resembles 
Jean-Raymond Abrial\'s B-Method very much.  When completed, it will be able to 
parse, typecheck and formally verify the correctness of formal specifications, 
refinements and implementations written in the language of the method, and also 
generate compilable or executable code from those implementations. 
Additionally, it may do other useful stuff (such as prettyprinting) to them.

The method is based on a typed, restricted variant of the ZFC set theory and on 
generalized substitution theory, which is a variant of Dijkstra\'s guarded 
command language. It includes a theory of refinement, which is used in 
verifying the correctness of refinements and implementations with respect to 
the original specification. The method is related to the Z notation, but covers 
a much wider area (while Z covers only the specification phase, B can be used 
from specification to implementation). The B-Method has been applied to several 
real-life problems where correctness of the program is important.

See http://www.afm.sbu.ac.uk/b/ for information on the B-Method.

It does not exist yet but I\'m working on it.  It\'s getting very near a point 
where I can make it public.