sbv-7.13: 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.Uninterpreted.AUF

Contents

- Model using functional arrays

Description

Formalizes and proves the following theorem, about arithmetic, uninterpreted functions, and arrays. (For reference, see http://research.microsoft.com/en-us/um/redmond/projects/z3/fmcad06-slides.pdf slide number 24):

       x + 2 = y  implies  f (read (write (a, x, 3), y - 2)) = f (y - x + 1)

We interpret the types as follows (other interpretations certainly possible):

x
  `SWord32` (32-bit unsigned address)
y
  `SWord32` (32-bit unsigned address)
a
  An array, indexed by 32-bit addresses, returning 32-bit unsigned integers
f
  An uninterpreted function of type ``SWord32` -> `SWord64``

The function `read` and `write` are usual array operations.

Synopsis

- f :: SWord32 -> SWord64
- thm :: SymArray a => SWord32 -> SWord32 -> a Word32 Word32 -> SBool
- proveSArray :: IO ThmResult
- proveSFunArray :: IO ThmResult

# Model using functional arrays

f :: SWord32 -> SWord64 Source #

Uninterpreted function in the theorem

thm :: SymArray a => SWord32 -> SWord32 -> a Word32 Word32 -> SBool Source #

Correctness theorem. We state it for all values of `x`, `y`, and the given array `a`. Note that we're being generic in the type of array we're expecting.

proveSArray :: IO ThmResult Source #

Prove it using SMT-Lib arrays.

    >>> proveSArray
    Q.E.D.

proveSFunArray :: IO ThmResult Source #

Prove it using SBV's internal functional arrays.

    >>> proveSFunArray
    Q.E.D.