1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
 void gcd(int a, int b) {
   int result;
   if (⟨(1 <= a) && (1 <= b)⟩ → ⟨(1 <= b) && (1 <= a)⟩) {
     while (⟨!(a == b)⟩ → ⟨!((a <= b) && (b <= a))⟩) {
       if (a <= b) {
         b = (b - a);
       } else {
         a = (a - b);
       };
     };
     result = a;
   } else {
     result = 0;
   };

 }