copilot-language-4.7.1: A Haskell-embedded DSL for monitoring hard real-time distributed systems.

Safe Haskell | Safe
Language | Haskell2010

Copilot.Language.Spec

Description

Copilot specifications consistute the main declaration of Copilot modules.

A specification normally contains the association between streams to monitor and their handling functions, or streams to observe, or a theorem that must be proved.

In order to be executed, `Spec`s must be turned into Copilot Core (see `Reify`) and either simulated or converted into C99 code to be executed.

Synopsis

- type Spec = Writer [SpecItem] ()
- type Spec' a = Writer [SpecItem] a
- runSpec :: Spec' a -> [SpecItem]
- data SpecItem
- data Observer where
  - Observer :: forall a. Typed a => String -> Stream a -> Observer
- observer :: Typed a => String -> Stream a -> Spec
- observers :: [SpecItem] -> [Observer]
- data Trigger where
  - Trigger :: Name -> Stream Bool -> [Arg] -> Trigger
- trigger :: String -> Stream Bool -> [Arg] -> Spec
- triggers :: [SpecItem] -> [Trigger]
- arg :: Typed a => Stream a -> Arg
- data Arg where
  - Arg :: forall a. Typed a => Stream a -> Arg
- data Property where
  - Property :: forall a. String -> Prop a -> Property
- data Prop a where
  - Forall :: Stream Bool -> Prop Universal
  - Exists :: Stream Bool -> Prop Existential
- prop :: String -> Prop a -> Writer [SpecItem] (PropRef a)
- properties :: [SpecItem] -> [Property]
- theorem :: String -> Prop a -> Proof a -> Writer [SpecItem] (PropRef a)
- theorems :: [SpecItem] -> [(Property, UProof)]
- forAll :: Stream Bool -> Prop Universal
- exists :: Stream Bool -> Prop Existential
- extractProp :: Prop a -> Stream Bool
- data Universal
- data Existential

# Documentation

type Spec = Writer [SpecItem] () Source #

A specification is a list of declarations of triggers, observers, properties and theorems.

Specifications are normally declared in monadic style, for example:

    monitor1 :: Stream Bool
    monitor1 = [False] ++ not monitor1

    counter :: Stream Int32
    counter = [0] ++ not counter

    spec :: Spec
    spec = do
      trigger "handler_1" monitor1 []
      trigger "handler_2" (counter > 10) [arg counter]

type Spec' a = Writer [SpecItem] a Source #

An action in a specification (e.g., a declaration) that returns a value that can be used in subsequent actions.

runSpec :: Spec' a -> [SpecItem] Source #

Return the complete list of declarations inside a `Spec` or `Spec'`.

The word run in this function is unrelated to running the underlying specifications or monitors, and is merely related to the monad defined by a `Spec`

data SpecItem Source #

An item of a Copilot specification.

data Observer where Source #

An observer, representing a stream that we observe during execution at every sample.

Constructors

Observer :: forall a. Typed a => String -> Stream a -> Observer |

observer Source #

Arguments

:: Typed a |
=> String | Name used to identify the stream monitored in the output produced during interpretation.
-> Stream a | The stream being monitored.
-> Spec |

Define a new observer as part of a specification. This allows someone to print the value at every iteration during interpretation. Observers do not have any functionality outside the interpreter.

observers :: [SpecItem] -> [Observer] Source #

Filter a list of spec items to keep only the observers.

data Trigger where Source #

A trigger, representing a function we execute when a boolean stream becomes true at a sample.

Constructors

Trigger :: Name -> Stream Bool -> [Arg] -> Trigger |

trigger Source #

Arguments

:: String | Name of the handler to be called.
-> Stream Bool | The stream used as the guard for the trigger.
-> [Arg] | List of arguments to the handler.
-> Spec |

Define a new trigger as part of a specification. A trigger declares which external function, or handler, will be called when a guard defined by a boolean stream becomes true.

triggers :: [SpecItem] -> [Trigger] Source #

Filter a list of spec items to keep only the triggers.

arg :: Typed a => Stream a -> Arg Source #

Construct a function argument from a stream.

`Arg`s can be used to pass arguments to handlers or trigger functions, to provide additional information to monitor handlers in order to address property violations. At any given point (e.g., when the trigger must be called due to a violation), the arguments passed using `arg` will contain the current samples of the given streams.

data Arg where Source #

Wrapper to use `Stream`s as arguments to triggers.

Constructors

Arg :: forall a. Typed a => Stream a -> Arg |

data Property where Source #

A property, representing a boolean stream that is existentially or universally quantified over time.

Constructors

Property :: forall a. String -> Prop a -> Property |

data Prop a where Source #

A proposition, representing the quantification of a boolean streams over time.

Constructors

Forall :: Stream Bool -> Prop Universal |
Exists :: Stream Bool -> Prop Existential |

prop :: String -> Prop a -> Writer [SpecItem] (PropRef a) Source #

A proposition, representing a boolean stream that is existentially or universally quantified over time, as part of a specification.

This function returns, in the monadic context, a reference to the proposition.

properties :: [SpecItem] -> [Property] Source #

Filter a list of spec items to keep only the properties.

theorem :: String -> Prop a -> Proof a -> Writer [SpecItem] (PropRef a) Source #

A theorem, or proposition together with a proof.

This function returns, in the monadic context, a reference to the proposition.

theorems :: [SpecItem] -> [(Property, UProof)] Source #

Filter a list of spec items to keep only the theorems.

forAll :: Stream Bool -> Prop Universal Source #

Universal quantification of boolean streams over time.

exists :: Stream Bool -> Prop Existential Source #

Existential quantification of boolean streams over time.

extractProp :: Prop a -> Stream Bool Source #

Extract the underlying stream from a quantified proposition.

Think carefully before using this function, as this function will remove the quantifier from a proposition. Universally quantified streams usually require separate treatment from existentially quantified ones, so carelessly using this function to remove quantifiers can result in hard-to-spot soundness bugs.

data Universal Source #

Empty datatype to mark proofs of universally quantified predicates.

data Existential Source #

Empty datatype to mark proofs of existentially quantified predicates.