MMT | Maude MSOS Tool |

## Simple ExampleLet us define a very simple functional programming language in which there are only two possible operations: the sum of two expressions and the binding declarations using an Standard ML "let"-like construction. We begin by defining the module name and two sets: (msos SIMPLE-LANGUAGE is Exp . Id . We need an environment for the bindings, which is declared as a map
from identifiers to integers (the set Env = (Id, Int) Map . Now let us define the abstract syntax of our language using the following BNF declaration: Exp ::= let Id = Int in Exp end | Exp sum Exp | Int | Id . As for the actual dynamic semantics, we first need to declare a
Label = { env : Env, ... } . The remainder of the specification are the dynamic transition rules for the language constructions Exp1 -{...}-> Exp'1 -- -------------------------------------------- (Exp1 sum Exp2) : Exp -{...}-> Exp'1 sum Exp2 . Exp2 -{...}-> Exp'2 -- ------------------------------------------ (Int sum Exp2) : Exp -{...}-> Int sum Exp'2 . Int3 := Int1 + Int2 -- ----------------------------- (Int1 sum Int2) : Exp --> Int3 . Env' := (Id |-> Int) / Env, Exp -{env = Env', ...}-> Exp' -- ------------------------------------------------ (let Id = Int in Exp end) : Exp -{env = Env, ...}-> (let Id = Int in Exp' end) . (let Id = Int in Int' end) : Exp --> Int' . Int := lookup (Id, Env) -- -------------------------- Id : Exp -{env = Env}-> Int . sosm) In order to test this simple language, let us execute the following program: let x = 10 in let y = 10 in x sum y end end We begin by defining the two constants (mod TEST is including SIMPLE-LANGUAGE . ops x y : -> Id . endm) Then, rewriting the following term gives us the expected result: (rew < (let x = 10 in let y = 10 in x sum y end end) ::: 'Exp, { env = void } > .) rewrite in TEST : < let x = 10 in let y = 10 in x sum y end end ::: 'Exp,{env = void}> result Conf : < 20 ::: 'Exp,{env = void}> |