-- -- mk(next(s)) = (next(s) (next(s) - 1) ... 0) -- -- Claim 100 guarantees that if Receiver receives number x, then she -- receied all the numbers up to x sent by Sender in the same order in -- which the numbers have been sent. -- -- -- Claim 100 (**PROVED**) (Used Lemmas: 110,120) -- -- invariant ((tag1(s) = tag2(s) implies mk(next(s)) = (next(s) list(s))) and -- (not(tag1(s) = tag2(s)) implies mk(next(s)) = list(s))) -- -- -- To prove Claim 100, we need to conjecture a dozen of invariants. -- To this end, we should observe how the system changes. -- The following is one possible execution of the system: -- -- ... -- tag1: up tag2: up -- next: x list: ... -- up ... up -- -- || -- \/ -- -- ... -- tag1: up tag2: down -- next: x list: x ... -- up ... up -- -- || -- \/ -- -- ... -- tag1: up tag2: down -- next: x list: x ... -- up ... up down ... down -- -- || -- \/ -- -- ... -- tag1: up tag2: down -- next: x list: x ... -- down ... down -- -- || -- \/ -- -- ... -- tag1: down tag2: down -- next: x' list: x ... -- down ... down -- -- || -- \/ -- -- ... ... -- tag1: down tag2: down -- next: x' list: x ... -- down ... down -- -- || -- \/ -- -- ... -- tag1: down tag2: down -- next: x' list: x ... -- down ... down -- -- || -- \/ -- -- ... -- tag1: down tag2: up -- next: x' list: x' x ... -- down ... down -- -- || -- \/ -- . -- . -- . -- -- From this, we can conjecture several invariants, especially Claim 230 -- and Claim 240. -- -- We can easily find Claims 110 - 180 necessary while we prove the -- claims that depend on the necessary claims. -- -- It is not a good idea to prove Claim 170 and CLaim 180 directly -- because we should consider many cases where the 2nd and 3rd -- elements are different, 3rd and 4th elements are diferent, etc. -- Instead of proving them, we prove the more general invariants Claim -- 190 and Claim 200, which are easier to prove, from which Claim 170 -- and Claim 180 can be deduced by reduction only. -- -- Besides, Claim 190 and Claim 200 depnds on Claim 210 and Claim 220. -- It is not a good idea to prove them directly due to a similar -- reason. -- Instead of proving them, we prove Claim 230 and Claim 240, from -- which and other invariants, Claim 210 and Claim 220 can be proved -- by simple case analyses only. -- -- The above simulation is really usefull when we conjecture Claim 230 -- and Claim 240. -- -- Intuitive understanding is not enough, but is necessary to prove -- somthing formally! -- -- -- Claim 110 (**PROVED**) (Used Lemmas: 120,130,140) -- -- invariant ((not empty?(fifo2(s)) and not(tag1(s) = top(fifo2(s)))) -- implies (tag2(s) = top(fifo2(s)))) -- -- -- Claim 120 (**PROVED**) (Used Lemmas: 110,150,160) -- -- invariant ((not empty?(fifo1(s)) and tag2(s) = 1st(top(fifo1(s)))) -- implies -- (tag1(s) = 1st(top(fifo1(s))) and next(s) = 2nd(top(fifo1(s))))) -- -- -- Claim 130 (**PROVED**) (Used Lemmas: 110,170) -- -- invariant ((not empty?(fifo2(s)) and -- not(tag1(s) = top(fifo2(s))) and tag \in fifo2(s)) -- implies (top(fifo2(s)) = tag)) -- -- -- Claim 140 (**PROVED**) (Used Lemmas: 110,120,130) -- -- invariant ((not empty?(fifo2(s)) and tag \in fifo2(s) and not(tag1(s) = tag)) -- implies (tag2(s) = tag)) -- -- -- Claim 150 (**PROVED**) (Used Lemmas: 120,180) -- -- invariant ((not empty?(fifo1(s)) and -- tag2(s) = 1st(top(fifo1(s))) and pair \in fifo1(s)) -- implies (top(fifo1(s)) = pair)) -- -- -- Claim 160 (**PROVED**) (Used Lemmas: 110,120,150,180) -- -- invariant ((not empty?(fifo1(s)) and pair \in fifo1(s) and tag2(s) = 1st(pair)) -- implies (tag1(s) = 1st(pair) and next(s) = 2nd(pair))) -- -- -- Claim 170 (**PROVED**) (Used Lemmas: 190) -- -- invariant ((fifo2(s) = tag1 | tag2 | bfifo and not(tag1 = tag2)) -- implies ((tag3 \in bfifo implies tag2 = tag3) and tag2 = tag2(s))) -- -- -- Claim 180 (**PROVED**) (Used Lemmas: 220) -- -- invariant ((fifo1(s) = pair1 | pair2 | pfifo and not(pair1 = pair2)) -- implies ((pair3 \in pfifo implies pair2 = pair3) and pair2 = < tag1(s) , next(s) >)) -- -- -- Claim 190 (**PROVED**) (Used Lemmas: 210) -- -- invariant ((fifo2(s) = bfifo1 @ (tag1 | tag2 | bfifo2) and not(tag1 = tag2)) -- implies ((tag3 \in bfifo2 implies tag2 = tag3) and tag2 = tag2(s))) -- -- -- Claim 200 (**PROVED**) (Used Lemmas: 220) -- -- invariant ((fifo1(s) = pfifo1 @ (pair1 | pair2 | pfifo2) and not(pair1 = pair2)) -- implies ((pair3 \in pfifo2 implies pair2 = pair3) and pair2 = < tag1(s) , next(s) >)) -- -- -- Claim 210 (**PROVED**) (Used Lemmas: 120,230) -- -- invariant ((not(empty?(fifo1(s))) and tag2(s) = 1st(top(fifo1(s)))) -- implies (tag \in fifo2(s) implies tag2(s) = tag)) -- -- -- Claim 220 (**PROVED**) (Used Lemmas: 110,240) -- -- invariant ((not(empty?(fifo2(s))) and not(tag1(s) = top(fifo2(s)))) -- implies (pair \in fifo1(s) implies pair = < tag1(s) , next(s) >)) -- -- -- Claim 230 (**PROVED**) (Used Lemmas: 120,130) -- -- invariant ((tag1(s) = tag2(s)) -- implies -- (tag \in fifo2(s) implies tag = tag2(s))) -- -- -- -- Claim 240 (**PROVED**) (Used Lemmas: 110,120,150) -- -- invariant (not(tag1(s) = tag2(s)) -- implies -- (pair \in fifo1(s) implies pair = < tag1(s) , next(s) >)) -- mod INV { pr(ABP) -- arbitrary objects ops tag tag1 tag2 tag3 : -> Tagvalue ops pair pair1 pair2 pair3 : -> Pair ops bfifo bfifo1 bfifo2 : -> BFifo ops pfifo pfifo1 pfifo2 : -> PFifo -- declare invariants to prove op inv100 : System -> Bool op inv110 : System -> Bool op inv120 : System -> Bool op inv130 : System Tagvalue -> Bool op inv140 : System Tagvalue -> Bool op inv150 : System Pair -> Bool op inv160 : System Pair -> Bool op inv170 : System Tagvalue Tagvalue Tagvalue BFifo -> Bool op inv180 : System Pair Pair Pair PFifo -> Bool op inv190 : System Tagvalue Tagvalue Tagvalue BFifo BFifo -> Bool op inv200 : System Pair Pair Pair PFifo PFifo -> Bool op inv210 : System Tagvalue -> Bool op inv220 : System Pair -> Bool op inv230 : System Tagvalue -> Bool op inv240 : System Pair -> Bool -- CafeOBJ variables var S : System vars TAG TAG1 TAG2 TAG3 : Tagvalue vars PAIR PAIR1 PAIR2 PAIR3 : Pair vars BFIFO BFIFO1 BFIFO2 : BFifo vars PFIFO PFIFO1 PFIFO2 : PFifo -- define invariants to prove eq inv100(S) = (tag1(S) = tag2(S) implies mk(next(S)) = (next(S) list(S))) and (not(tag1(S) = tag2(S)) implies mk(next(S)) = list(S)) . eq inv110(S) = (not(empty?(fifo2(S))) and not(tag1(S) = top(fifo2(S)))) implies (tag2(S) = top(fifo2(S))) . eq inv120(S) = (not(empty?(fifo1(S))) and tag2(S) = 1st(top(fifo1(S)))) implies (tag1(S) = 1st(top(fifo1(S))) and next(S) = 2nd(top(fifo1(S)))) . eq inv130(S,TAG) = (not(empty?(fifo2(S))) and not(tag1(S) = top(fifo2(S))) and TAG \in fifo2(S)) implies (top(fifo2(S)) = TAG) . eq inv140(S,TAG) = (not(empty?(fifo2(S))) and TAG \in fifo2(S) and not(tag1(S) = TAG)) implies (tag2(S) = TAG) . eq inv150(S,PAIR) = (not(empty?(fifo1(S))) and tag2(S) = 1st(top(fifo1(S))) and PAIR \in fifo1(S)) implies (top(fifo1(S)) = PAIR) . eq inv160(S,PAIR) = (not(empty?(fifo1(S))) and PAIR \in fifo1(S) and tag2(S) = 1st(PAIR)) implies (tag1(S) = 1st(PAIR) and next(S) = 2nd(PAIR)) . eq inv170(S,TAG1,TAG2,TAG3,BFIFO) = ((fifo2(S) = TAG1 | TAG2 | BFIFO and not(TAG1 = TAG2)) implies ((TAG3 \in BFIFO implies TAG2 = TAG3) and TAG2 = tag2(S))) . eq inv180(S,PAIR1,PAIR2,PAIR3,PFIFO) = ((fifo1(S) = PAIR1 | PAIR2 | PFIFO and not(PAIR1 = PAIR2)) implies ((PAIR3 \in PFIFO implies PAIR2 = PAIR3) and PAIR2 = < tag1(S) , next(S) >)) . eq inv190(S,TAG1,TAG2,TAG3,BFIFO1,BFIFO2) = ((fifo2(S) = BFIFO1 @ (TAG1 | TAG2 | BFIFO2) and not(TAG1 = TAG2)) implies ((TAG3 \in BFIFO2 implies TAG2 = TAG3) and TAG2 = tag2(S))) . eq inv200(S,PAIR1,PAIR2,PAIR3,PFIFO1,PFIFO2) = ((fifo1(S) = PFIFO1 @ (PAIR1 | PAIR2 | PFIFO2) and not(PAIR1 = PAIR2)) implies ((PAIR3 \in PFIFO2 implies PAIR2 = PAIR3) and PAIR2 = < tag1(S) , next(S) >)) . eq inv210(S,TAG) = ((not(empty?(fifo1(S))) and tag2(S) = 1st(top(fifo1(S)))) implies (TAG \in fifo2(S) implies tag2(S) = TAG)) . eq inv220(S,PAIR) = ((not(empty?(fifo2(S))) and not(tag1(S) = top(fifo2(S)))) implies (PAIR \in fifo1(S) implies PAIR = < tag1(S) , next(S) >)) . eq inv230(S,TAG) = ((tag1(S) = tag2(S)) implies (TAG \in fifo2(S) implies TAG = tag2(S))) . eq inv240(S,PAIR) = (not(tag1(S) = tag2(S)) implies (PAIR \in fifo1(S) implies PAIR = < tag1(S) , next(S) >)) . } mod ISTEP { pr(INV) -- arbitrary objects ops s s' : -> System -- declare predicates to prove in inductive step op istep100 : -> Bool op istep110 : -> Bool op istep120 : -> Bool op istep130 : Tagvalue -> Bool op istep140 : Tagvalue -> Bool op istep150 : Pair -> Bool op istep160 : Pair -> Bool -- -- op istep190 : Tagvalue Tagvalue Tagvalue BFifo BFifo -> Bool op istep200 : Pair Pair Pair PFifo PFifo -> Bool -- -- op istep230 : Tagvalue -> Bool op istep240 : Pair -> Bool -- CafeOBJ variables vars TAG TAG1 TAG2 TAG3 : Tagvalue vars PAIR PAIR1 PAIR2 PAIR3 : Pair vars BFIFO BFIFO1 BFIFO2 : BFifo vars PFIFO PFIFO1 PFIFO2 : PFifo -- define predicates to prove in inductive step eq istep100 = inv100(s) implies inv100(s') . eq istep110 = inv110(s) implies inv110(s') . eq istep120 = inv120(s) implies inv120(s') . eq istep130(TAG) = inv130(s,TAG) implies inv130(s',TAG) . eq istep140(TAG) = inv140(s,TAG) implies inv140(s',TAG) . eq istep150(PAIR) = inv150(s,PAIR) implies inv150(s',PAIR) . eq istep160(PAIR) = inv160(s,PAIR) implies inv160(s',PAIR) . -- -- eq istep190(TAG1,TAG2,TAG3,BFIFO1,BFIFO2) = inv190(s,TAG1,TAG2,TAG3,BFIFO1,BFIFO2) implies inv190(s',TAG1,TAG2,TAG3,BFIFO1,BFIFO2) . eq istep200(PAIR1,PAIR2,PAIR3,PFIFO1,PFIFO2) = inv200(s,PAIR1,PAIR2,PAIR3,PFIFO1,PFIFO2) implies inv200(s',PAIR1,PAIR2,PAIR3,PFIFO1,PFIFO2) . -- -- eq istep230(TAG) = inv230(s,TAG) implies inv230(s',TAG) . eq istep240(PAIR) = inv240(s,PAIR) implies inv240(s',PAIR) . }