----------------------------------------------------------------------------- -- | -- Module : Documentation.SBV.Examples.ProofTools.Strengthen -- Copyright : (c) Levent Erkok -- License : BSD3 -- Maintainer: erkokl@gmail.com -- Stability : experimental -- -- 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](http://theory.stanford.edu/~arbrad/papers/Understanding_IC3.pdf) 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. ----------------------------------------------------------------------------- {-# LANGUAGE DeriveFoldable #-} {-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE NamedFieldPuns #-} module Documentation.SBV.Examples.ProofTools.Strengthen where import Data.SBV import Data.SBV.Tools.Induction import Data.SBV.Control -- * System state -- | System state. We simply have two components, parameterized -- over the type so we can put in both concrete and symbolic values. data S a = S { x :: a, y :: a } deriving (Show, Functor, Foldable, Traversable) -- | 'Fresh' instance for our state instance Fresh IO (S SInteger) where fresh = S <\$> freshVar_ <*> freshVar_ -- * Encoding the problem -- | We parameterize over the transition relation and the strengthenings to -- investigate various combinations. problem :: (S SInteger -> [S SInteger]) -> [(String, S SInteger -> SBool)] -> IO (InductionResult (S Integer)) problem trans strengthenings = induct chatty setup initial trans strengthenings inv goal where -- Set this to True for SBV to print steps as it proceeds -- through the inductive proof chatty :: Bool chatty = False -- This is where we would put solver options, typically via -- calls to 'Data.SBV.setOption'. We do not need any for this problem, -- so we simply do nothing. setup :: Symbolic () setup = return () -- Initially, @x@ and @y@ are both @1@ initial :: S SInteger -> SBool initial S{x, y} = x .== 1 .&& y .== 1 -- Invariant to prove: inv :: S SInteger -> SBool inv S{y} = y .>= 1 -- We're not interested in termination/goal for this problem, so just pass trivial values goal :: S SInteger -> (SBool, SBool) goal _ = (sTrue, sTrue) -- | The first program, coded as a transition relation: pgm1 :: S SInteger -> [S SInteger] pgm1 S{x, y} = [S{x = x+1, y = y+x}] -- | The second program, coded as a transition relation: pgm2 :: S SInteger -> [S SInteger] pgm2 S{x, y} = [S{x = x+y, y = y+x}] -- * Examples -- | Example 1: First program, with no strengthenings. We have: -- -- >>> ex1 -- Failed while establishing consecution. -- Counter-example to inductiveness: -- S {x = -1, y = 1} ex1 :: IO (InductionResult (S Integer)) ex1 = problem pgm1 strengthenings where strengthenings :: [(String, S SInteger -> SBool)] strengthenings = [] -- | Example 2: First program, strengthened with @x >= 0@. We have: -- -- >>> ex2 -- Q.E.D. ex2 :: IO (InductionResult (S Integer)) ex2 = problem pgm1 strengthenings where strengthenings :: [(String, S SInteger -> SBool)] strengthenings = [("x >= 0", \S{x} -> x .>= 0)] -- | Example 3: Second program, with no strengthenings. We have: -- -- >>> ex3 -- Failed while establishing consecution. -- Counter-example to inductiveness: -- S {x = -1, y = 1} ex3 :: IO (InductionResult (S Integer)) ex3 = problem pgm2 strengthenings where strengthenings :: [(String, S SInteger -> SBool)] strengthenings = [] -- | 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} ex4 :: IO (InductionResult (S Integer)) ex4 = problem pgm2 strengthenings where strengthenings :: [(String, S SInteger -> SBool)] strengthenings = [("x >= 0", \S{x} -> x .>= 0)] -- | 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. ex5 :: IO (InductionResult (S Integer)) ex5 = problem pgm2 strengthenings where strengthenings :: [(String, S SInteger -> SBool)] strengthenings = [ ("x >= 0", \S{x} -> x .>= 0) , ("y >= 1", \S{y} -> y .>= 1) ] -- | 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! ex6 :: IO (InductionResult (S Integer)) ex6 = problem pgm2 strengthenings where strengthenings :: [(String, S SInteger -> SBool)] strengthenings = [("x >= 0 /\\ y >= 1", \S{x, y} -> x .>= 0 .&& y .>= 1)]