[Oberon] Re (2): LOOP conversion
peter at easthope.ca
peter at easthope.ca
Wed Jan 6 19:41:29 CET 2021
From: "Chris Burrows" <chris at cfbsoftware.com>
Date: Mon, 4 Jan 2021 20:49:56 +1030
> Here's a trickier example ... found in ETH Oberon - TextFrames.Menu:
Hello Chris & all,
My solution is 7th row from the bottom, 2nd column of the table.
Mulled it over during supper; then tried some typing with little
progress. Before taking it up again realized a better approach, for
me at least, was to convert all the LOOPs in the module beginning with
the easiest. You can see my conversions of procedures LocateString,
LocateChar, FlipSelection and Menu. LocateString was easy enough.
> I'd be interested to know how long it takes you ...
To convert LocateString, LocateChar and FlipSelection about 5 hours total.
One blunder necessitating a backtrack. About 2 hr and 45 minutes
to convert Menu. Worked in small steps, compiling and testing at each
(1) Isomorphism exists between LOOP texts and WHILE texts.
(2) Loops can be nested in a tree structure. At each level there can
be multiple loops and the number of levels is arbitrary.
(3) In the general case a continuation flag is needed for each level.
Eg. VAR continue0, continue1 ... : BOOLEAN;
(4) A LOOP having only one exit in the form "LOOP IF a THEN EXIT END;
... END" can be replaced with "WHILE ~a DO ... END".
(5) A LOOP having only one exit in the form "LOOP ... IF a THEN EXIT
END END" can be replaced with "REPEAT ... UNTIL a".
(6) Pattern "LOOP statements0 IF a THEN EXIT END; statements1 END"
becomes "continue := TRUE; WHILE continue DO; statements0 IF a THEN
continue := FALSE ELSE statements1 END END".
> ... time taken to prove to yourself that your conversion is
> identical in functionality.
Note (1) but I don't have a formal proof. Once I recognized the
conversion algorithm it was just a matter of doing it properly. Of
course dopey errors are easily made. Automation is the answer.
In a 2nd year course I learned a little about proof of correct
implementation. How much of the ETH Oberon, V4 and etc. source was
proven formally? I'd guess not much but might be wrong.
Regards, ... P. L.
Tel: +1 604 670 0140 Bcc: peter at easthope. ca
More information about the Oberon