Documentation.SBV.Examples.WeakestPreconditions.Append

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

data AppS a

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)

Queriable instance for the program state

Defined in Documentation.SBV.Examples.WeakestPreconditions.Append

Methods

create :: QueryT IO (AppS Integer)

project :: AppS Integer -> QueryT IO (AppC Integer)

embed :: AppC Integer -> QueryT IO (AppS Integer)

Generic (AppS a)

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, Show a) => Show (AppS a)

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.

Defined in Documentation.SBV.Examples.WeakestPreconditions.Append

Methods

showsPrec :: Int -> AppS a -> ShowS

show :: AppS a -> String

showList :: [AppS a] -> ShowS

SymVal a => Mergeable (AppS a)

Defined in Documentation.SBV.Examples.WeakestPreconditions.Append

Methods

symbolicMerge :: Bool -> SBool -> AppS a -> AppS a -> AppS a

select :: (Ord b, SymVal b, Num b) => [AppS a] -> AppS a -> SBV b -> AppS a

type Rep (AppS a)

Defined in Documentation.SBV.Examples.WeakestPreconditions.Append

type Rep (AppS a) = D1 ('MetaData "AppS" "Documentation.SBV.Examples.WeakestPreconditions.Append" "sbv-9.1-K2obF3Nc7RH75SD7QUXzc3" '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

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)

Queriable instance for the program state

Defined in Documentation.SBV.Examples.WeakestPreconditions.Append

Methods

create :: QueryT IO (AppS Integer)

project :: AppS Integer -> QueryT IO (AppC Integer)

embed :: AppC Integer -> QueryT IO (AppS Integer)

Show a => Show (AppC a)

Show instance, a bit more prettier than what would be derived:

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

Helper type synonym

The algorithm

algorithm :: Stmt A

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

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

Correctness

correctness :: IO (ProofResult (AppC Integer))

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

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