[Oberon] Multiple RETURN in a procedure
dsar at eml.cc
Mon Oct 24 09:56:37 CEST 2022
On Sun, Oct 23, 2022, at 10:18 PM, Skulski, Wojciech wrote:
> Diego Sardina wrote:
>> In structured programming and in formal verification of programs the return statement is a mistake and it's a fact, not a personal view.
> 1) Would you mind to provide a proof of your statement? It seems a bit
> unfounded at this point. Especially the "it is a fact" portion.
Briefly: formal verification requires an axiomatic language (such as Hoare logic) to describe the composition of the program and such languages require structured programming.
Structural irregularities can't be axiomatixed or can't be done easily, Joerg wrote a good example of a prematured return inside a loop that can't be axiomatixed (or it would require a complicated description that is not worth the effort).
On Sun, Oct 23, 2022, at 10:23 PM, Skulski, Wojciech wrote:
> I repeat my question: what are those significant gains of breaking lots of code?
If you want to know if there is a performance gain, no.
Goto-free code is (in most case) slower and sometimes lead to complications in the formulation of a new one. The gain is all about regularity, simplicity and verifiability of the program.
This is further discussed in the article below, especially starting from page 6 - Simplicity of composition schemes, but the whole document is worth to read, there are also some guidelines on how to convert some code to be goto-free.
Wirth - On the Composition of Well-Structured Programs.
An interesting part in the conclusion (about converting algorithms to equivalent goto-free forms):
"Skeptics will, of course, doubt that these methods represent any progress over the techniques of the old days - in fact, that they are methods at all. I can merely say that in my own experience, the new approach has improved my attitudes and abilities towards programming very considerably, and the experiences of others confirm this impression."
More information about the Oberon