Copyright  (c) Levent Erkok 

License  BSD3 
Maintainer  erkokl@gmail.com 
Stability  experimental 
Safe Haskell  None 
Language  Haskell2010 
Some basic aspects of weakest preconditions, demostrating programs that do not use while loops. We use a simple increment program as an example.
Program state
The state for the swap program, parameterized over a base type a
.
Instances
Functor IncS Source #  
Foldable IncS Source #  
Defined in Documentation.SBV.Examples.WeakestPreconditions.Basics fold :: Monoid m => IncS m > m # foldMap :: Monoid m => (a > m) > IncS a > m # foldr :: (a > b > b) > b > IncS a > b # foldr' :: (a > b > b) > b > IncS a > b # foldl :: (b > a > b) > b > IncS a > b # foldl' :: (b > a > b) > b > IncS a > b # foldr1 :: (a > a > a) > IncS a > a # foldl1 :: (a > a > a) > IncS a > a # elem :: Eq a => a > IncS a > Bool # maximum :: Ord a => IncS a > a #  
Traversable IncS Source #  
SymVal a => Fresh IO (IncS (SBV a)) Source # 

Show a => Show (IncS a) Source #  
(SymVal a, Show a) => Show (IncS (SBV a)) Source #  Show instance for 
Generic (IncS a) Source #  
Mergeable a => Mergeable (IncS a) Source #  
type Rep (IncS a) Source #  
Defined in Documentation.SBV.Examples.WeakestPreconditions.Basics type Rep (IncS a) = D1 (MetaData "IncS" "Documentation.SBV.Examples.WeakestPreconditions.Basics" "sbv8.7DbQHjiKtor73WzWR2O4MT3" False) (C1 (MetaCons "IncS" PrefixI True) (S1 (MetaSel (Just "x") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Just "y") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a))) 
The algorithm
algorithm :: Stmt I > Stmt I > Stmt I Source #
The increment algorithm:
y = x+1
The point here isn't really that this program is interesting, but we want to demonstrate various aspects of WP proofs. So, we take a before and after program to annotate our algorithm so we can experiment later.
Precondition for our program. Strictly speaking, we don't really need any preconditions,
but for example purposes, we'll require x
to be nonnegative.
imperativeInc :: Stmt I > Stmt I > Program I Source #
A program is the algorithm, together with its pre and postconditions.
Correctness
correctness :: Stmt I > Stmt I > IO (ProofResult (IncS Integer)) Source #
State the correctness with respect to before/after programs. In the simple case of nothing prior/after, we have the obvious proof:
>>>
correctness Skip Skip
Total correctness is established. Q.E.D.
Example proof attempts
It is instructive to look at how the proof changes as we put in different pre
and post
values.
Violating the post condition
If we stick in an extra increment for y
after, we can easily break the postcondition:
>>>
:set XNamedFieldPuns
>>>
import Control.Monad (void)
>>>
void $ correctness Skip $ Assign $ \st@IncS{y} > st{y = y+1}
Following proof obligation failed: ================================== Postcondition fails: Start: IncS {x = 0, y = 0} End : IncS {x = 0, y = 2}
We're told that the program ends up in a state where x=0
and y=2
, violating the requirement y=x+1
, as expected.
Using assert
There are two main use cases for assert
, which merely ends up being a call to Abort
.
One is making sure the inputs are well formed. And the other is the user putting in their
own invariants into the code.
Let's assume that we only want to accept strictly positive values of x
. We can try:
>>>
void $ correctness (assert "x > 0" (\st@IncS{x} > x .> 0)) Skip
Following proof obligation failed: ================================== Abort "x > 0" condition is satisfiable: Before: IncS {x = 0, y = 0} After : IncS {x = 0, y = 0}
Recall that our precondition (pre
) required x
to be nonnegative. So, we can put in something weaker and it would be fine:
>>>
void $ correctness (assert "x > 5" (\st@IncS{x} > x .> 5)) Skip
Total correctness is established.
In this case the precondition to our program ensures that the assert
will always be satisfied.
As another example, let us put a post assertion that y
is even:
>>>
void $ correctness Skip (assert "y is even" (\st@IncS{y} > y `sMod` 2 .== 0))
Following proof obligation failed: ================================== Abort "y is even" condition is satisfiable: Before: IncS {x = 0, y = 0} After : IncS {x = 0, y = 1}
It is important to emphasize that you can put whatever invariant you might want:
>>>
void $ correctness Skip (assert "y > x" (\st@IncS{x, y} > y .> x))
Total correctness is established.
Violating stability
What happens if our program modifies x
? After all, we can simply set x=10
and y=11
and our post condition would be satisfied:
>>>
void $ correctness Skip (Assign $ \st > st{x = 10, y = 11})
Following proof obligation failed: ================================== Stability fails for "x": Before: IncS {x = 0, y = 1} After : IncS {x = 10, y = 11}
So, the stability condition prevents programs from cheating!