examples/added used-in-papers

Author: dlucanu

examples/used-in-papers/fmtea2023/.DS_Store

@@ -0,0 +1,21 @@
+COMPACT_LIST_SEARCH(L, n, k)
+{
+    i = 0;
+    while (i < L.size() && L.at(i).key < k) 
+    {
+        uniform j from [1..n];
+        if (L.at(i).key < L.at(j).key && L.at(j).key < k) {
+            i = j;
+            if (L.at(i).key == k) return i;
+        }
+        i = i+1;
+    }
+    if (i == L.size() || L.at(i).key > k)
+        return -1;
+    else return i; 
+}
+
+x = COMPACT_LIST_SEARCH(L, n, k);
+
+//L = < {key -> 5}, {key -> 8}, {key -> 12}, {key -> 15}, {key -> 24} >;
+//x = COMPACT_LIST_SEARCH(L, 3, 12);

examples/used-in-papers/fmtea2023/compact-list-search.alk

@@ -0,0 +1,6 @@
+uniform j from [1..n];
+if (L.at(i).key < L.at(j).key && L.at(j).key < k) {
+    i = j;
+    if (L.at(i).key == k) return i;
+}
+i = i+1;

examples/used-in-papers/fmtea2023/fragment.alk

@@ -0,0 +1,17 @@
+/*base(out n)
+@requires n: int
+@requires n == 3
+@ensures n == 0
+*/
+{
+    // the first turn
+    // choose take from {1,2};
+    //  ... symbolically
+    n=3;
+    @havoc take: int;
+    @assume 1 <= take && take <= 2;
+    n = n - take;
+    // the next turn
+    take = n % 3;
+    n = n - take;
+}

examples/used-in-papers/fmtea2023/step1-with-spec.alk

@@ -0,0 +1,6 @@
+// the first turn
+choose take from {1,2};
+n = n - take;
+// the next turn
+take = n;
+n = n - take;

examples/used-in-papers/fmtea2023/step1.alk

@@ -0,0 +1,35 @@
+/*
+    A box contains N matches. Two players take turns taking one or two matches from the box.
+    The player, whose turn it is and has no legal move to make, loses. 
+    Who has the winning strategy?
+*/
+
+/*
+    We show first that 
+    - if N is a multiple of 3 then the second player has a strategy to win;
+    - otherwise, the first player has one.
+*/
+winingStrategy(n)
+@requires n: int
+@requires n > 0 && n % 3 == 0;
+@ensures \result == 2; 
+{
+    turn = 1;
+    while (n > 0) 
+    @modifies n, turn;
+    @invariant n % 3 == 0 && n >= 0
+    @invariant n > 0 ==> turn == 1;
+    @invariant n == 0 ==> turn == 2;
+    {
+        // the current turn
+        choose take from {1,2};
+        n = n - take;
+        // the next turn
+        turn = 3 - turn;
+        take = n % 3;
+        n = n - take;
+        // prepare the next current turn (if any)
+        if (n > 0) turn = 3 - turn;
+    }
+    return turn;
+}

examples/used-in-papers/fmtea2023/step2-with-spec.alk

@@ -0,0 +1,20 @@
+winingStrategy(n)
+{
+    turn = 1;
+    while (n > 0) 
+    {
+        // the current turn
+        choose take from {1,2};
+        n = n - take;
+        // the next turn
+        turn = 3 - turn;
+        take = n % 3;
+        n = n - take;
+        // prepare the next current turn (if any)
+        if (n > 0) turn = 3 - turn;
+    }
+    return turn;
+}
+
+for (i = 1; i < 6; ++i) 
+    w[i-1] = winingStrategy(3*i);

examples/used-in-papers/fmtea2023/step2.alk

@@ -0,0 +1,12 @@
+@havoc n: int;
+@assume n % 3 == 0; 
+// the first turn
+// choose take from {1,2};
+//  ... symbolically
+@havoc take: int;
+@assume 1 <= take && take <= 2;
+n = n - take;
+// the next turn
+take = n % 3;
+n = n - take;
+@assert n % 3 == 0;

examples/used-in-papers/fmtea2023/step3k-symb.alk

@@ -0,0 +1,37 @@
+/*
+    A box contains N matches. Two players take turns taking one or two matches from the box.
+    The player, whose turn it is and has no legal move to make, loses. 
+    Who has the winning strategy?
+*/
+winingStrategy(n) 
+@requires n: int;
+@requires n > 0;
+@ensures \result: int;
+@ensures (\old(n) % 3 == 0 ==> \result == 2) && (\old(n) % 3 != 0 ==> \result == 1); 
+{
+    turn = 1;
+    if (n % 3 != 0) {
+        take = n % 3;
+        n = n - take;
+        if (n > 0) turn = 2;
+    }
+    while (n > 0) 
+    @modifies n, turn
+    @invariant n % 3 == 0 && n >= 0 
+    @invariant n > 0 ==> (\old(n) % 3 == 0 ==> turn == 1) && (\old(n) % 3 != 0 ==> turn == 2);
+    @invariant n == 0 ==> ((\old(n) % 3 == 0 ==> turn == 2) && (\old(n) % 3 != 0 ==> turn == 1));
+    {
+        // the current turn
+        choose take from {1,2};
+        n = n - take;
+        // the next turn
+        turn = 3 - turn;
+        take = n % 3;
+        n = n - take;
+        // prepare the next current turn (if any)
+        if (n > 0) turn = 3 - turn;
+    }
+    return turn;
+}
+
+

examples/used-in-papers/fmtea2023/winstrat-with-spec.alk

@@ -0,0 +1,38 @@
+/*
+    A box contains N matches. Two players take turns taking one or two matches from the box.
+    The player, whose turn it is and has no legal move to make, loses. 
+    Who has the winning strategy?
+*/
+
+/*
+    We show first that 
+    - if N is a multiple of 3 then the second player has a strategy to win;
+    - otherwise, the first player has one.
+*/
+winingStrategy(n) 
+{
+    turn = 1;
+    if (n % 3 != 0) {
+        take = n % 3;
+        n = n - take;
+        if (n > 0) turn = 2;
+    }
+    while (n > 0) 
+    {
+        // the current turn
+        choose take from {1,2};
+        n = n - take;
+        // the next turn
+        turn = 3 - turn;
+        take = n % 3;
+        n = n - take;
+        // prepare the next current turn (if any)
+        if (n > 0) turn = 3 - turn;
+    }
+    return turn;
+}
+
+for (i = 1; i < 10; ++i) {
+    print([i, winingStrategy(i)]);
+}
+

examples/used-in-papers/fmtea2023/winstrat.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/used-in-papers/tase2022/askith_assert.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/used-in-papers/tase2022/askith_call.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/used-in-papers/tase2022/askith_verify.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/used-in-papers/tase2022/bubblesort.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;
+}