sbv-10.2: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | Safe-Inferred
Language | Haskell2010

Documentation.SBV.Examples.WeakestPreconditions.GCD

Contents

- Program state
- The algorithm
- Correctness
- Concrete execution

Description

Proof of correctness of an imperative GCD (greatest-common 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.

Synopsis

- data GCDS a = GCDS {
  - x :: a
  - y :: a
  - i :: a
  - j :: a
  }
- type G = GCDS SInteger
- algorithm :: Stmt G
- gcd :: SInteger -> SInteger -> SInteger
- axiomatizeGCD :: Symbolic ()
- pre :: G -> SBool
- post :: G -> SBool
- noChange :: Stable G
- imperativeGCD :: Program G
- correctness :: IO (ProofResult (GCDS Integer))

# Documentation

    >>> -- For doctest purposes only:
    >>> import Data.SBV
    >>> import Data.SBV.Control
    >>> import Data.SBV.Tools.WeakestPreconditions

# Program state

data GCDS a Source #

The state for the sum program, parameterized over a base type `a`.

Constructors

GCDS |

Fields

- x :: a

  First value

- y :: a

  Second value

- i :: a

  Copy of x to be modified

- j :: a

  Copy of y to be modified

#### Instances

Instances details

Foldable GCDS Source # |

Instance details

Defined in Documentation.SBV.Examples.WeakestPreconditions.GCD

Methods

fold :: Monoid m => GCDS m -> m Source #

foldMap :: Monoid m => (a -> m) -> GCDS a -> m Source #

foldMap' :: Monoid m => (a -> m) -> GCDS a -> m Source #

foldr :: (a -> b -> b) -> b -> GCDS a -> b Source #

foldr' :: (a -> b -> b) -> b -> GCDS a -> b Source #

foldl :: (b -> a -> b) -> b -> GCDS a -> b Source #

foldl' :: (b -> a -> b) -> b -> GCDS a -> b Source #

foldr1 :: (a -> a -> a) -> GCDS a -> a Source #

foldl1 :: (a -> a -> a) -> GCDS a -> a Source #

toList :: GCDS a -> [a] Source #

null :: GCDS a -> Bool Source #

length :: GCDS a -> Int Source #

elem :: Eq a => a -> GCDS a -> Bool Source #

maximum :: Ord a => GCDS a -> a Source #

minimum :: Ord a => GCDS a -> a Source #

sum :: Num a => GCDS a -> a Source #

product :: Num a => GCDS a -> a Source #

Traversable GCDS Source # |
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.GCD Methods traverse :: Applicative f => (a -> f b) -> GCDS a -> f (GCDS b) Source # sequenceA :: Applicative f => GCDS (f a) -> f (GCDS a) Source # mapM :: Monad m => (a -> m b) -> GCDS a -> m (GCDS b) Source # sequence :: Monad m => GCDS (m a) -> m (GCDS a) Source #
Functor GCDS Source # |
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.GCD Methods fmap :: (a -> b) -> GCDS a -> GCDS b Source # (<$) :: a -> GCDS b -> GCDS a Source #
SymVal a => Fresh IO (GCDS (SBV a)) Source # | `Fresh` instance for the program state
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.GCD Methods fresh :: QueryT IO (GCDS (SBV a)) Source #
Generic (GCDS a) Source # |
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.GCD Associated Types type Rep (GCDS a) :: Type -> Type Source # Methods from :: GCDS a -> Rep (GCDS a) x Source # to :: Rep (GCDS a) x -> GCDS a Source #
(SymVal a, Show a) => Show (GCDS (SBV a)) Source # | Show instance for `GCDS`. The above deriving clause would work just as well, but we want it to be a little prettier here, and hence the `OVERLAPS` directive.
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.GCD Methods showsPrec :: Int -> GCDS (SBV a) -> ShowS Source # show :: GCDS (SBV a) -> String Source # showList :: [GCDS (SBV a)] -> ShowS Source #
Show a => Show (GCDS a) Source # |
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.GCD Methods showsPrec :: Int -> GCDS a -> ShowS Source # show :: GCDS a -> String Source # showList :: [GCDS a] -> ShowS Source #
Mergeable a => Mergeable (GCDS a) Source # |
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.GCD Methods symbolicMerge :: Bool -> SBool -> GCDS a -> GCDS a -> GCDS a Source # select :: (Ord b, SymVal b, Num b) => [GCDS a] -> GCDS a -> SBV b -> GCDS a Source #
type Rep (GCDS a) Source # |

Instance details

Defined in Documentation.SBV.Examples.WeakestPreconditions.GCD

type Rep (GCDS a) = D1 ('MetaData "GCDS" "Documentation.SBV.Examples.WeakestPreconditions.GCD" "sbv-10.2-H7C8tpOUfNc9yHFfX3krPk" '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))))

type G = GCDS SInteger Source #

Helper type synonym

# The algorithm

algorithm :: Stmt G Source #

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.

pre :: G -> SBool Source #

Precondition for our program: `x` and `y` must be strictly positive

post :: G -> SBool Source #

Postcondition for our program: `i == j` and `i = gcd x y`

noChange :: Stable G Source #

Stability condition: Program must leave `x` and `y` unchanged.

imperativeGCD :: Program G Source #

A program is the algorithm, together with its pre- and post-conditions.

# 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 counter-examples. 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 concrete-execution 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`.