Copyright	Levent Erkok
License	BSD3
Maintainer	erkokl@gmail.com
Stability	experimental
Safe Haskell	None
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

Queriable IO (AppS Integer) (AppC Integer) Source #	`Queriable` instance for the program state
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.Append Methods create :: QueryT IO (AppS Integer) Source # project :: AppS Integer -> QueryT IO (AppC Integer) Source # embed :: AppC Integer -> QueryT IO (AppS Integer) 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 # show :: AppS a -> String # showList :: [AppS a] -> ShowS #
Generic (AppS a) Source #
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.Append Associated Types type Rep (AppS a) :: Type -> Type # Methods from :: AppS a -> Rep (AppS a) x # to :: Rep (AppS a) x -> AppS a #
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-8.4-LKcvIZGSCFCGr6QyM4W6l5" 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

Queriable IO (AppS Integer) (AppC Integer) Source #	`Queriable` instance for the program state
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.Append Methods create :: QueryT IO (AppS Integer) Source # project :: AppS Integer -> QueryT IO (AppC Integer) Source # embed :: AppC Integer -> QueryT IO (AppS Integer) Source #
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 # show :: AppC a -> String # showList :: [AppC a] -> ShowS #

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.