Why Use Annotations?

Because they add real value to code.

Here are some examples:

Annotations record programmer intent.

Some safety problems are obvious – for instance, in most programming languages, it’s illegal to access an array outside the array bounds, and we don’t need to annotate this requirement because (most) tools already know to check for buffer overflow problems.

When safety problems aren’t obvious, however, it becomes important to annotate the code with the programmer’s intent. For instance, whether or not an automated control will reliably turn off a heat source when temperature becomes excessive is a correctness (and safety) issue that can only be checked if the programmer states the intent of the components of the control software.

Annotations summarize the code or state its intention at a higher level.

Good annotations will state what is to be done, while the code specifies how this is to be accomplished. As a simple example, an annotation might state that a variable averageSalary contains the average of all the salaries in a data structure, while the code specifies how to obtain each salary field, count and sum them, and compute an average.

Another example would be a group of procedures that implement operations on sets. The annotation would be written in terms of sets, but the code might be written in terms of lower-level structures such as arrays. The best annotations will use an appropriately high level of abstraction, so that it is relatively clear to the reader that the annotation is correct. The code will need to implement a specific data structure and be appropriate optimized, and an automated tool will then ensure that the annotation and implementation are consistent.

Annotations on individual procedures (called modular specifications) help localize errors.

For example, if a pointer is NULL in a calling routine and thus causes a crash in a called routine, we don’t know whether the caller or the callee is at fault. But if an annotation specifies that the parameter must not, or alternately, may be, NULL, then we know that the fault is in the caller or the callee, respectively.

Annotations can state what must not happen.

Security problems often occur when software allows unintended behavior to occur, that is outside the expected scope of operation. By carefully specifying in annotations what the software should and shouldn’t do, tools can significantly help to reduce security vulnerabilities.