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

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

Documentation.SBV.Examples.WeakestPreconditions.Sum

Contents

- Program state
- The algorithm
- Correctness
- Example proof attempts

Description

Proof of correctness of an imperative summation algorithm, using weakest preconditions. We investigate a few different invariants and see how different versions lead to proofs and failures.

Synopsis

- data SumS a = SumS {
  - n :: a
  - i :: a
  - s :: a
  }
- type S = SumS SInteger
- algorithm :: Invariant S -> Maybe (Measure S) -> Stmt S
- pre :: S -> SBool
- post :: S -> SBool
- noChange :: Stable S
- imperativeSum :: Invariant S -> Maybe (Measure S) -> Program S
- correctness :: Invariant S -> Maybe (Measure S) -> IO (ProofResult (SumS Integer))

# Program state

data SumS a Source #

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

Constructors

SumS |

Fields

- n :: a

  The input value

- i :: a

  Loop counter

- s :: a

  Running sum

#### Instances

Instances details

Functor SumS Source # |
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.Sum Methods fmap :: (a -> b) -> SumS a -> SumS b (<$) :: a -> SumS b -> SumS a
Foldable SumS Source # |

Instance details

Defined in Documentation.SBV.Examples.WeakestPreconditions.Sum

Methods

fold :: Monoid m => SumS m -> m

foldMap :: Monoid m => (a -> m) -> SumS a -> m

foldMap' :: Monoid m => (a -> m) -> SumS a -> m

foldr :: (a -> b -> b) -> b -> SumS a -> b

foldr' :: (a -> b -> b) -> b -> SumS a -> b

foldl :: (b -> a -> b) -> b -> SumS a -> b

foldl' :: (b -> a -> b) -> b -> SumS a -> b

foldr1 :: (a -> a -> a) -> SumS a -> a

foldl1 :: (a -> a -> a) -> SumS a -> a

toList :: SumS a -> [a]

null :: SumS a -> Bool

length :: SumS a -> Int

elem :: Eq a => a -> SumS a -> Bool

maximum :: Ord a => SumS a -> a

minimum :: Ord a => SumS a -> a

sum :: Num a => SumS a -> a

product :: Num a => SumS a -> a

Traversable SumS Source # |
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.Sum Methods traverse :: Applicative f => (a -> f b) -> SumS a -> f (SumS b) sequenceA :: Applicative f => SumS (f a) -> f (SumS a) mapM :: Monad m => (a -> m b) -> SumS a -> m (SumS b) sequence :: Monad m => SumS (m a) -> m (SumS a)
SymVal a => Fresh IO (SumS (SBV a)) Source # | `Fresh` instance for the program state
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.Sum Methods fresh :: QueryT IO (SumS (SBV a)) Source #
Show a => Show (SumS a) Source # |
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.Sum Methods showsPrec :: Int -> SumS a -> ShowS show :: SumS a -> String showList :: [SumS a] -> ShowS
(SymVal a, Show a) => Show (SumS (SBV a)) Source # | Show instance for `SumS`. 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.Sum Methods showsPrec :: Int -> SumS (SBV a) -> ShowS show :: SumS (SBV a) -> String showList :: [SumS (SBV a)] -> ShowS
Generic (SumS a) Source # |
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.Sum Associated Types type Rep (SumS a) :: Type -> Type Methods from :: SumS a -> Rep (SumS a) x to :: Rep (SumS a) x -> SumS a
Mergeable a => Mergeable (SumS a) Source # |
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.Sum Methods symbolicMerge :: Bool -> SBool -> SumS a -> SumS a -> SumS a Source # select :: (Ord b, SymVal b, Num b) => [SumS a] -> SumS a -> SBV b -> SumS a Source #
type Rep (SumS a) Source # |

Instance details

Defined in Documentation.SBV.Examples.WeakestPreconditions.Sum

