copilot-theorem-4.7.1: 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 Prop = Prop {
  - propName :: String
  - propTerm :: Term
  }
- prettyPrint :: File -> String
- data File = File {
  - filePreds :: [PredDef]
  - fileProps :: [Prop]
  }
- data Style
  - = Inlined
  - | Modular
- toKind2 :: Style -> [PropId] -> [PropId] -> TransSys -> File
- data PredType
  - = Init
  - | Trans
- data StateVarDef = StateVarDef {
  - varId :: String
  - varType :: Type
  - varFlags :: [StateVarFlag]
  }
- data PredDef = PredDef {
  - predId :: String
  - predStateVars :: [StateVarDef]
  - predInit :: Term
  - predTrans :: Term
  }
- 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 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 predicates and propositions.

Constructors

File |

Fields

- filePreds :: [PredDef]
- fileProps :: [Prop]

data Style Source #

Style of the Kind2 files produced: modular (with multiple separate nodes), or all inlined (with only one node).

In the modular style, the graph is simplified to remove cycles by collapsing all nodes participating in a strongly connected components.

In the inlined style, the structure of the modular transition system is discarded and the graph is first turned into a non-modular transition system with only one node, which can be then converted into a Kind2 file.

Constructors

Inlined |
Modular |

toKind2 Source #

Arguments

:: Style | Style of the file (modular or inlined).
-> [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 PredDef Source #

A predicate definition.

Constructors

PredDef |

Fields

- predId :: String

  Identifier for the predicate.

- predStateVars :: [StateVarDef]

  Variables identifying the states in the underlying state transition system.

- predInit :: Term

  Predicate that holds for initial states.

- predTrans :: Term

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

data StateVarFlag Source #

Possible flags for a state variable.

Constructors

FConst |