Data.SBV.Tools.WeakestPreconditions

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.

Programs and statements

data Program st

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

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

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)

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

An invariant takes a state and evaluates to a boolean.

type Measure st = st -> [SInteger]

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)]

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

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

(Show st, Show m) => Show (VC st m)

Show instance for VC's

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

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

Show res => Show (ProofResult res)

Show instance for proofs, for readability.

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

Configuration for WP proofs.

Constructors

WPConfig

Fields

• wpSolver :: SMTConfig

  SMT Solver to use

• wpVerbose :: Bool

  Should we be chatty?

defaultWPCfg :: WPConfig

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)

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)

Checking WP based correctness

Concrete runs of programs

traceExecution

Arguments

:: 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

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

Show st => Show (Status st)

Show instance for Status

Defined in Data.SBV.Tools.WeakestPreconditions

Methods

showsPrec :: Int -> Status st -> ShowS

show :: Status st -> String

showList :: [Status st] -> ShowS