Copyright | Levent Erkok |
---|---|
License | BSD3 |
Maintainer | erkokl@gmail.com |
Stability | experimental |
Safe Haskell | None |
Language | Haskell2010 |
Documentation.SBV.Examples.WeakestPreconditions.Append
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.
Program state
The state of the length program, paramaterized over the element type a
Constructors
AppS | |
Instances
Queriable IO (AppS Integer) (AppC Integer) Source # |
|
(SymVal a, Show a) => Show (AppS a) Source # | Show instance for |
Generic (AppS a) Source # | |
SymVal a => Mergeable (AppS a) Source # | |
type Rep (AppS a) Source # | |
Defined in Documentation.SBV.Examples.WeakestPreconditions.Append type Rep (AppS a) = D1 ('MetaData "AppS" "Documentation.SBV.Examples.WeakestPreconditions.Append" "sbv-8.7-9mSEXJN8olRBwPWTmi3EMV" '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))))) |
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] |
The algorithm
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.