Re: Dijkstra's guarded commands

Andrew Haley <andrew29@xxxxxxxxxxxxxxxxxxxxxxx> writes:
Anton Ertl <anton@xxxxxxxxxxxxxxxxxxxxxxxxxx> wrote:
Andrew Haley <andrew29@xxxxxxxxxxxxxxxxxxxxxxx> writes:
Generating randomness at runtime where none is needed is surely
inefficient. It can't possibly make any difference to the correctness
of a program, so why do it?

Well, doing a deterministic implementation might turn incorrect
(according to the specification) programs into programs that behave
correctly, whereas this is more unlikely with a random
implementation.

I don't accept that. Here's another incorrect program:

i := 0; j = 0
do
i = 0 -> j := j + 1
| j = 0 -> i := i + 1
od

On a system that used randomness at runtime, this incorrect program
would eventually terminate. I don't think that randomness making a
program appear to work is necessarily more likely than randomness
making a program fail.

In my experience, failing to make progress is a rare bug, and it
usually also shows up in incorrect behaviour in other respects (so the
usual errors of this kind would be visible even with a randomizing
implementation).

OTOH, having a mistake in the rest of the action logic or in the
selection logic is relatively frequent, and if it shows up only in
corner cases, it can stay in programs for a long time, especially if
the corner case can never be excercised because a conditional prevents
it.

That's why I believe that determinism is more likely to cover up such
issues than randomness. OTOH, if we then make that determinism part
of the specification, the program is no longer incorrect, and the
language is better testable.

Of course, Dijkstra's idea of programming (at least later in his life)
was to write the program on paper and prove it correct before ever
letting it run on a computer.

For this approach, the actual implementation is irrelevant, and the
non-deterministic specification is nicer than, e.g., the deterministic
one outlined above, because then one only has to deal with one branch
at a time. In contrast, with a deterministic order, programs are
correct that would otherwise be incorrect, and proving them correct
then requires to look at the combination of conditions when dealing
with a particular branch.

- anton
--
M. Anton Ertl http://www.complang.tuwien.ac.at/anton/home.html
comp.lang.forth FAQs: http://www.complang.tuwien.ac.at/forth/faq/toc.html
New standard: http://www.forth200x.org/forth200x.html
.

Relevant Pages

  • Re: A misapplication of probability theory in exam grading
    ... I don't think it was an attempt to remove randomness, ... arrange so that random guessing doesn't score better than not ... normal system and then do a final subtraction of (number of ... people more than giving negative scores for incorrect answers. ...
    (sci.math)
  • Re: Java encryption implementation
    ... this could help an attacker to crack it.) ... Incorrect. ... Randomness and unpredictability are equivalent. ...
    (sci.crypt)
  • Re: real random
    ... One might say that the randomness of the ... A chaotic process is unpredictable in the long run, ... PRNG gives you 100% predictability if you know the algorithm and the ... "universal" determinism or indeterminism, however, in this case this ...
    (comp.lang.c)
  • Re: real random
    ... One might say that the randomness of the ... A chaotic process is unpredictable in the long run, ... "universal" determinism or indeterminism, however, in this case this ...
    (comp.lang.c)
  • Re: PI random? Debate running in circles (you try making math jokes)
    ... underlying bedrock of determinism somehow. ... at the beginning of the universe quantum mechanics was NOT random at ... The indeterminacy which you ... what this means for understanding randomness? ...
    (sci.math)