/** * -- Number of items in buffer. */ public int count() { // do if (free > start) return free - start; else return data_size() - start + free; // ensure // definition: Result = sequence.count }
// othersassert(result != old_this.start + old_this.free);assert(result != old_this.free - 1 - this.start - 1 - result + this.start - old_this.free + this.start);assert(result != old_this.free - 1 - this.start);assert(old_this.capacity_ > old_this.start - 1 - result);assert(result != old_this.free - 1 - this.start - 1);assert(old_this.data == this.data);assert(old_this.data.size != result);assert(old_this.capacity_ == this.capacity_);assert(this.data.size != result);assert(old_this.free == this.free);assert(old_this.start == this.start);
/** * -- Add `a_value' to end of buffer. */ public void extend(G a_value) { // require // not_full: not is_full boolean not_full = !is_full(); assert (not_full);
// do data.add(a_value); if (free == data_count()) free = 1; else free = free + 1; // ensure // definition: sequence = old sequence.extended (a_value) assert (data.contains(a_value)); }
// valude addedassert(ExpressionEvaluator.evaluateSetMembership(a_value,"this . data",this));// othersassert(old_this.data != this.data); assert(old_this.start == this.start);assert(old_this.capacity_ == this.capacity_);assert(old_this.free != this.free + 1); assert(old_this.free != this.free + 1 + this.start); assert(old_this.free != this.free);
/** * -- Current item of buffer. */ public Object item() { // require // not_empty: not is_empty boolean not_empty = !is_empty(); assert (not_empty);
// do Object result = data.get(start);
// ensure // definition: Result = sequence.first assert (result == data.get(start)); return result; }
// othersassert(old_this.data == this.data); assert(old_this.capacity_ == this.capacity_); assert(old_this.start == this.start); assert(old_this.free == this.free);
/** * -- Remove current item from buffer. */ public void remove() { // require // not_empty: not is_empty boolean not_empty = !is_empty(); assert (not_empty);
// do if (start == data_count()) start = 1; else start++;
// ensure // definition: sequence = old sequence.but_first }
// othersassert(old_this.start != this.start + this.free); assert(old_this.capacity_ != this.capacity_ + this.start); assert(old_this.data == this.data); assert(old_this.free == this.free); assert(old_this.start != this.start); assert(old_this.capacity_ == this.capacity_); /** * -- Remove all elements from buffer. */ public void wipe_out() { // do start = free;
// ensure // empty: is_empty boolean empty = is_empty(); assert (empty); }
// is_emptyassert(this.free == this.start);// othersassert(old_this.capacity_ == this.capacity_); assert(old_this.data == this.data);