Rappels Coq

Prédicats inductifs

Prédicat

une fonction dans bool. En Coq on a bool et Prop.

Exemple : parité

Inductive even:nat -> Prop:=
| even_0: even 0
| even_SS: forall m:nat, even m -> even(S(Sm))

Definition even n:= div2 n = div2(Sn)

Une autre façon de définir even (croisée avec odd):

Inductive even:nat -> Prop:=
| even_0 : even 0
| even_S : forall n, odd n -> even(Sn).
with odd:nat -> Prop:=
| odd_S : forall n, even n -> odd(Sn)
| odd_1 : odd S0.

La Relation "≤"

Definition le (n m:nat) Prop:= exists p:nat, m=n+p.

Inductive le (n:nat) :nat->Prop:=
| le_n: le n n   (* n ≤ n *)
| le_S: forall m:nat, le n m -> le n (Sm).

De la sémantique des langages de programmation aux obligations de preuve.

Pour prouver les programmes, il faut définir la sémantique du langage.

Références Bibliographiques

Types de sémantique

opérationnelle

un programme est vu et décrit comme une succession d'états

dénotationnelle

un programme est vu et décrit comme un fonction, c'est à dire une transformation d'une entrée en un résultat

axiomatique

un programme est vu et décrit comme un transformateur de propriété(s)

Quelques propriétés des langages de programmation

  • déterminisme : fait toujours la même chose sur la même entrée.
  • préservation du typage : le calcul ne change pas le type
    P:T
    P \sim\!\!> P' \quad \rightarrow P':T

Notre cadre : mini-langage

e ::= n | x | e + e (* expressions arithmétiques *)
b ::= e < e (* expressions booléennes *)
i ::= skip | x:= e | i;i | while b do i done (* instructions, dont affectation, séquence, boucle *)
Inductive aexpr:Type :=
| Avar: string -> aexpr
| Anum: Z -> aexpr
| Aplus: aexpr -> aexpr -> aexpr.

Sémantique opérationnelle

  • à grands pas (sémantique naturelle)
  • à petits pas (sémantique opérationnelle standard, ou SOS)
Environnement

modèle théorique de la mémoire. ⇒ liste de paires associant à chaque variable sa valeur. En Coq, Definition env:= list(string*Z).

Jugements

pour les expressions, les jugements sont de la forme E \vdash e \rightarrow v

Règles pour jugements

Hyp. rien en haut : axiome
Déduction E \vdash n \rightarrow n
Hyp.
Déd.
Hyp.
Déd.
Hyp.
Déd.
Hyp.
Déd.

Jugements en coq

Definition env := list (string * Z).

Inductive aeval: env -> aexpr -> Z -> Prop :=
| Aeint: forall E n, aeval E (Anum n) n
| Aeplus: forall E e1 e2 n1 n2, aeval E e1 n1 -> aeval E e2 n2 -> aeval E (Aplus e1 e2) (n1 +n2)
| Aevar1: forall E x n, aeval((x,n)::E) (Avar x) n
| Aevar2: forall E x y n m, aeval E (Avar x) n -> x<>y -> aeval((y, n)::E) (Avar x) m.

Jugements pour les instructions

E \vdash i \tilde \rightarrow E'

FIXME à completer


 
m2ilc/coq_2.txt · Dernière modification: 2011/02/08 18:09 par suitable