@hackage / spectacle

Embedded specification language & model checker in Haskell.

Latest1.0.0

About

Metadata

  • Last updated , by ParnellSpringmeyer
  • License Apache-2.0
  • Categories Concurrency, Testing

  • Maintained by: opensource@awakesecurity.com

  • Lottery factor: 0

Links

Installation

Tested Compilers

  1. 8.10.3

Readme

spectacle

ci

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.