Copyright  (c) Levent Erkok 

License  BSD3 
Maintainer  erkokl@gmail.com 
Stability  experimental 
Safe Haskell  None 
Language  Haskell2010 
Proof of correctness of an imperative integer division algorithm, using weakest preconditions. The algorithm simply keeps subtracting the divisor until the desired quotient and the remainder is found.
Program state
The state for the division program, parameterized over a base type a
.
Instances
Functor DivS Source #  
Foldable DivS Source #  
Defined in Documentation.SBV.Examples.WeakestPreconditions.IntDiv fold :: Monoid m => DivS m > m # foldMap :: Monoid m => (a > m) > DivS a > m # foldr :: (a > b > b) > b > DivS a > b # foldr' :: (a > b > b) > b > DivS a > b # foldl :: (b > a > b) > b > DivS a > b # foldl' :: (b > a > b) > b > DivS a > b # foldr1 :: (a > a > a) > DivS a > a # foldl1 :: (a > a > a) > DivS a > a # elem :: Eq a => a > DivS a > Bool # maximum :: Ord a => DivS a > a #  
Traversable DivS Source #  
(SymVal a, SMTValue a) => Fresh IO (DivS (SBV a)) Source # 

Show a => Show (DivS a) Source #  
(SymVal a, Show a) => Show (DivS (SBV a)) Source #  Show instance for 
Generic (DivS a) Source #  
Mergeable a => Mergeable (DivS a) Source #  
type Rep (DivS a) Source #  
Defined in Documentation.SBV.Examples.WeakestPreconditions.IntDiv type Rep (DivS a) = D1 (MetaData "DivS" "Documentation.SBV.Examples.WeakestPreconditions.IntDiv" "sbv8.6DBvpUlQTqMsBJjjQk7wU8u" False) (C1 (MetaCons "DivS" PrefixI True) ((S1 (MetaSel (Just "x") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Just "y") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a)) :*: (S1 (MetaSel (Just "q") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Just "r") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a)))) 
The algorithm
algorithm :: Invariant D > Maybe (Measure D) > Stmt D Source #
The imperative division algorithm, assuming nonnegative x
and strictly positive y
:
r = x  set remainder to x q = 0  set quotient to 0 while y <= r  while we can still subtract r = r  y  reduce the remainder q = q + 1  increase the quotient
Note that we need to explicitly annotate each loop with its invariant and the termination measure. For convenience, we take those two as parameters for simplicity.
Precondition for our program: x
must nonnegative and y
must be strictly positive.
Note that there is an explicit call to abort
in our program to protect against this case, so
if we do not have this precondition, all programs will fail.
Postcondition for our program: Remainder must be nonnegative and less than y
,
and it must hold that x = q*y + r
:
imperativeDiv :: Invariant D > Maybe (Measure D) > Program D Source #
A program is the algorithm, together with its pre and postconditions.
Correctness
invariant :: Invariant D Source #
The invariant is simply that x = q * y + r
holds at all times and r
is strictly positive.
We need the y > 0
part of the invariant to establish the measure decreases, which is guaranteed
by our precondition.
The measure. In each iteration r
decreases, but always remains positive.
Since y
is strictly positive, r
can serve as a measure for the loop.
correctness :: IO () Source #
Check that the program terminates and the post condition holds. We have:
>>>
correctness
Total correctness is established. Q.E.D.