type Rep (SumS a) = D1 ('MetaData "SumS" "Documentation.SBV.Examples.WeakestPreconditions.Sum" "sbv-8.7-9mSEXJN8olRBwPWTmi3EMV" 'False) (C1 ('MetaCons "SumS" 'PrefixI 'True) (S1 ('MetaSel ('Just "n") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: (S1 ('MetaSel ('Just "i") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Just "s") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a))))

type S = SumS SInteger Source #

Helper type synonym

# The algorithm

algorithm :: Invariant S -> Maybe (Measure S) -> Stmt S Source #

The imperative summation algorithm:

       i = 0
       s = 0
       while i < n
         i = i+1
         s = s+i

Note that we need to explicitly annotate each loop with its invariant and the termination measure. For convenience, we take those two as parameters, so we can experiment later.

pre :: S -> SBool Source #

Precondition for our program: `n` must be non-negative. 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.

post :: S -> SBool Source #

Postcondition for our program: `s` must be the sum of all numbers up to and including `n`.

noChange :: Stable S Source #

Stability condition: Program must leave `n` unchanged.

imperativeSum :: Invariant S -> Maybe (Measure S) -> Program S Source #

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

# Correctness

correctness :: Invariant S -> Maybe (Measure S) -> IO (ProofResult (SumS Integer)) Source #

Check that the program terminates and `s` equals `n*(n+1)/2` upon termination, i.e., the sum of all numbers upto `n`. Note that this only holds if `n >= 0` to start with, as guaranteed by the precondition of our program.

The correct termination measure is `n-i`: It goes down in each iteration provided we start with `n >= 0` and it always remains non-negative while the loop is executing. Note that we do not need a lexicographic measure in this case, hence we simply return a list of one element.

The correct invariant is a conjunction of two facts. First, `s` is equivalent to the sum of numbers `0` upto `i`. This clearly holds at the beginning when `i = s = 0`, and is maintained in each iteration of the body. Second, it always holds that `i <= n` as long as the loop executes, both before and after each execution of the body. When the loop terminates, it holds that `i = n`. Since the invariant says `s` is the sum of all numbers up to but not including `i`, we conclude that `s` is the sum of all numbers up to and including `n`, as requested.

Note that coming up with this invariant is neither trivial, nor easy to automate by any means. What SBV provides is a way to check that your invariant and termination measures are correct, not a means of coming up with them in the first place.

We have:

    >>> :set -XNamedFieldPuns
    >>> let invariant SumS{n, i, s} = s .== (i*(i+1)) `sDiv` 2 .&& i .<= n
    >>> let measure   SumS{n, i}    = [n - i]
    >>> correctness invariant (Just measure)
    Total correctness is established.
    Q.E.D.

# Example proof attempts

It is instructive to look at several proof attempts to see what can go wrong and how the weakest-precondition engine behaves.

## Always false invariant

Let's see what happens if we have an always false invariant. Clearly, this will not do the job, but it is instructive to see the output. For this exercise, we are only interested in partial correctness (to see the impact of the invariant only), so we will simply use `Nothing` for the measures.

    >>> import Control.Monad (void)
    >>> let invariant _ = sFalse
    >>> void $ correctness invariant Nothing
    Following proof obligation failed:
    ==================================
      Invariant for loop "i < n" fails upon entry:
        SumS {n = 0, i = 0, s = 0}

When the invariant is constant false, it fails upon entry to the loop, and thus the proof itself fails.

## Always true invariant

The invariant must hold prior to entry to the loop, after the loop-body executes, and must be strong enough to establish the postcondition. The easiest thing to try would be the invariant that always returns true:

    >>> let invariant _ = sTrue
    >>> void $ correctness invariant Nothing
    Following proof obligation failed:
    ==================================
      Postcondition fails:
        Start: SumS {n = 0, i = 0, s = 0}
        End  : SumS {n = 0, i = 0, s = 1}

In this case, we are told that the end state does not establish the post-condition. Indeed when `n=0`, we would expect `s=0`, not `s=1`.

The natural question to ask is how did SBV come up with this unexpected state at the end of the program run? If you think about the program execution, indeed this state is unreachable: We know that `s` represents the sum of all numbers up to `i`, so if `i=0`, we would expect `s` to be `0`. Our invariant is clearly an overapproximation of the reachable space, and SBV is telling us that we need to constrain and outlaw the state `{n = 0, i = 0, s = 1}`. Clearly, the invariant has to state something about the relationship between `i` and `s`, which we are missing in this case.

## Failing to maintain the invariant

What happens if we pose an invariant that the loop actually does not maintain? Here is an example:

    >>> let invariant SumS{n, i, s} = s .<= i .&& s .== (i*(i+1)) `sDiv` 2 .&& i .<= n
    >>> void $ correctness invariant Nothing
    Following proof obligation failed:
    ==================================
      Invariant for loop "i < n" is not maintaned by the body:
        Before: SumS {n = 2, i = 1, s = 1}
        After : SumS {n = 2, i = 2, s = 3}

Here, we posed the extra incorrect invariant that `s <= i` must be maintained, and SBV found us a reachable state that violates the invariant. The before state indeed satisfies `s <= i`, but the after state does not. Note that the proof fails in this case not because the program is incorrect, but the stipulated invariant is not valid.

## Having a bad measure, Part I

The termination measure must always be non-negative:

    >>> let invariant SumS{n, i, s} = s .== (i*(i+1)) `sDiv` 2 .&& i .<= n
    >>> let measure   SumS{n, i}    = [- i]
    >>> void $ correctness invariant (Just measure)
    Following proof obligation failed:
    ==================================
      Measure for loop "i < n" is negative:
        State  : SumS {n = 3, i = 2, s = 3}
        Measure: -2

The failure is pretty obvious in this case: Measure produces a negative value.

## Having a bad measure, Part II

The other way we can have a bad measure is if it fails to decrease through the loop body:

    >>> let invariant SumS{n, i, s} = s .== (i*(i+1)) `sDiv` 2 .&& i .<= n
    >>> let measure   SumS{n, i}    = [n + i]
    >>> void $ correctness invariant (Just measure)
    Following proof obligation failed:
    ==================================
      Measure for loop "i < n" does not decrease:
        Before : SumS {n = 1, i = 0, s = 0}
        Measure: 1
        After  : SumS {n = 1, i = 1, s = 1}
        Measure: 2

Clearly, as `i` increases, so does our bogus measure `n+i`. Note that a counterexample where `i` is negative is also possible for this failure, as the SMT solver will find a counter-example to induction, not necessarily a reachable state. Obviously, all such failures need to be addressed for the full proof.