[Prev][Next][Index]
Re: LSL boolean combinations involving undefined terms (and CJ's article)
One more thing in regrad to my earlier posting ...
Of course, in a Larch *Interface* specification, you can declare
properties of a factorial function, leaving the implementation
unconstrained by the extraneous behavior of the trait function
on negative numbers.
For example in Larch/C++...
uses JonesExample2; // the trait from the earlier message
int factorial(int x) {
requires x >= 0;
ensures result = fact(x);
}
This is the power of the two-tiered approach. There's probably a discussion
of this in Wing's thesis, among other places.
It may be of interest that in Larch/C++, one can also specify
nontermination in other cases, specifying exactly the least fixed point
(of the usual code) if desired....
int factorial2(int x) {
// case 1
requires x >= 0;
ensures result = fact(x);
example x = 3 /\ result = 6;
// case 2
requires x < 0;
ensures liberally false;
example x = -1 /\ post = bottom;
}
In the above, there are two cases, the second of which is a partial
correctness specification, while the first talks about termination.
See the Larch/C++ manual for details.
Gary Leavens
--
229 Atanasoff Hall, Department of Computer Science
Iowa State Univ., Ames, Iowa 50011-1040 USA / leavens@cs.iastate.edu
phone: (515)294-1580 fax: (515)294-0258 ftp site: ftp.cs.iastate.edu
URL: http://www.cs.iastate.edu/~leavens/homepage.html
Reference(s):