00001 00005 package edu.mit.csail.sdg.squander.examples.mock; 00006 00007 import java.util.Arrays; 00008 00009 import edu.mit.csail.sdg.annotations.Invariant; 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 00015 00025 @SpecField("data : String -> String from this.entries | this.data = {x in String, y : String | some e : this.entries[int] | e.entryName = x && e.entryEmail = y}") 00026 public class SquanderAddressBook implements AddressBook { 00027 00028 @Invariant("this.entryName != null && this.entryEmail != null") 00029 public static class Entry { 00030 String entryName = ""; 00031 String entryEmail = ""; 00032 00033 @Override 00034 public String toString() { 00035 return "entry: " + entryName + " = " + entryEmail; 00036 } 00037 } 00038 00039 @Invariant("null !in this.entries[int]") 00040 public Entry[] entries; 00041 00042 @Fresh({@FreshObjects(cls=Entry.class, num=1), @FreshObjects(cls=Entry[].class, num=1)}) 00043 @Override 00044 public void setEmailAddress(String name, String email) { 00045 Squander.exe(this, new Class<?>[]{String.class, String.class}, new Object[]{name, email}); 00046 } 00047 00048 @Override 00049 public String getEmailAddress(String name) { 00050 return Squander.exe(this, new Class<?>[]{String.class}, new Object[]{name}); 00051 } 00052 00053 @Override 00054 public boolean contains(String name) { 00055 return Squander.exe(this, new Class<?>[]{String.class}, new Object[]{name}); 00056 } 00057 00058 @Override 00059 public String toString() { 00060 return this.entries == null ? null : Arrays.toString(this.entries); 00061 } 00062 }