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

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

Documentation.SBV.Examples.WeakestPreconditions.IntSqrt

Contents

- Program state
- The algorithm
- Correctness

Description

Proof of correctness of an imperative integer square-root algorithm, using weakest preconditions. The algorithm computes the floor of the square-root of a given non-negative integer by keeping a running some of all odd numbers starting from 1. Recall that `1+3+5+...+(2n+1) = (n+1)^2`, thus we can stop the counting when we exceed the input number.

Synopsis

- data SqrtS a = SqrtS {
  - x :: a
  - sqrt :: a
  - i :: a
  - j :: a
  }
- type S = SqrtS SInteger
- algorithm :: Invariant S -> Maybe (Measure S) -> Stmt S
- pre :: S -> SBool
- post :: S -> SBool
- noChange :: Stable S
- imperativeSqrt :: Invariant S -> Maybe (Measure S) -> Program S
- invariant :: Invariant S
- measure :: Measure S
- correctness :: IO ()

# Program state

data SqrtS a Source #

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

Constructors

SqrtS |

Fields

- x :: a

  The input

- sqrt :: a

  The floor of the square root

- i :: a

  Successive squares, as the sum of j's

- j :: a

  Successive odds

#### Instances

Instances details

Functor SqrtS Source # |
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.IntSqrt Methods fmap :: (a -> b) -> SqrtS a -> SqrtS b (<$) :: a -> SqrtS b -> SqrtS a
Foldable SqrtS Source # |

Instance details

Defined in Documentation.SBV.Examples.WeakestPreconditions.IntSqrt

Methods

fold :: Monoid m => SqrtS m -> m

foldMap :: Monoid m => (a -> m) -> SqrtS a -> m

foldMap' :: Monoid m => (a -> m) -> SqrtS a -> m

foldr :: (a -> b -> b) -> b -> SqrtS a -> b

foldr' :: (a -> b -> b) -> b -> SqrtS a -> b

foldl :: (b -> a -> b) -> b -> SqrtS a -> b

foldl' :: (b -> a -> b) -> b -> SqrtS a -> b

foldr1 :: (a -> a -> a) -> SqrtS a -> a

foldl1 :: (a -> a -> a) -> SqrtS a -> a

toList :: SqrtS a -> [a]

null :: SqrtS a -> Bool

length :: SqrtS a -> Int

elem :: Eq a => a -> SqrtS a -> Bool

maximum :: Ord a => SqrtS a -> a

minimum :: Ord a => SqrtS a -> a

sum :: Num a => SqrtS a -> a

product :: Num a => SqrtS a -> a

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

Instance details

Defined in Documentation.SBV.Examples.WeakestPreconditions.IntSqrt

type Rep (SqrtS a) = D1 ('MetaData "SqrtS" "Documentation.SBV.Examples.WeakestPreconditions.IntSqrt" "sbv-8.7-9mSEXJN8olRBwPWTmi3EMV" 'False) (C1 ('MetaCons "SqrtS" 'PrefixI 'True) ((S1 ('MetaSel ('Just "x") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Just "sqrt") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)) :*: (S1 ('MetaSel ('Just "i") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Just "j") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a))))

type S = SqrtS SInteger Source #

Helper type synonym

# The algorithm

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

The imperative square-root algorithm, assuming non-negative `x`

       sqrt = 0                  -- set sqrt to 0
       i    = 1                  -- set i to 1, sum of j's so far
       j    = 1                  -- set j to be the first odd number i
       while i <= x              -- while the sum hasn't exceeded x yet
         sqrt = sqrt + 1              -- increase the sqrt
         j    = j + 2                 -- next odd number
         i    = i + j                 -- running sum of j's

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

pre :: S -> SBool Source #

Precondition for our program: `x` must be non-negative. Note that there is an explicit call to `abort` in our program to protect against this case, so if we do not have this precondition, all programs will fail.

post :: S -> SBool Source #

Postcondition for our program: The `sqrt` squared must be less than or equal to `x`, and `sqrt+1` squared must strictly exceed `x`.

noChange :: Stable S Source #

Stability condition: Program must leave `x` unchanged.

imperativeSqrt :: Invariant S -> Maybe (Measure S) -> Program S Source #

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

# Correctness

invariant :: Invariant S Source #

The invariant is that at each iteration of the loop `sqrt` remains below or equal to the actual square-root, and `i` tracks the square of the next value. We also have that `j` is the `sqrt`'th odd value. Coming up with this invariant is not for the faint of heart, for details I would strongly recommend looking at Manna's seminal Mathematical Theory of Computation book (chapter 3). The `j .> 0` part is needed to establish the termination.

measure :: Measure S Source #

The measure. In each iteration `i` strictly increases, thus reducing the differential `x - i`

correctness :: IO () Source #

Check that the program terminates and the post condition holds. We have:

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