copilot-core-4.6.1: An intermediate representation for Copilot.

Copyright | (c) 2011 National Institute of Aerospace / Galois Inc.
Safe Haskell | Safe
Language | Haskell2010

Copilot.Core.Spec

Description

Copilot specifications constitute 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, high-level Copilot Language Spec must be turned into Copilot Core's `Spec`. This module defines the low-level Copilot Core representations for Specs and the main types of element in a spec.

Synopsis

- data Stream = (Typeable a, Typed a) => Stream {
  - streamId :: Id
  - streamBuffer :: [a]
  - streamExpr :: Expr a
  - streamExprType :: Type a
  }
- data Observer = Typeable a => Observer {
  - observerName :: Name
  - observerExpr :: Expr a
  - observerExprType :: Type a
  }
- data Trigger = Trigger {
  - triggerName :: Name
  - triggerGuard :: Expr Bool
  - triggerArgs :: [UExpr]
  }
- data Spec = Spec {
  - specStreams :: [Stream]
  - specObservers :: [Observer]
  - specTriggers :: [Trigger]
  - specProperties :: [Property]
  }
- data Property = Property {
  - propertyName :: Name
  - propertyProp :: Prop
  }
- data Prop
  - = Forall (Expr Bool)
  - | Exists (Expr Bool)
- extractProp :: Prop -> Expr Bool

# Documentation

data Stream Source #

A stream in an infinite succession of values of the same type.

Stream can carry different types of data. Boolean streams play a special role: they are used by other parts (e.g., `Trigger`) to detect when the properties being monitored are violated.

Constructors

(Typeable a, Typed a) => Stream |

Fields

- streamId :: Id
- streamBuffer :: [a]
- streamExpr :: Expr a
- streamExprType :: Type a

data Observer Source #

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

Constructors

Typeable a => Observer |

Fields

- observerName :: Name
- observerExpr :: Expr a
- observerExprType :: Type a

data Trigger Source #

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

Constructors

Trigger |

Fields

- triggerName :: Name
- triggerGuard :: Expr Bool
- triggerArgs :: [UExpr]

data Spec Source #

A Copilot specification is a list of streams, together with monitors on these streams implemented as observers, triggers or properties.

Constructors

Spec |

Fields

- specStreams :: [Stream]
- specObservers :: [Observer]
- specTriggers :: [Trigger]
- specProperties :: [Property]

data Property Source #

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

Constructors

Property |

Fields

- propertyName :: Name
- propertyProp :: Prop

data Prop Source #

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

Constructors

Forall (Expr Bool) |
Exists (Expr Bool) |

extractProp :: Prop -> Expr 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.