Fun and Games with Streams and Cells
Fun with Streams and Cells
We prove properties of some simple combinations of streams and cells, with the
intention of later developing this theory further in the direction of
communication protocols. We use a simple notion of cell, where writing a new
datum simply overwrites the existing datum; these cells start with some
unknown (nondeterministic) value. Everything goes nicely, including some
checks that behavioral lemmas are really necessary for some proofs to work,
and that ordinary behavioral rewriting will not suffice. Note that although
several of these proofs are behavioral refinement proofs, we did not bother to
change the cobasis to that of the source theory, because the proofs go through
without doing so. As usual, after giving the BOBJ source code, we show its
output.
1. BOBJ Source Code
<![CDATA[
*** file: sandc.bob
***> fun with streams and cells
set trace on
*** the 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 1CELL is sort C . pr DATA .
op put__ : D C -> C .
op get_ : C -> D .
var D : D . var C : C .
eq get (put D C) = D .
end
show cobasis .
***> stream behaviorally refines 1-cell
*** (of course this is trivial)
select STREAM .
op get_ : S -> D .
eq get S = head S .
op put__ : D S -> S .
eq put D S = cons(D,S) .
red get (put D S) == D .
***> thus infinite stream is a model for 1-cell
***> a 1-cell lemma
select 1CELL .
***> first show the lemma is not strictly satisfied
red (put (get C) (put D C)) == C .
cred (put (get C) (put D C)) == C .
*** assert the lemma:
bth 1CELLL is pr 1CELL .
var D : D . var C : C .
eq put (get C) (put D C) = C .
end
***> stream + 1-cell behaviorally refines stream
bth P is pr (STREAM || 1CELLL) * (sort Tuple to P).
op cons : D P -> P .
op head_ : P -> D .
op tail_ : P -> P .
var D : D . var S : S . var C : C .
eq cons(D, < S, C >) = < cons(get C, S), put D C > .
eq head < S, C > = get C .
eq tail < S, C > = < tail S, put head S C > .
end
*** note the slightly clever definition for cons and tail
red head cons(D, < S, C >) == D .
red tail cons(D, < S, C >) == < S, C > .
***> check that the behavioral lemma is really needed above:
bth P is pr (STREAM || 1CELL) * (sort Tuple to P).
op cons : D P -> P .
op head_ : P -> D .
op tail_ : P -> P .
var D : D . var S : S . var C : C .
eq cons(D, < S, C >) = < cons(get C, S), put D C > .
eq head < S, C > = get C .
eq tail < S, C > = < tail S, put head S C > .
end
show cobasis .
***> the second reduction should be false:
red head cons(D, < S, C >) == D .
red tail cons(D, < S, C >) == < S, C > .
*** without the lemma, the following overflows:
*** cred tail cons(D, < S, C >) == < S, C > .
***> two 1-cells behaviorally refine one 1-cell
bth P is pr (1CELLL || 1CELLL) * (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 C1 C2 : C .
eq p1 D < C1, C2 > = < (put D C1), C2 > .
eq f < C1, C2 > = < C1, put (get C1) C2 > .
eq get < C1, C2 > = get C2 .
eq put D < C1, C2 > = f(p1 D < C1, C2 >).
end
*** uses action-like abbreviating notation
show cobasis .
red get (put D < C1, C2 >) == D .
ops c1 c2 : -> C . op d : -> D .
red get (put d < c1, c2 >) == 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-cells behaviorally refine one 2-cell
bth P is pr (1CELLL || 1CELLL) * (sort Tuple to P).
op get_ : P -> D .
op put__ : D P -> P .
vars D D1 D2 : D . vars C1 C2 : C .
eq put D < C1, C2 > = < put D C1, (put (get C1) C2) > .
eq get < C1, C2 > = get C2 .
end
red get(put D1 (put D2 < C1, C2 >)) == D2 .
***> stream + two 1-cells behaviorally refine stream
bth P is pr (STREAM || 1CELLL || 1CELLL) * (sort Tuple to P).
op head_ : P -> D .
op tail_ : P -> P .
op cons : D P -> P .
var D : D . var S : S . vars C1 C2 : C .
eq cons(D, < S, C1, C2 >) = < cons(get C1,S), (put(get C2) C1), put D C2 > .
eq head < S, C1, C2 > = get C2 .
eq tail < S, C1, C2 > = < tail S, put (head S) C1, put (get C1) C2 > .
end
*** closer to a sender-channel-receiver communication system
show cobasis .
red head cons(D, < S, C1, C2 >) == D .
red tail cons(D, < S, C1, C2 >) == < S, C1, C2 > .
***> check that the behavioral lemma is really needed above:
bth P is pr (STREAM || 1CELL || 1CELL) * (sort Tuple to P).
op head_ : P -> D .
op tail_ : P -> P .
op cons : D P -> P .
var D : D . var S : S . vars C1 C2 : C .
eq cons(D, < S, C1, C2 >) = < cons(get C1,S), (put(get C2) C1), put D C2 > .
eq head < S, C1, C2 > = get C2 .
eq tail < S, C1, C2 > = < tail S, put (head S) C1, put (get C1) C2 > .
end
***> the second reduction should be false:
red head cons(D, < S, C1, C2 >) == D .
red tail cons(D, < S, C1, C2 >) == < S, C1, C2 > .
*** without the lemma, the following overflows
*** cred tail cons(D, < S, C1, C2 >) == < S, C1, C2 > .
***> three 1-cells refine one 1-cell
bth P is pr (1CELL || 1CELL || 1CELL) * (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 C1 C2 C3 : C .
eq p1 D < C1, C2, C3 > = < (put D C1), C2, C3 > .
eq f1 < C1, C2, C3 > = < C1, (put get C1 C2), C3 > .
eq f2 < C1, C2, C3 > = < C1, C2, (put get C2 C3) > .
eq put D < C1, C2, C3 > = f2 f1 (p1 D < C1, C2, C3 >).
eq get < C1, C2, C3 > = get C3 .
end
*** action-like abbreviations used again
show cobasis .
red get (put D < C1, C2, C3 >) == D .
]]>
2. BOBJ Output
<![CDATA[
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 10:19:05 PST 2000
BOBJ> in sandc
==========================================
***> fun with streams and cells
==========================================
th DATA
==========================================
bth STREAM
==========================================
The cobasis for sort S is:
op head _ : S -> D
op tail _ : S -> S
==========================================
bth 1CELL
==========================================
The cobasis for sort C is:
op get _ : C -> D
==========================================
***> stream behaviorally refines 1-cell
==========================================
select STREAM
==========================================
opening module STREAM.
==========================================
reduce in STREAM : (get (put D S)) == D
result Bool: true
rewrite time: 56ms parse time: 10ms
==========================================
***> thus infinite stream is a model for 1-cell
==========================================
***> a 1-cell lemma
==========================================
select 1CELL
==========================================
***> first show the lemma is not strictly satisfied
==========================================
reduce in 1CELL : (put (get C) (put D C)) == C
result Bool: false
LHS sort C: put (get C) (put D C)
RHS sort C: C
rewrite time: 3ms parse time: 13ms
==========================================
c-reduce in 1CELL : (put (get C) (put D C)) == C
using cobasis for 1CELL:
op get _ : C -> D
---------------------------------------
reduced to: put (get C) (put D C) == C
-----------------------------------------
add rule (C1) : put (get C) (put D C) = C
-----------------------------------------
target is: put (get C) (put D C) == C
expand by: op get _ : C -> D
reduced to: true
nf: get C
-----------------------------------------
result: true
c-rewrite time: 241ms parse time: 49ms
==========================================
bth 1CELLL
==========================================
***> stream + 1-cell behaviorally refines stream
==========================================
bth P
==========================================
reduce in P : (head cons(D , < S , C >)) == D
result Bool: true
rewrite time: 28ms parse time: 13ms
==========================================
reduce in P : (tail cons(D , < S , C >)) == (< S , C >)
result Bool: true
rewrite time: 17ms parse time: 32ms
==========================================
***> check that the behavioral lemma is really needed above:
==========================================
bth P
Warning: redefining module P
==========================================
The cobasis for sort P is:
op head _ : P -> D
op cons : D P -> P
op tail _ : P -> P
==========================================
***> the second reduction should be false:
==========================================
reduce in P : (head cons(D , < S , C >)) == D
result Bool: true
rewrite time: 1ms parse time: 13ms
==========================================
reduce in P : (tail cons(D , < S , C >)) == (< S , C >)
result Bool: false
LHS sort P: < S , (put (get C) (put D C)) >
RHS sort P: < S , C >
rewrite time: 47ms parse time: 57ms
==========================================
***> two 1-cells behaviorally refine one 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 (< C1 , C2 >))) == D
result Bool: true
rewrite time: 4ms parse time: 14ms
==========================================
opening module P.
==========================================
reduce in P : (get (put d (< c1 , c2 >))) == d
result Bool: true
rewrite time: 4ms parse time: 16ms
==========================================
bth 2CELL
==========================================
The cobasis for sort C is:
op get _ : C -> D
op put _ _ : D C -> C
==========================================
***> two 1-cells behaviorally refine one 2-cell
==========================================
bth P
Warning: redefining module P
==========================================
reduce in P : (get (put D1 (put D2 (< C1 , C2 >)))) == D2
result Bool: true
rewrite time: 17ms parse time: 31ms
==========================================
***> stream + two 1-cells 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
==========================================
reduce in P : (head cons(D , < S , C1 , C2 >)) == D
result Bool: true
rewrite time: 15ms parse time: 13ms
==========================================
reduce in P : (tail cons(D , < S , C1 , C2 >)) == (< S , C1 , C2 >)
result Bool: true
rewrite time: 18ms parse time: 50ms
==========================================
***> 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 , C1 , C2 >)) == D
result Bool: true
rewrite time: 15ms parse time: 13ms
==========================================
reduce in P : (tail cons(D , < S , C1 , C2 >)) == (< S , C1 , C2 >)
result Bool: false
LHS sort P: < S , (put (get C1) (put (get C2) C1)) , (put (get C2) (put D
C2)) >
RHS sort P: < S , C1 , C2 >
rewrite time: 59ms parse time: 60ms
==========================================
***> three 1-cells refine one 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 (< C1 , C2 , C3 >))) == D
result Bool: true
rewrite time: 18ms parse time: 15ms
BOBJ> q
Bye.
awk%
]]>
To BOBJ examples homepage
To Tatami project homepage
Maintained by Joseph Goguen
Last modified: Sun Mar 19 18:09:40 PST 2000