| 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 Prop = Prop {}
- prettyPrint :: File -> String
- data File = File {}
- data Style
- toKind2 :: Style -> [PropId] -> [PropId] -> TransSys -> File
- data PredType
- data StateVarDef = StateVarDef {}
- data PredDef = PredDef {
- predId :: String
- predStateVars :: [StateVarDef]
- predInit :: Term
- predTrans :: Term
- 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 proposition is defined by a term.
prettyPrint :: File -> String Source #
Pretty print a Kind2 file.
A file is a sequence of predicates and propositions.
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.
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.
Type of the predicate, either belonging to an initial state or a pair of states with a transition.
A predicate definition.
Constructors
| PredDef | |
Fields
| |