| Copyright | (c) Levent Erkok |
|---|---|
| License | BSD3 |
| Maintainer | erkokl@gmail.com |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
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
- data Program st = Program {
- setup :: Symbolic ()
- precondition :: st -> SBool
- program :: Stmt st
- postcondition :: st -> SBool
- stability :: Stable st
- data 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
- data WPConfig = WPConfig {}
- defaultWPCfg :: WPConfig
- wpProve :: (Show res, Mergeable st, Queriable IO st res) => Program st -> IO (ProofResult res)
- wpProveWith :: forall st res. (Show res, Mergeable st, Queriable IO st res) => WPConfig -> Program st -> IO (ProofResult res)
- traceExecution :: forall st. Show st => Program st -> st -> IO (Status st)
- data Status st
Programs and statements
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.
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: |
| While String (Invariant st) (Maybe (Measure st)) (st -> SBool) (Stmt st) | A while loop: |
| Seq [Stmt st] | A sequence of statements. |
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 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
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 |
| 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 |
Result of a proof
data ProofResult res Source #
The result of a weakest-precondition proof.
Constructors
| Proven Bool | The property holds. If |
| Indeterminate String | Failed to establish correctness. Happens when the proof obligations lead to
the SMT solver to return |
| Failed [VC res Integer] | The property fails, failing to establish the conditions listed. |
Instances
| Show res => Show (ProofResult res) Source # |
|
Defined in Data.SBV.Tools.WeakestPreconditions Methods showsPrec :: Int -> ProofResult res -> ShowS # show :: ProofResult res -> String # showList :: [ProofResult res] -> ShowS # | |
Configuring the WP engine
Configuration for WP proofs.
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
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.