Quelle  Procs_Stat_Vars_Stat.thy   Sprache: Isabelle

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 ⊨ (c🚫1;;c🚫2, s🚫1) ==> s🚫3" |

IfTrue:  "\ bval b (s \ venv e); e \ (c\<^sub>1,s) \ t \ \
         e ⊨ (IF b THEN c🚫1 ELSE c🚫2, s) ==> t" |
IfFalse: "\ \bval b (s \ venv e); e \ (c\<^sub>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\<^sub>1 \ venv e); e \ (c,s\<^sub>1) \ s\<^sub>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