Lab for Automated Reasoning and Analysis LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

sizelist.java [2009/01/30 13:07] (current)
wies created
Line 1: Line 1:
 +====== Insertion and Removal from a List with Size Field ======
  
 +<code java>
 +class Node {
 +   ​public /*: claimedby SizeList */ Node next;
 +}
 +
 +class SizeList {
 +   ​private static Node root;
 +   ​private static int size;
 +   /*:
 +     ​public static specvar content :: objset;
 +     ​vardefs "​content == {n. n ~= null & (root,n) : {(u,v). u..next=v}^*}";​
 +     ​invariant sizeInv: "size = cardinality content";​
 +     ​invariant treeInv: "tree [next]";​
 +     ​invariant rootInv: "root ~= null --> (ALL n. n..next ~= root)";​
 +     ​invariant noNextInv: "ALL x. x ~= null & x ~: content --> x..next = null";
 +
 +   */
 +
 +   ​public static void add(Node x)
 +   /*: requires "x ~= null & x ~: content"​
 +       ​modifies content
 +       ​ensures "​content = old content Un {x}" */
 +   {
 +      x.next = root;
 +      root = x;
 +      size = size + 1;
 +   }
 +
 +   ​public static void remove(Node x)
 +   /*: requires "x : content"​
 +       ​modifies content
 +       ​ensures "​content = old content - {x}"
 +   */
 +   {
 +      Node e = root;
 +      Node prev = null;
 +      while (e != x) {
 +         prev = e;
 +         e = e.next;
 +      }
 +      if (prev == null) {
 +         root = e.next;
 +      } else {
 +         ​prev.next = e.next;
 +      }
 +      e.next = null;
 +      size = size - 1;
 +   }
 +}
 +</​code>​
 
sizelist.java.txt · Last modified: 2009/01/30 13:07 by wies