Umgebungen (Spezifikation)

• Grundbereich: Aussagen der Form $\mathsf {wert}$ (E, p, z) mathend000#

  (in Umgebung E mathend000# hat Programm p mathend000# den Wert z mathend000#)

  Umgebungen konstruiert aus ∅ mathend000# und E[v : = b] mathend000#

• Regeln für Operatoren $${\frac{{\operatorname{\mathsf{wert}}(E,X,a),\operatorname{\mathsf{wert}}(E,Y,b)}}{{\operatorname{\mathsf{wert}}(E,\texttt{Plus} X Y,a+b)}}}$$,... mathend000#
• Regeln für Umgebungen $${\frac{{}}{{\operatorname{\mathsf{wert}}(E[v:=b],v,b)}}}$$,    $${\frac{{\operatorname{\mathsf{wert}}(E,v',b')}}{{\operatorname{\mathsf{wert}}(E[v:=b],v',b')}}}$$ mathend000# für v≠v' mathend000#
• Regeln für Bindung: $${\frac{{\operatorname{\mathsf{wert}}(E,X,b), \operatorname{\maths... ...,Y,c)}}{{\operatorname{\mathsf{wert}}(E,\mathtt{let } v=X \mathtt{ in } Y,c)}}}$$ mathend000#