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

Copyright Levent Erkok BSD3 erkokl@gmail.com experimental None 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.

Synopsis

# Program state

data AppS a Source #

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

Constructors

 AppS Fieldsxs :: SList aThe first input listys :: SList aThe second input listts :: SList aTemporary variablezs :: SList aOutput
Instances
 Source # Queriable instance for the program state Instance details Methods (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 MethodsshowsPrec :: Int -> AppS a -> ShowS #show :: AppS a -> String #showList :: [AppS a] -> ShowS # Generic (AppS a) Source # Instance details Associated Typestype Rep (AppS a) :: Type -> Type # Methodsfrom :: AppS a -> Rep (AppS a) x #to :: Rep (AppS a) x -> AppS a # SymVal a => Mergeable (AppS a) Source # Instance details MethodssymbolicMerge :: 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 type Rep (AppS a) = D1 (MetaData "AppS" "Documentation.SBV.Examples.WeakestPreconditions.Append" "sbv-8.2-BpcWyxFKVuJBXlUtpLk21" 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)))))

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
 Source # Queriable instance for the program state Instance details Methods Show a => Show (AppC a) Source # Show instance, a bit more prettier than what would be derived: Instance details MethodsshowsPrec :: Int -> AppC a -> ShowS #show :: AppC a -> String #showList :: [AppC a] -> ShowS #

type A = AppS Integer Source #

Helper type synonym

# 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


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

# Correctness

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

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