sbv-8.4: 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

Contents

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
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-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

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.