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.annotations.Returns;
00011 import edu.mit.csail.sdg.squander.Squander;
00012
00018 public class MixedSqRoot extends DeclarativeSqRoot {
00019
00020 protected MixedSqRoot() {}
00021
00022 @Requires("myS >= 0")
00023 public MixedSqRoot(int myS) {
00024 super(myS);
00025 }
00026
00027 @Override
00028 public int sqRoot() {
00029 final int s = getS();
00030 while (getR() + 1 < getQ()) {
00031 final int p = findP();
00032
00033 if (s / p < p) {
00034 findQ(p);
00035 } else {
00036 findR(p);
00037 }
00038 }
00039 return getR();
00040 }
00041
00042 @Requires("this.r + 1 < this.q")
00043 @Ensures("return > this.r && return < this.q")
00044 protected int findP() {
00045 return Squander.exe(this);
00046 }
00047
00048 @Requires({"p > 0", "this.s/p < p", "p < this.q"})
00049 @Modifies("this.q")
00050 @Ensures("this.q < @old(this.q)")
00051 @Returns("this.q")
00052 protected int findQ(int p) {
00053 return Squander.exe(this, new Class[] { int.class }, new Object[] { p });
00054 }
00055
00056 @Requires({"p > 0", "this.s/p >= p", "this.r < p"})
00057 @Modifies("this.r")
00058 @Ensures("this.r > @old(this.r)")
00059 @Returns("this.r")
00060 protected int findR(int p) {
00061 return Squander.exe(this, new Class[] { int.class }, new Object[] { p });
00062 }
00063
00064 }