Go backward to
Behavior Descriptions
Go up to
Top
Go forward to
Summation
Bounded Buffer
C
(n)
C
(n)
:=
C
^
C
^...^
C
Behaves as bounded buffer of capacity
n
.
C
(n)
=
Buff
n
Specification
Buff
n
(
s
)
Buff
n
< > :=
in
(
x
).
Buff
n
<
x
>
Buff
n
<
v
1
,...,v
n
> :=
out
(
v
n
).
Buff
n
<
v
1
,...,v
n-1
>
Buff
n
<
v
1
,...,v
k
> :=
in
(
x
).
Buff
n
<
x,v
1
,...,v
k
>
+
out
(
v
k
).
Buff
n
<
v
1
,...,v
k-1
>(
0 < k < n
)
C
(n)
=
Buff
n
< >
Author:
Wolfgang Schreiner
Last Modification: June 8, 1998
