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.

### 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 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