Programs with Proofs: Euclid's GCD Algorithm

Method of Proving

This is a program which also contains annotations to help prove its correctness using the Frama-C software.

The annotations specify various properties for a method like the pre-condition, post-condition, assertions, states modified, loop-invariants and loop-variants. They are also used to define other artifacts to ease specification/proving like predicates, logic functions, axioms and lemmas. These annotations are provided inside code-comments of the form /*@ ... */ and //@ ....

Frama-C with its WP plugin works with external provers like Alt-Ergo and CVC4 to automatically prove these specified properties. The WP plugin internally works based on the Weakest Precondition calculus. You can read more about this plugin's usage and meaning of the annotations in this tutorial.

The programs provided here have been proved using these versions of the tools: Frama-C (contains WP plugin) 21.1, Alt-Ergo 2.3.1 and CVC4 1.6. The system is x86_64 running Debian 10 Linux.

In addition to proving the specified properties, we will also be checking for other issues like overflows via another Frama-C plugin called RTE (by using option -wp-rte).

Command to prove this program:
frama-c -wp -wp-prover cvc4 -wp-rte filename.c

Euclid's GCD Algorithm


/* Method euclid() computes the greatest-common-divisor (GCD) of positive
   integers A and B, using the Euclid's GCD algorithm. The variant of the
   algorithm below reduces 'a' (similarly 'b') to (a-b). There is another
   variant which reduces 'a' to the remainder (a mod b). */

typedef unsigned int uint;

/*@
  // is 'd' a common-divisor of 'a' and 'b' ?
  predicate is_common_divisor(uint d, uint a, uint b) =
    a%d == 0 && b%d == 0;

  lemma order_a_b:
    \forall uint a, b, d; is_common_divisor(d, a, b) <==> is_common_divisor(d, b, a);

  lemma divides_itself:
    \forall uint a; a > 0 ==> is_common_divisor(a, a, a);

  axiomatic axm {
    axiom subtraction:
      \forall uint a, b, d; a > b ==>
      (is_common_divisor(d, a, b) <==> is_common_divisor(d, (uint)(a-b), b));
  }
 */

/*@
  requires A > 0 && B > 0;
  assigns \nothing;
  ensures is_common_divisor(\result, A, B);

  // the result is the greatest among all common-divisors of A and B
  ensures \forall uint d; is_common_divisor(d, A, B) ==> d <= \result;
*/
uint euclid(uint A, uint B)
{
  uint a, b;

  a = A;
  b = B;

  /*@
    loop assigns a, b;
    loop invariant a > 0 && b > 0;
    loop invariant \forall uint d;
                   is_common_divisor(d, a, b) <==> is_common_divisor(d, A, B);
    loop variant a+b;
   */
  while(a != b)
  {
L1:
    if(a > b)
    {
      a = a - b;
      /*@assert \forall uint d; is_common_divisor(d, \at(a, L1), \at(b, L1)) <==>
                is_common_divisor(d, a, b); */
    }
    else
    {
      b = b - a;
      /*@assert \forall uint d; is_common_divisor(d, \at(a, L1), \at(b, L1)) <==>
                is_common_divisor(d, a, b); */
    }
  }

  return a;
}