Travaux dirigés du 14 février 2012 (TD3)

Preuves de programmes

• Imprimer les valeurs de negb et xorb
• Prouver

  forall x, negb (negb x) = x
  

• Prouver

  forall x y, xorb x y = xorb y x
  

• Prouver

  forall x y, xorb (negb x) y = negb (xorb y x)
  

• En utilisant la définition suivante

  Fixpoint ff (n:nat) :=
    match n with
      0 => true
    | S p => negb (ff p)
    end.
  

  Prouver

  forall x y, ff (x + y) = negb (xorb (ff x) (ff y))
  

• Prouver

  forall x, ff x = true -> exists y, x = 2 * y
  

Ecriture de programmes sémantiques

On considère le type de données suivant, qui représente les expressions arithmétique d'un langage de programmation.

Require Import ZArith String.
Open Scope Z_scope.

Inductive aexpr :=
  aplus (e1 e2 : aexpr) | avar (s : string) | anum (x : Z).

Ecrire un programme qui décrit l'évaluation des expressions arithmétiques. Les valeurs des variables seront données par une liste de couples associant chaque nom de variable à une valeur entière, de type

list (string * Z)

La valeur retourné par ce programme d'évaluation aura le type

option Z

La valeur retourné sera None si et seulement l'expression évaluée contient une variable dont la valeur n'est pas donnée dans la liste.