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

Equals(LengthOf,X) and Equation(LengthOf) Equivalences #8

Closed DavePearce closed 7 years ago

DavePearce commented 8 years ago

Currently, the following code fails to verify:

assert "assertion failure":
    forall ({int} r0):
        if:
            true
            |r0| != 0
        then:
            |r0| > 0

The reason being simply that we end up with this:

Exists[{[Var("r1"),AnyT]},And{
        Not(Equals[SetT[true,VoidT],{|Var("r1"),Set{}|}]),
        Equation[IntT,Sum[0.0,{|Mul[-1.0,{|LengthOf(Var("r1"))|}]|}]]
}]

Here, we want the Equation to be reformulated as an Equals. Currently we can get back from an Equation to an Equals as follows:

reduce Equation[IntT,LengthOf(SExpr x)]:
    => Equals[SetT[true,VoidT],{|x,Set{}|}]

But, this rule doesn't apply here...

... hmmm, ok so that rule is broken as it should never apply.

DavePearce commented 8 years ago

Fixing that rule causes these tests to now fail:

Test_List_18
Test_Set_16
Test_Set_26

Which seems odd ... !

DavePearce commented 8 years ago

Right, so actually I need both rules for this to work. That's because Sum_2 will reduce Sum[0.0,{|Mul[0.0,{|LengthOf(X)|}]|}] to LengthOf(X). However, in the above example, this rule wouldn't apply as we had a negative length (i.e. 0 == -1*|X|).

DavePearce commented 8 years ago

An alternative to having both rules would be to normalise equations of the form 0 == -x to be 0 == x. Curiously, I thought the rule Equation_Gcd_1 should do that already?

... no, because gcd always returns a positive number.