Language.Spectacle
defines an embedded language for writing formal specifications of software in the temporal logic of actions. Specifications written in spectacle can be model-checked and shown to either be correct with respect to temporal properties or refuted by a counterexample. Examples of specifications written in spectacle are provided under test/integration
.
nicolast / spectacle Goto Github PK
View Code? Open in Web Editor NEWThis project forked from awakesecurity/spectacle
Embedded specification language & model checker in Haskell
License: Apache License 2.0