sbv-8.12: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Data.SBV.Tools.WeakestPreconditions

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

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

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 #

show :: VC st m -> String #

showList :: [VC st m] -> ShowS #

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 #

show :: ProofResult res -> String #

showList :: [ProofResult res] -> ShowS #

Configuring the WP engine

data WPConfig Source #

Configuration for WP proofs.

Constructors

WPConfig 

Fields

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) => 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) => 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 #

show :: Status st -> String #

showList :: [Status st] -> ShowS #