Re: SPARK: missing case value

[Georg Bauhaus <bauhaus@futureapps.invalid>]

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 …!".

> 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,
preconditions usually being checked. (Yes, they can be incorrect
if their authors have made a mistake. I understand that, also,
not all theorem provers are prefect, so everything we do is
a method of introducing bugs.)

Which bugs? Notably, failures to make some earlier post-conditions true.
Seemingly, post-conditions are not usually checked. Programs can respond
to failure reports, programmers can respond, too, taking new knowledge
into account, or exploring different paths.

>> [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, 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?
Or should it just perform the test at run-time if you tell it to do so?

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