Fun with Streams and Buffers

Fun with Streams and Buffers

We prove the same properties of simple combinations of streams and buffers as were previously proved for streams and cells, using buffers into which data can only be written when they are empty, so that they must be cleared before they are written. Using streams for the sender process and a one item buffer for the receiver process seems a very natural approach to communication protocols in a behavioral setting. Everything works, though of course many details are more complex than for streams and cells, and in particular, one coinductive reduction contains at least three circularities in the proof (an occurrence of the word "deduced" in the output indicates that there was at least one circularity in that computation). Note that when representing a stream by a stream plus a buffer, the buffer must be nonempty or else it cannnot represent a stream. Although there are several refinement proofs here, we found it unnecessary to change the cobasis to that of the source theory, and therefore did not bother to do so. As usual, the BOBJ source code is followed by its output. Kai Lin helped with these examples.

1. BOBJ Source Code

*** file: sandb.bob ***> fun with streams and buffers set trace on *** shared data theory: th DATA is sort D . end bth STREAM is sort S . pr DATA . op cons : D S -> S . op head_ : S -> D . op tail_ : S -> S . var D : D . var S : S . eq head cons(D,S) = D . eq tail cons(D,S) = S . end show cobasis . bth 1BUFF is sort B . pr DATA . op nil : -> B . op err : -> D . op put__ : D B -> B . op get_ : B -> D . op clr_ : B -> B . op nil?_ : B -> Bool . vars D D1 D2 : D . var B B1 : B . eq clr B = nil . eq nil? nil = true . eq nil? put D B = false . eq get (put D B) = if nil? B then D else err fi . eq get nil = err . end ***> we prove some lemmas op b : -> B . eq nil? b = false . ***> first show that they are not strictly satisfied: red put (get b) nil == b . red put (get b) clr B1 == b . red put (get b) clr (put D clr B1) == b . red put D1 (put D2 B) == put err B . ***> now the behavioral proofs: cred put (get b) nil == b . cred put (get b) clr B1 == b . cred put (get b) clr (put D clr B1) == b . cred put D1 (put D2 B) == put err B . close ***> now assert the lemmas: bth 1BUFFL is pr 1BUFF . var B B1 : B . vars D D1 D2 : D . cq put (get B) nil = B if not nil? B . cq put (get B) clr B1 = B if not nil? B . cq put (get B) clr (put D clr B1) = B if not nil? B . eq put D1 (put D2 B) = put err B . end ***> stream + 1-buffer behaviorally refines stream bth P is pr (STREAM || 1BUFFL) * (sort Tuple to P). op cons : D P -> P . op head_ : P -> D . op tail_ : P -> P . var D : D . var S : S . var B : B . cq cons(D, < S, B >) = < cons(get B, S), put D clr B > if not nil? B . cq head < S, B > = get B if not nil? B . eq tail < S, B > = < tail S, put (head S) clr B > . end *** note the slightly clever definition for cons (and tail) show cobasis . open . op b : -> B . eq nil? b = false . red head cons(D, < S, b >) == D . red tail cons(D, < S, b >) == < S, b > . close ***> two 1-buffers behaviorally refine a 1-cell bth P is pr (1BUFFL || 1BUFFL) * (sort Tuple to P). op f_ : P -> P . op get_ : P -> D . op p1__ : D P -> P . op put__ : D P -> P . var D : D . vars B1 B2 : B . eq p1 D < B1, B2 > = < (put D clr B1), B2 > . eq f < B1, B2 > = < B1, put (get B1) clr B2 > . eq get < B1, B2 > = get B2 . eq put D < B1, B2 > = f(p1 D < B1, B2 >). end show cobasis . *** action-like abbreviating notation used above red get (put D < B1, B2 > ) == D . bth 2CELL is sort C . pr DATA . op put__ : D C -> C . op get_ : C -> D . vars D1 D2 : D . var C : C . eq get(put D1 (put D2 C)) = D2 . end show cobasis . ***> two 1-buffers behaviorally refine one 2-cell bth P is pr (1BUFFL || 1BUFFL) * (sort Tuple to P). op get_ : P -> D . op put__ : D P -> P . vars D D1 D2 : D . vars B1 B2 : B . eq put D < B1, B2 > = < put D clr B1, (put (get B1) clr B2) > . eq get < B1, B2 > = get B2 . end red get(put D1 (put D2 < B1, B2 >)) == D2 . ***> stream + two 1-buffers behaviorally refine stream bth P is pr (STREAM || 1BUFFL || 1BUFFL) * (sort Tuple to P). op head_ : P -> D . op tail_ : P -> P . op cons : D P -> P . var D : D . var S : S . vars B1 B2 : B . eq cons(D, < S, B1, B2 >) = < cons(get B1,S), (put(get B2) clr B1), put D clr B2 > . eq head < S, B1, B2 > = get B2 . eq tail < S, B1, B2 > = < tail S, put(head S) clr B1, put(get B1) clr B2 > . end *** this is closer to a sender-channel-receiver communication system show cobasis . open . ops b1 b2 : -> B . eq nil? b1 = false . eq nil? b2 = false . red head cons(D, < S, B1, B2 >) == D . red tail cons(D, < S, b1, b2 >) == < S, b1, b2 > . close ***> check that the behavioral lemma is really needed above: bth P is pr (STREAM || 1BUFF || 1BUFF) * (sort Tuple to P). op head_ : P -> D . op tail_ : P -> P . op cons : D P -> P . var D : D . var S : S . vars B1 B2 : B . eq cons(D, < S, B1, B2 >) = < cons(get B1,S), (put(get B2) clr B1), put D clr B2 > . eq head < S, B1, B2 > = get B2 . eq tail < S, B1, B2 > = < tail S, put(head S) clr B1, put(get B1) clr B2> . end ***> the second reduction should be false: red head cons(D, < S, B1, B2 >) == D . red tail cons(D, < S, B1, B2 >) == < S, B1, B2 > . ***> let BOBJ find the lemma itself: cred tail cons(D, < S, B1, B2 >) == < S, B1, B2 > . ***> three 1-buffers refine a 1-cell bth P is pr (1BUFF || 1BUFF || 1BUFF) * (sort Tuple to P). op get_ : P -> D . op put__ : D P -> P . op p1__ : D P -> P . ops (f1_)(f2_) : P -> P . var D : D . vars B1 B2 B3 : B . eq p1 D < B1, B2, B3 > = < (put D clr B1), B2, B3 > . eq f1 < B1, B2, B3 > = < B1, (put get B1 clr B2), B3 > . eq f2 < B1, B2, B3 > = < B1, B2, (put get B2 clr B3) > . eq put D < B1, B2, B3 > = f2 f1 (p1 D < B1, B2, B3 >). eq get < B1, B2, B3 > = get B3 . end *** action-like abbreviations used again show cobasis . red get (put D < B1, B2, B3 >) == D . bth 2BUFF is sort B . pr DATA . op nil : -> B . op err : -> D . op put__ : D B -> B . op get_ : B -> D . op sft_ : B -> B . op ok?_ : B -> Bool . var D D1 D2 : D . var B : B . eq sft nil = nil . eq sft sft B = nil . eq sft (put D sft B) = sft (put D nil). eq ok? nil = true . eq ok? sft B = true . eq ok? put D B = false . cq put D B = put err B if not ok? B and D =/= err . eq put err (put D B) = put err B . eq get put err B = err . eq get nil = err . eq get (put D nil) = err . eq get (put D sft B) = get sft B . cq get sft(put D B) = D if ok? B . cq get sft(put D B) = err if not ok? B . end show cobasis . ***> the following should be false: cred put (get B) nil == B . ***> but the following should be true: open . op b : -> B . eq ok? b = false . cred put(get sft b) sft (put get b nil) == b . ***> there are three circularities in this proof! close ***> two 1-buffers behaviorally refine a 2-buffer bth P is pr (1BUFFL || 1BUFFL) * (sort Tuple to P). op 2nil : -> P . op get_ : P -> D . op put__ : D P -> P . op sft_ : P -> P . op ok?_ : P -> Bool . vars D D1 D2 : D . vars B1 B2 : B . eq 2nil = < nil, nil > . eq sft < B1, B2 > = < nil, B1 > . eq put D < B1, B2 > = < put D B1, B2 > . cq < put D B1, B2 > = < put err B1, B2 > if not nil? B1 . eq get < put D B1, B2 > = if D == err then err else get B2 fi . eq get < nil, B2 > = get B2 . eq ok? <B1, B2> = nil? B1 . end show cobasis . ***> prove the equations of 2B: ***> first the key equation in 2 cases, & check another equation in 2nd case open . ops b1 b2 : -> B . eq ok? < b1, b2 > = true . eq nil? b1 = true . *** follows from above red get sft (put D < b1, b2 >) == D . close open . ops b1 b2 : -> B . eq ok? < b1, b2 > = false . eq nil? b1 = false . *** follows from above red get sft (put D < b1, b2 >) == err . cred put D < b1, b2 > == put err < b1, b2 > . close red sft 2nil == 2nil . red sft sft < B1, B2> == 2nil . red ok? 2nil == true . red ok? sft < B1, B2 > == true . red ok? put D < B1, B2 > == false . red sft (put D sft < B1, B2 >) == sft put D 2nil . red put err (put D < B1, B2 >) == put err < B1, B2 > . red get put err < B1, B2 > == err . red get 2nil == err . red get put D 2nil == err . red get put D sft < B1, B2 > == get sft < B1, B2 > . *** should also show 3 1-buffs refine one 2-buff

2. BOBJ Output

awk% bobj \|||||||||||||||||/ --- Welcome to BOBJ --- /|||||||||||||||||\ BOBJ version 0.0033 built: Fri Mar 17 16:55:05 PST 2000 University of California, San Diego Sun Mar 19 18:21:51 PST 2000 BOBJ> in sandb ========================================== ***> fun with streams and buffers ========================================== th DATA ========================================== bth STREAM ========================================== The cobasis for sort S is: op head _ : S -> D op tail _ : S -> S ========================================== bth 1BUFF ========================================== ***> we prove some lemmas ========================================== opening module 1BUFF. ========================================== ***> first show that they are not strictly satisfied: ========================================== reduce in 1BUFF : (put (get b) nil) == b result Bool: false LHS sort B: put (get b) nil RHS sort B: b rewrite time: 72ms parse time: 9ms ========================================== reduce in 1BUFF : (put (get b) (clr B1)) == b result Bool: false LHS sort B: put (get b) nil RHS sort B: b rewrite time: 53ms parse time: 36ms ========================================== reduce in 1BUFF : (put (get b) (clr (put D (clr B1)))) == b result Bool: false LHS sort B: put (get b) nil RHS sort B: b rewrite time: 62ms parse time: 15ms ========================================== reduce in 1BUFF : (put D1 (put D2 B)) == (put err B) result Bool: false LHS sort B: put D1 (put D2 B) RHS sort B: put err B rewrite time: 55ms parse time: 13ms ========================================== ***> now the behavioral proofs: ========================================== c-reduce in 1BUFF : (put (get b) nil) == b using cobasis for 1BUFF: op nil? _ : B -> Bool op get _ : B -> D --------------------------------------- reduced to: put (get b) nil == b ----------------------------------------- add rule (C1) : put (get b) nil = b ----------------------------------------- target is: put (get b) nil == b expand by: op nil? _ : B -> Bool reduced to: true nf: false ----------------------------------------- target is: put (get b) nil == b expand by: op get _ : B -> D reduced to: true nf: get b ----------------------------------------- result: true c-rewrite time: 114ms parse time: 6ms ========================================== c-reduce in 1BUFF : (put (get b) (clr B1)) == b reduced to: put (get b) nil == b ----------------------------------------- add rule (C1) : put (get b) nil = b ----------------------------------------- target is: put (get b) nil == b expand by: op nil? _ : B -> Bool reduced to: true nf: false ----------------------------------------- target is: put (get b) nil == b expand by: op get _ : B -> D reduced to: true nf: get b ----------------------------------------- result: true c-rewrite time: 22ms parse time: 37ms ========================================== c-reduce in 1BUFF : (put (get b) (clr (put D (clr B1)))) == b reduced to: put (get b) nil == b ----------------------------------------- add rule (C1) : put (get b) nil = b ----------------------------------------- target is: put (get b) nil == b expand by: op nil? _ : B -> Bool reduced to: true nf: false ----------------------------------------- target is: put (get b) nil == b expand by: op get _ : B -> D reduced to: true nf: get b ----------------------------------------- result: true c-rewrite time: 11ms parse time: 14ms ========================================== c-reduce in 1BUFF : (put D1 (put D2 B)) == (put err B) reduced to: put D1 (put D2 B) == put err B ----------------------------------------- add rule (C1) : put D1 (put D2 B) = put err B ----------------------------------------- target is: put D1 (put D2 B) == put err B expand by: op nil? _ : B -> Bool reduced to: true nf: false ----------------------------------------- target is: put D1 (put D2 B) == put err B expand by: op get _ : B -> D reduced to: true nf: err ----------------------------------------- result: true c-rewrite time: 135ms parse time: 12ms ========================================== close ========================================== ***> now assert the lemmas: ========================================== bth 1BUFFL ========================================== ***> stream + 1-buffer behaviorally refines stream ========================================== bth P ========================================== The cobasis for sort P is: op head _ : P -> D op cons : D P -> P op tail _ : P -> P ========================================== open ========================================== reduce in P : (head cons(D , < S , b >)) == D result Bool: true rewrite time: 3ms parse time: 15ms ========================================== reduce in P : (tail cons(D , < S , b >)) == (< S , b >) result Bool: true rewrite time: 6ms parse time: 38ms ========================================== close ========================================== ***> two 1-buffers behaviorally refine a 1-cell ========================================== bth P Warning: redefining module P ========================================== The cobasis for sort P is: op get _ : P -> D op f _ : P -> P op p1 _ _ : D P -> P op put _ _ : D P -> P ========================================== reduce in P : (get (put D (< B1 , B2 >))) == D result Bool: true rewrite time: 5ms parse time: 15ms ========================================== bth 2CELL ========================================== The cobasis for sort C is: op get _ : C -> D op put _ _ : D C -> C ========================================== ***> two 1-buffers behaviorally refine one 2-cell ========================================== bth P Warning: redefining module P ========================================== reduce in P : (get (put D1 (put D2 (< B1 , B2 >)))) == D2 result Bool: true rewrite time: 19ms parse time: 47ms ========================================== ***> stream + two 1-buffers behaviorally refine stream ========================================== bth P Warning: redefining module P ========================================== The cobasis for sort P is: op head _ : P -> D op tail _ : P -> P op cons : D P -> P ========================================== open ========================================== reduce in P : (head cons(D , < S , B1 , B2 >)) == D result Bool: true rewrite time: 4ms parse time: 17ms ========================================== reduce in P : (tail cons(D , < S , b1 , b2 >)) == (< S , b1 , b2 >) result Bool: true rewrite time: 18ms parse time: 61ms ========================================== close ========================================== ***> check that the behavioral lemma is really needed above: ========================================== bth P Warning: redefining module P ========================================== ***> the second reduction should be false: ========================================== reduce in P : (head cons(D , < S , B1 , B2 >)) == D result Bool: true rewrite time: 29ms parse time: 15ms ========================================== reduce in P : (tail cons(D , < S , B1 , B2 >)) == (< S , B1 , B2 >) result Bool: false LHS sort P: < S , (put (get B1) nil) , (put (get B2) nil) > RHS sort P: < S , B1 , B2 > rewrite time: 59ms parse time: 69ms ========================================== ***> let BOBJ find the lemma itself: ========================================== c-reduce in P : (tail cons(D , < S , B1 , B2 >)) == (< S , B1 , B2 >) using cobasis for P: op head _ : P -> D op tail _ : P -> P op cons : D P -> P --------------------------------------- reduced to: < S , (put (get B1) nil) , (put (get B2) nil) > == < S , B1 , B2 > ----------------------------------------- add rule (C1) : < S , (put (get B1) nil) , (put (get B2) nil) > = < S , B1 , B2 > ----------------------------------------- target is: < S , (put (get B1) nil) , (put (get B2) nil) > == < S , B1 , B2 > expand by: op head _ : P -> D reduced to: true nf: get B2 ----------------------------------------- target is: < S , (put (get B1) nil) , (put (get B2) nil) > == < S , B1 , B2 > expand by: op tail _ : P -> P reduced to: true nf: < (tail S) , (put (head S) nil) , (put (get B1) nil) > ----------------------------------------- target is: < S , (put (get B1) nil) , (put (get B2) nil) > == < S , B1 , B2 > expand by: op cons : D P -> P reduced to: true nf: < cons(get B1 , S) , (put (get B2) nil) , (put ~sysvar~D-1 nil) > ----------------------------------------- result: true c-rewrite time: 167ms parse time: 58ms ========================================== ***> three 1-buffers refine a 1-cell ========================================== bth P Warning: redefining module P ========================================== The cobasis for sort P is: op get _ : P -> D op put _ _ : D P -> P op p1 _ _ : D P -> P op f1 _ : P -> P op f2 _ : P -> P ========================================== reduce in P : (get (put D (< B1 , B2 , B3 >))) == D result Bool: true rewrite time: 19ms parse time: 17ms ========================================== bth 2BUFF ========================================== The cobasis for sort B is: op ok? _ : B -> Bool op get _ : B -> D op put _ _ : D B -> B op sft _ : B -> B ========================================== ***> the following should be false: ========================================== c-reduce in 2BUFF : (put (get B) nil) == B using cobasis for 2BUFF: op ok? _ : B -> Bool op get _ : B -> D op put _ _ : D B -> B op sft _ : B -> B --------------------------------------- reduced to: put (get B) nil == B ----------------------------------------- add rule (C1) : put (get B) nil = B ----------------------------------------- target is: put (get B) nil == B expand by: op ok? _ : B -> Bool reduced to: false == ok? B ----------------------------------------- result: false c-rewrite time: 21ms parse time: 5ms ========================================== ***> but the following should be true: ========================================== open ========================================== c-reduce in 2BUFF : (put (get (sft b)) (sft (put (get b) nil))) == b using cobasis for 2BUFF: op ok? _ : B -> Bool op get _ : B -> D op put _ _ : D B -> B op sft _ : B -> B --------------------------------------- reduced to: put (get (sft b)) (sft (put (get b) nil)) == b ----------------------------------------- add rule (C1) : put (get (sft b)) (sft (put (get b) nil)) = b ----------------------------------------- target is: put (get (sft b)) (sft (put (get b) nil)) == b expand by: op ok? _ : B -> Bool reduced to: true nf: false ----------------------------------------- target is: put (get (sft b)) (sft (put (get b) nil)) == b expand by: op get _ : B -> D reduced to: true nf: get b ----------------------------------------- target is: put (get (sft b)) (sft (put (get b) nil)) == b expand by: op put _ _ : D B -> B reduced to: put err (sft (put (get b) nil)) == put err b ----------------------------------------- target is: put (get (sft b)) (sft (put (get b) nil)) == b expand by: op sft _ : B -> B reduced to: sft (put (get (sft b)) nil) == sft b ----------------------------------------- add rule (C2) : put err (sft (put (get b) nil)) = put err b ----------------------------------------- add rule (C3) : sft (put (get (sft b)) nil) = sft b ----------------------------------------- target is: put err (sft (put (get b) nil)) == put err b expand by: op ok? _ : B -> Bool reduced to: true nf: false ----------------------------------------- target is: put err (sft (put (get b) nil)) == put err b expand by: op get _ : B -> D reduced to: true nf: err ----------------------------------------- target is: put err (sft (put (get b) nil)) == put err b expand by: op put _ _ : D B -> B deduced using (C2) : true nf: put err b ----------------------------------------- target is: put err (sft (put (get b) nil)) == put err b expand by: op sft _ : B -> B reduced to: sft (put err nil) == sft (put err b) ----------------------------------------- add rule (C4) : sft (put err nil) = sft (put err b) ----------------------------------------- target is: sft (put (get (sft b)) nil) == sft b expand by: op ok? _ : B -> Bool reduced to: true nf: true ----------------------------------------- target is: sft (put (get (sft b)) nil) == sft b expand by: op get _ : B -> D reduced to: true nf: get (sft b) ----------------------------------------- target is: sft (put (get (sft b)) nil) == sft b expand by: op put _ _ : D B -> B reduced to: put ~sysvar~D-1 (sft (put (get (sft b)) nil)) == put ~sysvar~D-1 (sft b) ----------------------------------------- target is: sft (put (get (sft b)) nil) == sft b expand by: op sft _ : B -> B reduced to: true nf: nil ----------------------------------------- add rule (C5) : put ~sysvar~D-1 (sft (put (get (sft b)) nil)) = put ~sysvar~D-1 (sft b) ----------------------------------------- target is: sft (put err nil) == sft (put err b) expand by: op ok? _ : B -> Bool reduced to: true nf: true ----------------------------------------- target is: sft (put err nil) == sft (put err b) expand by: op get _ : B -> D reduced to: true nf: err ----------------------------------------- target is: sft (put err nil) == sft (put err b) expand by: op put _ _ : D B -> B reduced to: put ~sysvar~D-2 (sft (put err nil)) == put ~sysvar~D-2 (sft (put err b)) ----------------------------------------- target is: sft (put err nil) == sft (put err b) expand by: op sft _ : B -> B reduced to: true nf: nil ----------------------------------------- add rule (C6) : put ~sysvar~D-2 (sft (put err nil)) = put ~sysvar~D-2 (sft (put err b)) ----------------------------------------- target is: put ~sysvar~D-1 (sft (put (get (sft b)) nil)) == put ~sysvar~D-1 (sft b) expand by: op ok? _ : B -> Bool reduced to: true nf: false ----------------------------------------- target is: put ~sysvar~D-1 (sft (put (get (sft b)) nil)) == put ~sysvar~D-1 (sft b) expand by: op get _ : B -> D reduced to: true nf: get (sft b) ----------------------------------------- target is: put ~sysvar~D-1 (sft (put (get (sft b)) nil)) == put ~sysvar~D-1 (sft b) expand by: op put _ _ : D B -> B deduced using (C5) : true nf: put err (sft b) ----------------------------------------- target is: put ~sysvar~D-1 (sft (put (get (sft b)) nil)) == put ~sysvar~D-1 (sft b) expand by: op sft _ : B -> B reduced to: true nf: sft (put ~sysvar~D-1 nil) ----------------------------------------- target is: put ~sysvar~D-2 (sft (put err nil)) == put ~sysvar~D-2 (sft (put err b)) expand by: op ok? _ : B -> Bool reduced to: true nf: false ----------------------------------------- target is: put ~sysvar~D-2 (sft (put err nil)) == put ~sysvar~D-2 (sft (put err b)) expand by: op get _ : B -> D reduced to: true nf: err ----------------------------------------- target is: put ~sysvar~D-2 (sft (put err nil)) == put ~sysvar~D-2 (sft (put err b)) expand by: op put _ _ : D B -> B deduced using (C6) : true nf: put err (sft (put err b)) ----------------------------------------- target is: put ~sysvar~D-2 (sft (put err nil)) == put ~sysvar~D-2 (sft (put err b)) expand by: op sft _ : B -> B reduced to: true nf: sft (put ~sysvar~D-2 nil) ----------------------------------------- result: true c-rewrite time: 462ms parse time: 13ms ========================================== ***> there are three circularities in this proof! ========================================== close ========================================== ***> two 1-buffers behaviorally refine a 2-buffer ========================================== bth P Warning: redefining module P ========================================== The cobasis for sort P is: op ok? _ : P -> Bool op get _ : P -> D op put _ _ : D P -> P op sft _ : P -> P ========================================== ***> prove the equations of 2B: ========================================== ***> first the key equation in 2 cases, & check another equation in 2nd case ========================================== open ========================================== reduce in P : (get (sft (put D (< b1 , b2 >)))) == D result Bool: true rewrite time: 23ms parse time: 20ms ========================================== close ========================================== open ========================================== reduce in P : (get (sft (put D (< b1 , b2 >)))) == err result Bool: true rewrite time: 41ms parse time: 22ms ========================================== c-reduce in P : (put D (< b1 , b2 >)) == (put err (< b1 , b2 >)) using cobasis for P: op ok? _ : P -> Bool op get _ : P -> D op put _ _ : D P -> P op sft _ : P -> P --------------------------------------- result: true c-rewrite time: 2ms parse time: 37ms ========================================== close ========================================== reduce in P : (sft 2nil) == 2nil result Bool: true rewrite time: 1ms parse time: 5ms ========================================== reduce in P : (sft (sft (< B1 , B2 >))) == 2nil result Bool: true rewrite time: 2ms parse time: 14ms ========================================== reduce in P : (ok? 2nil) == true result Bool: true rewrite time: 11ms parse time: 33ms ========================================== reduce in P : (ok? (sft (< B1 , B2 >))) == true result Bool: true rewrite time: 8ms parse time: 12ms ========================================== reduce in P : (ok? (put D (< B1 , B2 >))) == false result Bool: true rewrite time: 2ms parse time: 12ms ========================================== reduce in P : (sft (put D (sft (< B1 , B2 >)))) == (sft (put D 2nil)) result Bool: true rewrite time: 17ms parse time: 62ms ========================================== reduce in P : (put err (put D (< B1 , B2 >))) == (put err (< B1 , B2 >)) result Bool: true rewrite time: 18ms parse time: 81ms ========================================== reduce in P : (get (put err (< B1 , B2 >))) == err result Bool: true rewrite time: 2ms parse time: 13ms ========================================== reduce in P : (get 2nil) == err result Bool: true rewrite time: 1ms parse time: 4ms ========================================== reduce in P : (get (put D 2nil)) == err result Bool: true rewrite time: 3ms parse time: 7ms ========================================== reduce in P : (get (put D (sft (< B1 , B2 >)))) == (get (sft (< B1 , B2 >))) result Bool: true rewrite time: 16ms parse time: 140ms BOBJ> q Bye. awk%
To BOBJ examples homepage
To Tatami project homepage
Maintained by Joseph Goguen
Last modified: Sun Mar 19 18:24:33 PST 2000