[Oberon] Re (2): LOOP conversion

[peter at easthope.ca]

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.
https://en.wikibooks.org/wiki/Oberon/A2#Sources,_Tools_and_Configuration_Texts_in_A2

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 
step. 
 
Unrefined oberservations.

(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. 
 
Digression
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