An Experiment in Program Annotation ∗

It has been for a long time, and it still remains an open question how to annotate programs. We discuss the problem and describe a notational system of our own invention that we use for some time. Although simple, it proves very useful. Defining what we aim at Computer programs are very complicated formal objects. Often it is difficult not only to reason about a program but even to understand, by reading, what it does. That is why it is important to properly annotate code where necessary. By ‘annotating ’ we mean documenting that states program’s requirements and obligations and clarifies its working. Of course, efforts should be exerted to make programs as self-evident as possible, but this has its limits. Even very short programs, no matter how carefully written, may be impossible to comprehend without accompanying explanations; this is inevitable. The more algorithmically complex a program is, the more it needs annotation. How do we write code annotations? We certainly want to be as explicit as possible but without being too wordy, for then the code itself would be lost in the accompanying explanations and the effort of making them would be doubtful. Hence, what we need is