Case Analysis in CCRW, 2

# Case Analysis in Circular Coinductive Rewriting, 2

Here we apply BOBJ's circular coinductive rewriting algorithm, with its new feature for case analysis, to a real time asynchronous data transmission protocol. The spec and the proof are both due to Profs. Futatsugi and Ogata of JAIST (see Rewriting can verify distributed real-time systems - how to verify in CafeOBJ, in Proc. Int. Workshop on Rewriting in Proof and Computation, pp. 60-79, 2001). However the presentation of this proof is much simplified by using BOBJ's case analysis features, including named case declarations (so that they are first class citizens, that can be reused), "multiplying" cases to form compound cases (the cartesian product of the cases of the components), and excluding cases from a product (e.g., because they cannot occur). These features were developed jointly by Joseph Goguen and Kai Lin, and were implemented by Kai Lin.

### 1. BOBJ Source Code

dth BASIC-INT is sorts Zero NzNat Nat NgInt NpInt Int . subsort Zero NzNat < Nat . subsort NgInt Zero < NpInt . subsort NgInt Zero NpInt NzNat Nat < Int . op 0 : -> Zero . op s_ : Nat -> NzNat . op p_ : NpInt -> NgInt . op s_ : Int -> Int . op p_ : Int -> Int . var I : Int . eq s p I = I . eq p s I = I . end dth INT* is pr BASIC-INT . op _+_ : Int Int -> Int [assoc comm]. vars I J : Int . var N : NzNat . eq I + 0 = I . eq I + s J = s(I + J) . eq I + p J = p(I + J) . op -_ : Int -> Int . eq - 0 = 0 . eq - (s I) = p (- I) . eq - (p I) = s (- I) . op _*_ : Int Int -> Int . eq 0 * J = 0 . eq (s I) * J = J + (I * J) . eq (p I) * J = (- J) + (I * J) . ops inc dec : Int -> Int . eq inc(I) = s I . eq dec(I) = p I . op _<_ : Int Int -> Bool . eq I < I + N = true . end dth LIST [X :: TRIV]is sort List . op nil : -> List . op _\$_ : Elt List -> List . op car_ : List -> Elt . op cdr_ : List -> List . var E : Elt . var L : List . eq car (E \$ L) = E . eq cdr (E \$ L) = L . end dth ILIST is pr LIST[INT*]. op 0 upto _ : Int -> List . var N : NgInt . var M : Nat . var I : Int . var L : List . eq 0 upto N = nil . eq 0 upto 0 = nil . eq 0 upto (s M) = (M \$ (0 upto M)) . eq cdr (0 upto I) = 0 upto (p I) . eq (s I) \$ (0 upto I) = 0 upto (s I) . eq I \$ (0 upto p I) = 0 upto I . op put : List Int -> List . eq put(L, I) = I \$ L . end th REAL+ is sorts Real+ Timeval Timeval0 . subsort Real+ Timeval < Timeval0 . op 0 : -> Real+ . op oo : -> Timeval . op _+_ : Timeval0 Timeval0 -> Timeval0 [comm]. op _+_ : Real+ Real+ -> Real+ [comm]. op _+_ : Timeval Timeval -> Timeval [comm]. op _<=_ : Timeval0 Timeval0 -> Bool . op _<_ : Timeval0 Timeval0 -> Bool . vars T1 T2 T3 : Timeval0 . eq T1 + T2 <= T1 + T3 = T2 <= T3 . eq T1 + T2 < T1 + T3 = T2 < T3 . end ***> distributed real-time asynchoronous data transmission protocol bth ASEND is sort Sys . protecting INT* + ILIST + REAL+ . op init : -> Sys . op empty : Sys -> Bool . ops content data : Sys -> Nat . op list : Sys -> List . ops now l : Sys -> Real+ . op u : Sys -> Timeval . ops send rec : Sys -> Sys . op tick : Sys Real+ -> Sys . op d1 : -> Real+ . *** minimum delay for send op d2 : -> Real+ . *** maximum delay for rec eq d2 < d1 = true . var T : Timeval0 . var S : Sys . var D : Real+ . eq T < T + d1 = true . eq empty(init) = true . eq data(init) = 0 . eq list(init) = nil . eq now(init) = 0 . eq l(init) = d1 . eq u(init) = oo . ceq empty(send(S)) = false if l(S) <= now(S) . ceq empty(send(S)) = empty(S) if now(S) < l(S) . ceq content(send(S)) = data(S) if l(S) <= now(S) . ceq content(send(S)) = content(S) if now(S) < l(S) . ceq data(send(S)) = inc(data(S)) if l(S) <= now(S) . ceq data(send(S)) = data(S) if now(S) < l(S) . eq list(send(S)) = list(S) . eq now(send(S)) = now(S) . ceq l(send(S)) = now(S) + d1 if l(S) <= now(S) . ceq l(send(S)) = l(S) if now(S) < l(S) . ceq u(send(S)) = now(S) + d2 if l(S) <= now(S) . ceq u(send(S)) = u(S) if now(S) < l(S) . ceq empty(rec(S)) = true if empty(S) == false . ceq empty(rec(S)) = empty(S) if empty(S) == true . eq content(rec(S)) = content(S) . eq data(rec(S)) = data(S) . ceq list(rec(S)) = put(list(S),content(S)) if empty(S) == false . ceq list(rec(S)) = list(S) if empty(S) == true . eq now(rec(S)) = now(S) . eq l(rec(S)) = l(S) . ceq u(rec(S)) = oo if empty(S) == false . ceq u(rec(S)) = u(S) if empty(S) == true . eq empty(tick(S,D)) = empty(S) . eq content(tick(S,D)) = content(S) . eq data(tick(S,D)) = data(S) . eq list(tick(S,D)) = list(S) . ceq now(tick(S,D)) = now(S) + D if now(S) + D <= u(S) . ceq now(tick(S,D)) = now(S) if u(S) < now(S) + D . eq l(tick(S,D)) = l(S) . eq u(tick(S,D)) = u(S) . end dth INV is protecting ASEND . *** inv1 is the property we want to prove about the spec ASEND op inv1 : Sys -> Bool . var S : Sys . eq inv1(S) = (empty(S) implies (list(S) == 0 upto dec(data(S)))) and (not(empty(S)) implies (list(S) == 0 upto dec(dec(data(S))))) . op inv2 : Sys -> Bool . eq inv2(S) = empty(S) or (now(S) < l(S)) . op inv3 : Sys -> Bool . eq inv3(S) = (u(S) < l(S)) or empty(S) . op inv4 : Sys -> Bool . eq inv4(S) = (content(S) == dec(data(S))) or empty(S) . end ***> induction base: ***> inv1(init), inv2(init), inv3(init), inv4(init) hold open INV . red inv1(init) . red inv2(init) . red inv3(init) . red inv4(init) . close dth BASE is protecting INV . op s : -> Sys . var D : Real+ . end cases C1 for BASE is context s . case eq empty(s) = true . case eq empty(s) = false . end cases C2 for BASE is context s . case eq now(s) < l(s) = true . case eq l(s) <= now(s) = true . end cases C3 for BASE is var D : Real+ . context tick(s, D) . case eq now(s) + D <= u(s) = true . case eq u(s) < now(s) + D = true . end ***> ==== proof score for inv3 and inv4 ======= *** module for induction BASE for inv3 and inv4 dth BASE3and4 is protecting BASE . *** inv3 ceq u(s) < l(s) = true if not(empty(s)) . *** inv4 ceq content(s) = dec(data(s)) if not(empty(s)) . end open BASE3and4 . use C1 * C2 . cred inv3(send(s)) == true . cred inv4(send(s)) == true . cred inv3(rec(s)) == true . cred inv4(rec(s)) == true . op d : -> Real+ . cred inv3(tick(s,d)) == true . cred inv4(tick(s,d)) == true . close ***> ==== proof score for inv2 ======= dth BASE2 is protecting BASE . *** lemmata inv3 and inv4 are already proved var S : Sys . var D : Timeval0 . ceq (u(S) < l(S)) = true if not(empty(S)) . ceq content(S) = dec(data(S)) if not(empty(S)) . *** necessary proposition: validity is trivial ceq ((now(S) + D) < l(S)) = true if ((now(S) + D) <= u(S)) and (u(S) < l(S)) . *** inv2 ceq (now(s) < l(s)) = true if not(empty(s)) . end open BASE2 . use C1 * C2 . cred inv2(send(s)) == true . cred inv2(rec(s)) == true . op d : -> Real+ . cred with C3 * C1 * C2 inv2(tick(s,d)) == true . close ***> ==== proof score for inv1 ======= dth BASE1 is protecting BASE . var S : Sys . ceq (now(S) < l(S)) = true if not(empty(S)) . ceq (u(S) < l(S)) = true if not(empty(S)) . ceq content(S) = dec(data(S)) if not(empty(S)) . *** inv1: the property to be proved ceq list(s) = (0 upto dec(data(s))) if empty(s) . ceq list(s) = (0 upto dec(dec(data(s)))) if not(empty(s)) . end open BASE1 . cred with C1 * C2 exclude (2,2) inv1(send(s)) == true . cred with C1 inv1(rec(s)) == true . op d : -> Real+ . cred with C1 inv1(tick(s, d)) == true . close

