[Oberon] Eliminating RETURN statements

[Diego Sardina]

On Wed, Apr 8, 2020, at 11:41 PM, Chris Burrows wrote:
> 
> 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.

You are right, indeed the code has also a pre-condition as ASSERT:

PROCEDURE Includes* (s1, s2: ARRAY OF SET): BOOLEAN;
  VAR i: INTEGER;
BEGIN
  (* ASSERT(LEN(s1) <= LEN(s2)); *)
  i := 0;
  WHILE (i < LEN(s1)) & (s1[i] + s2[i] = s1[i]) DO INC(i) END;
  RETURN i = LEN(s1)
END Includes;

If I rember correct that ASSERT wasn't there in the original Sets.mod.

My programming style is a bit changed compared to more than 10 years ago. Today I would leave that ASSERT there (uncommented) since that pre-condition must be always satisfied.

Correctness is more important than performance.

--
Diego Sardina