spectacle: Embedded specification language & model checker in Haskell.
Spectacle is an embedded domain-specific language that provides a family of type-level combinators for authoring specifications of program behavior along with a model checker for verifying that user implementations of a program satisfy written specifications.
[Skip to Readme]
Modules
- Control
- Applicative
- Control.Applicative.Day
- Control.Applicative.Phases
- Control.Applicative.Queue
- Comonad
- Control.Comonad.Tape
- Control.Hyper
- Control.Mealy
- Monad
- Control.Monad.Levels
- Control.Monad.Levels.Internal
- Control.Monad.Ref
- Control.Monad.Levels
- Control.Natural
- Applicative
- Data
- Data.Ascript
- Data.Bag
- Data.Fingerprint
- Functor
- Data.Functor.Loom
- Data.Functor.Tree
- Data.Name
- Data.Node
- Type
- Data.Type.List
- Data.Type.Rec
- Data.World
- Language
- Language.Spectacle
- Language.Spectacle.AST
- Language.Spectacle.AST.Action
- Language.Spectacle.AST.Temporal
- Exception
- Language.Spectacle.Exception.RuntimeException
- Language.Spectacle.Fairness
- Language.Spectacle.Interaction
- Language.Spectacle.Interaction.CLI
- Language.Spectacle.Interaction.Diagram
- Language.Spectacle.Interaction.Doc
- Language.Spectacle.Interaction.Options
- Language.Spectacle.Interaction.Paths
- Language.Spectacle.Interaction.Point
- Language.Spectacle.Interaction.Pos
- Language.Spectacle.Lang
- Language.Spectacle.Lang.Internal
- Language.Spectacle.Lang.Member
- Language.Spectacle.Lang.Op
- Language.Spectacle.Lang.Scoped
- Language.Spectacle.Model
- Language.Spectacle.Model.ModelAction
- Language.Spectacle.Model.ModelEnv
- Language.Spectacle.Model.ModelError
- Language.Spectacle.Model.ModelNode
- Language.Spectacle.Model.ModelState
- Language.Spectacle.Model.ModelTemporal
- Language.Spectacle.Model.Monad
- RTS
- Language.Spectacle.RTS.Registers
- Language.Spectacle.Specification
- Language.Spectacle.Specification.Action
- Language.Spectacle.Specification.Prop
- Language.Spectacle.Specification.Variable
- Language.Spectacle.Syntax
- Language.Spectacle.Syntax.Closure
- Language.Spectacle.Syntax.Closure.Internal
- Language.Spectacle.Syntax.Enabled
- Language.Spectacle.Syntax.Enabled.Internal
- Language.Spectacle.Syntax.Env
- Language.Spectacle.Syntax.Env.Internal
- Language.Spectacle.Syntax.Error
- Language.Spectacle.Syntax.Error.Internal
- Language.Spectacle.Syntax.Logic
- Language.Spectacle.Syntax.Logic.Internal
- Language.Spectacle.Syntax.NonDet
- Language.Spectacle.Syntax.NonDet.Internal
- Language.Spectacle.Syntax.Plain
- Language.Spectacle.Syntax.Plain.Internal
- Language.Spectacle.Syntax.Prime
- Language.Spectacle.Syntax.Prime.Internal
- Language.Spectacle.Syntax.Quantifier
- Language.Spectacle.Syntax.Quantifier.Internal
- Language.Spectacle.Syntax.Closure
- Language.Spectacle.AST
- Language.Spectacle
Downloads
- spectacle-1.0.0.tar.gz [browse] (Cabal source package)
- Package description (as included in the package)
Maintainer's Corner
For package maintainers and hackage trustees
Candidates
- No Candidates
Versions [RSS] | 1.0.0 |
---|---|
Change log | CHANGELOG.md |
Dependencies | base (>=4.14 && <4.15), comonad, containers (>=0.6), hashable (>=1.3.0.0), logict, microlens, microlens-mtl, mtl (>=2.2), optparse-applicative, prettyprinter, prettyprinter-ansi-terminal, text, transformers (>=0.5) [details] |
License | Apache-2.0 |
Copyright | 2021 Arista Networks |
Author | Arista Networks |
Maintainer | opensource@awakesecurity.com |
Category | Testing, Concurrency |
Home page | https://github.com/awakesecurity/spectacle |
Bug tracker | https://github.com/awakesecurity/spectacle/issues |
Uploaded | by ParnellSpringmeyer at 2022-02-03T19:48:09Z |
Distributions | |
Downloads | 104 total (2 in the last 30 days) |
Rating | (no votes yet) [estimated by Bayesian average] |
Your Rating | |
Status | Docs not available [build log] All reported builds failed as of 2022-02-04 [all 2 reports] |