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

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | Safe-Inferred
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:
      Read = 1 :: Integer
      lo   = 0 :: Integer
      hi   = 0 :: Integer
      zero = 0 :: Integer
      idx  = 1 :: Integer