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, Specs 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 :: 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 Property where
- Property :: String -> Stream Bool -> 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 :: 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.

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 Property where Source #

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

Constructors

Property :: String -> Stream Bool -> Property

data Prop a where Source #

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

Constructors