В книге "Programming with Specifications" David Luckham-а есть следующая строчка:
> -- Цитата:
> The idea of virtual text is very simple: "write a program to describe a program, but keep the two programs separate." Virtual text is the separating feature.
и еще есть следующие интересные предложения:
> -- Цитата:
> Another observation is that most informal comments can be expressed in a formal language similar to the programming language itself. It is called  because precise rules define its syntax and semantics. Comments written in a formal language are called . They can be parsed, checked for semantic validity, and translated into an executable form by techniques similar to those used in compiling a program.

Насколько я понимаю, ANNA - это как бы препроцессор над Ada. Виртуальный текст находится в комментариях относительно исходной Ada программы. Но препроцессор ANNA распознает виртуальный текст (обычные комментарии в Ada "--", а формальные аннотации "--|") и вставляет определенные assert в нужных местах, то есть, насколько я понимаю таким образом они компилируют как бы debug версию, которая в run-time проверяет различные утверждения. Также формальные аннотации могут быть проверены формально, различными автоматическими верификаторами. Когда же нужно предоставить программу заказчику, то они компилируют release версию без дополнительных assert из ANNA. (Возможно, не совсем так, но я так понял).

Соответственно и для Oberon можно сделать формальные комментарии, которые относительно обычного компилятора будут просто комментариями, а специальный препроцессор (можно назвать его ANNO - ANNotated Oberon) сможет обрабатывать их и создавать специальную версию программы, которая будет работать и в то же время проверять саму себя.