Copyright | (c) Levent Erkok |
---|---|

License | BSD3 |

Maintainer | erkokl@gmail.com |

Stability | experimental |

Safe Haskell | None |

Language | Haskell2010 |

Proof of correctness of an imperative list-length algorithm, using weakest preconditions. Illustrates the use of SBV's symbolic lists together with the WP algorithm.

## Synopsis

- data LenS a = LenS {}
- data LenC a = LenC [a] [a] Integer
- type S = LenS Integer
- algorithm :: Invariant S -> Maybe (Measure S) -> Stmt S
- pre :: S -> SBool
- post :: S -> SBool
- noChange :: Stable S
- imperativeLength :: Invariant S -> Maybe (Measure S) -> Program S
- invariant :: Invariant S
- measure :: Measure S
- correctness :: IO ()

# Program state

The state of the length program, paramaterized over the element type `a`

## Instances

Queriable IO (LenS Integer) (LenC Integer) Source # | We have to write the bijection between |

(SymVal a, Show a) => Show (LenS a) Source # | Show instance: A simplified version of what would otherwise be generated. |

Generic (LenS a) Source # | |

SymVal a => Mergeable (LenS a) Source # | |

type Rep (LenS a) Source # | |

Defined in Documentation.SBV.Examples.WeakestPreconditions.Length type Rep (LenS a) = D1 (MetaData "LenS" "Documentation.SBV.Examples.WeakestPreconditions.Length" "sbv-8.7-DbQHjiKtor73WzWR2O4MT3" False) (C1 (MetaCons "LenS" PrefixI True) (S1 (MetaSel (Just "xs") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (SList a)) :*: (S1 (MetaSel (Just "ys") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (SList a)) :*: S1 (MetaSel (Just "l") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 SInteger)))) |

The concrete counterpart to `LenS`

. Note that we can no longer use the duality
between `SBV a`

and `a`

as in other examples and just use one datatype for both.
This is because `SList a`

and `[a]`

are fundamentally different types. This can
be a bit confusing at first, but the point is that it is the list that is symbolic
in case of an `SList a`

, not that we have a concrete list with symbolic elements
in it. Subtle difference, but it is important to keep these two separate.

# The algorithm

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

The imperative length algorithm:

ys = xs l = 0 while not (null ys) l = l+1 ys = tail ys

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.

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

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

invariant :: Invariant S Source #

The invariant simply relates the length of the input to the length of the current suffix and the length of the prefix traversed so far.

The measure is obviously the length of `ys`

, as we peel elements off of it through the loop.

# Correctness

correctness :: IO () Source #

We check that `l`

is the length of the input list `xs`

upon termination.
Note that even though this is an inductive proof, it is fairly easy to prove with our SMT based
technology, which doesn't really handle induction at all! The usual inductive proof steps are baked
into the invariant establishment phase of the WP proof. We have:

`>>>`

Total correctness is established. Q.E.D.`correctness`