[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Savannah-hackers] submission of The Ebba toolset

From: gaia
Subject: [Savannah-hackers] submission of The Ebba toolset
Date: Wed, 27 Mar 2002 16:28:49 -0500

A package was submitted to
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 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.

reply via email to

[Prev in Thread] Current Thread [Next in Thread]