sbv-10.2: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | Safe-Inferred
Language | Haskell2010

Documentation.SBV.Examples.WeakestPreconditions.Basics

Contents

- Program state
- The algorithm
- Correctness
- Example proof attempts

Description

Some basic aspects of weakest preconditions, demonstrating programs that do not use while loops. We use a simple increment program as an example.

Synopsis

- data IncS a = IncS {
  - x :: a
  - y :: a
  }
- type I = IncS SInteger
- algorithm :: Stmt I -> Stmt I -> Stmt I
- pre :: I -> SBool
- post :: I -> SBool
- noChange :: Stable I
- imperativeInc :: Stmt I -> Stmt I -> Program I
- correctness :: Stmt I -> Stmt I -> IO (ProofResult (IncS Integer))

# Documentation

    >>> -- For doctest purposes only:
    >>> import Data.SBV
    >>> import Data.SBV.Control
    >>> import Data.SBV.Tools.WeakestPreconditions

# Program state

data IncS a Source #

The state for the swap program, parameterized over a base type `a`.

Constructors

IncS |

Fields

- x :: a

  Input value

- y :: a

  Output

#### Instances

Instances details

Foldable IncS Source # |

Instance details

Defined in Documentation.SBV.Examples.WeakestPreconditions.Basics

Methods

fold :: Monoid m => IncS m -> m Source #

foldMap :: Monoid m => (a -> m) -> IncS a -> m Source #

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

foldr :: (a -> b -> b) -> b -> IncS a -> b Source #

foldr' :: (a -> b -> b) -> b -> IncS a -> b Source #

foldl :: (b -> a -> b) -> b -> IncS a -> b Source #

foldl' :: (b -> a -> b) -> b -> IncS a -> b Source #

foldr1 :: (a -> a -> a) -> IncS a -> a Source #

foldl1 :: (a -> a -> a) -> IncS a -> a Source #

toList :: IncS a -> [a] Source #

null :: IncS a -> Bool Source #

length :: IncS a -> Int Source #

elem :: Eq a => a -> IncS a -> Bool Source #

maximum :: Ord a => IncS a -> a Source #

minimum :: Ord a => IncS a -> a Source #

sum :: Num a => IncS a -> a Source #

product :: Num a => IncS a -> a Source #

Traversable IncS Source # |
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.Basics Methods traverse :: Applicative f => (a -> f b) -> IncS a -> f (IncS b) Source # sequenceA :: Applicative f => IncS (f a) -> f (IncS a) Source # mapM :: Monad m => (a -> m b) -> IncS a -> m (IncS b) Source # sequence :: Monad m => IncS (m a) -> m (IncS a) Source #
Functor IncS Source # |
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.Basics Methods fmap :: (a -> b) -> IncS a -> IncS b Source # (<$) :: a -> IncS b -> IncS a Source #
SymVal a => Fresh IO (IncS (SBV a)) Source # | `Fresh` instance for the program state
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.Basics Methods fresh :: QueryT IO (IncS (SBV a)) Source #
Generic (IncS a) Source # |
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.Basics Associated Types type Rep (IncS a) :: Type -> Type Source # Methods from :: IncS a -> Rep (IncS a) x Source # to :: Rep (IncS a) x -> IncS a Source #
(SymVal a, Show a) => Show (IncS (SBV a)) Source # | Show instance for `IncS`. 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.Basics Methods showsPrec :: Int -> IncS (SBV a) -> ShowS Source # show :: IncS (SBV a) -> String Source # showList :: [IncS (SBV a)] -> ShowS Source #
Show a => Show (IncS a) Source # |
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.Basics Methods showsPrec :: Int -> IncS a -> ShowS Source # show :: IncS a -> String Source # showList :: [IncS a] -> ShowS Source #
Mergeable a => Mergeable (IncS a) Source # |
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.Basics Methods symbolicMerge :: Bool -> SBool -> IncS a -> IncS a -> IncS a Source # select :: (Ord b, SymVal b, Num b) => [IncS a] -> IncS a -> SBV b -> IncS a Source #
type Rep (IncS a) Source # |

