Hackage :: [Package]

spectacle: Embedded specification language & model checker in Haskell.

[ apache, concurrency, library, testing ] [ Propose Tags ]

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.Natural
  • 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

Downloads

Maintainer's Corner

Package maintainers

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 83 total (3 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]

Readme for spectacle-1.0.0

[back to package description]

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.