Copyright	(c) Levent Erkok
License	BSD3
Maintainer	erkokl@gmail.com
Stability	experimental
Safe Haskell	None
Language	Haskell2010

Documentation.SBV.Examples.Misc.LambdaArray

Description

Demonstrates how lambda-abstractions can be used to model arrays.

Synopsis

memset :: SArray Integer Integer -> SInteger -> SInteger -> SInteger -> SArray Integer Integer
memsetExample :: IO ThmResult
outOfInit :: IO SatResult

Documentation

memset :: SArray Integer Integer -> SInteger -> SInteger -> SInteger -> SArray Integer Integer Source #

Given an array, and bounds on it, initialize it within the bounds to the element given. Otherwise, leave it untouched.

memsetExample :: IO ThmResult Source #

Prove a simple property: If we read from the initialized region, we get the initial value. We have:

>>> memsetExample
Q.E.D.

outOfInit :: IO SatResult Source #

Get an example of reading a value out of range. The value returned should be out-of-range for lo/hi

>>> outOfInit
Satisfiable. Model:
  mem  = ([], 1) :: Array Integer Integer
  lo   =       0 :: Integer
  hi   =       0 :: Integer
  zero =       0 :: Integer
  idx  =       1 :: Integer
  Read =       1 :: Integer