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
.
Embedded specification language & model checker in Haskell
License
awakesecurity/spectacle
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Folders and files
Name | Name | Last commit message | Last commit date | |
---|---|---|---|---|
Repository files navigation
About
Embedded specification language & model checker in Haskell
Resources
License
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published