/** * -- Number of elements in map. */ public int count() { // do int result = keys.size();
// ensure // Result = keys.sequence.count assert (result == keys.size()); return result; }
// result okassert(this.data.size() == result);// othersassert(old_this.keys == this.keys); assert(old_this.data == this.data);
/** * -- Extend map with key `k' mapped to `v'. Returns index of key `k' (ghost value). */ public int extend(K k, V v) { // do int result = index_of_key(k); if (result >= 0) { data.set(result, v); } else { keys.add(k); data.add(v); result = keys.size() - 1; }
// ensure // key_set: keys.sequence[Result] = k // data_set: data.sequence[Result] = v // other_keys_unchanged: keys.sequence.interval (1, Result-1) = old keys.sequence.interval (1, // Result-1) // other_keys_unchanged: keys.sequence.interval (Result+1, keys.sequence.count) = old // keys.sequence.interval (Result+1, keys.sequence.count) // other_data_unchanged: data.sequence.interval (1, Result-1) = old data.sequence.interval (1, // Result-1) // other_data_unchanged: data.sequence.interval (Result+1, data.sequence.count) = old // data.sequence.interval (Result+1, data.sequence.count) boolean key_set = keys.get(result) == k; boolean data_set = data.get(result) == v; assert (key_set && data_set); return result;}// key_setassert(ExpressionEvaluator.evaluateSetMembership(k,"this . keys",this)); // data_setassert(ExpressionEvaluator.evaluateSetMembership(v,"this . data",this)); // othersassert(this.keys.size != result); /** * -- Remove element mapped to `k'. Returns index of removed key `k' (ghost value). */ public int remove(K k) { // require // has_key (k) // not_empty: count > 0 boolean has_key = has_key(k); boolean not_empty = count() > 0; if (!has_key) throw new IllegalArgumentException(); if (!not_empty) throw new IllegalStateException();
// do int result = index_of_key(k); keys.remove(result); data.remove(result);
// ensure // result_is_index: old keys.sequence[Result] = k // key_removed: not keys.sequence.has (k) // other_keys_unchanged: keys.sequence.interval (1, Result-1) = old keys.sequence.interval (1, // Result-1) // other_keys_unchanged: keys.sequence.interval (Result, keys.sequence.count) = old // keys.sequence.interval (Result+1, keys.sequence.count+1) // other_data_unchanged: data.sequence.interval (1, Result-1) = old data.sequence.interval (1, // Result-1) // other_data_unchanged: data.sequence.interval (Result, data.sequence.count) = old // data.sequence.interval (Result+1, data.sequence.count+1) boolean key_removed = !keys.contains(k); assert (key_removed); return result; }
// key_removedassert(!ExpressionEvaluator.evaluateSetMembership(k,"this . keys",this)); // othersassert(this.data.size != result);assert(this.data != null); assert(this.keys != null);