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.

  • 2
    $\begingroup$ The input format for the tool OTT uses ASCII and looks like type/operational semantics rules. Maybe you could use that. $\endgroup$ – Dave Clarke Jul 24 '12 at 6:46
  • $\begingroup$ Why can't you use UTF8? $\endgroup$ – Raphael Jul 24 '12 at 8:53
  • $\begingroup$ @Raphael, How does UTF-8 help me here? $\endgroup$ – Mike Samuel Jul 24 '12 at 16:51
  • $\begingroup$ @MikeSamuel: It has loads of nice math symbols that might come in handy if you want to write formulae. Of course, you'd need help users entering them. $\endgroup$ – Raphael Jul 24 '12 at 18:19
  • $\begingroup$ @Raphael, oh, by UTF-8 you mean unicode. Understood. $\endgroup$ – Mike Samuel Jul 24 '12 at 18:32

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.

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.