A Complete and Documented K Definition
In this lesson you will learn how to add formal comments to your K definition, in order to nicely document it. The generated document can be then used for various purposes: to ease understanding the K definition, to publish it, to send it to others, etc.
The K tool allows a literate programming style, where the executable
language definition can be documented by means of annotations. One such
annotation is the latex(_) annotation, where you can specify how to format
the given production when producing Latex output via the --output latex
option to krun, kast, and kprove.
There are three types of comments, which we discuss next.
Ordinary comments
These use // or /* ... */, like in various programming languages. These
comments are completely ignored.
Document annotations
Use the @ symbol right after // or /* in order for the comment to be
considered an annotation and thus be processed by the K tool when it
generates documentation.
As an example, we can go ahead and add such an annotation at the beginning of the LAMBDA module, explaining how we define the syntax of this language.
Header annotations
Use the ! symbol right after // or /* if you want the comment to be
considered a header annotation, that is, one which goes before
\begin{document} in the generated Latex. You typically need header
annotations to include macros, or to define a title, etc.
As an example, let us set a Latex length and then add a title and an author to this K definition.
Compile the documentation and take a look at the results. Notice the title.
Feel free to now add lots of annotations to lambda.k.
Then compile and check the result. Depending on your PDF viewer, you may also see a nice click-able table of contents, with all the sections of your document. This could be quite convenient when you define large languages, because it helps you jump to any part of the semantics.
Tutorial 1 is now complete. The next tutorial will take us through the definition of a simple imperative language and will expose us to more feature of the K framework and the K tool.