From: "Chris Burrows" <chris@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_Tex... 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
On 2021-01-06 19:41, peter@easthope.ca wrote:
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".
We should also note that this is only the first step to make the program compile. If comprehensibility is the goal the variables named "continue", "done" etc. should ideally be replaced with something more descriptive and specific. When skimming through the program a loop like continue := TRUE; WHILE continue DO ... END; is not very informative. After the loop we know that `continue' is false but what does that imply? -- August
participants (2)
-
August Karlstrom -
peter＠easthope.ca