Formal Specification 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.
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!
More here: [alloy: the neat formal
method].
It is also designed to check liveness properties of systems.
[Hillel] has a good article on modeling a complex system in the
software development world with formal methods.
There are a lot more, but I'll investigate them further as I learn
more.
Examples
Terms
- 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.