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.ProofTools.Strengthen

Contents

- System state
- Encoding the problem
- Examples

Description

An example showing how traditional state-transition invariance problems can be coded using SBV, using induction. We also demonstrate the use of invariant strengthening.

This example comes from Bradley's Understanding IC3 paper, which considers the following two programs:

         x, y := 1, 1                    x, y := 1, 1
         while *:                        while *:
           x, y := x+1, y+x                x, y := x+y, y+x

Where `*` stands for non-deterministic choice. For each program we try to prove that `y >= 1` is an invariant.

It turns out that the property `y >= 1` is indeed an invariant, but is not inductive for either program. We proceed to strengten the invariant and establish it for the first case. We then note that the same strengthening doesn't work for the second program, and find a further strengthening to establish that case as well. This example follows the introductory example in Bradley's paper quite closely.

Synopsis

- data S a = S {
  - x :: a
  - y :: a
  }
- problem :: (S SInteger -> [S SInteger]) -> [(String, S SInteger -> SBool)] -> IO (InductionResult (S Integer))
- pgm1 :: S SInteger -> [S SInteger]
- pgm2 :: S SInteger -> [S SInteger]
- ex1 :: IO (InductionResult (S Integer))
- ex2 :: IO (InductionResult (S Integer))
- ex3 :: IO (InductionResult (S Integer))
- ex4 :: IO (InductionResult (S Integer))
- ex5 :: IO (InductionResult (S Integer))
- ex6 :: IO (InductionResult (S Integer))

# System state

data S a Source #

System state. We simply have two components, parameterized over the type so we can put in both concrete and symbolic values.

Constructors

S |

Fields

- x :: a
- y :: a

#### Instances

Instances details

Foldable S Source # |

Instance details

Defined in Documentation.SBV.Examples.ProofTools.Strengthen

Methods

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

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

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

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

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

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

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

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

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

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

null :: S a -> Bool Source #

length :: S a -> Int Source #

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

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

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

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

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

Traversable S Source # |
Instance details Defined in Documentation.SBV.Examples.ProofTools.Strengthen Methods traverse :: Applicative f => (a -> f b) -> S a -> f (S b) Source # sequenceA :: Applicative f => S (f a) -> f (S a) Source # mapM :: Monad m => (a -> m b) -> S a -> m (S b) Source # sequence :: Monad m => S (m a) -> m (S a) Source #
Functor S Source # |
Instance details Defined in Documentation.SBV.Examples.ProofTools.Strengthen Methods fmap :: (a -> b) -> S a -> S b Source # (<$) :: a -> S b -> S a Source #
Fresh IO (S SInteger) Source # | `Fresh` instance for our state
Instance details Defined in Documentation.SBV.Examples.ProofTools.Strengthen Methods fresh :: QueryT IO (S SInteger) Source #
Show a => Show (S a) Source # |
Instance details Defined in Documentation.SBV.Examples.ProofTools.Strengthen Methods showsPrec :: Int -> S a -> ShowS Source # show :: S a -> String Source # showList :: [S a] -> ShowS Source #

# Encoding the problem

problem :: (S SInteger -> [S SInteger]) -> [(String, S SInteger -> SBool)] -> IO (InductionResult (S Integer)) Source #

We parameterize over the transition relation and the strengthenings to investigate various combinations.

pgm1 :: S SInteger -> [S SInteger] Source #

The first program, coded as a transition relation:

pgm2 :: S SInteger -> [S SInteger] Source #

The second program, coded as a transition relation:

# Examples

ex1 :: IO (InductionResult (S Integer)) Source #

Example 1: First program, with no strengthenings. We have:

    >>> ex1
    Failed while establishing consecution.
    Counter-example to inductiveness:
      S {x = -1, y = 1}

ex2 :: IO (InductionResult (S Integer)) Source #

Example 2: First program, strengthened with `x >= 0`. We have:

    >>> ex2
    Q.E.D.

ex3 :: IO (InductionResult (S Integer)) Source #

Example 3: Second program, with no strengthenings. We have:

    >>> ex3
    Failed while establishing consecution.
    Counter-example to inductiveness:
      S {x = -1, y = 1}

ex4 :: IO (InductionResult (S Integer)) Source #

Example 4: Second program, strengthened with `x >= 0`. We have:

    >>> ex4
    Failed while establishing consecution for strengthening "x >= 0".
    Counter-example to inductiveness:
      S {x = 0, y = -1}

ex5 :: IO (InductionResult (S Integer)) Source #

Example 5: Second program, strengthened with `x >= 0` and `y >= 1` separately. We have:

    >>> ex5
    Failed while establishing consecution for strengthening "x >= 0".
    Counter-example to inductiveness:
      S {x = 0, y = -1}

Note how this was sufficient in `ex2` to establish the invariant for the first program, but fails for the second.

ex6 :: IO (InductionResult (S Integer)) Source #

Example 6: Second program, strengthened with `x >= 0 /\ y >= 1` simultaneously. We have:

    >>> ex6
    Q.E.D.

Compare this to `ex5`. As pointed out by Bradley, this shows that a conjunction of assertions can be inductive when none of its components, on its own, is inductive. It remains an art to find proper loop invariants, though the science is improving!