Formal Spec Langauges

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.


The first specification language to reach widespread use. Relies on set theory to describe states and schemas to describe behavior, first catalogued as a way of managing 'data semantics'.
A response to Z's complex syntax and tooling. Alloy is an attempt to simplify both of these, specifying everything as either a type signature or relationship between signatures. Alloy is popular for SAT problems and models; it easily visualizes models to share properties with nontechnical people as well. This would be the tool to try!

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


Temporal logic
Extending standard mathematical notation to allow temporal logic to change over time. Temporal logic of actions is a subset of this concept that scales to real world systems.
Liveness properties
Similar to the definition in the compiler sphere, liveness properties are properties of systems that must eventually be true for the spec to be valid.


Joey Eremondi on Twitter: "Has anyone seen a "reference" implementation of an SMT solver? Not one that is fast like Z3 or CVC4, but one that implements the algorithm in a fairly straightforward way that's slow but grokkable. I'm particularly interested in how it handles uninterpreted functions (UF)." / Twitter alloy: the neat formal method