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

Limitation with TypeTestClosure #114

Open DavePearce opened 7 years ago

DavePearce commented 7 years ago

Here is another example which highlights a limitation with TypeTestClosure:

type nat is (int x)
where:
    x >= 0

type Expr is (int|(Expr[])|ListAccess this)
type ListAccess is ({Expr index, Expr src} this)
type Value is (int|(Value[]) this)

function evaluate(Expr e) -> (null|Value $)

assert "type invariant not satisfied":
    forall(Value v, Expr[] e, nat i):
        if:
            v == evaluate(e[i])
        then:
            v is Value

Observe that removing the condition v == evaluate(e[i]) and this verifies. The failing proof is:

 135. exists(Value v, Expr[] e, nat i).((((v == evaluate(e[i]))) && ((v is ! () 
 137. exists(Value v, Expr[] e, nat i).((v == evaluate(e[i])) && (v  (Simp 135) 
 144. nat(i) && ((v == evaluate(e[i])) && (v is !Value))         (Exists-E 137) 
 145. nat(i) && (v == evaluate(e[i])) && (v is !Value)               (Simp 144) 
 143. nat(i)                                                        (And-E 145) 
 127. v == evaluate(e[i])                                           (And-E 145) 
 130. v is !Value                                                   (And-E 145) 
 147. (i >= 0)                                                    (Macro-I 143) 
 148. evaluate(e[i]) is Value                                        (Eq-S 127) 
 149. evaluate(e[i]) is !Value                                   (Eq-S 130,127) 
 146. i >= 0                                                         (Simp 147)

From this, it's completely unclear how v is !Value is not leading to a contradiction.