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 :: a
- ys :: a
- ts :: a
- zs :: a
}
type A = AppS (SList Integer)
algorithm :: Stmt A
imperativeAppend :: Program A
correctness :: IO (ProofResult (AppS [Integer]))

Program state

data AppS a Source #

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

Constructors

AppS
Fields xs :: a The first input list ys :: a The second input list ts :: a Temporary variable zs :: a Output

Instances

Instances details

Functor AppS Source #

Instance details

Defined in Documentation.SBV.Examples.WeakestPreconditions.Append

Methods

fmap :: (a -> b) -> AppS a -> AppS b #

(<$) :: a -> AppS b -> AppS a #

Foldable AppS Source #

Instance details

Defined in Documentation.SBV.Examples.WeakestPreconditions.Append

Methods

fold :: Monoid m => AppS m -> m #

foldMap :: Monoid m => (a -> m) -> AppS a -> m #

foldMap' :: Monoid m => (a -> m) -> AppS a -> m #

foldr :: (a -> b -> b) -> b -> AppS a -> b #

foldr' :: (a -> b -> b) -> b -> AppS a -> b #

foldl :: (b -> a -> b) -> b -> AppS a -> b #

foldl' :: (b -> a -> b) -> b -> AppS a -> b #

foldr1 :: (a -> a -> a) -> AppS a -> a #

foldl1 :: (a -> a -> a) -> AppS a -> a #

toList :: AppS a -> [a] #

null :: AppS a -> Bool #

length :: AppS a -> Int #

elem :: Eq a => a -> AppS a -> Bool #

maximum :: Ord a => AppS a -> a #

minimum :: Ord a => AppS a -> a #

sum :: Num a => AppS a -> a #

product :: Num a => AppS a -> a #

Traversable AppS Source #

Instance details

Defined in Documentation.SBV.Examples.WeakestPreconditions.Append

Methods

traverse :: Applicative f => (a -> f b) -> AppS a -> f (AppS b) #

sequenceA :: Applicative f => AppS (f a) -> f (AppS a) #

mapM :: Monad m => (a -> m b) -> AppS a -> m (AppS b) #

sequence :: Monad m => AppS (m a) -> m (AppS a) #

Queriable IO (AppS (SList Integer)) Source #

Queriable instance for the program state

Instance details

Defined in Documentation.SBV.Examples.WeakestPreconditions.Append

Associated Types

type QueryResult (AppS (SList Integer))
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.Append type QueryResult (AppS (SList Integer)) = AppS [Integer]

Methods

create :: QueryT IO (AppS (SList Integer)) Source #

project :: AppS (SList Integer) -> QueryT IO (QueryResult (AppS (SList Integer))) Source #

embed :: QueryResult (AppS (SList Integer)) -> QueryT IO (AppS (SList Integer)) Source #

Generic (AppS a) Source #

Instance details

Defined in Documentation.SBV.Examples.WeakestPreconditions.Append

Associated Types

type Rep (AppS a)

Instance details

Defined in Documentation.SBV.Examples.WeakestPreconditions.Append

type Rep (AppS a) = D1 ('MetaData "AppS" "Documentation.SBV.Examples.WeakestPreconditions.Append" "sbv-11.4-inplace" 'False) (C1 ('MetaCons "AppS" 'PrefixI 'True) ((S1 ('MetaSel ('Just "xs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Just "ys") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)) :*: (S1 ('MetaSel ('Just "ts") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Just "zs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a))))

Methods

from :: AppS a -> Rep (AppS a) x #

to :: Rep (AppS a) x -> AppS a #

Show (f a) => Show (AppS (f 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 -> AppS (f a) -> ShowS #

show :: AppS (f a) -> String #

showList :: [AppS (f a)] -> ShowS #

Mergeable 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, Num (SBV 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-11.4-inplace" 'False) (C1 ('MetaCons "AppS" 'PrefixI 'True) ((S1 ('MetaSel ('Just "xs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Just "ys") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)) :*: (S1 ('MetaSel ('Just "ts") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Just "zs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a))))

type QueryResult (AppS (SList Integer)) Source #

Instance details

Defined in Documentation.SBV.Examples.WeakestPreconditions.Append

type QueryResult (AppS (SList Integer)) = AppS [Integer]

type A = AppS (SList 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 (AppS [Integer])) Source #

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

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