[Oberon] Multiple RETURN in a procedure
fusionfile at gmail.com
Mon Oct 24 22:33:17 CEST 2022
On 2022-10-23 18:51, Skulski, Wojciech wrote:
>> 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;
IF x <= y THEN
result := x
result := y
ASSERT((result = x) OR (result = y))
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
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?
More information about the Oberon