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

Expanding Recursive Functions #111

Open DavePearce opened 7 years ago

DavePearce commented 7 years ago

The following goes into a loop:

type Link is ({int data, test.LinkedList next} this)
type LinkedList is (null|test.Link this)

define isLength(test.LinkedList list, int len) is:
    (list is !null) || (len == 0)
    (list is !test.Link) || test.isLength(list.next, len - 1)

define f_ensures_0(test.LinkedList l, test.LinkedList r) is:
    test.isLength(l, 0)

assert "postcondition not satisfied":
    forall(test.LinkedList l):
        f_ensures_0(l, l)

With limit=100 the proof looks like this:

Parsed 1 source file(s). ....................................................... [35ms+1mb]
Typed 1 source file(s). ............................................................ [15ms]
 134. exists(test.LinkedList l).(!f_ensures_0(l, l))                         () 
 135. exists(test.LinkedList l).!f_ensures_0(l, l)                   (Simp 134) 
 131. !f_ensures_0(l, l)                                         (Exists-E 135) 
 138. !test.isLength(l, 0)                                        (Macro-I 131) 
 137. !test.isLength(l, 0)                                           (Simp 138) 
 150. ((l is !!null) && (0 != 0)) || ((l is !!test.Link) && !test (Macro-I 137) 
 155. (l is !!test.Link) && !test.isLength(l.next, -1)               (Simp 150) 
 144. l is !!test.Link                                              (And-E 155) 
 154. !test.isLength(l.next, -1)                                    (And-E 155) 
 165. ((l.next is !!null) && (-1 != 0)) || ((l.next is !!test.Lin (Macro-I 154) 
 171. (l.next is !!null) || ((l.next is !!test.Link) && !test.isLeng (Simp 165) 
 183. (l.next is !!null) || ((l.next is !!test.Link) && (((l.next (Macro-I 171) 
 191. (l.next is !!null) || ((l.next is !!test.Link) && ((l.next.nex (Simp 183) 
 205. (l.next is !!null) || ((l.next is !!test.Link) && ((l.next. (Macro-I 191) 
 215. (l.next is !!null) || ((l.next is !!test.Link) && ((l.next.nex (Simp 205) 
 231. (l.next is !!null) || ((l.next is !!test.Link) && ((l.next. (Macro-I 215) 
 243. (l.next is !!null) || ((l.next is !!test.Link) && ((l.next.nex (Simp 231) 
 261. (l.next is !!null) || ((l.next is !!test.Link) && ((l.next. (Macro-I 243) 
 275. (l.next is !!null) || ((l.next is !!test.Link) && ((l.next.nex (Simp 261) 
 295. (l.next is !!null) || ((l.next is !!test.Link) && ((l.next. (Macro-I 275) 
 311. (l.next is !!null) || ((l.next is !!test.Link) && ((l.next.nex (Simp 295) 
 333. (l.next is !!null) || ((l.next is !!test.Link) && ((l.next. (Macro-I 311) 
 351. (l.next is !!null) || ((l.next is !!test.Link) && ((l.next.nex (Simp 333) 
 375. (l.next is !!null) || ((l.next is !!test.Link) && ((l.next. (Macro-I 351) 
 395. (l.next is !!null) || ((l.next is !!test.Link) && ((l.next.nex (Simp 375) 
 421. (l.next is !!null) || ((l.next is !!test.Link) && ((l.next. (Macro-I 395) 
 443. (l.next is !!null) || ((l.next is !!test.Link) && ((l.next.nex (Simp 421) 
 471. (l.next is !!null) || ((l.next is !!test.Link) && ((l.next. (Macro-I 443) 
 495. (l.next is !!null) || ((l.next is !!test.Link) && ((l.next.nex (Simp 471) 
 525. (l.next is !!null) || ((l.next is !!test.Link) && ((l.next. (Macro-I 495) 
 551. (l.next is !!null) || ((l.next is !!test.Link) && ((l.next.nex (Simp 525) 
 583. (l.next is !!null) || ((l.next is !!test.Link) && ((l.next. (Macro-I 551) 
 611. (l.next is !!null) || ((l.next is !!test.Link) && ((l.next.nex (Simp 583) 
 645. (l.next is !!null) || ((l.next is !!test.Link) && ((l.next. (Macro-I 611) 
 675. (l.next is !!null) || ((l.next is !!test.Link) && ((l.next.nex (Simp 645) 
 711. (l.next is !!null) || ((l.next is !!test.Link) && ((l.next. (Macro-I 675) 
 743. (l.next is !!null) || ((l.next is !!test.Link) && ((l.next.nex (Simp 711) 
 781. (l.next is !!null) || ((l.next is !!test.Link) && ((l.next. (Macro-I 743) 
 815. (l.next is !!null) || ((l.next is !!test.Link) && ((l.next.nex (Simp 781) 
 855. (l.next is !!null) || ((l.next is !!test.Link) && ((l.next. (Macro-I 815) 
 891. (l.next is !!null) || ((l.next is !!test.Link) && ((l.next.nex (Simp 855) 
 933. (l.next is !!null) || ((l.next is !!test.Link) && ((l.next. (Macro-I 891) 
 971. (l.next is !!null) || ((l.next is !!test.Link) && ((l.next.nex (Simp 933) 
 1015. (l.next is !!null) || ((l.next is !!test.Link) && ((l.next (Macro-I 971) 
 1055. (l.next is !!null) || ((l.next is !!test.Link) && ((l.next.n (Simp 1015) 
 1101. (l.next is !!null) || ((l.next is !!test.Link) && ((l.nex (Macro-I 1055) 
 1143. (l.next is !!null) || ((l.next is !!test.Link) && ((l.next.n (Simp 1101) 
 1191. (l.next is !!null) || ((l.next is !!test.Link) && ((l.nex (Macro-I 1143) 
 1235. (l.next is !!null) || ((l.next is !!test.Link) && ((l.next.n (Simp 1191) 
 1285. (l.next is !!null) || ((l.next is !!test.Link) && ((l.nex (Macro-I 1235) 
./test.wyal:11: postcondition not satisfied
assert "postcondition not satisfied":
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
DavePearce commented 7 years ago

Another example:

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

function abs(int x) -> (nat r)

assert "postcondition not satisfied":
    forall(nat item):
        if:
            (abs(item) == item) || (abs(item) == -item)
            abs(item) >= 0
        then:
            item == abs(item)
DavePearce commented 7 years ago

Z3 uses bounded unrolling of recursive functions:

http://prosecco.gforge.inria.fr/personal/hritcu/students/alejandro/report.pdf