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 }