- ... Leavens1
- Leavens's work was
supported in part by NSF grants CCR-9593168 and CCR-9803843.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
- ...
operator2
-
The specifications in Object Orientation in Z
[45]
are a bit vague on exactly what capabilities are needed by
the scalar type.
As there is no easy way to implement an exact length function
(because some lengths are irrational)
the specification in PreVector allows
the length operator to return an approximate result.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
- ... clause3
-
Following Leino's work [34],
if an object o mentioned in a modifies clause has been declared to depend
on some other object o', then o' may also be modified.
The same qualification is also applied to the trashes clause.
But this qualification is not needed to understand the examples in this paper.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
- ... variables4
-
Indeed, Larch/C++ is the only Larch-style BISL for which
abstract models can be given by using specification variables.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.