| Copyright | (c) Levent Erkok |
|---|---|
| License | BSD3 |
| Maintainer | erkokl@gmail.com |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Documentation.SBV.Examples.Uninterpreted.AUF
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.
Model using functional arrays
type A = SFunArray Word32 Word32 Source #
The array type, takes symbolic 32-bit unsigned indexes and stores 32-bit unsigned symbolic values. These are functional arrays where reading before writing a cell throws an exception.
thm1 :: SWord32 -> SWord32 -> A -> SBool Source #
Correctness theorem. We state it for all values of x, y, and
the given array a.
Model using SMT arrays
type B = SArray Word32 Word32 Source #
This version directly uses SMT-arrays and hence does not need an initializer. Reading an element before writing to it returns an arbitrary value.