The ABZ community is explicitly not meant to be limited to the methods listed here. This page only serves to give an overview of some popular representatives of rigorous state based methods.
Any other state-based formal method is welcome!
If you would like to have another method listed here, please contact one of the webmasters mentioned in the
The Alloy language can be used to describe structures based on a collection of constraints. This created Alloy model can then be analyzed by the Alloy Analyzer, a solver that finds concrete structures that satisfy the constraints defined in the Alloy model.
Z is the “ultimate language” as stated by Jean-Raymond Abrial who invented this formal specification language in 1977. This language aims for a precise and clear specification of computer-based systems based on the Zermelo-Fraenkel set theory, lambda calculus, and first-order predicate logic.