added tests

examples/analysis/tase2022/askith_assert.alk

@@ -0,0 +1,34 @@
+/*
+    alki -a askith_assert.alk -s -smt="Z3"
+
+    a |-> $a_0
+    res |-> 0
+    i |-> $i_0
+    Path condition:
+       ((($a_0.size()>0)&&(0<=$i_0))&&($i_0<($a_0.size()-1))) &&
+       !($a_0[$i_0]>$a_0[($i_0+1)])
+
+    a |-> (store (store $a_0 $i_0 $a_0[($i_0+1)]) ($i_0+1) $a_0[$i_0])
+    res |-> 0
+    tmp |-> $a_0[$i_0]
+    i |-> $i_0
+    Path condition:
+       ((($a_0.size()>0)&&(0<=$i_0))&&($i_0<($a_0.size()-1))) &&
+       ($a_0[$i_0]>$a_0[($i_0+1)]) &&
+       validStore($a_0, $i_0, $a_0[($i_0+1)]) &&
+       validStore((store $a_0 $i_0 $a_0[($i_0+1)]), ($i_0+1), $a_0[$i_0])
+*/
+
+@havoc a : array<int>;
+@havoc i : int;
+@assume a.size() > 0 && 0 <= i && i < a.size() - 1;
+if (a[i] > a[i + 1])
+{
+    tmp = a[i];
+    a[i] = a[i + 1];
+    a[i + 1] = tmp;
+    res = i;
+}
+res = 0;
+@assert a[i] <= a[i + 1];
+@assert res > 0 ==> res == i;

examples/analysis/tase2022/askith_call.alk

@@ -0,0 +1,36 @@
+/*
+    alki -a askith_call.alk -m -s -smt="Z3"
+
+    Successfully verified: askIth
+
+    a |-> $a_1
+    last |-> $\result_0
+    Path condition:
+       ($a.size()>3) &&
+       ($a_1[2]<=$a_1[3]) &&
+       ($\result_0>0) ==> ($\result_0==2)
+
+*/
+
+askIth(out a, i)
+@requires a : array<int>
+@requires i : int
+@requires a.size() > 0 && 0 <= i && i < a.size() - 1
+@ensures a[i] <= a[i + 1]
+@ensures \result > 0 ==> \result == i
+@ensures \result : int
+{
+    if (a[i] > a[i + 1])
+    {
+        tmp = a[i];
+        a[i] = a[i + 1];
+        a[i + 1] = tmp;
+        return i;
+    }
+    return 0;
+}
+
+@symbolic $a : array<int>;
+a = $a;
+@assume a.size() > 3;
+last = askIth(a, 2);

examples/analysis/tase2022/askith_verify.alk

@@ -0,0 +1,23 @@
+/*
+    alki -a askith_verify.alk -s -smt="Z3"
+
+    Successfully verified: askIth
+*/
+
+askIth(out a, i)
+@requires a : array<int>
+@requires i : int
+@requires a.size() > 0 && 0 <= i && i < a.size() - 1
+@ensures a[i] <= a[i + 1]
+@ensures \result > 0 ==> \result == i
+@ensures \result : int
+{
+    if (a[i] > a[i + 1])
+    {
+        tmp = a[i];
+        a[i] = a[i + 1];
+        a[i + 1] = tmp;
+        return i;
+    }
+    return 0;
+}

examples/analysis/tase2022/bubblesort.alk

