I want to define a semantics of a DSL through transition semantics. For my DSL I defined the syntax and implemented a code generator. Although I can provide a demo by giving examples, I want to write the semantics of my DSL to provide a formal specification of it.
However I don't know how to do it!. Can someone provide me with an example?