Skip to content

Commit defbb94

Browse files
author
Alex Lungu
committed
added various fixes
1 parent e25f93d commit defbb94

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

44 files changed

+1882
-1408
lines changed

‎.idea/misc.xml‎

Lines changed: 4 additions & 1 deletion
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎bin/alk.jar‎

841 Bytes
Binary file not shown.

‎input/symb/test1.alk‎

Lines changed: 7 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -5,20 +5,20 @@ attacked(i, j, b)
55
@requires 0 <= i && i < b.size()
66
@requires 0 <= j && j < b.size()
77
@ensures \result : boolean
8-
@ensures \result <==> (exists k : int :: 0 <= k && k < i && ((b[k] == j) || (abs(b[k] - j) == i - k)))
8+
@ensures \result <==> (exists k : int :: 0 <= k && k < i && ((b[k] == j) || ((b[k] - j) == (k - i)) || ((b[k] - j) == (i - k))))
99
{
1010
attack = false;
1111
for (k = 0; k < i; k++)
1212
@invariant 0 <= k && k <= i
13-
@invariant attack <==> (exists k1 : int :: 0 <= k1 && k1 < k && ((b[k1] == j) || (abs(b[k1] - j) == i - k1)))
13+
@invariant attack <==> (exists k1 : int :: 0 <= k1 && k1 < k && ((b[k1] == j) || ((b[k1] - j) == (k1 - i)) || ((b[k1] - j) == (i - k1))))
1414
@modifies k, attack
1515
{
16-
if ((b[k] == j) || (abs(b[k] - j) == abs(k - i)))
16+
if ((b[k] == j) || ((b[k] - j) == (k - i)) || ((b[k] - j) == (i - k)))
1717
attack = true;
1818
}
1919
return attack;
2020
}
21-
21+
2222
nqueens (n, out b)
2323
@requires n : int
2424
@requires b : array<int>
@@ -27,19 +27,13 @@ nqueens (n, out b)
2727
@ensures forall i : int :: (forall j : int :: 0 <= i && i < j && j < n ==> !(b[i] == b[j]))
2828
@ensures forall i : int :: (forall j : int :: 0 <= i && i < j && j < n ==> !(abs(b[j] - b[i]) == j - i))
2929
{
30-
k = 0;
31-
32-
while (k < n)
30+
for (k = 0; k < n; k++)
3331
@invariant 0 <= k && k <= n
3432
@invariant forall i : int :: (forall j : int :: 0 <= i && i < j && j < k ==> !(b[i] == b[j]))
3533
@invariant forall i : int :: (forall j : int :: 0 <= i && i < j && j < k ==> !(abs(b[j] - b[i]) == j - i))
3634
@modifies k, b
3735
{
38-
choose j from {0 .. n-1} s.t. !attacked(k, j, b); // abs
36+
choose j from {0 .. n-1} s.t. !attacked(k, j, b);
3937
b[k] = j;
40-
k++;
4138
}
42-
}
43-
44-
// b = [-1 | i from [0..n-1]];
45-
// nqueens(n);
39+
}

‎input/symb/test7.alk‎

