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.Invariant;
00009 import edu.mit.csail.sdg.annotations.Modifies;
00010 import edu.mit.csail.sdg.annotations.Returns;
00011 import edu.mit.csail.sdg.annotations.SpecField;
00012
00013 @SpecField({"s : int", "r : int", "q : int"})
00014 @Invariant({
00015 "this.r > 0 => this.r <= this.s / this.r",
00016 "this.s / this.q < this.q",
00017 "this.r >= 0",
00018 "this.s >= 0",
00019 "this.q > 0"
00020 })
00021 public interface ISqRoot {
00022
00023 @Returns("this.s") public int getS();
00024 @Returns("this.r") public int getR();
00025 @Returns("this.q") public int getQ();
00026
00027 @Ensures({"this.s / (this.r + 1) < (this.r + 1)"})
00028 @Returns("this.r")
00029 @Modifies({"this.r", "this.q"})
00030 public int sqRoot();
00031
00032 }
