[Prev][Next][Index]

Re: Control in interface spec languages

The topic that Chris has brought up is an interesting one,
and one that I've been thinking about for Larch/C++.
I guess I had missed the "control" variable in my reading of Larch/C,
and we could certainly add that to Larch/C++.

Another way of approaching this comes from my reading (and teaching) of 

  Wim H. Hesselink, Programs, Recursion, and Unbounded Choice.
  Cambridge, 1992.

(which builds on ideas of Greg Nelson, Dijkstra, and others.)
In this book, Hesselink gives a weakest precondition semantics to
a small programming language using both a weakest-precondition (wp)
and weakest-liberal precondition (wlp) predicate transformer.
That is, he characterizes commands using 2 kinds of specifications
both total correctness (wp) and partial correctness.
The model of execution that goes with this is roughly that a command
can "refuse to execute" (as in a guard or test for an if-statement),
and if it does "want" to execute, then it may either terminate or not.

For example, the specification of abort is,
	for any predicate P:
	wp(abort(), P) = false
	wlp(abort(), P) = true
This says: when you call abort, it's not guaranteed to terminate and ensure P,
and when you call abort, it always either fails to terminate or terminates
in a state in which P holds.  That means, of course, that it can never
terminate, because we have
	wlp(abort(), false) = true,
which says that it always either fails to terminate or terminates
in a state in which false holds.

My idea for Larch/C++ is to allow one to write:
	ensures liberally P;
for a partial-correctness specification.
For example, one could write

	int fact(int n) {
	  uses FactorialTrait;
	  ensures liberally result = n!;
	}

which means that, when calls terminate, the result is the factorial of n.
(A valid implementation would be an infinite loop;
another implementation would loop only on negative arguments.)

To get back to the control issue, the idea of liberal specifications
meshes well with the case analysis feature of Larch/C++.
To give an example of that first, consider the following.
(In C++, "throw(FactError)" says that the procedure can signal an exception,
and in Larch/C++, "thrown" is used like "result" for exceptions.)

	uses FactorialTrait;
	import FactError;

	int fact(int n) throw(FactError) {
	  requires n >= 0;
	  ensures result = n!;

	  requires n < 0;
	  ensures thrown(FactError) = mkFactError;
	}

The above says the same thing as the following equivalent.

	uses FactorialTrait;
	import FactError;

	int fact(int n) throw(FactError) {
	  requires n >= 0 \/ n < 0;
	  ensures ((n >= 0) => result = n!)
		  /\ ((n < 0) => thrown(FactError) = mkFactError);
	}

(See the manual for details).

Now, here's where these ideas come together...
In Larch/C++, with this addition one could write the following,
as the specification of the C++ procedure abort

	void abort() {
	  requires false;
	  ensures true;

	  requires true;
	  ensures liberally false;
	}

(This wouldn't have a single case equivalent specification...)
Any reaction to this idea?

	Gary
Reference(s):