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. Some back-ends of the K tool, such as those enabled with the --latex, --pdf and the --html options to the kompile tool, know how to interpret such annotations.

There are three types of comments, which we discuss next.

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. Note that we can simply use any Latex commands, including sections, subsections, mathematical symbols, and so on.

Once we are done typing the annotations, we can kompile lambda.k with a document generation option, say --pdf, and take a look at the generated PDF document. Other options are also possible, for example --html and --latex. The latter is particularly useful when you want to incorporate documentation generated by the K tool into your papers. Feel free to experiment with these options.

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.

MOVIE (out of date) [6'07"]