[Oberon] Eliminating RETURN statements

[Chris Burrows]

> -----Original Message-----
> From: Oberon [mailto:oberon-bounces at lists.inf.ethz.ch] On Behalf Of Diego
> Sardina
> Sent: Thursday, 9 April 2020 5:36 AM
> To: oberon at lists.inf.ethz.ch
> Subject: Re: [Oberon] Eliminating RETURN statements
> 
> This is the best way to write the algorithm, by putting the post-condition
> expression in the RETURN part.
> 
> I did something similar while porting Sets.mod to Oberon-07:
> 
> (* Oberon *)
> PROCEDURE Includes*(VAR s1, s2: ARRAY OF SET): BOOLEAN;
>   VAR i: INTEGER;
> BEGIN
>   i := 0;
>   WHILE i < LEN(s1) DO
>     IF s1[i] + s2[i] # s1[i] THEN RETURN FALSE END;
>     INC(i)
>   END;
>   RETURN TRUE;
> END Includes;
> 
> (* Oberon-07 *)
> PROCEDURE Includes*(s1, s2: ARRAY OF SET): BOOLEAN;
>   VAR i: INTEGER;
> BEGIN
>   i := 0;
>   WHILE (i < LEN(s1)) & (s1[i] + s2[i] = s1[i]) DO INC(i) END;
>   RETURN i = LEN(s1);
> END Includes;
> 
> The post-condition of the algorithm is (i = LEN(s1)) OR (s1[i] + s2[i] #
> s1[i]) but i = LEN(s1) suffice.
> 

What if LEN(s1) # LEN(s2), particularly if LEN(s2) < LEN(s1)?

Note that this is a problem with the original algorithm not necessarily your
translation.

Regards,
Chris Burrows
CFB Software
https://www.astrobe.com