Re: SPARK: missing case value

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Sat, 10 Oct 2015 16:19:31 +0200, Georg Bauhaus wrote:

> On 10.10.15 12:00, Dmitry A. Kazakov wrote:
>> 
>>  aircraft shattered into pieces and burned down, check!
> 
> The system has failed to respond to assertion failure. That's what robustness
> is about.

How much robust...

The only problem is again confusion of terms. When the system responds [as
required], it is no more failure, just per definition of response.

>> Post-conditions are *proved* to be implied by the pre-conditions. 
> 
> Uhm, no, post-conditions (after "Post => ") are stated, nothing more.

Then the thing after "Post => " is not a post-condition. See above.

>> Proof /= check.
> 
> Absolutely. And contract based design encourages proofs, but proofs
> need not be part of the contract.

Proofs are never a part of the contract. Proofs is the contract enforcer.
No enforcement, no contract, just hot air.

>>>>> [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?

A set of states.

> 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.

Given a decision framework it is either decidable or not. If not decidable
then it is not a condition.

>>>  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.

Good to them, but unrelated to the case at hand. There no such thing as
truth outside a decision framework. If the framework is a compiler, then
the only truth is what the compiler decides as truth. You can define a set
of compilers having the same property of being able to prove truths you
want to be true. That is what language design is about.

>> 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?"

No difference. There is no tests at run-time either. Run-time means program
deployed and performing expected actions which is different from a program
under test, as VW guys could wisely point out...

> I note that one can also demonstrate correctness by testing each
> possible set of values, so a proof is not the only means.

Covering all program states IS a proof.

>>> (*) "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".

Right, what about 2 and 3?

> 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.

You confuse achieving correctness with defining correctness. Regardless
whether correctness is achievable and any means of doing so, you must
define what a correct program is. Even in the case when a correct program
may not exist in the given computational framework (e.g.
Turing-incomplete). [*]

The goal of SW design is writing correct programs.

>>  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?

That depends on how we defined it being correct.

> By narrowing program design so that what is allowed in programming
> needs to be statically decidable?

It is a good idea to define correctness decidable. But of course all sorts
of informal requirements could easily do it undecidable or non-existent.

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

We should prove as much as possible and economically/ethically/legally
reasonable.

> Contracts as in "contract based design" are, I think, not about after-the-fact
> properties of a program. They exist prior to implementation.

Which precludes any run-time semantics, obviously. Thank you for agreeing
with my point.

> Hopefully, skillful programmers will feel obliged to show that the contract
> is good and that their programs follow the contract.

Huh, contradicting yourself in just two consequent sentences?

----------------
* Correctness is defined is much more powerful frameworks that programming
language, e.g. when requirements are written in natural language or given
as mathematical expressions etc. Which is the core problem of programming
and design, as a mapping of the problem space semantic (correctness #1)
onto the language semantics (correctness #2).

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de