Copyright  (c) Levent Erkok 

License  BSD3 
Maintainer  erkokl@gmail.com 
Stability  experimental 
Safe Haskell  None 
Language  Haskell2010 
Proof of correctness of an imperative integer squareroot algorithm, using
weakest preconditions. The algorithm computes the floor of the squareroot
of a given nonnegative integer by keeping a running some of all odd numbers
starting from 1. Recall that 1+3+5+...+(2n+1) = (n+1)^2
, thus we can
stop the counting when we exceed the input number.
Program state
The state for the division program, parameterized over a base type a
.
Instances
Functor SqrtS Source #  
Foldable SqrtS Source #  
Defined in Documentation.SBV.Examples.WeakestPreconditions.IntSqrt fold :: Monoid m => SqrtS m > m # foldMap :: Monoid m => (a > m) > SqrtS a > m # foldr :: (a > b > b) > b > SqrtS a > b # foldr' :: (a > b > b) > b > SqrtS a > b # foldl :: (b > a > b) > b > SqrtS a > b # foldl' :: (b > a > b) > b > SqrtS a > b # foldr1 :: (a > a > a) > SqrtS a > a # foldl1 :: (a > a > a) > SqrtS a > a # elem :: Eq a => a > SqrtS a > Bool # maximum :: Ord a => SqrtS a > a # minimum :: Ord a => SqrtS a > a #  
Traversable SqrtS Source #  
(SymVal a, SMTValue a) => Fresh IO (SqrtS (SBV a)) Source # 

Show a => Show (SqrtS a) Source #  
(SymVal a, Show a) => Show (SqrtS (SBV a)) Source #  Show instance for 
Generic (SqrtS a) Source #  
Mergeable a => Mergeable (SqrtS a) Source #  
type Rep (SqrtS a) Source #  
Defined in Documentation.SBV.Examples.WeakestPreconditions.IntSqrt type Rep (SqrtS a) = D1 (MetaData "SqrtS" "Documentation.SBV.Examples.WeakestPreconditions.IntSqrt" "sbv8.6DBvpUlQTqMsBJjjQk7wU8u" False) (C1 (MetaCons "SqrtS" PrefixI True) ((S1 (MetaSel (Just "x") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Just "sqrt") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a)) :*: (S1 (MetaSel (Just "i") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Just "j") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a)))) 
The algorithm
algorithm :: Invariant S > Maybe (Measure S) > Stmt S Source #
The imperative squareroot algorithm, assuming nonnegative x
sqrt = 0  set sqrt to 0 i = 1  set i to 1, sum of j's so far j = 1  set j to be the first odd number i while i <= x  while the sum hasn't exceeded x yet sqrt = sqrt + 1  increase the sqrt j = j + 2  next odd number i = i + j  running sum of j's
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 be nonnegative. 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: The sqrt
squared must be less than or equal to x
, and
sqrt+1
squared must strictly exceed x
.
imperativeSqrt :: Invariant S > Maybe (Measure S) > Program S Source #
A program is the algorithm, together with its pre and postconditions.
Correctness
invariant :: Invariant S Source #
The invariant is that at each iteration of the loop sqrt
remains below or equal
to the actual squareroot, and i
tracks the square of the next value. We also
have that j
is the sqrt
'th odd value. Coming up with this invariant is not for
the faint of heart, for details I would strongly recommend looking at Manna's seminal
Mathematical Theory of Computation book (chapter 3). The j .> 0
part is needed
to establish the termination.
The measure. In each iteration i
strictly increases, thus reducing the differential x  i
correctness :: IO () Source #
Check that the program terminates and the post condition holds. We have:
>>>
correctness
Total correctness is established. Q.E.D.