Re: SPARK: missing case value

[Georg Bauhaus <bauhaus@futureapps.invalid>]

On 10.10.15 12:00, Dmitry A. Kazakov wrote:
> 
>> That's what clauses of contracts do: they state conditions.
>> "Don't touch it or it'll …!".
> 
> You are free to touch. Killing you is a proper execution of laws of physics
> when you jump head down from the sky scrapper...

Killed as agreed in the contract, so to speak.

>  aircraft shattered into pieces and burned down, check!

The system has failed to respond to assertion failure. That's what robustness
is about. https://en.wikipedia.org/wiki/Robustness_(computer_science)

> Post-conditions are *proved* to be implied by the pre-conditions. 

Uhm, no, post-conditions (after "Post => ") are stated, nothing more.
If someone proves implication (hopefully), that's only related.
(The work would be from the obligation part of DbC.)

> Proof /= check.

Absolutely. And contract based design encourages proofs, but proofs
need not be part of the contract. However, it is the right of either
party to misbehave if the contract was violated. Checks will help detect
violations.

>>>> [dynamic being more than static]
>>> No idea what this was supposed to mean.
>>
>> Dynamic predicates may express conditions that the compiler cannot
>> show to always be true,
> 
> They may not. The only way to express a condition to show it true.

Is "condition" to mean "state", then?

I think "X > 0" is a perfectly normal condition in the sense of
boolean_expression; also, in another sense, it expresses
the possible "conditions" in which variable X would be, making
the quoted text evaluate to True or False.

So, just write a predicate that takes a long time to compute, say, so
long that the compiler gives up (in some way), but is otherwise easily
stated and only assumed to be true, like a conjecture.

>>  Should the compiler reject known truths?
> 
> Known to who?

The experts. See previous discussions. Programmers will then
be able to draw conclusions from the stated truth.

> The compiler knows the language, nothing else, nothing more.
> The rest is bad philosophy.
> 
>> Or should it just perform the test at run-time if you tell it to do so?
> 
> There is no compiler at run-time.

Sorry, correction: "should [the compiler] just arrange for performing
the test at run-time?" That's instead of rejecting a predicate, just because
the compiler does not have the powers for "testing" all values at once by
formal demonstration.

I note that one can also demonstrate correctness by testing each
possible set of values, so a proof is not the only means. Just so much
more useful, early, possibly preventing exceptions, and likely fast enough,
unlike testing.

>> (*) "should …" above seems to imply the ideal situation of universally
>> correct programs. This seems wishful thinking. At the risk of repeating
>> old stuff, some designs are built on top of conjectures. Also,
>> unforeseen program states are pretty normal in many programs, and not all
>> of them will necessarily make the programs miss their stated goals.
> 
> So what?
> 2+2=4 even if you meant 2*2. That does not make it correct.

The outcome does make the programs "not ... miss their stated goals".
It does make the result correct even though the program did not
correctly implement some specification. So, the latter correctness ("*")
does not exhaust possible causes for programs apparently being correct,
that's all. (Seems better to me to have correct results, rather than
stop producing results at all because they could be got the wrong way.)

And that's what.

Also this: the paragraph was meant to emphasize that correct programs
seem to be a pipe dream in the sense that there will always only be
particular programs achieving some amount of correctness. But in general,
we need to write and debug programs without being hindered by some
expressions not being static or possibly failing. That seems more
practical than just giving up, dreaming the dream.


>  A program is correct (as defined)
> or not independently on the skills of any given programmer.

How do we know that some given program is correct or not?
By narrowing program design so that what is allowed in programming
needs to be statically decidable?

Should we prove larger systems correct or else not run them at all?

Contracts as in "contract based design" are, I think, not about after-the-fact
properties of a program. They exist prior to implementation.
Hopefully, skillful programmers will feel obliged to show that the contract
is good and that their programs follow the contract.