/** * -- Insert node `n' to the right of the current node. */ public void insert_right(DoublyLinkedListNode n) { // require // n_singleton: n.left = n boolean n_singleton = n.left == n; if (!n_singleton) { throw new IllegalArgumentException(); } // do DoublyLinkedListNode r = right; n.setRight(r); n.setLeft(this); r.setLeft(n); setRight(n); // ensure // n_left_set: right = n // n_right_set: n.right = old right boolean n_left_set = right == n; boolean n_right_set = n.right == r; assert (n_left_set && n_right_set); }// n_left_setassert(n == this.right);// othersassert(ExpressionEvaluator.evaluateQuantifiedExpression("all","this . * left + right","n in n . ^ left",this)); assert(ExpressionEvaluator.evaluateQuantifiedExpression("all","this . * left + right","n in n . ^ right",this)); /** * -- Remove the current node from the list. */ public void remove() { // do DoublyLinkedListNode l = left; DoublyLinkedListNode r = right; setLeft(this); setRight(this); l.setRight(r); r.setLeft(l); // ensure // singleton: right = Current // neighbors_connected: (old left).right = old right boolean singleton = right == this; boolean neighbors_connected = l.right == r; assert (singleton && neighbors_connected); }// singletonassert(old_this.right.left == this.left); assert(old_this.left.right == this.right);