@@ -0,0 +1,44 @@
+/*
+    alki -a bubblesort.alk -m -i "b |-> [2, 3, 1]"
+    b |-> [1, 2, 3]
+    alki -a bubblesort.alk -m -i "b |-> [1.2, 1.5, 1.4]"
+    b |-> [1.2, 1.4, 1.5]
+    alki -a bubblesort.alk -m -i "b |-> [\"ab\", \"ac\", \"aa\"]"
+    b |-> ["aa", "ab", "ac"]
+*/
+
+swap(out a, i, j)
+@requires 0 <= i && i < a.size()
+@requires 0 <= j && j < a.size()
+{
+    temp = a[i];
+    a[i] = a[j];
+    a[j] = temp;
+}
+
+askIth(out a, i)
+@requires a.size() > 1
+@requires 0 <= i && i < a.size() - 1
+{
+    if (a[i] > a[i + 1]) {
+        swap(a, i, i + 1);
+        return i;
+    }
+    return 0;
+}
+
+bubbleSort(out a)
+@requires a.size() > 0
+{
+    last = a.size() - 1;
+    while (last > 0)
+    {
+        n1 = last;
+        for (i = 0; i < n1; ++i)
+        {
+            last = askIth(a, i);
+        }
+    }
+}
+
+bubbleSort(b);

examples/analysis/tase2022/fstalg.alk

@@ -0,0 +1,16 @@
+/*
+    alki -a fstalg.alk -m -i "a |-> [1, 2, 2, 3, 3, 3]"
+
+    a |-> [1, 2, 2, 3, 3, 3]
+    slp |-> 3
+    i |-> 6
+*/
+
+slp = 1;
+i = 1;
+while (i < a.size())
+{
+    if (a[i] == a[i - slp])
+        slp = slp + 1;
+    i = i + 1;
+}

examples/analysis/tase2022/fstalg_assert.alk

@@ -0,0 +1,35 @@
+/*
+    alki -a fstalg_assert.alk -m -s -smt="Z3"
+
+    a |-> $a_0
+    slp |-> $slp_0
+    i |-> ($i_1+1)
+    Path condition:
+       ($a_0.size()>0) &&
+       forall $i_0 : int :: ((0<=$i_0)&&($i_0<($a_0.size()-1))) ==> ($a_0[$i_0]<=$a_0[($i_0+1)]) &&
+       exists $k_0 : int :: (((($slp_0-1)<=$k_0)&&($k_0<$i_1))&&($a_0[$k_0]==$a_0[(($k_0-$slp_0)+1)])) &&
+       !($a_0[$i_1]==$a_0[($i_1-$slp_0)])
+
+    a |-> $a_0
+    slp |-> ($slp_0+1)
+    i |-> ($i_1+1)
+    Path condition:
+       ($a_0.size()>0) &&
+       forall $i_0 : int :: ((0<=$i_0)&&($i_0<($a_0.size()-1))) ==> ($a_0[$i_0]<=$a_0[($i_0+1)]) &&
+       exists $k_0 : int :: (((($slp_0-1)<=$k_0)&&($k_0<$i_1))&&($a_0[$k_0]==$a_0[(($k_0-$slp_0)+1)])) &&
+       ($a_0[$i_1]==$a_0[($i_1-$slp_0)])
+*/
+
+@havoc a : array<int>;
+slp = 1;
+i = 1;
+@assume a.size() > 0;
+@assume forall i : int :: 0 <= i && i < a.size() - 1 ==> a[i] <= a[i + 1];
+
+@havoc i : int;
+@havoc slp : int;
+@assume exists k:int :: slp - 1 <= k && k < i && a[k] == a[k - slp + 1];
+if (a[i] == a[i - slp])
+    slp = slp + 1;
+i = i + 1;
+@assert exists k:int :: slp - 1 <= k && k < i && a[k] == a[k - slp + 1];

examples/analysis/tase2022/fstalg_assume.alk

@@ -0,0 +1,31 @@
+/*
+    alki -a fstalg_assume.alk -m -s -smt="Z3"
+
+    a |-> $a_0
+    slp |-> 2
+    i |-> 3
+
+    a |-> $a_0
+    slp |-> 3
+    i |-> 3
+
+    a |-> $a_0
+    slp |-> 2
+    i |-> 3
+
+    a |-> $a_0
+    slp |-> 1
+    i |-> 3
+*/
+
+@havoc a : array<int>;
+@assume forall i : int :: 0 <= i && i < a.size() - 1 ==> a[i] <= a[i + 1];
+@assume a.size() == 3;
+slp = 1;
+i = 1;
+while (i < a.size())
+{
+    if (a[i] == a[i - slp])
+        slp = slp + 1;
+    i = i + 1;
+}

