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.

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).

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

• Glynn Winskel, “The formal semantics of programming languages,” The MIT Press, 1993. ISBN-13: 978-0262731034.
• Tobias Nipkow, ”Winskel is (almost) Right: Toward a Mechanized Semantics Textbook.”
  • @article{Nipkow-FAC98,author={Tobias Nipkow}, title={Winskel is (almost) Right: Towards a Mechanized Semantics Textbook}, journal={Formal Aspects of Computing},volume=10,pages={171–186},year=1998}
• Yves Bertot, ”Theorem poving support in programming language semantics.”

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)

• 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

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

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.

E \vdash i \tilde \rightarrow E'

à completer

• suite : 6/12/2010
• projet Réflexions sur la dynamique
• TP coq_tp