Copyright | (c) Levent Erkok |
---|---|

License | BSD3 |

Maintainer | erkokl@gmail.com |

Stability | experimental |

Safe Haskell | None |

Language | Haskell2010 |

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

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.

`>>>`

Q.E.D.`proveSArray`

proveSFunArray :: IO ThmResult Source #

Prove it using SBV's internal functional arrays.

`>>>`

Q.E.D.`proveSFunArray`