<div dir="ltr"><div>There is one publication on the subject:</div>
<h3>The Formal Specification of Oberon</h3>
            
            <p>
              <strong> Philipp W. Kutter</strong> (Eidgenössische Technische Hochschule, Switzerland)<br> 
              
            </p>
            
            <p>
              <strong> Alfonso Pierantonio</strong> (Università di L'Aquila, Italy)<br> 
              
            </p>
                    
            <p>
              <strong>Abstract:</strong> This paper presents the formal 
specification of the programming language Oberon. Using Montages we give
 a description of syntax, static, and dynamic semantics of all 
constructs of the language. The specification is arranged in five 
refinement steps, each of them results in a working sub-language of 
Oberon. The compactness and readability of the specification make us 
believe that it can be used for a reference manual. 
            </p>
            <p>
              <strong>Keywords:</strong> Montages, Oberon, abstract state machines, programming languages specifications, reference manuals 
            </p>

<div><a href="http://www.jucs.org/doi?doi=10.3217/jucs-003-05-0443">http://www.jucs.org/doi?doi=10.3217/jucs-003-05-0443</a></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Jan 7, 2021 at 9:47 AM Frans-Pieter Vonck <<a href="mailto:fp@vonck.nl">fp@vonck.nl</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">In Oberon Steps Beyond Pascal And Modula:<br>
"[..]we formally define the control structures by means of predicates <br>
and their transformation rules."{pg. 47, Chapter 5: Control Structures.<br>
<br>
"The danger of using the repeat statement lies in the fact, that the <br>
statement sequence is not guarded by an explicit condition.[..] In <br>
general it is wise to use the WHILE statement whenever REPEAT does not <br>
offer a clear advantage." (pg.58)<br>
<br>
Interesting is that the LOOP statement is not formally defined in this <br>
book, see 5.2.5.<br>
Probably due tot the fact that there are multiple exits.<br>
Also the FOR statement is not formally defined (pg. 273).<br>
<br>
It is possible I've overlooked some good explanations about this <br>
subject.<br>
What is your favorite examples of formal definitions of control <br>
structures in Wirth's work?<br>
<br>
Grts,<br>
F.P.<br>
<br>
<br>
Chris Burrows schreef op 2021-01-07 07:16:<br>
>> -----Original Message-----<br>
>> From: Oberon [mailto:<a href="mailto:oberon-bounces@lists.inf.ethz.ch" target="_blank">oberon-bounces@lists.inf.ethz.ch</a>] On Behalf Of<br>
>> Skulski, Wojciech<br>
>> Sent: Thursday, 7 January 2021 1:53 PM<br>
>> To: ETH Oberon and related systems<br>
>> Subject: Re: [Oberon] [EXT] LOOP conversion<br>
>> <br>
>> Andreas:<br>
>> <br>
>> >I have a sneaking suspicion that the participants in this discussion<br>
>> >have (probably?) already spent more time on this question than the<br>
>> time<br>
>> >it would take to add LOOP to the compiler ;-)<br>
>> <br>
>> I would if I could. But there are some limits to my knowledge and<br>
>> skills. I know how to do many things, but not this one.<br>
>> <br>
>> Other users are in a similar situation. Not every user is capable to<br>
>> define a language and to implement or change the compiler.<br>
>> <br>
>> We are at your mercy.<br>
>> <br>
> <br>
> I believe in that clichéd quote "Give a man a fish and you feed him for <br>
> a<br>
> day. Teach a man to fish and you feed him for a lifetime".<br>
> <br>
> How much of your time would you be prepared to invest to learn how to <br>
> add<br>
> LOOP and multiple EXITs to Wirth's published Project Oberon Oberon-07<br>
> compiler?<br>
> <br>
> If you give a reasonable answer I am prepared to give you (and anybody <br>
> else<br>
> watching this list) step by step instructions of the approach you can <br>
> take<br>
> to achieve it. As far as compiler modifications go it is relatively<br>
> straightforward. The completed exercise consists of approximately 20<br>
> additional statements in two of the compiler modules and makes use of<br>
> existing code generation procedures. Once you have completed those <br>
> steps you<br>
> should have learnt enough to be able to add multiple RETURNs as well <br>
> with<br>
> little or no assistance and to make similar changes to Andreas's source <br>
> code<br>
> if you want to build on that instead.<br>
> <br>
> Step 1. Prepare an environment to allow you to edit the compiler source<br>
> code, compile it and execute it.<br>
> <br>
> I expect that you will find it to be a very empowering exercise. The <br>
> only<br>
> fear I have is that once "the genie is out of the bottle" there will be <br>
> no<br>
> putting it back ;-)<br>
> <br>
> Regards,<br>
> Chris Burrows<br>
> <a href="https://www.astrobe.com" rel="noreferrer" target="_blank">https://www.astrobe.com</a><br>
> <br>
> <br>
> --<br>
> <a href="mailto:Oberon@lists.inf.ethz.ch" target="_blank">Oberon@lists.inf.ethz.ch</a> mailing list for ETH Oberon and related <br>
> systems<br>
> <a href="https://lists.inf.ethz.ch/mailman/listinfo/oberon" rel="noreferrer" target="_blank">https://lists.inf.ethz.ch/mailman/listinfo/oberon</a><br>
--<br>
<a href="mailto:Oberon@lists.inf.ethz.ch" target="_blank">Oberon@lists.inf.ethz.ch</a> mailing list for ETH Oberon and related systems<br>
<a href="https://lists.inf.ethz.ch/mailman/listinfo/oberon" rel="noreferrer" target="_blank">https://lists.inf.ethz.ch/mailman/listinfo/oberon</a><br>
</blockquote></div>