minor fixes

Author: Alex Lungu

.idea/modules.xml

@@ -0,0 +1,7 @@
+@havoc A : array<int>;
+@assume A.size() == 10;
+@assume forall x : int :: 0 <= x && x < 10 ==> A[x] == 2;
+
+choose x from A;
+
+@assert x == 2;

.idea/vcs.xml

@@ -0,0 +1,6 @@
+@havoc A : set<int>;
+@assume forall x : int :: x in A ==> x == 2;
+
+choose x from A;
+
+@assert x == 2;

bin/alk.jar

@@ -0,0 +1,15 @@
+@havoc n : int;
+@assume n > 1;
+
+sum = 0;
+i = 1;
+
+do
+{
+    sum += i;
+    i++;
+} while (i <= n)
+@invariant sum == i * (i - 1) / 2;
+@invariant i <= n + 1;
+
+@assert sum == n * (n + 1) / 2;

input/symb/set0/choose.alk

@@ -0,0 +1,11 @@
+@havoc n : int;
+@assume n > 1;
+sum = 0;
+for (i = 1; i <= n; i++)
+@invariant sum == i * (i - 1) / 2
+@invariant i <= n + 1
+{
+    sum += i;
+}
+
+@assert sum == n * (n + 1) / 2;

input/symb/set0/choose2.alk

@@ -0,0 +1,44 @@
+@havoc A : array<int>;
+@assume A.size() == 3;
+@assume forall x : int :: 0 <= x && x < A.size() ==> A[x] == x;
+
+sum = 0;
+foreach x from A
+{
+    sum += x;
+}
+
+// A |-> $a
+while (A.size() > 0)
+// (size (set-difference $a (store emptySet x true))) > 0
+{
+    choose x from A;
+    A.remove(x); // A = A \ { x }
+    // A |-> (set-difference $a (store emptySet x true))
+    ...
+}
+
+A = A \ { x } ---> (set-difference $a (store emptySet x true))
+A.remove(x)   ---> (store $a x false)
+
+(size (store $a x false)) == (size $a) - 1 daca   (store $a x true)
+                             (size $a)     altfel
+
+A = A \ {x, y, z}
+==================
+
+A.remove(x).remove(y).remove(z)
+
+A = A ^ {x, y, z}
+
+(store $a x true)  ==> (size (store $a x false)) == (size $a) - 1
+(store $a x false) ==> (size (store $a x false)) == (size $a)
+
+
+// x in A
+// $a.size() > (size (set-difference $a (store emptySet x true))) >= 0
+
+
+(size (set-difference $a (store emptySet x true))) :=
+    forall x, y, a :: (size (set-difference x (store y a true)) ==
+                      (size (set-difference x y)) daca (store x a) == false sau (size (set-difference x y)) - 1 altfel

input/symb/set0/do.alk

@@ -0,0 +1,12 @@
+@havoc A : array<int>;
+@assume A.size() == 10;
+@assume forall x : int :: 0 <= x && x < 10 ==> A[x] == 2;
+
+
+sum = 0;
+foreach x from A
+{
+    sum += x;
+}
+@assert A.size() * 2 == sum;
+

input/symb/set0/for.alk

@@ -0,0 +1,15 @@
+@havoc n : int;
+@assume n > 1;
+
+sum = 0;
+i = 1;
+
+repeat
+{
+    sum += i;
+    i++;
+} until (i > n)
+@invariant sum == i * (i - 1) / 2;
+@invariant i <= n + 1;
+
+@assert sum == n * (n + 1) / 2;