Footnotes

 

(1)

The annotations lead to proof obligations, which can be later discharged with a theorem proving tool, increasing the trust in the correctness of the specifications.  

(2)

Well, to let the specifications pass the static analysis, we had to make some minor modifications: we had to add explicit fitting morphisms for instantitations of generic specifications. These modifications are contained only in the ASCII distribution.  

(3)

We have rewritten the annotations as comments. Further we had to fix errors caused by the translation with hyperlatex: sometimes the space character disappears, sometimes a space character appears and makes two operator names from one operator name, the comment signs %% appear in another line than the comment etc. We would greatly appreciate if some LaTeXpert could design a style file (along the lines of Peter Mosses's casl.sty) for a good ASCII output.