Theory Procs_Stat_Vars_Stat
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⇩1,s⇩1) ⇒ s⇩2; e ⊢ (c⇩2,s⇩2) ⇒ s⇩3 ⟧ ⟹
e ⊢ (c⇩1;;c⇩2, s⇩1) ⇒ s⇩3" |
IfTrue: "⟦ bval b (s ∘ venv e); e ⊢ (c⇩1,s) ⇒ t ⟧ ⟹
e ⊢ (IF b THEN c⇩1 ELSE c⇩2, s) ⇒ t" |
IfFalse: "⟦ ¬bval b (s ∘ venv e); e ⊢ (c⇩2,s) ⇒ t ⟧ ⟹
e ⊢ (IF b THEN c⇩1 ELSE c⇩2, s) ⇒ t" |
WhileFalse: "¬bval b (s ∘ venv e) ⟹ e ⊢ (WHILE b DO c,s) ⇒ s" |
WhileTrue:
"⟦ bval b (s⇩1 ∘ venv e); e ⊢ (c,s⇩1) ⇒ s⇩2;
e ⊢ (WHILE b DO c, s⇩2) ⇒ s⇩3 ⟧ ⟹
e ⊢ (WHILE b DO c, s⇩1) ⇒ s⇩3" |
Var: "(pe,ve(x:=f),f+1) ⊢ (c,s) ⇒ t ⟹
(pe,ve,f) ⊢ ({VAR x; c}, s) ⇒ 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) ⊢ (CALL p, s) ⇒ t" |
Proc: "((p,cp,ve)#pe,ve,f) ⊢ (c,s) ⇒ t
⟹ (pe,ve,f) ⊢ ({PROC p = cp; c}, s) ⇒ t"
code_pred big_step .
values "{map t [10,11] |t.
([], <''x'' := 10, ''y'' := 11>, 12)
⊢ (test_com, <>) ⇒ t}"
end