00001 00005 package edu.mit.csail.sdg.squander.examples.list.func2; 00006 00007 import edu.mit.csail.sdg.annotations.Ensures; 00008 import edu.mit.csail.sdg.annotations.Returns; 00009 import edu.mit.csail.sdg.annotations.SpecField; 00010 import edu.mit.csail.sdg.squander.Squander; 00011 00017 @SpecField({ 00018 "size : one int", 00019 "keys : int -> int" 00020 }) 00021 public abstract class IntList { 00022 00023 @Returns("this.size") 00024 public final int size() { return Squander.exe(this); } 00025 00026 @Returns("this.keys[idx]") 00027 public final int get(int idx) { return Squander.exe(this, idx); } 00028 00029 @Ensures("return.keys[0] = this.keys[startIdx] && return.size = this.size - startIdx") 00030 public final IntList sublist(int startIdx) { return Squander.exe(this, startIdx); } 00031 00032 public static void main(String[] args) { 00033 IntList lst = new Nil(); 00034 int[] elems = new int[] {7, 2, 4, 5, 8, 4}; 00035 for (int k : elems) { 00036 lst = new Cons(k, lst); 00037 } 00038 System.out.println(lst); 00039 System.out.println(lst.size()); 00040 } 00041 00042 }