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

Casting Record Types #76

Open DavePearce opened 7 years ago

DavePearce commented 7 years ago

The following Whiley code fails to verify:

type Rec1 is {int x, int y}
type Rec2 is {int x}

function f(Rec2 rec) -> int:
    return rec.x

public export method test() :
    Rec1 rec = {x: 1, y: 2}
    assume f((Rec2) rec) == 1

The problem is that it generates this assertion:

assert:
    forall(Rec1 rec):
        if:
            rec == {x: 1, y: 2}
            f(rec) == 1
        then:
            rec == {x: 1, y: 2}

And, it cannot resolve the method call f(rec). This clearly makes sense and arises because there is no cast at the WyAL level...