Copyright  (c) Levent Erkok 

License  BSD3 
Maintainer  erkokl@gmail.com 
Stability  experimental 
Safe Haskell  None 
Language  Haskell2010 
An example showing how traditional statetransition 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 nondeterministic 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 {}
 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
System state. We simply have two components, parameterized over the type so we can put in both concrete and symbolic values.
Instances
Functor S Source #  
Foldable S Source #  
Defined in Documentation.SBV.Examples.ProofTools.Strengthen fold :: Monoid m => S m > m # foldMap :: Monoid m => (a > m) > S a > m # foldr :: (a > b > b) > b > S a > b # foldr' :: (a > b > b) > b > S a > b # foldl :: (b > a > b) > b > S a > b # foldl' :: (b > a > b) > b > S a > b # foldr1 :: (a > a > a) > S a > a # foldl1 :: (a > a > a) > S a > a # elem :: Eq a => a > S a > Bool # maximum :: Ord a => S a > a #  
Traversable S Source #  
Fresh IO (S SInteger) Source # 

Show a => Show (S a) 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.
Examples
ex1 :: IO (InductionResult (S Integer)) Source #
Example 1: First program, with no strengthenings. We have:
>>>
ex1
Failed while establishing consecution. Counterexample 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. Counterexample 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". Counterexample 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". Counterexample 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!