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.WeakestPreconditions

Contents

- Programs and statements
- Invariants, measures, and stability
- Verification conditions
- Result of a proof
- Configuring the WP engine
- Checking WP correctness
- Concrete runs of programs

Description

A toy imperative language with a proof system based on Dijkstra's weakest preconditions methodology to establish partial/total correctness proofs.

See `Documentation.SBV.Examples.WeakestPreconditions` directory for several example proofs.

Synopsis

- data Program st = Program {
  - setup :: Symbolic ()
  - precondition :: st -> SBool
  - program :: Stmt st
  - postcondition :: st -> SBool
  - stability :: Stable st
  }
- data Stmt st
  - = Skip
  - | Abort String
  - | Assign (st -> st)
  - | If (st -> SBool) (Stmt st) (Stmt st)
  - | While String (Invariant st) (Maybe (Measure st)) (st -> SBool) (Stmt st)
  - | Seq [Stmt st]
- assert :: String -> (st -> SBool) -> Stmt st
- stable :: EqSymbolic a => String -> (st -> a) -> st -> st -> (String, SBool)
- type Invariant st = st -> SBool
- type Measure st = st -> [SInteger]
- type Stable st = [st -> st -> (String, SBool)]
- data VC st m
  - = BadPrecondition st
  - | BadPostcondition st st
  - | Unstable String st st
  - | AbortReachable String st st
  - | InvariantPre String st
  - | InvariantMaintain String st st
  - | MeasureBound String (st, [m])
  - | MeasureDecrease String (st, [m]) (st, [m])
- data ProofResult res
  - = Proven Bool
  - | Indeterminate String
  - | Failed [VC res Integer]
- data WPConfig = WPConfig {
  - wpSolver :: SMTConfig
  - wpVerbose :: Bool
  }
- defaultWPCfg :: WPConfig
- wpProve :: (Show res, Mergeable st, Queriable IO st, res ~ QueryResult st) => Program st -> IO (ProofResult res)
- wpProveWith :: forall st res. (Show res, Mergeable st, Queriable IO st, res ~ QueryResult st) => WPConfig -> Program st -> IO (ProofResult res)
- traceExecution :: forall st. Show st => Program st -> st -> IO (Status st)
- data Status st
  - = Good st
  - | Stuck (VC st Integer)

# Programs and statements

data Program st Source #

A program over a state is simply a statement, together with a pre-condition capturing environmental assumptions and a post-condition that states its correctness. In the usual Hoare-triple notation, it captures:

     {precondition} program {postcondition}

We also allow for a stability check, which is ensured at every assignment statement to deal with ghost variables. In general, this is useful for making sure what you consider as "primary inputs" remain unaffected. Of course, you can also put any arbitrary condition you want to check that you want performed for each `Assign` statement.

Note that stability is quite a strong condition: It is intended to capture constants that never change during execution. So, if you have a program that changes an input temporarily but always restores it at the end, it would still fail the stability condition.

The `setup` field is reserved for any symbolic code you might want to run before the proof takes place, typically for calls to `setOption`. If not needed, simply pass `return ()`. For an interesting use case where we use setup to axiomatize the spec, see Documentation.SBV.Examples.WeakestPreconditions.Fib and Documentation.SBV.Examples.WeakestPreconditions.GCD.

Constructors

Program |

Fields

- setup :: Symbolic ()

  Any set-up required

- precondition :: st -> SBool

  Environmental assumptions

- program :: Stmt st

  Program

- postcondition :: st -> SBool

  Correctness statement

- stability :: Stable st

  Each assignment must satisfy stability

data Stmt st Source #

A statement in our imperative program, parameterized over the state.

Constructors

Skip | Skip, do nothing.
Abort String | Abort execution. The name is for diagnostic purposes.
Assign (st -> st) | Assignment: Transform the state by a function.
If (st -> SBool) (Stmt st) (Stmt st) | Conditional: `If condition thenBranch elseBranch`.
While String (Invariant st) (Maybe (Measure st)) (st -> SBool) (Stmt st) | A while loop: `While name invariant measure condition body`. The string `name` is merely for diagnostic purposes. If the measure is `Nothing`, then only partial correctness of this loop will be proven.
Seq [Stmt st] | A sequence of statements.

assert :: String -> (st -> SBool) -> Stmt st Source #

An `assert` is a quick way of ensuring some condition holds. If it does, then it's equivalent to `Skip`. Otherwise, it is equivalent to `Abort`.

stable :: EqSymbolic a => String -> (st -> a) -> st -> st -> (String, SBool) Source #

