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 = forall a.(Typeable a, Typed a) => Stream {
- streamId :: Id
- streamBuffer :: [a]
- streamExpr :: Expr a
- streamExprType :: Type a
}
data Observer = forall a.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

forall a.(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

forall a.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.