| 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
- data Type
- data Node = Node {
- nodeId :: String
- nodeStateVars :: [StateVarDef]
- nodeInit :: Term
- nodeTrans :: Term
- data Prop = Prop {}
- prettyPrint :: File -> String
- data File = File {}
- toKind2 :: [PropId] -> [PropId] -> TransSys -> File
- data PredType
- data StateVarDef = StateVarDef {}
- data StateVarFlag = FConst
Documentation
module Copilot.Theorem.Kind2.Prover
Datatype to describe a term in the Kind language.
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.).
A node definition.
Constructors
| Node | |
Fields
| |
A proposition is defined by a term.
prettyPrint :: File -> String Source #
Pretty print a Kind2 file.
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.
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.
Type of the predicate, either belonging to an initial state or a pair of states with a transition.