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

Documentation.SBV.Examples.Uninterpreted.AUF

Contents

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

# Model using functional arrays

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.

Prove it using SMT-Lib arrays.

>>> proveSArray
Q.E.D.


Prove it using SBV's internal functional arrays.

>>> proveSFunArray
Q.E.D.