Re: SPARK: missing case value

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

On Sat, 10 Oct 2015 11:10:48 +0200, Georg Bauhaus wrote:

> On 09.10.15 23:01, Dmitry A. Kazakov wrote:
>> On Fri, 9 Oct 2015 22:29:21 +0200, Georg Bauhaus wrote:
>>
>>> A precondition states conditionality of proper execution.
>>
>> You said that.
> 
> 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...

>> Proper execution should be unconditional to the program
>> state. Otherwise it is called 'bug'.
> 
> Yes, of course! If a contract is violated, that's the work of
> a bug.(*)
> 
>> Ergo, precondition, especially a
>> dynamic one, is a method of introducing bugs.
> 
> A precondition is also used as a method of detecting bugs,

Likewise, aircraft crash is a method of detecting engine failures...

> preconditions usually being checked.

Yes, the aircraft shattered into pieces and burned down, check!

> Which bugs? Notably, failures to make some earlier post-conditions true.
> Seemingly, post-conditions are not usually checked.

Post-conditions are *proved* to be implied by the pre-conditions. Proof /=
check.

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

> the compiler reflecting some state of the art.
> A predicate may be known or assumed to be true and yet the compiler
> cannot decide this. Should the compiler reject known truths?

Known to who? 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. Your reasoning is ridden with logical
fallacies only possible because you confuse terms proof vs. check, compile
vs. run-time, program vs. semantics of...
 
> (*) "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. Bad
philosophy, again. Multiplication exists and is well-defined independently
if somebody fell asleep in his classes. A program is correct (as defined)
or not independently on the skills of any given programmer.

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