00001 00005 package edu.mit.csail.sdg.squander.examples.list.func2; 00006 00007 import edu.mit.csail.sdg.annotations.SpecField; 00008 00009 @SpecField({ 00010 "size : one int | this.size = 1 + this.rest.size", 00011 "keys : int -> int | #this.keys = this.size && " + 00012 "(0 -> this.key) in this.keys && " + 00013 "(all i: int | i < 0 ? no this.keys[i] : lone this.keys[i] && this.keys[i+1]=this.rest.keys[i])" 00014 }) 00015 public class Cons extends IntList { 00016 00017 private final int key; 00018 private final IntList rest; 00019 00020 public Cons(int key, IntList rest) { 00021 this.key = key; 00022 this.rest = rest; 00023 } 00024 00025 public int getKey() { 00026 return key; 00027 } 00028 00029 public IntList getRest() { 00030 return rest; 00031 } 00032 00033 @Override 00034 public String toString() { 00035 return "Cons(" + key + ", " + rest + ")"; 00036 } 00037 00038 }