Completing and Documenting IMP
We here learn no new concepts, but it is a good moment to take a break and contemplate what we learned so far.
Let us add lots of formal annotations to imp.k.
Once we are done with the annotations, we kompile with the documentation option and then take a look at the produced document. We often call these documents language posters. Depending on how much information you add to these language posters, they can serve as standalone, formal presentations of your languages. For example, you can print them as large posters and post them on the wall, or in poster sessions at conferences.
This completes our second tutorial. The next tutorials will teach us more
features of the K framework, such as how to define languages with complex
control constructs (like callcc), languages which are concurrent, and so on.