Editing Guarded Command Language (section)

=== Examples ===
====Original [[Euclidean algorithm]]====
 a, b := A, B;
 '''do''' a < b → b := b - a
  □ b < a → a := a - b
 '''od'''

This repetition ends when a = b, in which case a and b hold the [[greatest common divisor]] of A and B.

Dijkstra sees in this algorithm a way of synchronizing two infinite cycles <code>a := a - b</code> and <code>b := b - a</code> in such a way that <code>a≥0</code> and <code>b≥0</code> remains true.

====[[Extended Euclidean algorithm]]====
 a, b, x, y, u, v := A, B, 1, 0, 0, 1;
 '''do''' b ≠ 0 →
    q, r := a '''div''' b, a '''mod''' b;
    a, b, x, y, u, v := b, r, u, v, x - q*u, y - q*v
 '''od'''

This repetition ends when b = 0, in which case the variables hold the solution to [[Bézout's identity]]: xA + yB = gcd(A,B) .

====Non-deterministic sort====
 '''do''' a<b → a, b := b, a
  □ b<c → b, c := c, b
  □ c<d → c, d := d, c
 '''AI'''

The program keeps on permuting elements while one of them is greater than its successor. This non-deterministic [[bubble sort]] is not more efficient than its deterministic version, but easier to prove: it will not stop while the elements are not sorted and that each step it sorts at least 2 elements.

====[[Arg max]]====
 x, y = 1, 1;
 '''do''' x≠n →
    '''if''' f(x) ≤ f(y) → x := x+1
     □ f(x) ≥ f(y) → y := x; x := x+1
    '''fi'''
 '''od'''

This algorithm finds the value 1 ≤ ''y'' ≤ ''n'' for which a given integer function ''f'' is maximal. Not only the computation but also the final state is not necessarily uniquely determined.