|
theory Procs_Stat_Vars_Stat imports Procs
begin
subsubsection "Static Scoping of Procedures and Variables"
type_synonym addr = nat
type_synonym venv = "vname \ addr"
type_synonym store = "addr \ val"
type_synonym penv = "(pname \ com \ venv) list"
fun venv :: "penv \ venv \ nat \ venv" where
"venv(_,ve,_) = ve"
inductive
big_step :: "penv \ venv \ nat \ com \ store \ store \ bool"
("_ \ _ \ _" [60,0,60] 55)
where
Skip: "e \ (SKIP,s) \ s" |
Assign: "(pe,ve,f) \ (x ::= a,s) \ s(ve x := aval a (s o ve))" |
Seq: "\ e \ (c\<^sub>1,s\<^sub>1) \ s\<^sub>2; e \ (c\<^sub>2,s\<^sub>2) \ s\<^sub>3 \ \
e \<turnstile> (c\<^sub>1;;c\<^sub>2, s\<^sub>1) \<Rightarrow> s\<^sub>3" |
IfTrue: "\ bval b (s \ venv e); e \ (c\<^sub>1,s) \ t \ \
e \<turnstile> (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow> t" |
IfFalse: "\ \bval b (s \ venv e); e \ (c\<^sub>2,s) \ t \ \
e \<turnstile> (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow> t" |
WhileFalse: "\bval b (s \ venv e) \ e \ (WHILE b DO c,s) \ s" |
WhileTrue:
"\ bval b (s\<^sub>1 \ venv e); e \ (c,s\<^sub>1) \ s\<^sub>2;
e \<turnstile> (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3 \<rbrakk> \<Longrightarrow>
e \<turnstile> (WHILE b DO c, s\<^sub>1) \<Rightarrow> s\<^sub>3" |
Var: "(pe,ve(x:=f),f+1) \ (c,s) \ t \
(pe,ve,f) \<turnstile> ({VAR x; c}, s) \<Rightarrow> t" |
Call1: "((p,c,ve)#pe,ve,f) \ (c, s) \ t \
((p,c,ve)#pe,ve',f) \ (CALL p, s) \ t" |
Call2: "\ p' \ p; (pe,ve,f) \ (CALL p, s) \ t \ \
((p',c,ve')#pe,ve,f) \<turnstile> (CALL p, s) \<Rightarrow> t" |
Proc: "((p,cp,ve)#pe,ve,f) \ (c,s) \ t
\<Longrightarrow> (pe,ve,f) \<turnstile> ({PROC p = cp; c}, s) \<Rightarrow> t"
code_pred big_step .
values "{map t [10,11] |t.
([], <''x'' := 10, ''y'' := 11>, 12)
\<turnstile> (test_com, <>) \<Rightarrow> t}"
end
¤ Dauer der Verarbeitung: 0.18 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
