class BOUNDED_QUEUE [T] creation make feature buffer : ARRAY [T] in_count : INTEGER out_count : INTEGER capacity : INTEGER make(size : INTEGER) is do in_count := 1 out_count := 1 capacity := size !!buffer.make(1, size) end get : T is require not empty do Result := buffer @ (out_count \\ capacity) out_count := out_count + 1 ensure not full end put(x : T) is require not full do buffer.put(x, in_count \\ capacity) in_count := in_count + 1 ensure not empty end full : BOOLEAN is do Result := (in_count = out_count + capacity) end empty : BOOLEAN is do Result := (in_count = out_count) end end -- class BOUNDED_QUEUE