[Oberon] Multiple RETURN in a procedure

Skulski, Wojciech skulski at pas.rochester.edu
Sun Oct 23 22:18:51 CEST 2022

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.

2) I have not heard whether formal verification was ever applied to a the actual Oberon System 2013. We all probably care whether it works or not, rather than whether it can be formally verified, and what it would mean if it was verified.


More information about the Oberon mailing list