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

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

Documentation.SBV.Examples.WeakestPreconditions.Append

Contents

- Program state
- The algorithm
- Correctness

Description

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

Synopsis

- data AppS a = AppS {
  - xs :: SList a
  - ys :: SList a
  - ts :: SList a
  - zs :: SList a
  }
- data AppC a = AppC [a] [a] [a] [a]
- type A = AppS Integer
- algorithm :: Stmt A
- imperativeAppend :: Program A
- correctness :: IO (ProofResult (AppC Integer))

# Program state

data AppS a Source #

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

Constructors

AppS |

Fields

- xs :: SList a

  The first input list

- ys :: SList a

  The second input list

- ts :: SList a

  Temporary variable

- zs :: SList a

  Output

#### Instances

Instances details

Queriable IO (AppS Integer) Source # | `Queriable` instance for the program state
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.Append Associated Types type QueryResult (AppS Integer) Source # Methods create :: QueryT IO (AppS Integer) Source # project :: AppS Integer -> QueryT IO (QueryResult (AppS Integer)) Source # embed :: QueryResult (AppS Integer) -> QueryT IO (AppS Integer) Source #
Generic (AppS a) Source # |
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.Append Associated Types type Rep (AppS a) :: Type -> Type Source # Methods from :: AppS a -> Rep (AppS a) x Source # to :: Rep (AppS a) x -> AppS a Source #
(SymVal a, Show a) => Show (AppS a) Source # | Show instance for `AppS`. 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.Append Methods showsPrec :: Int -> AppS a -> ShowS Source # show :: AppS a -> String Source # showList :: [AppS a] -> ShowS Source #
SymVal a => Mergeable (AppS a) Source # |
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.Append Methods symbolicMerge :: Bool -> SBool -> AppS a -> AppS a -> AppS a Source # select :: (Ord b, SymVal b, Num b) => [AppS a] -> AppS a -> SBV b -> AppS a Source #
type Rep (AppS a) Source # |

Instance details

Defined in Documentation.SBV.Examples.WeakestPreconditions.Append

type Rep (AppS a) = D1 ('MetaData "AppS" "Documentation.SBV.Examples.WeakestPreconditions.Append" "sbv-10.2-Gi6nXbGJVKyDE1oJouGknK" 'False) (C1 ('MetaCons "AppS" '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 "ts") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (SList a)) :*: S1 ('MetaSel ('Just "zs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (SList a)))))

type QueryResult (AppS Integer) Source # |
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.Append type QueryResult (AppS Integer) = AppC Integer

data AppC a Source #

The concrete counterpart of `AppS`. Again, we can't simply use the duality between `SBV a` and `a` due to the difference between `SList a` and `[a]`.

Constructors

AppC [a] [a] [a] [a] |

#### Instances

Instances details

Show a => Show (AppC a) Source # | Show instance, a bit more prettier than what would be derived:
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.Append Methods showsPrec :: Int -> AppC a -> ShowS Source # show :: AppC a -> String Source # showList :: [AppC a] -> ShowS Source #

type A = AppS Integer Source #

Helper type synonym

# The algorithm

algorithm :: Stmt A Source #

The imperative append algorithm:

       zs = []
       ts = xs
       while not (null ts)
         zs = zs ++ [head ts]
         ts = tail ts
       ts = ys
       while not (null ts)
         zs = zs ++ [head ts]
         ts = tail ts

imperativeAppend :: Program A Source #

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

# Correctness

correctness :: IO (ProofResult (AppC Integer)) Source #

We check that `zs` is `xs ++ ys` upon termination.

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