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.IntDiv

Contents

- Program state
- The algorithm
- Correctness

Description

Proof of correctness of an imperative integer division algorithm, using weakest preconditions. The algorithm simply keeps subtracting the divisor until the desired quotient and the remainder is found.

Synopsis

- data DivS a = DivS {
  - x :: a
  - y :: a
  - q :: a
  - r :: a
  }
- type D = DivS SInteger
- algorithm :: Invariant D -> Maybe (Measure D) -> Stmt D
- pre :: D -> SBool
- post :: D -> SBool
- noChange :: Stable D
- imperativeDiv :: Invariant D -> Maybe (Measure D) -> Program D
- invariant :: Invariant D
- measure :: Measure D
- correctness :: IO ()

# Program state

data DivS a Source #

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

Constructors

DivS |

Fields

- x :: a

  The dividend

- y :: a

  The divisor

- q :: a

  The quotient

- r :: a

  The remainder

#### Instances

Instances details

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

Instance details

Defined in Documentation.SBV.Examples.WeakestPreconditions.IntDiv

Methods

fold :: Monoid m => DivS m -> m

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

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

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

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

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

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

foldr1 :: (a -> a -> a) -> DivS a -> a

foldl1 :: (a -> a -> a) -> DivS a -> a

toList :: DivS a -> [a]

null :: DivS a -> Bool

length :: DivS a -> Int

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

maximum :: Ord a => DivS a -> a

minimum :: Ord a => DivS a -> a

sum :: Num a => DivS a -> a

product :: Num a => DivS a -> a

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

Instance details

Defined in Documentation.SBV.Examples.WeakestPreconditions.IntDiv

type Rep (DivS a) = D1 ('MetaData "DivS" "Documentation.SBV.Examples.WeakestPreconditions.IntDiv" "sbv-8.7-9mSEXJN8olRBwPWTmi3EMV" 'False) (C1 ('MetaCons "DivS" 'PrefixI 'True) ((S1 ('MetaSel ('Just "x") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Just "y") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)) :*: (S1 ('MetaSel ('Just "q") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Just "r") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a))))

type D = DivS SInteger Source #

Helper type synonym

# The algorithm

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

The imperative division algorithm, assuming non-negative `x` and strictly positive `y`:

       r = x                     -- set remainder to x
       q = 0                     -- set quotient  to 0
       while y <= r              -- while we can still subtract
         r = r - y                    -- reduce the remainder
         q = q + 1                    -- increase the quotient

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 :: D -> SBool Source #

Precondition for our program: `x` must non-negative and `y` must be strictly positive. 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 :: D -> SBool Source #

Postcondition for our program: Remainder must be non-negative and less than `y`, and it must hold that `x = q*y + r`:

noChange :: Stable D Source #

Stability: `x` and `y` must remain unchanged.

imperativeDiv :: Invariant D -> Maybe (Measure D) -> Program D Source #

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

# Correctness

invariant :: Invariant D Source #

The invariant is simply that `x = q * y + r` holds at all times and `r` is strictly positive. We need the `y > 0` part of the invariant to establish the measure decreases, which is guaranteed by our precondition.

measure :: Measure D Source #

The measure. In each iteration `r` decreases, but always remains positive. Since `y` is strictly positive, `r` can serve as a measure for the loop.

correctness :: IO () Source #

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

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