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

Nested Type Invariants #69

Closed DavePearce closed 7 years ago

DavePearce commented 7 years ago

The following fails:

type Buffer is ({int[] data} b) where |b.data| > 0

type NonFull is (Buffer b)

assert "division by zero":
    forall(NonFull b):
        |b.data| != 0

But, replace NonFull by Buffer and it's fine. Clearly it would see the invariant from Buffer are not being passed forward into NonFull b. But, the proof looks like this:

 57. exists(NonFull b).(0 == |b.data|)                                       () 
 64. NonFull(b) && (0 == |b.data|)                                (Exists-E 57) 
 63. NonFull(b)                                                      (And-E 64) 
 56. 0 == |b.data|                                                              
 67. Buffer(b)                                                     (Macro-I 63) 
 70. |b.data| >= 1                                                 (Macro-I 67)

This suggests that the invariant is making its way through the various macro expansions ... ?

DavePearce commented 7 years ago

UPDATE: yet again, this is a representation issue. Macro expansion was not moving generated formulae into normal form (see #68,#67)