ContinueCase and RestartCase?

[jchd]

I mean, in a state machine, your code is basically:

do
  select
    if conditions for state_A are realised then perform relevant actions and switch to state_K
    if conditions for state_B are realised then perform relevant actions and switch to state_U
    if conditions for state_C are realised then perform relevant actions and switch to state_X
    ...
    if no condition is realised then red alert as there is a specification hole
  end
until stop_run
 

[czardas]

Your descriptions are interesting as usual.

[jchd]

I ain't being pedantic. Just old (call me seasonned if you wish) as, when you face a machine with 18000+ possible states and myriads of associated conditions, you better avoid gotos as hell else your code will be a giant mess full of hidden bugs that your next collegue won't be able to find in decades.

That's why mission-critical software where dependability is an absolute prerequisite is specified and developped by formal methods. Is such framework, you have to mathematically prove (a very strong word!) that preconditions are satisfied before "perform relevant actions from state_X to state_Y" (thus proving that you're allowed to perform some action here) AND prove that postconditions are also satisfied (proving there that your actions never have any unexpected side effect). With the right tooling, you can then "refine" abstract formal specifications down to computer code with a complete mathematical proof of correctness covering 100% (not 99.999999...%) of the baby and without the need to test anything.

I've used a number of formal specifications/methods but none can cope with non-block structure, just because allowing gotos in the middle of somewhere precludes checking preconditions and postconditions, ruining the whole process.

Such formal projects always start with very abstract specifications that, once formalized, become the fundamental invariants of the machine. Note: the term machine here comes from formal methods but doesn't refer to any form of physical implementation. For instance you can build a formal model (a machine) of a series of laws and confront them to their invariants --the applicable constitution-- to check if they are constitutional or not. The theorem prover will insist that you formally specify first in which cases the laws are applicable or not, hereby checking that there is no specification hole. The keywords are completeness and correctness.

Basic machine invariants are the crux of safety in general. For instance, the main invariant of a train speed/brake control system (both on board and at ground) is awfully simple but abstract: "the speed of the train must always be such that the distance to any obstacle (known to the whole system) remains strictly positive". Once that invariant is proven to be satisfied at all time in the final code, you can be 100% certain that the speed/brake subsystem won't let the train hit a knocker or pass a red signal (stop) or hit another train unless the speed is zero (which you can infer is fairly harmless).

If you interest asks for more, start here (I've worked as a project leader in J-R Abrial group, the inventor of the B-method). B method is the exact counterpoint of Floyd's well-know paper ("Assigning Meanings to Programs") in that Abrial authored "The B-Book: Assigning Programs to Meanings". Note: Abrial's book is definitely NOT for the faint-hearted!

Indeed, it sound pretty much logical to derive a program, using strong derivation rules, from a strict, unambiguous description of the work to be done, rather than having a full software written and then only examine it in an attempt to understand what it actually does in full detail.

In short there are good reasons why a strict block structure is always preferable, unless you need to hastily write a 50-line .au3 to reformat a test file for CSV processing.

[czardas]

That's a brilliant explanation. I was thinking specifically of the real-world goto scenario which forms the basis for many musical repeat instructions. Changing the format is certainly doable, but doing so may add unwarranted complication. My example is very specific and not generally relevant in many other situations. Still, what already exists should not be ignored. This will have to be a short response right now because I have some time constraints.

[jchd]

Yes of course, there are many real-world scenarii where a hammer isn't the right tool and others where legacy prevails. Yet, there are also ubiquitous cases where a formal development would be a winner. Think OS for instance.

Granted, a modern OS is a monster but having built the first version on strong feet would have greatly helped making more complex successors correct (I mean robust = bug-free). I find it nonsensical to limit robust OSes to mission-critical systems, as the gross loss in countless trillions of work hours and disastrous consequences of zillion bugs in worldwide laymen OSes has been (or is, or will be) much more costly than having spent the time, money, energy and rigor to make it/them correct in the first place.

But as you know that money governs instead of brains, you also know that it won't happen anytime soon.

[czardas]

57 minutes ago, jchd said:

money governs instead of brains

How true indeed. It's very difficult to build any kind of foundation in an ocean of fish all swimming in the opposite direction. The human condition is frequently an obstacle, both to ourselves as well as to others. This is all too philosophical for me right now though: I just like to admire the great work of the masters and be content to play around with the concepts. 

[kylomas]

1 hour ago, jchd said:

Granted, a modern OS is a monster

Perhaps they were trying to make spaghetti...

[jchd]

... with a secret sauce !

[czardas]

... made from fish brains !