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.Length

Contents

- Program state
- The algorithm
- Correctness

Description

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 {
  - xs :: SList a
  - ys :: SList a
  - l :: SInteger
  }
- 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

data LenS a Source #

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

Constructors

LenS |

Fields

- xs :: SList a

  The input list

- ys :: SList a

  Copy of input

- l :: SInteger

  Running length

#### Instances

Instances details

Queriable IO (LenS Integer) Source # | We have to write the bijection between `LenS` and `LenC` explicitly. Luckily, the definition is more or less boilerplate.
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.Length Associated Types type QueryResult (LenS Integer) Source # Methods create :: QueryT IO (LenS Integer) Source # project :: LenS Integer -> QueryT IO (QueryResult (LenS Integer)) Source # embed :: QueryResult (LenS Integer) -> QueryT IO (LenS Integer) Source #
Generic (LenS a) Source # |
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.Length Associated Types type Rep (LenS a) :: Type -> Type Source # Methods from :: LenS a -> Rep (LenS a) x Source # to :: Rep (LenS a) x -> LenS a Source #
(SymVal a, Show a) => Show (LenS a) Source # | Show instance: A simplified version of what would otherwise be generated.
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.Length Methods showsPrec :: Int -> LenS a -> ShowS Source # show :: LenS a -> String Source # showList :: [LenS a] -> ShowS Source #
SymVal a => Mergeable (LenS a) Source # |
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.Length Methods symbolicMerge :: Bool -> SBool -> LenS a -> LenS a -> LenS a Source # select :: (Ord b, SymVal b, Num b) => [LenS a] -> LenS a -> SBV b -> LenS a Source #
type Rep (LenS a) Source # |

Instance details

Defined in Documentation.SBV.Examples.WeakestPreconditions.Length

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

type QueryResult (LenS Integer) Source # |
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.Length type QueryResult (LenS Integer) = LenC Integer

data LenC a Source #

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.

Constructors

LenC [a] [a] Integer |

#### Instances

Instances details

Show a => Show (LenC a) Source # | Show instance: Similarly, we want to be a bit more concise here.
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.Length Methods showsPrec :: Int -> LenC a -> ShowS Source # show :: LenC a -> String Source # showList :: [LenC a] -> ShowS Source #

type S = LenS Integer Source #

Helper type synonym

# 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.

pre :: S -> SBool Source #

Precondition for our program. Nothing! It works for all lists.

post :: S -> SBool Source #

Postcondition for our program: `l` must be the length of the input list.

noChange :: Stable S Source #

Stability condition: Program must leave `xs` unchanged.

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.

measure :: Measure S Source #

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:

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