Following the lead of LSL and Tan's work on LCL [Tan94], Larch/C++ includes several features that allow one to write checkable redundancy into specifications. Tan's work featured claims, which included the redundant postconditions found in Larch/C++. To this Larch/C++ adds several new kinds of redundancy: redundant preconditions, redundant framing, and examples. Examples were first described in [Leavens96]. The others are described in [Leavens-Baker99].
All redundant clauses do not affect the meaning of a specification. Instead they introduce things that one can check (e.g., with the Larch Prover).
Besides allowing for sanity checking of specifications, their main use is to point out things to the reader of the specification that are not needed otherwise. Stating them in the non-redundant parts of the specification, however, might cause people who are implementing or reasoning about the specification to do extra work. Also, when one has more than one way to specify a function, it may be best to retain both ways, putting one in a redundant clauses.
Go to the first, previous, next, last section, table of contents.