Umgebungen (Spezifikation)

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

  (in Umgebung E hat Programm p den Wert z)

  Umgebungen konstruiert aus ∅ und E[v : = p]

• 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)}}}$$,...
• 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')}}}$$ für v≠v'
• 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)}}}$$