00001
00005 package edu.mit.csail.sdg.squander.examples.numbers;
00006
00007 import java.util.Arrays;
00008 import java.util.Random;
00009
00010 import edu.mit.csail.sdg.annotations.Case;
00011 import edu.mit.csail.sdg.annotations.Ensures;
00012 import edu.mit.csail.sdg.annotations.Modifies;
00013 import edu.mit.csail.sdg.annotations.Requires;
00014 import edu.mit.csail.sdg.annotations.Returns;
00015 import edu.mit.csail.sdg.annotations.Specification;
00016 import edu.mit.csail.sdg.squander.Squander;
00017 import edu.mit.csail.sdg.squander.annotations.Options;
00018
00023 public class Arithmetic {
00024
00025 @Requires("m > 0 && n > 0")
00026 @Ensures({"no x : int | x > return && m % x = 0 && n % x = 0",
00027 "return > 0",
00028 "m % return = 0",
00029 "n % return = 0"})
00030 public static int gcd(final int m, final int n) {
00031 return Squander.exe(null, new Class<?>[] {int.class, int.class}, new Object[] {m, n});
00032 }
00033
00034 @Requires("m > 0 && n > 0")
00035 @Ensures({"no x : int | x > return && m % x = 0 && n % x = 0",
00036 "return > 0",
00037 "m % return = 0",
00038 "n % return = 0"})
00039 public static int gcd_impl(int m, int n) {
00040 if (m < n) {
00041 int t = m;
00042 m = n;
00043 n = t;
00044 }
00045
00046 int r = m % n;
00047
00048 if (r == 0) {
00049 return n;
00050 } else {
00051 return gcd(n, r);
00052 }
00053 }
00054
00055
00056
00057
00058
00059
00060
00061
00062 @Ensures( { "all i: int | #{j:int | a[j] = i} = #{j:int | @old(a[j]) = i}",
00063 "all i: int | all j: int | 0 <= i && i < j && j < a.length => a[i] <= a[j]" })
00064 @Modifies("a.elems")
00065 @Returns("a")
00066 public static int[] sort(int[] a) {
00067 return Squander.exe(null, new Class[] { int[].class }, new Object[] { a });
00068 }
00069
00070 @Specification({
00071 @Case(
00072 requires = "s = 0",
00073 ensures = "return = 0"
00074 ),
00075 @Case(
00076 requires = "s > 0",
00077 ensures = "return > 0 && return <= s / return && s / (return + 1) < (return + 1)"
00078 )
00079 })
00080 public static int square_root(int s) {
00081 return Squander.exe(null, new Class<?>[] {int.class}, new Object[]{s});
00082 }
00083
00084
00085
00086
00087 @Requires("s >= 0")
00088 @Ensures({"return >= 0",
00089 "return <= s / return",
00090 "s / (return + 1) < (return + 1)"})
00091 public static int square_root_finite(int s) {
00092 return Squander.exe(null, new Class<?>[] {int.class}, new Object[]{s});
00093 }
00094
00095 public static int square_root_mixed(final int s) {
00096 int r = 1;
00097 int q = s;
00098 while (r+1 < q) {
00099 int p = findP(r, q);
00100 if (s < p*p) {
00101 q = findQ(p, q, r, s);
00102 } else {
00103 r = findR(p, q, r, s);
00104 }
00105 }
00106 return r;
00107 }
00108
00109 @Requires("r + 1 < q")
00110 @Ensures("return > r && return < q")
00111 @Options(ensureAllInts = true)
00112 private static int findP(final int r, final int q) {
00113 return Squander.exe(null, new Class[] {int.class, int.class}, new Object[] {r, q});
00114 }
00115
00116 @Requires({"r <= s/r && s/q < q", "s/p < p", "p < q"})
00117 @Ensures("return < q && return > 0 && r <= s/r && s/return < return")
00118 private static int findQ(final int p, final int q, final int r, final int s) {
00119 return Squander.exe(null, new Class[] {int.class, int.class, int.class, int.class},
00120 new Object[] {p, q, r, s});
00121 }
00122
00123 @Requires({"r <= s/r && s/q < q", "s/p >= p", "r < p"})
00124 @Ensures("return > r && return <= s/return && s/q < q")
00125 private static int findR(final int p, final int q, final int r, final int s) {
00126 return Squander.exe(null, new Class[] {int.class, int.class, int.class, int.class},
00127 new Object[] {p, q, r, s});
00128 }
00129
00130 public static int _square_root_mixed(final int s) {
00131 int r = 1;
00132 int q = s;
00133 while (r+1 < q) {
00134 int p = findP(r, q);
00135 if (s < p*p) {
00136 q = _findQ(p, q, r, s);
00137 } else {
00138 r = _findR(p, q, r, s);
00139 }
00140 }
00141 return r;
00142 }
00143
00144 @Requires({"r*r <= s && s < q*q", "s < p*p", "p < q"})
00145 @Ensures("return < q && return > 0 && r*r <= s && s < return * return")
00146 private static int _findQ(final int p, final int q, final int r, final int s) {
00147 return Squander.exe(null, new Class[] {int.class, int.class, int.class, int.class},
00148 new Object[] {p, q, r, s});
00149 }
00150
00151 @Requires({"r <= s/r && s/q < q", "s >= p*p", "r < p"})
00152 @Ensures("return > r && return * return <= s && s < q*q")
00153 private static int _findR(final int p, final int q, final int r, final int s) {
00154 return Squander.exe(null, new Class[] {int.class, int.class, int.class, int.class},
00155 new Object[] {p, q, r, s});
00156 }
00157
00158 public static void main(String[] args) {
00159 int n = 24;
00160 int[] a = new int[n];
00161 Random r = new Random();
00162 for (int i = 0; i < n; i++) {
00163 a[i] = r.nextInt(n) - n/2;
00164 }
00165 System.out.println(Arrays.toString(a));
00166
00167 long t1 = System.currentTimeMillis();
00168 a = sort(a);
00169 long t2 = System.currentTimeMillis();
00170 System.out.println(Arrays.toString(a));
00171 System.out.println("time: " + Double.toString((t2 - t1)/1000));
00172 }
00173
00174 }