sbv-10.2: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | Safe-Inferred
Language | Haskell2010

Data.SBV.Tools.Induction

Description

Induction engine for state transition systems. See the following examples for details:

- Documentation.SBV.Examples.ProofTools.Strengthen: Use of strengthening to establish inductive invariants.
- Documentation.SBV.Examples.ProofTools.Sum: Proof for correctness of an algorithm to sum up numbers,
- Documentation.SBV.Examples.ProofTools.Fibonacci: Proof for correctness of an algorithm to fast-compute fibonacci numbers, using axiomatization.

Synopsis

- data InductionResult a
  - = Failed InductionStep a
  - | Proven
- data InductionStep
  - = Initiation (Maybe String)
  - | Consecution (Maybe String)
  - | PartialCorrectness
- induct :: (Show res, Queriable IO st, res ~ QueryResult st) => Bool -> Symbolic () -> (st -> SBool) -> (st -> [st]) -> [(String, st -> SBool)] -> (st -> SBool) -> (st -> (SBool, SBool)) -> IO (InductionResult res)
- inductWith :: (Show res, Queriable IO st, res ~ QueryResult st) => SMTConfig -> Bool -> Symbolic () -> (st -> SBool) -> (st -> [st]) -> [(String, st -> SBool)] -> (st -> SBool) -> (st -> (SBool, SBool)) -> IO (InductionResult res)

# Documentation

data InductionResult a Source #

Result of an inductive proof, with a counter-example in case of failure.

If a proof is found (indicated by a `Proven` result), then the invariant holds and the goal is established once the termination condition holds. If it fails, then it can fail either in an initiation step or in a consecution step:

- A `Failed` result in an `Initiation` step means that the invariant does not hold for the initial state, and thus indicates a true failure.
- A `Failed` result in a `Consecution` step will return a state s. This state is known as a CTI (counterexample to inductiveness): It will lead to a violation of the invariant in one step. However, this does not mean the property is invalid: It could be the case that it is simply not inductive. In this case, human intervention---or a smarter algorithm like IC3 for certain domains---is needed to see if one can strengthen the invariant so an inductive proof can be found. How this strengthening can be done remains an art, but the science is improving with algorithms like IC3.
- A `Failed` result in a `PartialCorrectness` step means that the invariant holds, but assuming the termination condition the goal still does not follow. That is, the partial correctness does not hold.

Constructors

Failed InductionStep a |
Proven |

#### Instances

Instances details

Show a => Show (InductionResult a) Source # | Show instance for `InductionResult`, diagnostic purposes only.
Instance details Defined in Data.SBV.Tools.Induction Methods showsPrec :: Int -> InductionResult a -> ShowS Source # show :: InductionResult a -> String Source # showList :: [InductionResult a] -> ShowS Source #

data InductionStep Source #

A step in an inductive proof. If the tag is present (i.e., `Just nm`), then the step belongs to the subproof that establishes the strengthening named `nm`.

Constructors

Initiation (Maybe String) |
Consecution (Maybe String) |
PartialCorrectness |

#### Instances

Instances details

Show InductionStep Source # | Show instance for `InductionStep`, diagnostic purposes only.
Instance details Defined in Data.SBV.Tools.Induction Methods showsPrec :: Int -> InductionStep -> ShowS Source # show :: InductionStep -> String Source # showList :: [InductionStep] -> ShowS Source #

induct Source #

Arguments

:: (Show res, Queriable IO st, res ~ QueryResult st) |
=> Bool | Verbose mode
-> Symbolic () | Setup code, if necessary. (Typically used for `setOption` calls. Pass `return ()` if not needed.)
-> (st -> SBool) | Initial condition
-> (st -> [st]) | Transition relation
-> [(String, st -> SBool)] | Strengthenings, if any. The `String` is a simple tag.
-> (st -> SBool) | Invariant that ensures the goal upon termination
-> (st -> (SBool, SBool)) | Termination condition and the goal to establish
-> IO (InductionResult res) | Either proven, or a concrete state value that, if reachable, fails the invariant.

Induction engine, using the default solver. See Documentation.SBV.Examples.ProofTools.Strengthen and Documentation.SBV.Examples.ProofTools.Sum for examples.

inductWith :: (Show res, Queriable IO st, res ~ QueryResult st) => SMTConfig -> Bool -> Symbolic () -> (st -> SBool) -> (st -> [st]) -> [(String, st -> SBool)] -> (st -> SBool) -> (st -> (SBool, SBool)) -> IO (InductionResult res) Source #

Induction engine, configurable with the solver