Louden’s Simple Language for Describing Formal SemanticsA variety of notationsLogical Inference RulesStructural Operational SemanticsAdding Assignment Changes Things SlightlyControl Flow is Not Much HarderLouden’s Simple Language for Describing Formal Semanticsprogram → stmt-liststmt-list → stmt ‘;’ stmt-list | stmtstmt → assign-stmt | if-stmt | while-stmtassign-stmt →identifier ‘:=’ exprif-stmt → ‘if’ expr ‘then’ stmt-list ‘else’ stmt-list ‘fi’while-stmt → ‘while’ expr ‘do’ stmt-list ‘od’identifier → ‘a’ | ‘b’ | ‘c’ | ... | ‘z’ expr → expr ‘+’ term | expr ‘-’ term | termterm → term ‘*’ factor | factorfactor → ‘(‘ expr ‘)’ | number | identifiernumber → number digit | digitdigit → ‘0’ | ’1’ | ’2’ | ’3’ | ’4’ | ’5’ | ’6’ | ’7’ | ’8’ | ’9’•One oddity about Louden’s little language: In if-stmt (resp. while-stmt) the expr is evaluated in the current environment. If it is greater than 0, the then (resp. do) is executed otherwise the else is executed (resp. while is terminated).A variety of notations•For our language, the semantic domain Environment, the set of all environments, is the collection of all (partial) functions mapping identifiers into Integer values. That isEnvironment = Identifier → Integer.•We might express an element of this set by a name such as Env or σ.•The empty environment would be an empty map, one that doesn’t map any identifier into any Integer value.•A function can be modified by changing its map at exactly one element of its domain I, to have value n. This can be expressed variously asEnv[n/I] σ[n/I] (relatively standard)[n/i]Env [n/I]σ (somewhat standard)[I n]Env [I n]σ (somewhat nonstandard)Env&{I=n} (very nonstandard)Logical Inference Rules•Inference rules are all of the following form:•This inference rule embodies the transitive property:conclusionpremisecacbba ,Structural Operational Semantics•Meaning is assigned to a program by reducing it (and its input) to the value it yields.•A reduction rule has either a syntactic component (or a mixture of sentactic components and semantic values) on the left side and a semantic value on the right side. Consider the rules for digits:‘0’ => 0‘1’ => 1‘2’ => 2...‘9’ => 9and the rules for numbers:V ‘0’ => 10*VV ‘1’ => 10*V + 1V ‘2’ => 10*V + 2...V ‘9’ => 10*V + 9V1 ‘+’ V2 => V1 + V2 V1 ‘-’ V2 => V1 - V2’ V1 ‘*’ V2 => V1 * V2 ‘(‘ V ’)’ => V...etc.2121E''E E '' EE E11E'' V E '' VE E‘2’ ‘+’ ‘1’=> 2 ‘+’ ‘1’=> 2 ‘+’ 1=> 2 + 1=> 3Adding Assignment Changes Things SlightlyEnvEEEnvEEEnvEEnvE|''|''||2121EnvVEnvIVIEnv||)(}{&|':' VIEnvEnvVI EnvEIEnvEIEnvEEnvE|':'|':'||1111||';'|EnvLEnvLSEnvEnvS0| EnvLL<a := 2 + 3 | Env0>=> <a := 5 | Env0>=> Env0&{a = 5}<a := 2 + 3; b := a * 4 ; a := b - 5| Env0>=> <b := a * 4; a := b - 5 | { a = 5}>=> {a = 5}=> {a = 5}=> <b := 5 * 4; a := b - 5 | { a = 5}>=> <b := 20; a := b - 5 | { a = 5}>=> <a := b - 5 | { a = 5, b = 20}>=> <a := 20 - 5 | { a = 5, b = 20}>=> <a := 20 - 5 | { a = 5, b = 20}>=> <a := 15 | { a = 5, b = 20}>=> { a = 15, b = 20}Control Flow is Not Much