examples/analysis/tase2022/fstalg_inv.alk

@@ -0,0 +1,30 @@
+/*
+    alki -a fstalg_inv.alk -m -s -smt="Z3"
+
+    a |-> $a_0
+    slp |-> $slp_0
+    i |-> $i_1
+
+    [13:11] Loop invariant was verified!
+    [14:12] Loop invariant was verified!
+    [13:11] Loop invariant was verified!
+    [14:12] Loop invariant was verified!
+
+*/
+
+@havoc a : array<int>;
+slp = 1;
+i = 1;
+@assume a.size() > 0;
+@assume forall i : int :: 0 <= i && i < a.size() - 1 ==> a[i] <= a[i + 1];
+while (i < a.size())
+@invariant 1 <= slp && i <= a.size();
+@invariant (exists k:int :: slp - 1 <= k && k < i && a[k] == a[k - slp + 1]);
+// @invariant (forall k:int :: slp <= k && k < i ==> a[k] != a[k - slp]);
+// Z3 TIMEOUT, Dafny TIMEOUT; Why3 with Alt-Ergo WORKS FINE
+@modifies slp, i;
+{
+    if (a[i] == a[i - slp])
+        slp = slp + 1;
+    i = i + 1;
+}

examples/analysis/tase2022/fstalg_loopassert.alk

@@ -0,0 +1,33 @@
+/*
+    alki -a fstalg_loopassert.alk -m -s -smt="Z3"
+
+    a |-> $a_0
+    slp |-> 1
+    i |-> 3
+
+    a |-> $a_0
+    slp |-> 2
+    i |-> 3
+
+    a |-> $a_0
+    slp |-> 3
+    i |-> 3
+
+    a |-> $a_0
+    slp |-> 2
+    i |-> 3
+*/
+
+@havoc a : array<int>;
+slp = 1;
+i = 1;
+@assume a.size() == 3;
+@assume forall i : int :: 0 <= i && i < a.size() - 1 ==> a[i] <= a[i + 1];
+while (i < a.size())
+@modifies slp, i;
+{
+    if (a[i] == a[i - slp])
+        slp = slp + 1;
+    i = i + 1;
+}
+@loopassert 1 <= slp && i <= a.size() && (exists k:int :: slp - 1 <= k && k < i && a[k] == a[k - slp + 1]);

examples/analysis/tase2022/fstalg_req.alk

@@ -0,0 +1,16 @@
+/*
+    alki -a fstalg_req.alk -m -s -smt="Z3"
+
+    TIMEOUT: a.size() is not bounded
+*/
+
+@havoc a : array<int>;
+@assume forall i : int :: 0 <= i && i < a.size() - 1 ==> a[i] <= a[i + 1]
+slp = 1;
+i = 1;
+while (i < a.size())
+{
+    if (a[i] == a[i - slp])
+        slp = slp + 1;
+    i = i + 1;
+}

input/symb/notes.ts

@@ -0,0 +1,6 @@
+//
+
+// (Array T Bool)
+
+// x in A -> (select A x) unde A : set
+// x in A -> (exists j int :: 0 <= j && j < A.size() ==> (select A j) == x) unde A : array

input/symb/test0.alk

@@ -1,28 +1,6 @@
-findMin(a : array<int>) : int
-@ensures forall j : int :: 0 <= j && j < a.size() ==> \result <= a[j]
-@ensures exists j : int :: 0 <= j && j < a.size() ==> \result == a[j]
-{
-    i = 0;
-    minim = a[0];
-
-    while (i < a.size())
-    @invariant i <= a.size();
-    @invariant forall j : int :: 0 <= j && j < i ==> minim <= a[j];
-    @modifies i, minim;
-    {
-        if (a[i] < minim)
-        {
-            minim = a[i];
-        }
-        i++;
+a(i) {
+    b(j){
+        j++;
     }
-
-    return minim;
-}
-
-@symbolic $a : array<int>;
-a = $a;
-x = findMin(a);
-
-
-
+    i++;
+}