The following exercices use PlusCal and TLA to write and check algorithms. Please refer to the documentation `~herbrete/public/TLA/c-manual.pdf`

and `~herbrete/public/TLA/pluscal.pdf`

.

PlusCal is an algorithmic language. It differs from programming languages since:

- PlusCal algorithms can manipulate arbitrary mathematical objects (graphs, etc). Programming languages require to implement these objects using low-level types (integers, booleans, etc).
- PlusCal algorithms can be non-deterministic. Programs need to be deterministic in order to be executable.
- PlusCal has a well-defined notion of an atomic step. In general, the instructions in a program are not atomic (mechanisms are usually provided to group instructions in atomic steps)
- PlusCal has a formal semantics defined as TLA+ expressions.

The TLA tools offer three main features:

- The translation of PlusCal programs into TLA+ expressions.
- The TLC model-checker that allows to find bugs in algorithms, and to prove algorithms with finite resources.
- The TLA prover which is not in the scope of this class.

Follow the short tutorial on TLA+ extension webpage to get started with the environment.

Create an empty file `euclid.tla`

and a module in thie file. Then, copy and paste Euclid’s algorithm below inside the module.

```
EXTENDS TLC, Integers
CONSTANT MAXINT (* Maximal integer *)
(* PlusCal options (-termination) *)
(*
--algorithm EuclidAlg {
variables
u \in 1..MAXINT;
v \in 1..MAXINT;
{
print <<u, v>>;
while (u /= 0) {
if (u < v) {
u := v || v := u
};
u := u - v
}
}
}
*)
```

In this algorithm:

`EXTENDS`

is used to import libraries (here, the TLC library and the natural numbers library).`CONSTANT`

introduces new symbolic names. Here`MAXINT`

is a parameter of the algorithm. Its value is unspecified yet.- The algorithm itself is placed inside a comment bloc
`(* ... *)`

. Its specification starts with`--algorithm`

followed by a name. - Two variables
`u`

and`v`

are declared. The declaration`u \in 1..MAXINT`

defines the initial value of variable`u`

. It is non-deterministically chosen in the set`1..MAXINT`

. - The statement
`print <<u, v>>`

displays the value of the tuple`<<u, v>>`

. Tuples can be made from any values, for instance ``<<"foo", u, 7>>`

is a valid tuple. - PlusCal supports parallel assignment like
`u := v || v := u`

. The two assignments are executed in parallel. Thus the values of`u`

and`v`

are swapped by this statement.

Use the `parse module`

command to check for syntax errors, and get a translation of Euclid’s algorithm in TLA+. The TLA+ translation corresponds to a logical description of the algorithm. It is used by the model-checking tool `TLC`

to assess correcteness of the algorithm.

Our goal is to check that this algorithm computest the greatest common divisor (gcd) of `u`

and `v`

.

- To that purpose, first add the following definition of the gcd immediately after the definition of constant
`MAXINT`

:

```
gcd(x,y) == CHOOSE i \in 1..x:
/\ x % i = 0
/\ y % i = 0
/\ \A j \in 1..x: x % j = 0 /\ y % j = 0 => i >= j
```

- Then, add 2 new variables
`u_init`

and`v_init`

that are initialized to`u`

and`v`

respectively. - Finally, add the following statements after the while loop in the algorithm:

```
print <<u_init, v_init, "have gcd", v>>;
assert v = gcd(u_init, v_init);
```

- Translate the definition of
`gcd`

in natural language. What is provided by this definition? - Edit the file
`euclid.cfg`

and set`CONSTANT MAXINT = 5`

. What is provided by this definition? - Use command
`Check module with TLC`

and observe the output. What can you conclude on the algorithm? - Observe the effect of choosing bigger values for constant
`MAXINT`

. - Replace the instruction
`u := u - v`

by`u := u - v + 1`

in the algorithm, then parse and check the algorithm. What do you observe? - Replace the instruction
`u := u - v + 1`

by`u := u - v - 1`

. Parse and check the algorithm. What can you conclude?

Assertion can be used to fail the model-checker when some condition is not met, just as a C program. However, this is not a convenient way to verify a program since the model-checker just stops and does not provide any insight on why the property is violated. We are going to replace the assertion in the algorithm by the following specification:

`Postcond == [] (pc = "Done" => v = gcd(u_init, v_init))`

- What is expressed by the property
`Postcond`

above? - Comment the assertion using
`(* ... *)`

. Then, copy and paste the property`Postcond`

above after the`\* END TRANSLATION`

. Add`PROPERTY Postcond`

in the file`euclid.cfg`

. Parse the algorithm, then run the model-checker. Explain what you observe. - Then fix the algorithm by setting back
`u := u - v`

instead of`u := u - v`

. Check the algorithm. What can you conclude about your algorithm?

We now want to compare testing with model-checking.

- Download the C implementation of Euclid’s algorithm euclid.c. Compile it:
`cc -std=c99 -Wall -o euclid euclid.c`

. Run the resulting executable`euclid`

for different input values. What do you observe? - Read the source code
`euclid.c`

. What are the differences with the PlusCal model? - What can you conclude regarding the termination of correctness of this implementation?