# From Hillel Wayne's writing

A notation to describe the design of a system without implementing it.Can test the **design** for bugs rather than the implementation.

## Examples

z

The first specification language to reach widespread use. Relies on settheory to describe states and schemas to describe behavior, firstcatalogued as a way of managing 'data semantics'.

Alloy

A response to Z's complex syntax and tooling. Alloy is an attempt tosimplify both of these, specifying everything as either a type signatureor relationship between signatures. Alloy is popular for SAT problemsand models; it easily visualizes models to share properties withnontechnical people as well. This would be the tool to try! More here:alloy: the neat formalmethod.

- TLA^+ is a formalspecification langauge used to model concurrent and distributedsystems; it's best respected as testable pseudocode and is similar tothe drawing of blueprints for complex software systems. It is alsodesigned to check liveness properties of systems.Hillelhas a good article on modeling a complex system in the softwaredevelopment world with formal methods.
- Prism :: Used to model
**probabilistic**specifications, in whichdifferent things have different chances of happening and events areall dependent. Its syntax is very restrictive in order to betractable, but the opportunity to model probabilistic systems isincredible. - Spin :: As expressive as TLA+, but written to model network protocols.

There are a lot more, but I'll investigate them further as I learn more.

# Terms

Temporal logic

Extending standard mathematical notation to allow temporal logic tochange over time. Temporal logic of actions is a subset of this conceptthat scales to real world systems.

Liveness properties

Similar to the definition in the compiler sphere, liveness propertiesare properties of systems that must *eventually* be true for the spec tobe valid.