1 import gov.nasa.jpf.jvm.Verify; 20 21 22 25 class sorter2 { 26 public static void main (String [] args) { 27 int a = Verify.random(4); 28 int b = Verify.random(4); 29 int c = Verify.random(4); 30 int d = Verify.random(4); 31 int temp = 0; 32 Verify.instrumentPoint("pre-sort"); 33 34 if (a > b) { 35 temp = b; 36 b = a; 37 a = temp; 38 } 39 40 if (b > c) { 41 temp = c; 42 c = b; 43 b = temp; 44 } 45 46 if (c > d) { 47 temp = d; 48 d = c; 49 c = temp; 50 } 51 52 if (b > c) { 53 temp = c; 54 c = b; 55 b = temp; 56 } 57 58 if (a > b) { 59 temp = b; 60 b = a; 61 a = temp; 62 } 63 64 Verify.instrumentPoint("post-sort"); 65 66 assert ((a <= b) && (b <= c) && (c <= d)); 67 } 68 } | Popular Tags |