Lines changed: 60 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -1,37 +1,62 @@
1-
choose x from A;
2-
// x |-> $x, exists i : int :: lft(A) <= i && i < rgh(A) ==> A[i] == $x
3-
4-
foreach x in A
5-
{
6-
A.pushBack(10);
7-
}
8-
9-
======================= A : array
10-
11-
i = 0;
12-
B = A;
13-
while (i < B.size())
1+
queens(n)
2+
@requires n : int
3+
@requires 1 <= n
4+
@ensures \result : array< array<int> >
5+
@ensures true
146
{
15-
x = B[i];
16-
17-
i++;
7+
// a = [ false | i from {1..n} ];
8+
@havoc a : array<boolean>, b : array<boolean>, c : array<boolean>;
9+
@assume a.size() == 0;
10+
@assume b.size() == 0;
11+
@assume c.size() == 0;
12+
13+
for (i = 0; i < n; i++)
14+
@invariant 0 <= i && i <= n
15+
@invariant a.size() == i
16+
@invariant forall j : int :: 0 <= j && j < i ==> !a[j]
17+
@modifies i, a, a.size
18+
{
19+
a[i] = false;
20+
}
21+
22+
@assert a.size() == n;
23+
@assert forall k : int :: 0 <= k && k < a.size() ==> !a[k];
24+
25+
@assert 2 * n >= 2;
26+
27+
// b = [ false | i from {1..2*n} ];
28+
// c = [ false | i from {1..2*n} ];
29+
for (i = 0; i < 2 * n; i++)
30+
@invariant 0 <= i && i <= 2 * n
31+
@invariant b.size() == i;
32+
@invariant c.size() == i;
33+
@invariant forall j : int :: 0 <= j && j < i ==> !b[j]
34+
@invariant forall j : int :: 0 <= j && j < i ==> !c[j]
35+
@modifies i, b, b.size, c, c.size
36+
{
37+
b[i] = false;
38+
c[i] = false;
39+
}
40+
41+
@assert b.size() == 2 * n;
42+
@assert c.size() == 2 * n;
43+
44+
@havoc cb : array< array<int> >;
45+
@assume cb.size() == n;
46+
//@assume forall i : int :: 0 <= i && i < n ==> cb[i].size() == n;
47+
48+
for (col = 0; col < n; ++col)
49+
@invariant 0 <= col && col <= n
50+
@invariant forall j : int :: 0 <= j && j < col ==> (exists i : int :: 0 <= i && i < n && cb[i][j] == 1)
51+
@modifies col, a, b, c, cb
52+
{
53+
choose row from {0..n - 1} s.t. !(a[row] || b[row + col] || c[n + (row-col)]);
54+
55+
a[row] = true;
56+
b[row + col] = true;
57+
c[n + (row-col)] = true;
58+
cb[row][col] = 1;
59+
}
60+
61+
return cb;
1862
}
19-
20-
21-
foreach x in A
22-
@invariant A.size() > 10
23-
{
24-
A = A U { 1 };
25-
}
26-
27-
======================= A : set
28-
29-
S = A;
30-
while (S.size() > 0)
31-
@invariant S.size() > 10
32-
{
33-
choose x from S;
34-
35-
36-
S.remove(x);
37-
}

‎input/symb/test8.alk‎

Lines changed: 21 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -1,35 +1,24 @@
1-
DNFS(out arr: array<int>)
2-
@requires arr.size() > 0
3-
@requires forall k: int :: 0 <= k && k < arr.size()
4-
==> (arr[k] == 0 || arr[k] == 1)
5-
@ensures (forall j:int :: 1 <= j && j < arr.size() ==> arr[j - 1] <= arr[j])
6-
{
7-
low = 0;
8-
high = arr.size() - 1;
1+
queens(n)
2+
@requires n : int
3+
@requires 2 <= n
4+
@ensures \result : array< array<int> >
5+
@ensures true
6+
{
7+
// a = [ false | i from {1..n} ];
8+
@havoc a : array<int>;
99

10-
while (low < high)
11-
@invariant 0 <= low && low <= high && high < arr.size();
12-
@invariant forall k: int :: 0 <= k && k < arr.size() ==> (arr[k] == 0 || arr[k] == 1);
13-
@invariant forall k: int :: 0 <= k && k < low ==> arr[k] == 0;
14-
@invariant forall k: int :: high < k && k < arr.size() ==> arr[k] == 1;
15-
@modifies arr;
16-
@modifies low;
17-
@modifies high;
10+
@assume a.size() == n;
11+
@assume forall i : int :: 0 <= i && i < n ==> a[i] == 0;
12+
13+
col = 0;
14+
15+
while (col < n)
16+
@invariant 0 <= col && col <= n
17+
@modifies col, a, b, c, cb
1818
{
19-
if (arr[low] == 0)
20-
{
21-
low++;
22-
}
23-
else
24-
{
25-
temp = arr[low];
26-
arr[low] = arr[high];
27-
arr[high] = temp;
28-
high--;
29-
}
19+
//choose row from {0 .. n-1} s.t. a[row] || b[row + col] || c[n + (row-col)];
20+
col++;
3021
}
31-
@assert low == high;
32-
@assert arr[low] == 0 || arr[low] == 1;
33-
@assert forall k: int :: 0 <= k && k < low ==> arr[k] == 0;
34-
@assert forall k: int :: high < k && k < arr.size() ==> arr[k] == 1;
35-
}
22+
23+
return cb;
24+
}

‎input/test.alk‎