### 2. BOBJ Output with Full Trace Off

We first give the output with full trace off, which is much more compact, though less informative, than the output with full trace on, as shown in the next section below. awk% bobj \|||||||||||||||||/ --- Welcome to BOBJ --- /|||||||||||||||||\ BOBJ version 0.9.146 built: Mon Jan 7 18:30:55 PST 2002 University of California, San Diego Tue Jan 08 13:14:43 PST 2002 BOBJ> in realcase ========================================== dth BASIC-INT ========================================== dth INT* ========================================== dth LIST ========================================== dth ILIST ========================================== th REAL+ ========================================== ***> distributed real-time asynchoronous data transmission protocol ========================================== bth ASEND ========================================== dth INV ========================================== ***> induction base: ========================================== ***> inv1(init), inv2(init), inv3(init), inv4(init) hold ========================================== open INV ========================================== reduce in INV : inv1(init) result Bool: true rewrite time: 144ms parse time: 1ms ========================================== reduce in INV : inv2(init) result Bool: true rewrite time: 2ms parse time: 2ms ========================================== reduce in INV : inv3(init) result Bool: true rewrite time: 22ms parse time: 1ms ========================================== reduce in INV : inv4(init) result Bool: true rewrite time: 3ms parse time: 1ms ========================================== close ========================================== dth BASE ========================================== cases C1 ========================================== cases C2 ========================================== cases C3 ========================================== ***> ==== proof score for inv3 and inv4 ======= ========================================== dth BASE3and4 ========================================== open BASE3and4 ========================================== use C1 * C2 ========================================== c-reduce in BASE3and4 : inv3(send(s)) == true result: true c-rewrite time: 85ms parse time: 11ms ========================================== c-reduce in BASE3and4 : inv4(send(s)) == true result: true c-rewrite time: 57ms parse time: 3ms ========================================== c-reduce in BASE3and4 : inv3(rec(s)) == true result: true c-rewrite time: 46ms parse time: 4ms ========================================== c-reduce in BASE3and4 : inv4(rec(s)) == true result: true c-rewrite time: 42ms parse time: 3ms ========================================== op d : -> Real+ ========================================== c-reduce in BASE3and4 : inv3(tick(s, d)) == true result: true c-rewrite time: 44ms parse time: 4ms ========================================== c-reduce in BASE3and4 : inv4(tick(s, d)) == true result: true c-rewrite time: 39ms parse time: 4ms ========================================== close ========================================== ***> ==== proof score for inv2 ======= ========================================== dth BASE2 ========================================== open BASE2 ========================================== use C1 * C2 ========================================== c-reduce in BASE2 : inv2(send(s)) == true result: true c-rewrite time: 46ms parse time: 3ms ========================================== c-reduce in BASE2 : inv2(rec(s)) == true result: true c-rewrite time: 32ms parse time: 3ms ========================================== op d : -> Real+ ========================================== c-reduce in BASE2 : inv2(tick(s, d)) == true use: C3 * C1 * C2 result: true c-rewrite time: 87ms parse time: 4ms ========================================== close ========================================== ***> ==== proof score for inv1 ======= ========================================== dth BASE1 ========================================== open BASE1 ========================================== c-reduce in BASE1 : inv1(send(s)) == true use: C1 * C2 exclude (2,2) result: true c-rewrite time: 99ms parse time: 3ms ========================================== c-reduce in BASE1 : inv1(rec(s)) == true use: C1 result: true c-rewrite time: 81ms parse time: 4ms ========================================== op d : -> Real+ ========================================== c-reduce in BASE1 : inv1(tick(s, d)) == true use: C1 result: true c-rewrite time: 69ms parse time: 4ms ========================================== close BOBJ> q Bye.

