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

Problem with Type Test Closure #82

Closed DavePearce closed 7 years ago

DavePearce commented 7 years ago

The following assertion fails:

type Leaf is (int this)
type Link is ({LinkedList next} this)
type LinkedList is (Leaf|Link this)

assert "type invariant not satisfied":
    forall(LinkedList list, int distance):
        if:
            distance == 0
            list is Link
        then:
            list.next is LinkedList

The unusual thing is that removing the unnecessary term distance == 0 and it verifies.

Proof with distance == 0:

 80. exists(LinkedList list, int distance).((((distance == 0) && (list is !! () 
 82. exists(LinkedList list, int distance).(((distance == 0) && (list (Simp 80) 
 81. ((distance == 0) && (list is !!Link)) && (list.next is !Link (Exists-E 82) 
 72. (distance == 0) && (list is !!Link)                             (And-E 81) 
 75. list.next is !LinkedList                                        (And-E 81) 
 67. distance == 0                                                   (And-E 72) 
 71. list is !!Link                                                  (And-E 72)

Proof without distance == 0:

 74. exists(LinkedList list, int distance).((((list is !!Link)) && ((list.ne () 
 76. exists(LinkedList list, int distance).((list is !!Link) && (list (Simp 74) 
 75. (list is !!Link) && (list.next is !LinkedList)               (Exists-E 76) 
 69. list.next is !LinkedList                                        (And-E 75) 
 58. false

It looks like list is !!Link reduces to false in the latter proof.

DavePearce commented 7 years ago

UPDATE: the following does verify:

assert "type invariant not satisfied":
    forall(LinkedList list, int distance):
        if:
            list is Link
            list.next is !LinkedList
        then:
            distance == 0

This gives the following proof:

 82. exists(LinkedList list, int distance).((((list is !!Link) && (list.next () 
 84. exists(LinkedList list, int distance).(((list is !!Link) && (lis (Simp 82) 
 83. ((list is !!Link) && (list.next is !!!LinkedList)) && (dista (Exists-E 84) 
 75. (list is !!Link) && (list.next is !!!LinkedList)                (And-E 83) 
 74. list.next is !!!LinkedList                                      (And-E 75) 
 63. false                                                            (Is-I 74)

Hmmmm, it's almost as though TypeTestClosure doesn't witness list is !!Link or something?

DavePearce commented 7 years ago

Hmmm, ok when it fails the terms are witnessed in this order:

WITNESSING: list.next is !(LinkedList)
WITNESSING: list is !(!(Link))

and when it passes (in both cases above) they are witnessed in this order:

WITNESSING: list is !(!(Link))
WITNESSING: list.next is !(LinkedList)

The problem is that it doesn't retype list when list.next is encountered. It only closes over it.

DavePearce commented 7 years ago

This is closed now though, of course, another bug / problem is exposed.