tobast/mpri-coq-project
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Compare commits

base: tobast:653e155f412676b503fe8314c5ca95fb2918679d
Branches Tags
tobast:master
tobast:submitted
tobast:certain_termination_wip
tobast:MEH
...
compare: tobast:94bc771b16a5159f5baa733abf8a956ee367336f
Branches Tags
tobast:master
tobast:submitted
tobast:certain_termination_wip
tobast:MEH

2 commits
653e155f41 ... 94bc771b16

Author SHA1 Message Date
Théophile Bastian 94bc771b16 Update deadlines 2017-10-26 14:43:31 +02:00
Théophile Bastian 23ca813c8c Define instructions 2017-10-19 15:25:03 +02:00
2 changed files with 22 additions and 1 deletions
Show stats Expand all files Collapse all files

5
README.md
View file

@ -1,3 +1,6 @@
# 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
View 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.