[Oberon] Multiple RETURN in a procedure

[August Karlstrom]

On 2022-10-23 18:51, Skulski, Wojciech wrote:
> August:
> 
>> How do you add your postconditions to a procedure with multiple returns?
> 
> What kind of postconditions should I add to the following code? Why do I need any postconditions in this case?
> 
> PROCEDURE min (x,y: INTEGER) : INTEGER;
> BEGIN IF x < y THEN RETURN (x) ELSE RETURN (y) END END min;

I agree that no postcondition is necessary for this trivial function but 
if you added one it would be that the result is either x or y:

	PROCEDURE Min(x, y: INTEGER): INTEGER;
		VAR result: INTEGER;
	BEGIN
		IF x <= y THEN
			result := x
		ELSE
			result := y
		END;
		ASSERT((result = x) OR (result = y))
	RETURN result
	END Min;

To further emphasize that RETURN is not a statement but a clause, I 
prefer to indent it to line up with the procedure heading.

Another ugly aspect of return statements is that they potentially make 
the code lie. Consider this statement for instance:

	WHILE i < 100 DO
		...
	END

When we see the loop it's natural to conclude that it will go on until i 
 >= 100. However, with return statements there is no such guarantee.

What I would like to know is why the return statement was introduced in 
Modula-2. Was it to compensate for the removal of goto in Pascal?


-- August