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 ⊨ (c1,s1) → s2; pe ⊨ (c2,s2) → s3]==> pe ⊨ (c1;;c2, s1) → s3" |
IfTrue: "[ bval b s; pe ⊨ (c1,s) → t ]==> pe ⊨ (IF b THEN c1 ELSE c2, s) → t" |
IfFalse: "[¬bval b s; pe ⊨ (c2,s) → t ]==> pe ⊨ (IF b THEN c1 ELSE c2, s) → t" |
WhileFalse: "¬bval b s ==> pe ⊨ (WHILE b DO c,s) → s" |
WhileTrue: "[ bval b s1; pe ⊨ (c,s1) → s2; pe ⊨ (WHILE b DO c, s2) → s3]==> pe ⊨ (WHILE b DO c, s1) → s3" |
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 und die Messung sind noch experimentell.
