La syntaxe complète de Micro C est donnée dans la documentation de Why3.

En première approximation, vous pouvez considérer que Micro C est comme le C standard, mais avec un seul type de donnée : int.

Vous trouverez ci-dessous un rappel des annotations qui vous seront utiles.

Annotation de programmes Micro C

Les commentaires spéciaux contenant des annotations sont de la forme : //@ <annotation jusqu'en fin de ligne>

Les mots-clefs suivants peuvent être utilisés :

requires

pour donner une précondition : requires n >=0 ;

ensures

pour donner une postcondition : ensures result == n*n ;

invariant

pour donner l'invariant d'une boucle : invariant i+j == n ;

variant

pour donner un variant d'une boucle (valeur qui décroit à chaque tour de boucle et reste positive ou nulle) : variant j - i;

lemma

pour donner un lemme (permet de guider le prouveur) :

lemma mul_distr_r: forall a b c; (a+b)*c == a*c + b*c ;

assert

pour indiquer qu'une propriété est vraie à ce point du programme : assert i > 0 && j > 0 ;

predicate

pour définir un prédicat logique : predicate even(int n) = n%2 == 0 ;

function

pour définir une fonction logique : function int twice(int n) = 2*n ;

result

pour faire référence à la valeur de retour d'une fonction

label

pour définir un endroit du programme où on s'intéresse à la valeur des variables : label mon_label ;

at

pour faire référence à la valeur d'une variable à un label : at(i, mon_label)

forall

pour le quantificateur universel : forall n. n+1 > n;

exists

pour le quantificateur d'existence : exists k. 4 == 2*k ;

->

pour l'implication : forall x. x == 3 -> x/2 == 1 ;

<->

pour l'équivalence : forall x. x%2 == 0 <-> x == 2*(x/2) ;