00001
00005 package edu.mit.csail.sdg.squander.examples.mock;
00006
00007 import edu.mit.csail.sdg.annotations.Ensures;
00008 import edu.mit.csail.sdg.annotations.Invariant;
00009 import edu.mit.csail.sdg.annotations.Modifies;
00010 import edu.mit.csail.sdg.annotations.Requires;
00011 import edu.mit.csail.sdg.annotations.Returns;
00012 import edu.mit.csail.sdg.annotations.SpecField;
00013
00014
00015
00016 @SpecField("data : String -> String")
00017 @Invariant("all x:String | lone this.data[x]")
00018 public interface AddressBook {
00019
00020 @Requires("@arg(0) != null && @arg(1) != null")
00021 @Ensures("this.data = @old(this.data) ++ @arg(0) -> @arg(1)")
00022 @Modifies("this.data")
00023 void setEmailAddress(String name, String email);
00024
00025 @Ensures("return - null = this.data[@arg(0)]")
00026 String getEmailAddress(String name);
00027
00028 @Returns("some this.data[@arg(0)]")
00029 boolean contains(String name);
00030 }