Path: utzoo!attcan!utgpu!jarvis.csri.toronto.edu!rutgers!ucsd!ames!uhccux!munnari.oz.au!murtoa.cs.mu.oz.au!otc!metro!bunyip!moondance!batserver.cs.uq.oz!gjc
From: gjc@batserver.cs.uq.oz (Cumming)
Newsgroups: comp.lang.eiffel
Subject: Implies
Message-ID: <1473@moondance.cs.uq.oz>
Date: 9 Sep 89 05:08:49 GMT
Sender: news@moondance.cs.uq.oz
Reply-To: gjc@batserver.cs.uq.oz
Organization: Computer Science Department, The University of Queensland, Brisbane, Australia
Lines: 23

Again with respect to the call for suggested changes to the language, may I 
suggest the following

	1.	The unwieldy 

			not P or Q 
			not P or else Q

		be supplemented by

			P implies Q
			P limplies Q

		where limplies is a "lazy" implies, i.e. Q is not executed if
		P is false, as per not P or else Q.

		Maybe not a great change, but certainly makes reading an
		assertion a bit easier.

These queries have arisen out of my attempts to formalise the translation of
specifications written in the Z specification language into Eiffel. 

G.J.Cumming