subsubsection "Static Scoping of Procedures, Dynamic of Variables"
type_synonym penv = "(pname \ com) list"
inductive
big_step :: "penv \ com \ state \ state \ bool" (\_ \ _ \ _\ [60,0,60] 55) where
Skip: "pe \ (SKIP,s) \ s" |
Assign: "pe \ (x ::= a,s) \ s(x := aval a s)" |
Seq: "\ pe \ (c\<^sub>1,s\<^sub>1) \ s\<^sub>2; pe \ (c\<^sub>2,s\<^sub>2) \ s\<^sub>3 \ \
pe \<turnstile> (c\<^sub>1;;c\<^sub>2, s\<^sub>1) \<Rightarrow> s\<^sub>3" |
IfTrue: "\ bval b s; pe \ (c\<^sub>1,s) \ t \ \
pe \<turnstile> (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow> t" |
IfFalse: "\ \bval b s; pe \ (c\<^sub>2,s) \ t \ \
pe \<turnstile> (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow> t" |
WhileFalse: "\bval b s \ pe \ (WHILE b DO c,s) \ s" |
WhileTrue: "\ bval b s\<^sub>1; pe \ (c,s\<^sub>1) \ s\<^sub>2; pe \ (WHILE b DO c, s\<^sub>2) \ s\<^sub>3 \ \
pe \<turnstile> (WHILE b DO c, s\<^sub>1) \<Rightarrow> s\<^sub>3" |
Var: "pe \ (c,s) \ t \ pe \ ({VAR x; c}, s) \ t(x := s x)" |
Call1: "(p,c)#pe \ (c, s) \ t \ (p,c)#pe \ (CALL p, s) \ t" |
Call2: "\ p' \ p; pe \ (CALL p, s) \ t \ \
(p',c)#pe \ (CALL p, s) \ t" |
Proc: "(p,cp)#pe \ (c,s) \ t \ pe \ ({PROC p = cp; c}, s) \ t"
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.
