00001
00005 package edu.mit.csail.sdg.squander.examples.list.func;
00006
00007 import edu.mit.csail.sdg.annotations.Returns;
00008 import edu.mit.csail.sdg.annotations.SpecField;
00009 import edu.mit.csail.sdg.squander.Squander;
00010
00016 @SpecField({
00017 "next : one List",
00018 "size : one int | this.next == null ? this.size = 1 : this.size = 1 + this.next.size"
00019 })
00020 public abstract class IntList {
00021
00022 @Returns("this.next")
00023 public IntList next() { return Squander.exe(this); }
00024
00025 @Returns("this.size")
00026 public final int size() { return Squander.exe(this); }
00027
00028
00029
00030
00031
00032
00033
00034
00035
00036
00037
00038 public static void main(String[] args) {
00039 IntList lst = null;
00040 for (int k : new int[] {7, 3, 4 }) {
00041 lst = new Cons(k, lst);
00042 }
00043 System.out.println(lst.size());
00044 }
00045
00046 }
00047