Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
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
- propertyExpr :: Expr Bool
Documentation
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.
forall a.(Typeable a, Typed a) => Stream | |
|
An observer, representing a stream that we observe during interpretation at every sample.
forall a.Typeable a => Observer | |
|
A trigger, representing a function we execute when a boolean stream becomes true at a sample.
Trigger | |
|
A Copilot specification is a list of streams, together with monitors on these streams implemented as observers, triggers or properties.
Spec | |
|
A property, representing a boolean stream that is existentially or universally quantified over time.
Property | |
|