/** * -- Add `c' to `children'. */ public void add_child(Composite c) { // require // c_different: c /= Current // c_singleton_1: c.parent = Void // c_singleton_2: c.children.is_empty boolean c_different = c != this; boolean c_singleton_1 = c.parent == null; boolean c_singleton_2 = c.children.isEmpty(); if (!c_different || !c_singleton_1 || !c_singleton_2) throw new IllegalArgumentException(); int old_c_value = c.value; Set<Composite> old_children_set = children_set(); Set<Composite> old_ancestors = new HashSet<>(ancestors); // do lemma_ancestors_have_children(c); assert (c.invariant()); assert (!ancestors.contains(c)); c.set_parent(this); children.add(c); update(c); // ensure // child_added: children.has (c) // c_value_unchanged: c.value = old c.value // c_children_unchanged: c.children_set = old c.children_set // ancestors_unchanged: ancestors = old ancestors boolean child_added = children.contains(c); boolean c_value_unchanged = old_c_value == c.value; boolean ancestors_unchanged = old_ancestors.equals(ancestors); assert (child_added && c_value_unchanged && ancestors_unchanged); }// ancestors_unchangedassert(old_this.ancestors == this.ancestors);// child_addedassert(ExpressionEvaluator.evaluateSetMembership(c,"this . children",this));// othersassert(this.value >= old_this.value); assert(old_this.children != this.children); assert(ExpressionEvaluator.evaluateQuantifiedExpression("all","this . * parent","n !in n . ^ parent",this)); assert(ExpressionEvaluator.evaluateQuantifiedExpression("all","this . * parent","!(n . parent != null) || n . value <= n . parent . value",this)); assert(old_this.parent == this.parent);