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

Define instructions

Browse source
This commit is contained in:
Théophile Bastian 2017-10-19 15:25:03 +02:00
parent 653e155f41
commit 23ca813c8c
1 changed files with 18 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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.