Newer
Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
package nl.uu;
import static nl.uu.impress.EDSL.*;
public class Arrays {
// // 1) Simple array arithmetic
// public static void swap1_1(int[] a, int i, int j) {
// pre(i >= 0 && j >= 0);
// swap(a, i, j);
// post(a[j] == oldai && a[i] == oldaj);
// }
// public static void swap2_1(int[] a, int i, int j) {
// pre(i >= 0);
// pre(j > 0 || (i + 1) * j >= 0);
// swap(a, i, j);
// post(a[i] == oldaj);
// post(a[j] == oldai);
// }
//
// // 2) Quantifying over array (max)
// public static void max1_2(int[] a) {
// pre(a != null && a.length > 0);
// int retval = getMax(a);
// post(exists(a, i -> a[i] == retval));
// post(forall(a, i -> a[i] <= retval));
// }
// public static void max2_2(int[] a) {
// pre(a != null && a.length >= 1);
// int retval = getMax(a);
// post(exists(a, i -> retval * 2 == a[i] + a[i]));
// post(!exists(a, i -> a[i] > retval));
// }
// 3) Quantifying over array (sort)
public static void sort1_3(int[] a) {
pre(a != null && a.length >= 0);
int[] sa = a.sort();
post(forall(a, i ->
forallr(a, i + 1, a.length, j -> a[i] <= a[j])));
}
// public static void sort2_3(int[] a) {
// pre(a != null && a.length > -1);
// int[] sa = a.sort();
// post(forall(a, i ->
// !existsr(a, i + 1, a.length, j -> a[i] > a[j])));
// }
// 4) Quantifying over array (unique sort)
public static void sort1_4(int[] a) {
pre(a != null && a.length > 1);
pre(forall(a, i ->
forall(a, j -> i == j || a[i] != a[j])));
int[] sa = a.sort();
post(a.length > 1);
post(forallr(a, 0, a.length - 1, i -> a[i] < a[i + 1]));
}
// public static void sort2_4(int[] a) {
// pre(a != null);
// pre(a.length >= 2);
// pre(forall(a, i ->
// forall(a, j -> i == j || a[i] != a[j])));
// // forallr(a, i + 1, a.length, j -> a[i] != a[j])));
// // pre(forallr(a, a.length, 0, i ->
// // forallr(a, 0, i, j -> a[j] != a[i])));
// int[] sa = a.sort();
// // post(forall(a, i ->
// // forallr(a, i + 1, a.length, j -> a[i] < a[j])));
// post(a.length >= 2);
// post(forallr(a, 1, a.length, i -> a[i] > a[i - 1]));
// }
}