00001 00005 package edu.mit.csail.sdg.squander.examples.sort; 00006 00007 import java.util.Arrays; 00008 import java.util.Random; 00009 00010 import edu.mit.csail.sdg.annotations.Ensures; 00011 import edu.mit.csail.sdg.annotations.Invariant; 00012 import edu.mit.csail.sdg.annotations.Modifies; 00013 import edu.mit.csail.sdg.annotations.Returns; 00014 import edu.mit.csail.sdg.squander.Squander; 00015 import edu.mit.csail.sdg.squander.annotations.Options; 00016 import edu.mit.csail.sdg.squander.log.Log; 00017 import edu.mit.csail.sdg.squander.options.GlobalOptions; 00018 00019 public class Sort { 00020 00021 @Invariant("this.a != null") 00022 private int[] a = new int[0]; 00023 00024 public Sort(int... array) { 00025 this.a = new int[array.length]; 00026 for (int i = 0; i < a.length; i++) { 00027 this.a[i] = array[i]; 00028 } 00029 } 00030 00031 @Returns("this.a") 00032 public int[] getA() { 00033 return a; 00034 } 00035 00036 @Ensures( { "all i: int | #{j:int | this.a[j] = i} = #{j:int | @old(this.a[j]) = i}", 00037 "all i: int | all j: int | 0 <= i && i < j && j < this.a.length => this.a[i] <= this.a[j]" }) 00038 @Modifies("this.a.elems") 00039 @Options(ensureAllInts=false) 00040 public void sort() { 00041 Squander.exe(this); 00042 } 00043 00044 00045 @Override 00046 public String toString() { 00047 return Arrays.toString(a); 00048 } 00049 00050 public static void main(String[] args) { 00051 GlobalOptions.INSTANCE.log_level = Log.Level.ALL; 00052 int n = 10; 00053 int[] a = new int[n]; 00054 Random r = new Random(); 00055 for (int i = 0; i < n; i++) { 00056 a[i] = r.nextInt(n) - n / 2; 00057 } 00058 Sort sort = new Sort(a); 00059 long t = System.currentTimeMillis(); 00060 sort.sort(); 00061 long dt = System.currentTimeMillis() - t; 00062 System.out.println("## sorted_array: " + sort); 00063 System.out.println("## time: " + dt); 00064 } 00065 }