copilot-theorem-4.8: k-induction for Copilot.

Safe Haskell | Safe
Language | Haskell2010

Copilot.Theorem.Kind2

Description

Copilot backend for the Kind 2 SMT based model checker.

Synopsis

- module Copilot.Theorem.Kind2.Prover
- data Term
  - = ValueLiteral String
  - | PrimedStateVar String
  - | StateVar String
  - | FunApp String [Term]
  - | PredApp String PredType [Term]
- data Type
  - = Int
  - | Real
  - | Bool
- data Node = Node {
  - nodeId :: String
  - nodeStateVars :: [StateVarDef]
  - nodeInit :: Term
  - nodeTrans :: Term
  }
- data Prop = Prop {
  - propName :: String
  - propTerm :: Term
  }
- prettyPrint :: File -> String
- data File = File {
  - fileNodes :: [Node]
  - fileTopNode :: Node
  - fileProps :: [Prop]
  }
- toKind2 :: [PropId] -> [PropId] -> TransSys -> File
- data PredType
  - = Init
  - | Trans
- data StateVarDef = StateVarDef {
  - varId :: String
  - varType :: Type
  - varFlags :: [StateVarFlag]
  }
- data StateVarFlag = FConst

# Documentation

module Copilot.Theorem.Kind2.Prover

data Term Source #

Datatype to describe a term in the Kind language.

Constructors

ValueLiteral String |
PrimedStateVar String |
StateVar String |
FunApp String [Term] |
PredApp String PredType [Term] |

data Type Source #

Types used in Kind2 files to represent Copilot types.

The Kind2 backend provides functions to, additionally, constrain the range of numeric values depending on their Copilot type (`Int8`, `Int16`, etc.).

Constructors

Int |
Real |
Bool |

data Node Source #

A node definition.

Constructors

Node |

Fields

- nodeId :: String

  Identifier for the node.

- nodeStateVars :: [StateVarDef]

  Variables identifying the states in the underlying state transition system.

- nodeInit :: Term

  Predicate that holds for initial states.

- nodeTrans :: Term

  Predicate that holds for two states, if there is a state transition between them.

data Prop Source #

A proposition is defined by a term.

Constructors

Prop |

Fields

- propName :: String
- propTerm :: Term

prettyPrint :: File -> String Source #

Pretty print a Kind2 file.

data File Source #

A file is a sequence of node definitions, together with a distinguished top node and a series of propositions about the top node.

Kind2 analyzes the last node defined in a file as the top system, so the top node is always printed after all the other nodes.

Constructors

File |

Fields

- fileNodes :: [Node]

  Nodes other than the top node, in dependency order (a node may only refer to nodes defined before it).

- fileTopNode :: Node

  The top node, which the propositions are attached to.

- fileProps :: [Prop]

  Propositions about the top node.

toKind2 Source #

Arguments

:: [PropId] | Assumptions
-> [PropId] | Properties to be checked
-> TransSys | Modular transition system holding the system spec
-> File |

Produce a Kind2 file that checks the properties specified.

data PredType Source #

Type of the predicate, either belonging to an initial state or a pair of states with a transition.

Constructors

Init |
Trans |

data StateVarDef Source #

A definition of a state variable.

Constructors

StateVarDef |

Fields

- varId :: String

  Name of the variable.

- varType :: Type

  Type of the variable.

- varFlags :: [StateVarFlag]

  Flags for the variable.

data StateVarFlag Source #

Possible flags for a state variable.

Constructors

FConst |