copilot-core-3.5: An intermediate representation for Copilot.
Safe HaskellSafe
LanguageHaskell2010

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

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

data Observer Source #

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

Constructors

forall a.Typeable a => Observer 

data Trigger Source #

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

Constructors

Trigger 

data Spec Source #

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

data Property Source #

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

Constructors

Property