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