search

Whiley / WhileyTheoremProver

The Whiley Theorem Prover (WyTP) is an automatic and interactive theorem prover designed to discharge verification conditions generated by the Whiley Compiler. WyTP operates over a variant of first-order logic which includes integer arithmetic, arrays and quantification.
Apache License 2.0
8 stars 2 forks source link

Support for Versioned Heap #127

Open DavePearce opened 7 years ago

DavePearce commented 7 years ago

(this follows WyC#743 and WyC#750)

We need to allow for "heap versioning". The proposed syntax is to employ a tick notation. Consider this simply Whiley file:

method f(&int x)
requires *x != 0:
    //
    *x = 0
    //
    assert (*x) == 0

This could generate the following WyAL file:

assert "assertion failed":
    forall(&int x):
        if:
            *x != 0
            *' == *[x:=0]
        then:
            *'x == 0

Here, *' represents a completely "new version" of the heap that is related to * only via the heap update operator (i.e. *' == *[x:=0]).

DavePearce commented 7 years ago

This will require a relatively simple inference rule (I think). Imagine this example:

assert "assertion failed":
    forall(&int x, &int y):
        if:
            *y == 0
            *' == *[x:=0]
        then:
            *'y == 0

In this case, we'll end up with a conjunction of these atoms:

*y == 0
*' == *[x:=0]
*'y != 0

By congruence closure, we end up with this:

*y == 0
*' == *[x:=0]
*[x:=0](y) != 0

(what syntax for *[x:=0](y) ?)

Then, we have to perform a case analysis on *[x:=0](y). Specifically, either x == y and *[x:=0](y) reduces to 0. Or, x != y and *[x:=0](y) reduces to *y.

DavePearce commented 7 years ago

To implement this feature requires the following changes: