Copyright  (c) Levent Erkok 

License  BSD3 
Maintainer  erkokl@gmail.com 
Stability  experimental 
Safe Haskell  None 
Language  Haskell2010 
Proof of correctness of an imperative GCD (greatestcommon divisor) algorithm, using weakest preconditions. The termination measure here illustrates the use of lexicographic ordering. Also, since symbolic version of GCD is not symbolically terminating, this is another example of using uninterpreted functions and axioms as one writes specifications for WP proofs.
Program state
The state for the sum program, parameterized over a base type a
.
Instances
Functor GCDS Source #  
Foldable GCDS Source #  
Defined in Documentation.SBV.Examples.WeakestPreconditions.GCD fold :: Monoid m => GCDS m > m # foldMap :: Monoid m => (a > m) > GCDS a > m # foldr :: (a > b > b) > b > GCDS a > b # foldr' :: (a > b > b) > b > GCDS a > b # foldl :: (b > a > b) > b > GCDS a > b # foldl' :: (b > a > b) > b > GCDS a > b # foldr1 :: (a > a > a) > GCDS a > a # foldl1 :: (a > a > a) > GCDS a > a # elem :: Eq a => a > GCDS a > Bool # maximum :: Ord a => GCDS a > a #  
Traversable GCDS Source #  
(SymVal a, SMTValue a) => Fresh IO (GCDS (SBV a)) Source # 

Show a => Show (GCDS a) Source #  
(SymVal a, Show a) => Show (GCDS (SBV a)) Source #  Show instance for 
Generic (GCDS a) Source #  
Mergeable a => Mergeable (GCDS a) Source #  
type Rep (GCDS a) Source #  
Defined in Documentation.SBV.Examples.WeakestPreconditions.GCD type Rep (GCDS a) = D1 (MetaData "GCDS" "Documentation.SBV.Examples.WeakestPreconditions.GCD" "sbv8.2BpcWyxFKVuJBXlUtpLk21" False) (C1 (MetaCons "GCDS" PrefixI True) ((S1 (MetaSel (Just "x") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Just "y") 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
The imperative GCD algorithm, assuming strictly positive x
and y
:
i = x j = y while i != j  While not equal if i > j i = i  j  i is greater; reduce it by j else j = j  i  j is greater; reduce it by i
When the loop terminates, i
equals j
and contains GCD(x, y)
.
gcd :: SInteger > SInteger > SInteger Source #
Symbolic GCD as our specification. Note that we cannot really implement the GCD function since it is not symbolically terminating. So, we instead uninterpret and axiomatize it below.
NB. The concrete part of the definition is only used in calls to traceExecution
and is not needed for the proof. If you don't need to call traceExecution
, you
can simply ignore that part and directly uninterpret. In that case, we simply
use Prelude's version.
axiomatizeGCD :: Symbolic () Source #
Constraints and axioms we need to state explicitly to tell the SMT solver about our specification for GCD.
imperativeGCD :: Program G Source #
A program is the algorithm, together with its pre and postconditions.
Correctness
correctness :: IO (ProofResult (GCDS Integer)) Source #
With the axioms in place, it is trivial to establish correctness:
>>>
correctness
Total correctness is established. Q.E.D.
Note that I found this proof to be quite fragile: If you do not get the algorithm right or the axioms aren't in place, z3 simply goes to an infinite loop, instead of providing counterexamples. Of course, this is to be expected with the quantifiers present.
Concrete execution
Example concrete run. As we mentioned in the definition for gcd
, the concreteexecution
function cannot deal with uninterpreted functions and axioms for obvious reasons. In those
cases we revert to the concrete definition. Here's an example run:
>>>
traceExecution imperativeGCD $ GCDS {x = 14, y = 4, i = 0, j = 0}
*** Precondition holds, starting execution: {x = 14, y = 4, i = 0, j = 0} ===> [1.1] Conditional, taking the "then" branch {x = 14, y = 4, i = 0, j = 0} ===> [1.1.1] Skip {x = 14, y = 4, i = 0, j = 0} ===> [1.2] Assign {x = 14, y = 4, i = 14, j = 4} ===> [1.3] Loop "i != j": condition holds, executing the body {x = 14, y = 4, i = 14, j = 4} ===> [1.3.{1}] Conditional, taking the "then" branch {x = 14, y = 4, i = 14, j = 4} ===> [1.3.{1}.1] Assign {x = 14, y = 4, i = 10, j = 4} ===> [1.3] Loop "i != j": condition holds, executing the body {x = 14, y = 4, i = 10, j = 4} ===> [1.3.{2}] Conditional, taking the "then" branch {x = 14, y = 4, i = 10, j = 4} ===> [1.3.{2}.1] Assign {x = 14, y = 4, i = 6, j = 4} ===> [1.3] Loop "i != j": condition holds, executing the body {x = 14, y = 4, i = 6, j = 4} ===> [1.3.{3}] Conditional, taking the "then" branch {x = 14, y = 4, i = 6, j = 4} ===> [1.3.{3}.1] Assign {x = 14, y = 4, i = 2, j = 4} ===> [1.3] Loop "i != j": condition holds, executing the body {x = 14, y = 4, i = 2, j = 4} ===> [1.3.{4}] Conditional, taking the "else" branch {x = 14, y = 4, i = 2, j = 4} ===> [1.3.{4}.2] Assign {x = 14, y = 4, i = 2, j = 2} ===> [1.3] Loop "i != j": condition fails, terminating {x = 14, y = 4, i = 2, j = 2} *** Program successfully terminated, post condition holds of the final state: {x = 14, y = 4, i = 2, j = 2} Program terminated successfully. Final state: {x = 14, y = 4, i = 2, j = 2}
As expected, gcd 14 4
is 2
.