Notation for operational semantics that can be used in code comments
-
16-10-2019 - |
Question
I'm defining an intermediate language for a multi-backend code generator that I'm writing. I want to document the operational semantics for this intermediate language in a way that is readable both from within the source code and generated documentation (ocamldoc). The notation introduced used in "Types and Programming" languages is great for a book, but I don't want to try to do the prerequisite over conclusion style notation via ASCII art.
Is there a widely recognized notation for operational semantics that doesn't require non-ASCII characters? I looked through various RFCs but can't find any that use a non-natural language way of specifying semantics.
Solution
The input format for the tool OTT is based on ASCII and the rules look very much like type system/operational semantics rules. Maybe you could use that format. I'm sure that the parser for the input format is available as open source.