Stability: A call of the form `stable "f" f` means the value of the field `f` does not change during any assignment. The string argument is for diagnostic purposes only. Note that we use strong-equality here, so if the program is manipulating floats, we don't get a false-positive on `NaN` and also not miss `+0` and `-`@ changes.

# Invariants, measures, and stability

type Invariant st = st -> SBool Source #

An invariant takes a state and evaluates to a boolean.

type Measure st = st -> [SInteger] Source #

A measure takes the state and returns a sequence of integers. The ordering will be done lexicographically over the elements.

type Stable st = [st -> st -> (String, SBool)] Source #

A stability condition captures a primary input that does not change. Use `stable` to create elements of this type.

# Verification conditions

data VC st m Source #

A verification condition. Upon failure, each `VC` carries enough state and diagnostic information to indicate what particular proof obligation failed for further debugging.

Constructors

BadPrecondition st | The precondition doesn't hold. This can only happen in `traceExecution`.
BadPostcondition st st | The postcondition doesn't hold
Unstable String st st | Stability condition is violated
AbortReachable String st st | The named abort condition is reachable
InvariantPre String st | Invariant doesn't hold upon entry to the named loop
InvariantMaintain String st st | Invariant isn't maintained by the body
MeasureBound String (st, [m]) | Measure cannot be shown to be non-negative
MeasureDecrease String (st, [m]) (st, [m]) | Measure cannot be shown to decrease through each iteration

#### Instances

Instances details

(Show st, Show m) => Show (VC st m) Source # | Show instance for VC's
Instance details Defined in Data.SBV.Tools.WeakestPreconditions Methods showsPrec :: Int -> VC st m -> ShowS Source # show :: VC st m -> String Source # showList :: [VC st m] -> ShowS Source #

# Result of a proof

data ProofResult res Source #

The result of a weakest-precondition proof.

Constructors

Proven Bool | The property holds. If `Bool` is `True`, then total correctness, otherwise partial.
Indeterminate String | Failed to establish correctness. Happens when the proof obligations lead to the SMT solver to return `Unk`. This can happen, for instance, if you have non-linear constraints, causing the solver to give up.
Failed [VC res Integer] | The property fails, failing to establish the conditions listed.

#### Instances

Instances details

Show res => Show (ProofResult res) Source # | `Show` instance for proofs, for readability.
Instance details Defined in Data.SBV.Tools.WeakestPreconditions Methods showsPrec :: Int -> ProofResult res -> ShowS Source # show :: ProofResult res -> String Source # showList :: [ProofResult res] -> ShowS Source #

# Configuring the WP engine

data WPConfig Source #

Configuration for WP proofs.

Constructors

WPConfig |

Fields

- wpSolver :: SMTConfig

  SMT Solver to use

- wpVerbose :: Bool

  Should we be chatty?

defaultWPCfg :: WPConfig Source #

Default WP configuration: Uses the default solver, and is not verbose.

# Checking WP correctness

wpProve :: (Show res, Mergeable st, Queriable IO st, res ~ QueryResult st) => Program st -> IO (ProofResult res) Source #

Check correctness using the default solver. Equivalent to ``wpProveWith` `defaultWPCfg``.

wpProveWith :: forall st res. (Show res, Mergeable st, Queriable IO st, res ~ QueryResult st) => WPConfig -> Program st -> IO (ProofResult res) Source #

Checking WP based correctness

# Concrete runs of programs

traceExecution Source #

Arguments

:: forall st. Show st |
=> Program st | Program
-> st | Starting state. It must be fully concrete.
-> IO (Status st) |

Trace the execution of a program, starting from a sufficiently concrete state. (Sufficiently here means that all parts of the state that is used uninitialized must have concrete values, i.e., essentially the inputs. You can leave the "temporary" variables initialized by the program before use undefined or even symbolic.) The return value will have a `Good` state to indicate the program ended successfully, if that is the case. The result will be `Stuck` if the program aborts without completing: This can happen either by executing an `Abort` statement, or some invariant gets violated, or if a metric fails to go down through a loop body.

data Status st Source #

Are we in a good state, or in a stuck state?

Constructors

Good st | Execution finished in the given state.
Stuck (VC st Integer) | Execution got stuck, with the failing VC

#### Instances

Instances details

Show st => Show (Status st) Source # | Show instance for `Status`
Instance details Defined in Data.SBV.Tools.WeakestPreconditions Methods showsPrec :: Int -> Status st -> ShowS Source # show :: Status st -> String Source # showList :: [Status st] -> ShowS Source #