Copilot.Language.Spec

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, Specs must be turned into Copilot Core (see Reify) and either simulated or converted into C99 code to be executed.

Documentation

type Spec = Writer [SpecItem] ()

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

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

runSpec :: Spec' a -> [SpecItem]

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

An item of a Copilot specification.

data Observer where

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

Constructors

Observer :: Typed a => String -> Stream a -> Observer

observer

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]

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

data Trigger where

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

Constructors

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

trigger

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]

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

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

Construct a function argument from a stream.

Args 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

Wrapper to use Streams as arguments to triggers.

Constructors

Arg :: Typed a => Stream a -> Arg

data Property where

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

Constructors

Property :: String -> Prop a -> Property

data Prop a where

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)

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]

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

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

A theorem, or proposition together with a proof.

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

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

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

forAll :: Stream Bool -> Prop Universal

Universal quantification of boolean streams over time.

exists :: Stream Bool -> Prop Existential

Existential quantification of boolean streams over time.

extractProp :: Prop a -> Stream Bool

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

Empty datatype to mark proofs of universally quantified predicates.

data Existential

Empty datatype to mark proofs of existentially quantified predicates.