class Buffer

instance variables

data : [nat] := nil

operations

public Buffer: () ==> Buffer
Buffer() == 
 data := nil;

public Write: nat ==> ()
Write(newData) ==
  (IO`print("Writer wrote: "); IO`print(newData); IO`print("\n");
   data := newData;
  );

public Read: () ==> nat
Read() ==
  let oldData : nat = data
  in
    (IO`print("Reader read: "); IO`print(oldData); IO`print("\n");
     data := nil;     
     return oldData;
    );

public IsFinished: () ==> ()
IsFinished() == skip;

sync

per Write => #fin(Read) = #fin(Write);
per Read => (#fin(Read) + 1) = #fin(Write);
--per Write => data = nil;
--per Read => data <> nil;
per IsFinished => #fin(Read) = 3;


end Buffer