Browse Books

Reviewer: Daniel M. Berry

The name ANNA stands for Annotated Ada. It is the form of the Ada language in which specially marked comments serve as formal annotations about the program to which they are attached. Much has appeared in the literature about ANNA in the past few years while it was being developed. It is nice to have a single document containing all the current information on the language. The book was a disappointment in that it does not present much new beyond what has already been published. To be fair, however, the purpose of the monograph series that contains this book is to publish manuscripts describing work in progress. Therefore, I am evaluating the book relative to this goal. The organization of the book is just right for it to be used for a variety of purposes without boring the reader. If one desires a general overview hitting the basic principles of Ada program annotation, she or he can just read section 1 and it will be enough. This section explains the concept of virtual Ada text (Ada statements containing expressions extended with quantifiers and constrained not to have side effects on variables not declared in virtual text) and annotations (assertions) and their semantics. One may execute annotations while the containing program is being executed in order to get run-time verification that the annotations are not false for that particular execution of the program. Alternatively, she or he may subject the annotated program to a formal verification of the consistency of the program with the annotations. The implementation of the latter is apparently left to future work. If one is interested in more than just an overview and wants to understand the basic kinds of annotations, she or he can read the beginnings of sections 3 through 13, concentrating on section 7. Section 7 discusses annotations of Ada packages and is applicable to any other language with a data abstraction module construct. Finally, one could finish each section for all of the gory details. As with most programming language manuals, however, these details are so repetitious that they get boring after a while. Because I am working on program verification, I really appreciated getting to review this book. I learned a lot and recommend this book to anyone working or interested in the area.