Re: Building blocks (Was: Design By Contract)

[Paul M Gover <Paul_Gover@uk.ibm.com>]

Anonymous wrote:
> ... 
> > Makes sense to me. OTOH there is a school of thought that eschews
> > multiple exits. But that's another story. The point is, is that both
> > versions show in a minimum number of lines the various options one has
> > in Ada ( -83 at least, there are more in -95), which was the basic idea.
> 
> I'm aware of those who think multiple exits are bad. This is something
> that came out of program correctness proving. However, when you look at
> languages that only allow a single exit from a loop (Pascal, excluding
> gotos) you find many common situations in which this results in
> unreadable code. For this reason, "exit" and the possiblity of multiple
> exits were included in Ada, and are considered acceptable by all
> competent software engineers.
> ...

Some of my colleagues worked on a language which had a
	loop
		exit when
	end
construct, but with the restriction that each loop had
exactly one exit.  So it didn't allow multiple exits from
a loop, but still allowed:
	loop
		record = file.read()
	exit when file.eof()
		thing.accept(record)
	end
which keeps the code readable, and prevents duplication.
Does this have any impact on correctness proofs?
Presumably not much, as the loop can be converted to a
true while-loop by duplication.

(One of the while-loop problem is that for a tidy
record processing program you have to write
	record = file.read()
	Do while(~file.eof())
		thing.accept(record)
		record = file.read()
	End while
)

-- 
Paul Gover
IBM Warwick Development Group
Mumbling for myself, not IBM