An informal description can be used escape the rigor of formal specification. In Larch/C++ an informal description can be used anywhere an equality-term can be used, which allows it to be used as a conjunct or disjunct of a predicate, for example. This syntax is also used in other places in Larch/C++ where informal specification is permitted. (See section 9.2 The Uses Clause for how abstract values can be informally described. See section 6.9.1 Examples in Function Specifications for how examples can be described informally.)
Informal descriptions have the following syntax.
informal-desc ::= informally string-literal [ string-literal ] ...
| informal-comment
The first form is more wordy, but that may be useful in communicating with
users who are not very familiar with Larch/C++.
An informal-comment has the syntax (% ... %)
(see section 4.12 Informal Comments for the detailed syntax), and is more useful when
writing multi-line comments than the first form.
For example, the following specification uses an informal precondition, and an informal postcondition.
// @(#)$Id: isqrt-informal.lh,v 1.5 1999/01/11 21:20:14 leavens Exp $
extern int isqrt(int x) throw();
//@ behavior {
//@ requires informally "x is not negative";
//@ ensures (% result is an approximation to
//@ the square root of x %);
//@ }
Informal descriptions are considered to have sort Bool,
and thus should be written as true or false statements.
If the find yourself describing some activity,
you should rephrase your statement to describe the result of that
activity.
The use of informal descriptions allows the level of formality of a Larch/C++ specification to be tuned to some extent. That is, one can write completely informal statements about the behavior of a function, later make some parts of the informal statements formal, and still later refine these into completely formal statements. For example, the following specification has a completely formal precondition, and a partly informal postcondition.
// @(#)$Id: isqrt4.lh,v 1.5 1999/01/11 22:05:52 leavens Exp $
extern int isqrt4(int x) throw();
//@ behavior {
//@ requires x >= 0;
//@ ensures result >= 0
//@ /\ (% result is an approximation to
//@ the square root of x %);
//@ }
(See section 10.2 Class Refinement for how to do this within Larch/C++.)
However, if you need to use informal descriptions to get around some limitation
of Larch/C++, we ask that you tell us about the problem instead
(send e-mail to lc++@cs.iastate.edu),
so that we may consider enhancing the language.
If you wish to add informal explanation to a formal Larch/C++ specification,
you can also use comments (see section 4.2 Comments).
See section 10.2 Class Refinement for an example using informal descriptions.
Since informal descriptions have no formal semantics, nothing further can be said about them. Hence the rest of this manual largely ignores informal descriptions. (Any formal semantics of Larch/C++ would only apply to specifications that did not use informal descriptions.)
Go to the first, previous, next, last section, table of contents.