Instance details

Defined in Documentation.SBV.Examples.WeakestPreconditions.Basics

type Rep (IncS a) = D1 ('MetaData "IncS" "Documentation.SBV.Examples.WeakestPreconditions.Basics" "sbv-10.2-H7C8tpOUfNc9yHFfX3krPk" 'False) (C1 ('MetaCons "IncS" 'PrefixI 'True) (S1 ('MetaSel ('Just "x") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Just "y") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))

type I = IncS SInteger Source #

Helper type synonym

# The algorithm

algorithm :: Stmt I -> Stmt I -> Stmt I Source #

The increment algorithm:

       y = x+1

The point here isn't really that this program is interesting, but we want to demonstrate various aspects of WP proofs. So, we take a before and after program to annotate our algorithm so we can experiment later.

pre :: I -> SBool Source #

Precondition for our program. Strictly speaking, we don't really need any preconditions, but for example purposes, we'll require `x` to be non-negative.

post :: I -> SBool Source #

Postcondition for our program: `y` must equal `x+1`.

noChange :: Stable I Source #

Stability: `x` must remain unchanged.

imperativeInc :: Stmt I -> Stmt I -> Program I Source #

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

# Correctness

correctness :: Stmt I -> Stmt I -> IO (ProofResult (IncS Integer)) Source #

State the correctness with respect to before/after programs. In the simple case of nothing prior/after, we have the obvious proof:

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

# Example proof attempts

It is instructive to look at how the proof changes as we put in different `pre` and `post` values.

## Violating the post condition

If we stick in an extra increment for `y` after, we can easily break the postcondition:

    >>> :set -XNamedFieldPuns
    >>> import Control.Monad (void)
    >>> void $ correctness Skip $ Assign $ \st@IncS{y} -> st{y = y+1}
    Following proof obligation failed:
    ==================================
      Postcondition fails:
        Start: IncS {x = 0, y = 0}
        End  : IncS {x = 0, y = 2}

We're told that the program ends up in a state where `x=0` and `y=2`, violating the requirement `y=x+1`, as expected.

## Using `assert`

There are two main use cases for `assert`, which merely ends up being a call to `Abort`. One is making sure the inputs are well formed. And the other is the user putting in their own invariants into the code.

Let's assume that we only want to accept strictly positive values of `x`. We can try:

    >>> void $ correctness (assert "x > 0" (\st@IncS{x} -> x .> 0)) Skip
    Following proof obligation failed:
    ==================================
      Abort "x > 0" condition is satisfiable:
        Before: IncS {x = 0, y = 0}
        After : IncS {x = 0, y = 0}

Recall that our precondition (`pre`) required `x` to be non-negative. So, we can put in something weaker and it would be fine:

    >>> void $ correctness (assert "x > -5" (\st@IncS{x} -> x .> -5)) Skip
    Total correctness is established.

In this case the precondition to our program ensures that the `assert` will always be satisfied.

As another example, let us put a post assertion that `y` is even:

    >>> void $ correctness Skip (assert "y is even" (\st@IncS{y} -> y `sMod` 2 .== 0))
    Following proof obligation failed:
    ==================================
      Abort "y is even" condition is satisfiable:
        Before: IncS {x = 0, y = 0}
        After : IncS {x = 0, y = 1}

It is important to emphasize that you can put whatever invariant you might want:

    >>> void $ correctness Skip (assert "y > x" (\st@IncS{x, y} -> y .> x))
    Total correctness is established.

## Violating stability

What happens if our program modifies `x`? After all, we can simply set `x=10` and `y=11` and our post condition would be satisfied:

    >>> void $ correctness Skip (Assign $ \st -> st{x = 10, y = 11})
    Following proof obligation failed:
    ==================================
      Stability fails for "x":
        Before: IncS {x = 0, y = 1}
        After : IncS {x = 10, y = 11}

So, the stability condition prevents programs from cheating!