00001
00005 package edu.mit.csail.sdg.squander.examples.equiv;
00006
00007 import java.util.Arrays;
00008
00009 import edu.mit.csail.sdg.annotations.Ensures;
00010 import edu.mit.csail.sdg.annotations.SpecField;
00011 import edu.mit.csail.sdg.squander.Squander;
00012 import edu.mit.csail.sdg.squander.annotations.Fresh;
00013 import edu.mit.csail.sdg.squander.annotations.FreshObjects;
00014
00020 @SpecField("equiv : set Object from Node.left, Node.right | " +
00021 " this.equiv = {x : Node | (this.value = x.value) && " +
00022 " (this.left -> x.left in equiv + null -> null) && " +
00023 " (this.right -> x.right in equiv + null -> null)" +
00024 "}")
00025 public class Node {
00026
00027 int value;
00028 Node left;
00029 Node right;
00030
00031 public Node(int value) {
00032 this.value = value;
00033 }
00034
00035 @Ensures("return[int] = this.equiv && return.length = #this.equiv")
00036 @Fresh({@FreshObjects(cls = Node[].class, num = 1)})
00037 public Node[] getEquiv(Node n1, Node n2) {
00038 return Squander.exe(this, new Class[] {Node.class, Node.class}, new Object[] {n1, n2});
00039 }
00040
00041 @Override
00042 public String toString() {
00043 return String.format("%d: (v=%d, l=%d, r=%d)", System.identityHashCode(this), value,
00044 System.identityHashCode(left), System.identityHashCode(right));
00045 }
00046
00047 public static void main(String[] args) {
00048 Node n11 = new Node(2);
00049 Node n12 = new Node(1);
00050 Node n13 = new Node(3);
00051 n11.left = n12;
00052 n11.right = n13;
00053
00054 Node n21 = new Node(2);
00055 Node n22 = new Node(1);
00056 Node n23 = new Node(3);
00057 n21.left = n22;
00058 n21.right = n23;
00059
00060 Node n31 = new Node(2);
00061 Node n32 = new Node(1);
00062 Node n33 = new Node(3);
00063 n31.left = n32;
00064 n32.left = n33;
00065
00066 System.out.println(Arrays.toString(n11.getEquiv(n21, n31)));
00067 System.out.println(System.identityHashCode(n11));
00068 System.out.println(System.identityHashCode(n21));
00069 System.out.println(System.identityHashCode(n31));
00070 }
00071
00072 }