[m-dev.] runtime checking of assertions

[Fergus Henderson]

On 21-Jul-1999, Zoltan Somogyi <zs at cs.mu.OZ.AU> wrote:
> 
> There is another problem with runtime checking of assertions (pre- and post-
> conditions as well as exclusive and exhaustive assertions) that I haven't
> seen raised so far. This is that a large fraction (probably a significant
> majority) of the assertions that programmers would want to write are
> recursive. The precondition of a merge algorithm would be that the inputs
> are sorted, which is linear in the lengths of the lists; checking the
> precondition at each call would turn a linear merge algorithm into a
> quadratic one. I think a straightforward approach to the checking of
> assertions will introduce similar or worse slowdowns in sufficiently many
> cases to piss off programmers.
> 
> Clearly, what is needed is a way of checking assertions incrementally;
> i.e. checking only the part that other, recursive invocations of the same
> assertion will not check. This is doable (there have been algorithms designed
> to incrementally evaluate integrity constraints in databases that could
> probably be adapted, or mined for ideas), but it is not trivial.

One possible way of handling this would be to perform checks in full,
rather than incrementally, but to try to eliminate redundant checks at
compile time.  We could define two entry points for each predicate,
one checked, and one unchecked.  The checked one would check the
preconditions (in full), and then call the unchecked one. 
For every call, or at least for every recursive call, the compiler would
try to prove the preconditions of the callee from the preconditions of
the caller and the code in the caller which precedes that call.
If it could prove the callee's precondition was satisfied, then it
would call the unchecked entry point rather than the checked one.

This proof would be very simple in most cases, I think;
it could often be obtained by just unfolding the precondition of
the caller and then applying some very basic simplifications.

For example, consider the case of merge:

	:- pred list__merge(list(T), list(T), list(T)).
	:- mode list__merge(in, in, out) is det.

	:- inadmissable merge(L1, L2, _) unless sorted(L1), sorted(L2).

	sorted([]).
	sorted([S1,S2|Ss]) :-
		S1 < S2,
		sorted([S2|Ss]).

	list__merge(A, B, C) :-
		( A = [X|Xs] ->
			( B = [Y|Ys] ->
				( compare(<, X, Y) ->
					Z = X,
					list__merge(Xs, B, Zs)
				;
					Z = Y,
					list__merge(A, Ys, Zs)
				),
				C = [Z|Zs]
			;
				C = A
			)
		;
			C = B
		).

After conversion to SHF and common sub-expression elimination,
sorted/1 would look like this:

	sorted(L) :-
		( L = []
		; L = [S1|Ss], Ss = [S2|_], S1 < S2, sorted(Ss)
		).

For the first recursive call the compiler would need to prove that

		sorted(A), sorted(B),
		A = [X|Xs], B = [Y|Ys], compare(<, X, Y), Z = X
	implies
		sorted(Xs), sorted(Ys)


Unfolding the precondition of the caller gives

		( A = []
		; A = [SA1|SAs], SAs = [SA2|_], SA1 < SA2, sorted(SAs)
		),
		( B = []
		; B = [SB1|SBs], SBs = [SB2|_], SB1 < SB2, sorted(SBs)
		),
		A = [X|Xs], B = [Y|Ys], 

We can eliminate disjunctions by treating each case at a time.
For the first case, we get

		A = [],
		B = [],
		A = [X|Xs], B = [Y|Ys], compare(<, X, Y), Z = X

and then interpreting the unifications gives us `false',
which implies anything, so `sorted(Xs), sorted(Ys)' is satisfied in this
case.  The second and third cases are similar.
For the last case, we get

		A = [SA1|SAs], SAs = [SA2|_], SA1 < SA2, sorted(SAs),
		B = [SB1|SBs], SBs = [SB2|_], SB1 < SB2, sorted(SBs),
		A = [X|Xs], B = [Y|Ys], 

and interpreting the unifications gives us

		..., sorted(Xs),
		..., sorted(Ys),
		...

so we're done.

Of course the question is how often these techniques
(unfolding the caller's preconditions, eliminating disjunctions
by case analysis, and simplifying unifications using abstract
interpretation and the usual unification algorithm) are sufficient.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------