Commit a62c9473 authored by Heiko Becker's avatar Heiko Becker
Browse files

Fix minor flaw. Ret was not evaluated. This would theoretically make programs...

Fix minor flaw. Ret was not evaluated. This would theoretically make programs that crash in  the return expression valid
parent c1eb0b5e
(*
Formalization of the Abstract Syntax Tree of a subset used in the Daisy framework
*)
needs "Infra/tactics.ml";;
needs "Infra/tactics.hl";;
(*
Define expressions parametric over some value type V.
......@@ -37,12 +37,10 @@ let exp_eval_DEF = new_specification ["exp_eval"] exp_eval_EXISTS;;
(*
Toy examples showing how to evaluate terms and functions in HOL Light
let test = `exp_eval (Const (&1)) (\x. &1)`;;
let test = REWRITE_CONV[exp_eval_DEF] test;;
rhs (concl test);;
*)
`exp_eval (Const (&1)) (\x. &1)`;;
REWRITE_CONV[exp_eval_DEF] it;;
rhs (concl it);;
(*
Prove totality of expression evaluation for reals assuming totality of the environment
......@@ -107,9 +105,10 @@ let greq_simps = define
Final return statement
*)
let cmd_INDUCT, cmd_REC = define_type
"cmd = Ass num (V)exp cmd
"cmd = Let num (V)exp cmd
| Ite (V)bexp cmd cmd
| Ret (V)exp";;
| Ret (V)exp
| Nop ";;
(*
Define environment update function for arbitrary type as abbreviation
......@@ -126,7 +125,7 @@ let sstep_RULES,sstep_INDUCT,sstep_CASES = new_inductive_definition
(beval:(V)bexp->(num->V)->bool)
(env:num->V).
eval e env = v ==>
sstep (Ass x e s) env eval beval s (upd_env x v env)) /\
sstep (Let x e s) env eval beval s (upd_env x v env)) /\
(!(c:(V)bexp) s t
(eval:(V)exp->(num->V)->V)
(beval:(V)bexp->(num->V)->bool)
......@@ -138,7 +137,13 @@ let sstep_RULES,sstep_INDUCT,sstep_CASES = new_inductive_definition
(beval:(V)bexp->(num->V)->bool)
(env:num->V).
beval c env = F ==>
sstep (Ite c s t) env eval beval t env)`;;
sstep (Ite c s t) env eval beval t env) /\
(!(e:(V)exp) (v:V)
(eval:(V)exp->(num->V)->V)
(beval:(V)bexp->(num->V)->bool)
(env:num->V).
eval e env = v ==>
sstep (Ret e) env eval beval Nop (upd_env (0) v env))`;;
(*
Analogously define Big Step semantics for the Daisy language,
......@@ -149,7 +154,7 @@ let bstep_RULES,bstep_INDUCT,bstep_CASES = new_inductive_definition
(beval:(V)bexp->(num->V)->bool)
(env:num->V).
eval e env = v /\ bstep s (upd_env x v env) eval beval s ==>
bstep (Ass x e s) env eval beval s ) /\
bstep (Let x e s) env eval beval s ) /\
(!(c:(V)bexp) s1 s2 t
(eval:(V)exp->(num->V)->V)
(beval:(V)bexp->(num->V)->bool)
......@@ -161,4 +166,10 @@ let bstep_RULES,bstep_INDUCT,bstep_CASES = new_inductive_definition
(beval:(V)bexp->(num->V)->bool)
(env:num->V).
beval c env = F /\ bstep t1 env eval beval t2
==> bstep (Ite c s t1) env eval beval t2 )`;;
==> bstep (Ite c s t1) env eval beval t2 ) /\
(!(e:(V)exp) (v:V)
(eval:(V)exp->(num->V)->V)
(beval:(V)bexp->(num->V)->bool)
(env:num->V).
eval e env = v ==>
bstep (Ret e) env eval beval Nop)`;;
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment