added in examples/used-in-papers gc examples

Author: dlucanu

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

@@ -0,0 +1,17 @@
+gcd(a, b, out x, out y)
+@requires a : int && b : int && x : int && y : int
+@ensures \result : int
+@ensures x * a + y * b == \result
+{
+    x = 1; y = 0; x1 = 0; y1 = 1; a1 = a; b1 = b;
+    while (b1 > 0) 
+    @invariant x * a + y * b == a1
+    @invariant x1 * a + y1 * b == b1
+    {
+        q = a1 / b1;
+        tmp = x; x = x1; x1 = tmp - q * x1;
+        tmp = y; y = y1; y1 = tmp - q * y1;
+        tmp = a1; a1 = b1; b1 = tmp - q * b1;
+    }
+    return a1;
+}

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

@@ -0,0 +1,13 @@
+gcd(a, b, out x, out y) {
+    x = 1; y = 0; x1 = 0; y1 = 1; a1 = a; b1 = b;
+    while (b1 > 0) {
+        q = a1 / b1;
+        tmp = x; x = x1; x1 = tmp - q * x1;
+        tmp = y; y = y1; y1 = tmp - q * y1;
+        tmp = a1; a1 = b1; b1 = tmp - q * b1;
+    }
+    return a1;
+}
+x = 0; y = 0; a = 55; b = 80;
+g = gcd(a, b, x, y);
+@assert a * x + b * y == g; // certification check

examples/used-in-papers/fmtea2023/step3k-symb.alk renamed to examples/used-in-papers/fmtea2023/n3k-symb.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;
+        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)]);
+}
+