[mercury-users] Newbie problem. :)

Thomas Conway conway at cs.mu.OZ.AU
Thu Jun 17 15:55:14 AEST 1999


On Thu, Jun 17, 1999 at 02:45:50PM EST, Richard A. O'Keefe wrote:
> In general, verifying that a negative rule is a consequence of
> the positive rules may be impossible.  That's one reason why
> you have to declare them.

Okay, so we're talking about two different, but related things,
both of which are worthwhile:
	(i) checkable declarations of mutual exclusion.
	(ii) uncheckable assertions of mutual exclusion.

(i) is useful for letting me export important information about
abstract entities - so that I can get determinism information out
from behind abstraction boundaries. Being checkable is good, because
it is another way in which the programmer and the compiler can
conspire to produce implementations that agree with the specification.

(ii) is useful for two kinds of thing:
	(a) doing the work of (i) for builtin types (as in the case of
	    the integer comparison operators).
	(b) giving the compiler high level information that it can't
	    figure out for itself,  which can allow people to write
	    programs in a natural way and have the compiler believe
	    that they really are deterministic.
The bit that worries me is the last, simply because unlike the other
declarations, it can't be checked; is intended for routine use by
users (unlike (ii)(a)); and can lead to broken programs.

Once again, I'm happy to be persuaded that I'm being too paranoid,
but I think paranoia is useful in a language designer. :-)
(Of course, I could be plain wrong too.)

Thomas
-- 
 Thomas Conway )O+     Every sword has two edges.
     Mercurian            <conway at cs.mu.oz.au>
--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------



More information about the users mailing list