Compare commits
2 commits
653e155f41
...
94bc771b16
Author | SHA1 | Date | |
---|---|---|---|
Théophile Bastian | 94bc771b16 | ||
Théophile Bastian | 23ca813c8c |
|
@ -1,3 +1,6 @@
|
||||||
# mpri-coq-project
|
# mpri-coq-project
|
||||||
|
|
||||||
Projet de cours Coq (2.7.1) du MPRI — WP.
|
Projet de cours Coq (2.7.1) du MPRI — WP.
|
||||||
|
|
||||||
|
Deadline : probablement jusqu'à ~exam, rien de fixe.
|
||||||
|
(Examen : probablement 30/11, ~14h)
|
||||||
|
|
18
wp.v
Normal file
18
wp.v
Normal file
|
@ -0,0 +1,18 @@
|
||||||
|
(* Projet Coq - WP - MPRI 2.7.1 *)
|
||||||
|
|
||||||
|
(***** Partie 1 : definition de While ****************************************)
|
||||||
|
|
||||||
|
Require Import ZArith.BinInt.
|
||||||
|
Import Z.
|
||||||
|
|
||||||
|
Parameter Var: Type.
|
||||||
|
Definition Mem := Var -> Z.
|
||||||
|
Definition Expr:= Mem -> Z.
|
||||||
|
|
||||||
|
Inductive Instr : Type :=
|
||||||
|
| skip: Instr
|
||||||
|
| abort: Instr
|
||||||
|
| assign: Var -> Expr -> Instr
|
||||||
|
| seq: Instr -> Instr -> Instr
|
||||||
|
| ifelse: Expr -> Instr -> Instr -> Instr
|
||||||
|
| while: Expr -> Instr -> Instr.
|
Loading…
Reference in a new issue