Documentation.SBV.Examples.WeakestPreconditions.Length

Proof of correctness of an imperative list-length algorithm, using weakest preconditions. Illustrates the use of SBV's symbolic lists together with the WP algorithm.

Program state

data LenS a b

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

Constructors

LenS

Fields

• xs :: a

  The input list

• ys :: a

  Copy of input

• l :: b

  Running length

Instances

Queriable IO (LenS (SList Integer) SInteger)

Injection/projection from concrete and symbolic values.

Defined in Documentation.SBV.Examples.WeakestPreconditions.Length

Associated Types

type QueryResult (LenS (SList Integer) SInteger)

Defined in Documentation.SBV.Examples.WeakestPreconditions.Length

type QueryResult (LenS (SList Integer) SInteger) = LenS [Integer] Integer

Methods

create :: QueryT IO (LenS (SList Integer) SInteger)

project :: LenS (SList Integer) SInteger -> QueryT IO (QueryResult (LenS (SList Integer) SInteger))

embed :: QueryResult (LenS (SList Integer) SInteger) -> QueryT IO (LenS (SList Integer) SInteger)

Generic (LenS a b)

Defined in Documentation.SBV.Examples.WeakestPreconditions.Length

Associated Types

type Rep (LenS a b)

Defined in Documentation.SBV.Examples.WeakestPreconditions.Length

type Rep (LenS a b) = D1 ('MetaData "LenS" "Documentation.SBV.Examples.WeakestPreconditions.Length" "sbv-11.0-inplace" 'False) (C1 ('MetaCons "LenS" 'PrefixI 'True) (S1 ('MetaSel ('Just "xs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: (S1 ('MetaSel ('Just "ys") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Just "l") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 b))))

Methods

from :: LenS a b -> Rep (LenS a b) x

to :: Rep (LenS a b) x -> LenS a b

(SymVal a, Show (f a), Show b) => Show (LenS (f a) b)

Show instance: A simplified version of what would otherwise be generated.

Defined in Documentation.SBV.Examples.WeakestPreconditions.Length

Methods

showsPrec :: Int -> LenS (f a) b -> ShowS

show :: LenS (f a) b -> String

showList :: [LenS (f a) b] -> ShowS

(Mergeable a, Mergeable b) => Mergeable (LenS a b)

Defined in Documentation.SBV.Examples.WeakestPreconditions.Length

Methods

symbolicMerge :: Bool -> SBool -> LenS a b -> LenS a b -> LenS a b

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

type Rep (LenS a b)

Defined in Documentation.SBV.Examples.WeakestPreconditions.Length

type Rep (LenS a b) = D1 ('MetaData "LenS" "Documentation.SBV.Examples.WeakestPreconditions.Length" "sbv-11.0-inplace" 'False) (C1 ('MetaCons "LenS" 'PrefixI 'True) (S1 ('MetaSel ('Just "xs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: (S1 ('MetaSel ('Just "ys") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Just "l") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 b))))

type QueryResult (LenS (SList Integer) SInteger)

Defined in Documentation.SBV.Examples.WeakestPreconditions.Length

type QueryResult (LenS (SList Integer) SInteger) = LenS [Integer] Integer

type S = LenS (SList Integer) SInteger

Helper type synonym

The algorithm

algorithm :: Invariant S -> Maybe (Measure S) -> Stmt S

The imperative length algorithm:

   ys = xs
   l  = 0
   while not (null ys)
     l  = l+1
     ys = tail ys

Note that we need to explicitly annotate each loop with its invariant and the termination measure. For convenience, we take those two as parameters, so we can experiment later.

pre :: S -> SBool

Precondition for our program. Nothing! It works for all lists.

post :: S -> SBool

Postcondition for our program: l must be the length of the input list.

noChange :: Stable S

Stability condition: Program must leave xs unchanged.

imperativeLength :: Invariant S -> Maybe (Measure S) -> Program S

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

invariant :: Invariant S

The invariant simply relates the length of the input to the length of the current suffix and the length of the prefix traversed so far.

measure :: Measure S

The measure is obviously the length of ys, as we peel elements off of it through the loop.

Correctness

correctness :: IO ()

We check that l is the length of the input list xs upon termination. Note that even though this is an inductive proof, it is fairly easy to prove with our SMT based technology, which doesn't really handle induction at all! The usual inductive proof steps are baked into the invariant establishment phase of the WP proof. We have:

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