00001 00005 package edu.mit.csail.sdg.squander.examples.numbers; 00006 00007 import edu.mit.csail.sdg.annotations.Ensures; 00008 import edu.mit.csail.sdg.annotations.Modifies; 00009 import edu.mit.csail.sdg.annotations.Requires; 00010 import edu.mit.csail.sdg.squander.Squander; 00011 00017 public class DeclarativeSqRoot implements ISqRoot { 00018 00019 protected DeclarativeSqRoot() {} 00020 00021 public DeclarativeSqRoot(int myS) { 00022 init(myS); 00023 } 00024 00025 @Requires("myS >= 0") 00026 @Ensures({"this.s = myS", "this.r = 0", "this.q = (myS = 0 ? 1 : myS)"}) 00027 @Modifies({"this.s", "this.r", "this.q"}) 00028 private void init(int myS) { 00029 Squander.exe(this, new Class[] { int.class }, new Object[] { myS }); 00030 } 00031 00032 @Override public int getS() { return Squander.exe(this); } 00033 @Override public int getR() { return Squander.exe(this); } 00034 @Override public int getQ() { return Squander.exe(this); } 00035 00036 @Ensures("this.r = r") 00037 @Modifies("this.r") 00038 protected void setR(int r) { Squander.exe(this, new Class[] {int.class}, new Object[] {r}); } 00039 00040 @Ensures("this.q = q") 00041 @Modifies("this.q") 00042 protected void setQ(int q) { Squander.exe(this, new Class[] {int.class}, new Object[] {q}); } 00043 00044 @Override 00045 public int sqRoot() { 00046 return Squander.exe(this); 00047 } 00048 00049 }