Alternatives to Alloy
Z & Object Z
Object Constraint Language in UML (OCL)
Developer of Z
Professor Jean-Raymond Abrial
As Alloy was heavily influenced by Z, it is only natural
to compare the two.
Z was first developed in 1977 by Jean-Raymond Abrial at
Oxford University. Being both based on logic and set
theory, Alloy closely resembles Z. In fact, Alloy can
be viewed as a subset of the Z language.
One of the advantages of Z is that it has a rich mathematical
notation making it more expressive than Alloy. However, Alloy is
first order making it automatically analyzable, theorem provers in Z
are rather more limited. They are automated only up to a point,
complex proofs often require guidance from an experienced user.
The distinct style and notation of schema calculus gives it the ability
to support many different idioms. Alloy on the other hand has a pure
ASCII notation and requires no special typesetting tools. Writing out
schemas can be tedious in comparison to typing a signature on Alloy!
Overall, Z has had much more widespread use in education and research. Z has
already been applied to several large projects including that on the CICS
system by IBM and Oxford University. With continuing development and research being
done, perhaps Alloy will one day emulate and even surpass Z.
Vienna Development Method (VDM)
The Object Constraint Language(OCL) is the constraint language of UML. It was developed at
IBM and ObjecTime Limited and was added to the UML in 1997. Because it was initially designed
to be an annotation language for UML class diagrams, it does not include a textual notation
for declarations. Variants of OCL such as USE
overcome this limitation.
OCL is based on first-order predicate logic but uses a syntax similar to programming languages and
closely related to the syntax of UML. Alloy is similar to OCL, but its creators claim that
Alloy has a more conventional syntax and simpler semantics. Alloy is fully declarative, whereas OCL allows
mixing declarative and operational elements. The creators of Alloy argue
that OCL is too implementation-oriented and therefore not well-suited for conceptual modelling though
believe that experience can help keep the
specification process with OCL at an abstract level.
Many tools are available supporting OCL such as Octopus
Eclipse Model Development Tools
. Typical features
include the interpretation of OCL constraints over test cases and code generation. Some, such as the USE
tool mentioned above, support design-time analysis and allow exhaustive search over a finite space of
cases similar to Alloy.
Co-developer of VDM
Professor Cliff Jones
Vienna Development Method (VDM) is a set of techniques for developing computer systems.
It originated from IBM's Vienna Laboratory in the mid-1970s and was developed by Cliff Jones
and Dines Bjorner. VDM includes a specification language called VDM-SL
(VDM specification language).
After the development of VDM in the 1970s there were a few tools for checking VDM
specifications, but these were mostly informal projects. In 1988 Peter Froome developed
a tool called SpecBox which was the first industrialised tool for checking VDM specification.
SpecBox is used in civil nuclear, railway and security applications.
There are many other tools for checking VDM specification such as IFAD VDM-SL
and Centaur-VDM environment which is an interactive and graphical tool for VDM.
However unlike Alloy these do not provide fully automatic analysis in the style of
a model checker. Both Alloy and VDM support object-orientation and concurrency.
Although it is one of the first formal methods in development, it has been refined,
standardized and is still widely used in industry by such organisations as British Aerospace Systems &
Equipment, Rolls Royce and Dutch Department of Defence. Alloy is not used as much in industry as VDM.