How is Alloy related to Z?
Z was a major influence on Alloy. Very roughly, Alloy can be viewed as a subset of Z. Unlike Z, Alloy is first order, which makes it analyzable (but also less expressive). Alloy’s composition mechanisms are designed to have the flexibility of Z’s schema calculus, but are based on different idioms: extension by addition of fields, similar to inheritance in an object-oriented language, and reuse of formulas by explicit parameterization, similar to functions in a functional programming language. Alloy is a pure ASCII notation and doesn’t require special typesetting tools.
