Pour ce travail, nous utiliserons Why3, (éventuellement Eclipse) et Isabelle. Les instructions d'installation et d'utilisation sont données sur cette page.

La syntaxe Micro C est décrite ici.

Méthode du paysan russe

Cette technique permet de calculer le produit de deux entiers en n'utilisant que la somme, la différence, et les multiplication et division entières par 2 (décalages d'un bit à gauche et à droite).

Cet exercice doit vous permettre de vérifier que votre environnement de travail fonctionne correctement, il n'y a rien à compléter dans le code Micro C fourni ci-dessous pour prouver la correction du programme.

int product(int a, int n) {
  // Fonction product(a, n) returns a*n if n is greater or equal to 0
  //@ requires n >= 0;
  //@ ensures result == a * n ;
  int r = 0;
  //@ label start ;
  while (n != 0) {
    // We give a loop invariant (for the correction) and a variant (for termination)
    //@ invariant r + a*n == at (a, start) * at (n, start) && n >= 0 ;
    //@ variant n;
    if (n%2 != 0) {
      n--;
      r += a;
    }
    //@ assert n % 2 == 0 ;
    n /= 2;
    a *= 2;
  }
  return r;
}

Partie entière de la racine carrée d'un entier

Écrire en Micro C une fonction isqrt calculant la partie entière de la racine carrée d'un entier en utilisant la propriété suivante : {$$n^2=\sum_{i=0}^{n-1}(2i+1)$$} Ajouter les prérequis, post-condition et invariant pour démontrer que votre code calcule bien cette partie entière. Ajouter un variant pour montrer que le programme termine. Le code Micro C vous est fourni ci-dessous.

// Some useful lemmas for non linear arithmetics
//@ lemma distr_right: forall x, y, z. x*(y+z) == (x*y)+(x*z) ;
//@ lemma distr_left: forall x, y, z. (x+y)*z == (x*z)+(y*z) ;


int isqrt(int n) {
  // When n is greater or equal to 0, the result should be the integer square root of n

  int count = 0;
  int sum = 1;
  while (sum <= n) {

    count++;
    sum = sum + 2*count+1;
  }
  return count;
}

Calcul du PGCD par la méthode d'Euclide

Faire de même avec un programme qui calcule le PGCD de deux entiers par soustractions successives. Il faudra définir un prédicat is_gcd(int x, int y, int d) qui est vrai lorsque d est le PGCD de x et y. Vous aurez pour cela besoin d'un prédicat divides(int x, int y) qui indique si x divise y, ainsi que d'autres prédicats auxiliaires selon votre façon de modéliser ce problème. Le code Micro C vous est fourni ci-dessous.

// Add here the predicates and lemmas needed by your proof

int gcd(int a, int b) {
  // The result should be the GCD of a and b

  while (a != b) {

    if (a < b) {
      b -= a;
    } else {
      a -= b;
    }
  }
  return a;
}