### 3. BOBJ Output with Full Trace On

We next give the output with full trace on, which shows many more details about the computations that are performed. awk% bobj \|||||||||||||||||/ --- Welcome to BOBJ --- /|||||||||||||||||\ BOBJ version 0.9.146 built: Mon Jan 7 18:30:55 PST 2002 University of California, San Diego Tue Jan 08 13:14:56 PST 2002 BOBJ> set full trace on . BOBJ> in realcase ========================================== dth BASIC-INT ========================================== dth INT* ========================================== dth LIST ========================================== dth ILIST ========================================== th REAL+ ========================================== ***> distributed real-time asynchoronous data transmission protocol ========================================== bth ASEND ========================================== dth INV ========================================== ***> induction base: ========================================== ***> inv1(init), inv2(init), inv3(init), inv4(init) hold ========================================== open INV ========================================== reduce in INV : inv1(init) result Bool: true rewrite time: 158ms parse time: 1ms ========================================== reduce in INV : inv2(init) result Bool: true rewrite time: 2ms parse time: 2ms ========================================== reduce in INV : inv3(init) result Bool: true rewrite time: 22ms parse time: 1ms ========================================== reduce in INV : inv4(init) result Bool: true rewrite time: 4ms parse time: 2ms ========================================== close ========================================== dth BASE ========================================== cases C1 ========================================== cases C2 ========================================== cases C3 ========================================== ***> ==== proof score for inv3 and inv4 ======= ========================================== dth BASE3and4 ========================================== open BASE3and4 ========================================== use C1 * C2 ========================================== c-reduce in BASE3and4 : inv3(send(s)) == true ------------------------------------------- case analyse by C1 * C2 ------------------------------------------- case (1,1) : assume: empty(s) = true now(s) < l(s) = true reduce: inv3(send(s)) == true nf: true ------------------------------- case (1,2) : assume: empty(s) = true l(s) <= now(s) = true reduce: inv3(send(s)) == true nf: true ------------------------------- case (2,1) : assume: empty(s) = false now(s) < l(s) = true reduce: inv3(send(s)) == true nf: true ------------------------------- case (2,2) : assume: empty(s) = false l(s) <= now(s) = true reduce: inv3(send(s)) == true nf: true ------------------------------- result: true c-rewrite time: 101ms parse time: 11ms ========================================== c-reduce in BASE3and4 : inv4(send(s)) == true ------------------------------------------- case analyse by C1 * C2 ------------------------------------------- case (1,1) : assume: empty(s) = true now(s) < l(s) = true reduce: inv4(send(s)) == true nf: true ------------------------------- case (1,2) : assume: empty(s) = true l(s) <= now(s) = true reduce: inv4(send(s)) == true nf: true ------------------------------- case (2,1) : assume: empty(s) = false now(s) < l(s) = true reduce: inv4(send(s)) == true nf: true ------------------------------- case (2,2) : assume: empty(s) = false l(s) <= now(s) = true reduce: inv4(send(s)) == true nf: true ------------------------------- result: true c-rewrite time: 63ms parse time: 3ms ========================================== c-reduce in BASE3and4 : inv3(rec(s)) == true ------------------------------------------- case analyse by C1 * C2 ------------------------------------------- case (1,1) : assume: empty(s) = true now(s) < l(s) = true reduce: inv3(rec(s)) == true nf: true ------------------------------- case (1,2) : assume: empty(s) = true l(s) <= now(s) = true reduce: inv3(rec(s)) == true nf: true ------------------------------- case (2,1) : assume: empty(s) = false now(s) < l(s) = true reduce: inv3(rec(s)) == true nf: true ------------------------------- case (2,2) : assume: empty(s) = false l(s) <= now(s) = true reduce: inv3(rec(s)) == true nf: true ------------------------------- result: true c-rewrite time: 59ms parse time: 3ms ========================================== c-reduce in BASE3and4 : inv4(rec(s)) == true ------------------------------------------- case analyse by C1 * C2 ------------------------------------------- case (1,1) : assume: empty(s) = true now(s) < l(s) = true reduce: inv4(rec(s)) == true nf: true ------------------------------- case (1,2) : assume: empty(s) = true l(s) <= now(s) = true reduce: inv4(rec(s)) == true nf: true ------------------------------- case (2,1) : assume: empty(s) = false now(s) < l(s) = true reduce: inv4(rec(s)) == true nf: true ------------------------------- case (2,2) : assume: empty(s) = false l(s) <= now(s) = true reduce: inv4(rec(s)) == true nf: true ------------------------------- result: true c-rewrite time: 54ms parse time: 3ms ========================================== op d : -> Real+ ========================================== c-reduce in BASE3and4 : inv3(tick(s, d)) == true ------------------------------------------- case analyse by C1 * C2 ------------------------------------------- case (1,1) : assume: empty(s) = true now(s) < l(s) = true reduce: inv3(tick(s, d)) == true nf: true ------------------------------- case (1,2) : assume: empty(s) = true l(s) <= now(s) = true reduce: inv3(tick(s, d)) == true nf: true ------------------------------- case (2,1) : assume: empty(s) = false now(s) < l(s) = true reduce: inv3(tick(s, d)) == true nf: true ------------------------------- case (2,2) : assume: empty(s) = false l(s) <= now(s) = true reduce: inv3(tick(s, d)) == true nf: true ------------------------------- result: true c-rewrite time: 58ms parse time: 3ms ========================================== c-reduce in BASE3and4 : inv4(tick(s, d)) == true ------------------------------------------- case analyse by C1 * C2 ------------------------------------------- case (1,1) : assume: empty(s) = true now(s) < l(s) = true reduce: inv4(tick(s, d)) == true nf: true ------------------------------- case (1,2) : assume: empty(s) = true l(s) <= now(s) = true reduce: inv4(tick(s, d)) == true nf: true ------------------------------- case (2,1) : assume: empty(s) = false now(s) < l(s) = true reduce: inv4(tick(s, d)) == true nf: true ------------------------------- case (2,2) : assume: empty(s) = false l(s) <= now(s) = true reduce: inv4(tick(s, d)) == true nf: true ------------------------------- result: true c-rewrite time: 53ms parse time: 4ms ========================================== close ========================================== ***> ==== proof score for inv2 ======= ========================================== dth BASE2 ========================================== open BASE2 ========================================== use C1 * C2 ========================================== c-reduce in BASE2 : inv2(send(s)) == true ------------------------------------------- case analyse by C1 * C2 ------------------------------------------- case (1,1) : assume: empty(s) = true now(s) < l(s) = true reduce: inv2(send(s)) == true nf: true ------------------------------- case (1,2) : assume: empty(s) = true l(s) <= now(s) = true reduce: inv2(send(s)) == true nf: true ------------------------------- case (2,1) : assume: empty(s) = false now(s) < l(s) = true reduce: inv2(send(s)) == true nf: true ------------------------------- case (2,2) : assume: empty(s) = false l(s) <= now(s) = true reduce: inv2(send(s)) == true nf: true ------------------------------- result: true c-rewrite time: 64ms parse time: 3ms ========================================== c-reduce in BASE2 : inv2(rec(s)) == true ------------------------------------------- case analyse by C1 * C2 ------------------------------------------- case (1,1) : assume: empty(s) = true now(s) < l(s) = true reduce: inv2(rec(s)) == true nf: true ------------------------------- case (1,2) : assume: empty(s) = true l(s) <= now(s) = true reduce: inv2(rec(s)) == true nf: true ------------------------------- case (2,1) : assume: empty(s) = false now(s) < l(s) = true reduce: inv2(rec(s)) == true nf: true ------------------------------- case (2,2) : assume: empty(s) = false l(s) <= now(s) = true reduce: inv2(rec(s)) == true nf: true ------------------------------- result: true c-rewrite time: 45ms parse time: 3ms ========================================== op d : -> Real+ ========================================== c-reduce in BASE2 : inv2(tick(s, d)) == true use: C3 * C1 * C2 ------------------------------------------- case analyse by C3 * C1 * C2 ------------------------------------------- case (1,1,1) : assume: (now(s) + d) <= u(s) = true empty(s) = true now(s) < l(s) = true reduce: inv2(tick(s, d)) == true nf: true ------------------------------- case (1,1,2) : assume: (now(s) + d) <= u(s) = true empty(s) = true l(s) <= now(s) = true reduce: inv2(tick(s, d)) == true nf: true ------------------------------- case (1,2,1) : assume: (now(s) + d) <= u(s) = true empty(s) = false now(s) < l(s) = true reduce: inv2(tick(s, d)) == true nf: true ------------------------------- case (1,2,2) : assume: (now(s) + d) <= u(s) = true empty(s) = false l(s) <= now(s) = true reduce: inv2(tick(s, d)) == true nf: true ------------------------------- case (2,1,1) : assume: u(s) < (now(s) + d) = true empty(s) = true now(s) < l(s) = true reduce: inv2(tick(s, d)) == true nf: true ------------------------------- case (2,1,2) : assume: u(s) < (now(s) + d) = true empty(s) = true l(s) <= now(s) = true reduce: inv2(tick(s, d)) == true nf: true ------------------------------- case (2,2,1) : assume: u(s) < (now(s) + d) = true empty(s) = false now(s) < l(s) = true reduce: inv2(tick(s, d)) == true nf: true ------------------------------- case (2,2,2) : assume: u(s) < (now(s) + d) = true empty(s) = false l(s) <= now(s) = true reduce: inv2(tick(s, d)) == true nf: true ------------------------------- result: true c-rewrite time: 104ms parse time: 4ms ========================================== close ========================================== ***> ==== proof score for inv1 ======= ========================================== dth BASE1 ========================================== open BASE1 ========================================== c-reduce in BASE1 : inv1(send(s)) == true use: C1 * C2 exclude (2,2) ------------------------------------------- case analyse by C1 * C2 exclude (2,2) ------------------------------------------- case (1,1) : assume: empty(s) = true now(s) < l(s) = true reduce: inv1(send(s)) == true nf: true ------------------------------- case (1,2) : assume: empty(s) = true l(s) <= now(s) = true reduce: inv1(send(s)) == true nf: true ------------------------------- case (2,1) : assume: empty(s) = false now(s) < l(s) = true reduce: inv1(send(s)) == true nf: true ------------------------------- result: true c-rewrite time: 117ms parse time: 3ms ========================================== c-reduce in BASE1 : inv1(rec(s)) == true use: C1 ------------------------------------------- case analyse by C1 ------------------------------------------- case 1 : assume: empty(s) = true reduce: inv1(rec(s)) == true nf: true ------------------------------- case 2 : assume: empty(s) = false reduce: inv1(rec(s)) == true nf: true ------------------------------- result: true c-rewrite time: 74ms parse time: 3ms ========================================== op d : -> Real+ ========================================== c-reduce in BASE1 : inv1(tick(s, d)) == true use: C1 ------------------------------------------- case analyse by C1 ------------------------------------------- case 1 : assume: empty(s) = true reduce: inv1(tick(s, d)) == true nf: true ------------------------------- case 2 : assume: empty(s) = false reduce: inv1(tick(s, d)) == true nf: true ------------------------------- result: true c-rewrite time: 82ms parse time: 4ms ========================================== close BOBJ> q Bye. awk%

To the BOBJ Examples homepage
To the Tatami project homepage
Maintained by Joseph Goguen