sbv-9.0: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
CopyrightLevent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

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 

Fields

Instances

Instances details
Queriable IO (AppS Integer) (AppC Integer) Source #

Queriable instance for the program state

Instance details

Defined in Documentation.SBV.Examples.WeakestPreconditions.Append

(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-9.0-INK6XkxWq6t98anprLNznC" '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

Instances details
Queriable IO (AppS Integer) (AppC Integer) Source #

Queriable instance for the program state

Instance details

Defined in Documentation.SBV.Examples.WeakestPreconditions.Append

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.