merge

Author: vladvlad00

.idea/misc.xml

@@ -1,3 +1,13 @@
+# Introduction
+This repository includes Alk, an educational platform designed to help in learning algorithms and acquiring algorithmic thinking.
+Some references:
+1. Lungu, A., Lucanu, D.: _A matching logic foundation for Alk_. In: Seidl, H., Liu, Z., Pasareanu, C.S. (eds.) Theoretical Aspects of Computing -
+ICTAC 2022 - 19th International Colloquium, Tbilisi, Georgia, September 27-29, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13572, pp. 290–304. Springer (2022). https://doi.org/10.1007/978-3-031-17715-6“ ̇19
+2. Lungu, A., Lucanu, D.: _Supporting algorithm analysis with symbolic execution in Alk_. In: Ameur, Y.A., Craciun, F. (eds.) Theoretical Aspects of Software Engineering - 16th International Symposium, TASE 2022, Proceedings. Lecture Notes in Computer Science, vol. 13299, pp. 406–423. Springer (2022), https://doi.org/10.1007/978-3-031-10363-6 27
+
+Read the [reference manual](../../wiki/Reference-Manual) to review the Alk syntax.
+Also consider the [Alk-by example](../../wiki/Alk-by-examples) wiki to understand how Alk behaves in real-scenarios.
+
 # Using the Alk VS Code Extension
 1. Install VS Code from the official [page](https://code.visualstudio.com/download).
 2. In the Extensions tag in the left side, check for the "Alk Visual Studio Code Extension" and install.
@@ -47,8 +57,6 @@ Optionally (and remmended) is to create a symbolic link named `alki`:
     ```
     ln -s ../../bin/alki.sh ../../bin/alki
     ```
-Read the [reference manual](../../wiki/Reference-Manual) to review the Alk syntax.
-Also consider the [Alk-by example](../../wiki/Alk-by-examples) wiki to understand how Alk behaves in real-scenarios.
 
 # Set Alk in PATH system variable
 * Linux/Mac OS:

.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;

README.md

@@ -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;

bin/alk.jar

@@ -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;