Lines changed: 39 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,40 @@
1-
x(out a)
1+
vertex_cover(e)
2+
@requires e : array< array<int> >
3+
@ensures \result : array<boolean>
4+
@ensures forall i : int :: 0 <= i && i < e.size() && !\result[i] ==> (forall j : int :: 0 <= j && j < e[i].size() ==> \result[e[i][j]])
25
{
3-
@requires a < 10;
4-
a++;
5-
@ensures \old(a) + 1 == a;
6-
@ensures \result == 2;
7-
return 2;
8-
}
9-
10-
a = 2;
11-
x(a);
6+
@havoc S : array<boolean>;
7+
@assume S.size() == e.size();
8+
9+
for (i = 0; i < e.size(); i++)
10+
@invariant 0 <= i && i <= e.size()
11+
@modifies i, S
12+
{
13+
choose b from {true, false};
14+
S[i] = b;
15+
}
16+
17+
@assert S.size() == e.size();
18+
19+
for (i = 0; i < e.size(); i++)
20+
@invariant 0 <= i && i <= e.size()
21+
@invariant forall k : int :: 0 <= k && k < i && !S[k] ==> (forall l : int :: 0 <= l && l < e[k].size() ==> S[e[k][l]])
22+
@modifies i
23+
{
24+
if (!S[i])
25+
{
26+
for (j = 0; j < e[i].size(); j++)
27+
@invariant 0 <= j && j <= e[i].size()
28+
@invariant forall l : int :: 0 <= l && l < j ==> S[e[i][l]]
29+
@modifies j
30+
{
31+
if (!S[e[i][j]])
32+
{
33+
failure;
34+
}
35+
}
36+
}
37+
}
38+
39+
return S;
40+
}

‎input/test2.alk‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -27,12 +27,12 @@ nqueens (n, out b)
2727
@requires 0 < n
2828
@requires b.size() == n
2929
@ensures forall i : int :: (forall j : int :: 0 <= i && i < j && j < n ==> !(b[i] == b[j]))
30-
//@ensures forall i : int :: (forall j : int :: 0 <= i && i < j && j < n ==> !(abs(b[j] - b[i]) == j - i))
30+
@ensures forall i : int :: (forall j : int :: 0 <= i && i < j && j < n ==> !(abs(b[j] - b[i]) == j - i))
3131
{
3232
for (k = 0; k < n; k++)
3333
@invariant 0 <= k && k <= n
3434
@invariant forall i : int :: (forall j : int :: 0 <= i && i < j && j < k ==> !(b[i] == b[j]))
35-
//@invariant forall i : int :: (forall j : int :: 0 <= i && i < j && j < k ==> !(abs(b[j] - b[i]) == j - i))
35+
@invariant forall i : int :: (forall j : int :: 0 <= i && i < j && j < k ==> !(abs(b[j] - b[i]) == j - i))
3636
@modifies k, b
3737
{
3838
choose j from {0 .. n-1} s.t. !attacked(k, j, b);

‎input/test3.alk‎

Lines changed: 43 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,45 @@
1-
for (i=1; i<10; i++)
1+
attacked(i, j, b)
2+
@requires i : int
3+
@requires j : int
4+
@requires b : array<int>
5+
@requires 0 <= i && i < b.size()
6+
@requires 0 <= j && j < b.size()
7+
@ensures \result : boolean
8+
@ensures \result <==> (exists k : int :: 0 <= k && k < i && ((b[k] == j) || (abs(b[k] - j) == i - k)))
29
{
3-
if (i>5)
4-
continue;
5-
print(i);
10+
attack = false;
11+
for (k = 0; k < i; k++)
12+
@invariant 0 <= k && k <= i
13+
@invariant attack <==> (exists k1 : int :: 0 <= k1 && k1 < k && ((b[k1] == j) || (abs(b[k1] - j) == i - k1)))
14+
@modifies k, attack
15+
{
16+
if ((b[k] == j) || (abs(b[k] - j) == abs(k - i)))
17+
attack = true;
18+
}
19+
return attack;
620
}
7-
print(i);
21+
22+
nqueens (n, out b)
23+
@requires n : int
24+
@requires b : array<int>
25+
@requires 0 < n
26+
@requires b.size() == n
27+
@ensures forall i : int :: (forall j : int :: 0 <= i && i < j && j < n ==> !(b[i] == b[j]))
28+
@ensures forall i : int :: (forall j : int :: 0 <= i && i < j && j < n ==> !(abs(b[j] - b[i]) == j - i))
29+
{
30+
k = 0;
31+
32+
while (k < n)
33+
@invariant 0 <= k && k <= n
34+
@invariant forall i : int :: (forall j : int :: 0 <= i && i < j && j < k ==> !(b[i] == b[j]))
35+
@invariant forall i : int :: (forall j : int :: 0 <= i && i < j && j < k ==> !(abs(b[j] - b[i]) == j - i))
36+
@modifies k, b
37+
{
38+
choose j from {0 .. n-1} s.t. !attacked(k, j, b); // abs
39+
b[k] = j;
40+
k++;
41+
}
42+
}
43+
44+
// b = [-1 | i from [0..n-1]];
45+
// nqueens(n);

0 commit comments

Comments
 (0)