Discussion:
SPARK: missing case value
(too old to reply)
Maciej Sobczak
2015-10-09 11:38:32 UTC
Permalink
Consider:

type Enum is (A, B, C);

procedure Test (E : in Enum)
with Pre => E /= C
is
begin
case E is
when A => null;
when B => null;
end case;
end Test;

The Pre contract says that C is never used as a value for E. Still, GNATProve complains about missing case value C in the case statement. The compiler complains, too.

An appropriate subtype (subtype SEnum is Enum range A .. B) can solve this, but it shows some asymmetry between subtypes and contracts, where I would expect that the same subsetting effect can be achieved in both ways. Apparently (and according to AARM), the case statement does not take contracts into account, but my understanding of the rules is that it would not be against the spirit of "covering values that satisfy the predicate".

On the other hand, SPARK is supposed to be a subset of Ada, so even if the above is feasible from the SPARK point of view, it should compile as regular Ada as well and compilers are not required to do this level of static analysis. So, SPARK does not do it, because Ada might not be able to keep the pace.

What are your thoughts on this?
--
Maciej Sobczak * http://www.inspirel.com
Mark Lorenzen
2015-10-09 12:35:03 UTC
Permalink
Post by Maciej Sobczak
On the other hand, SPARK is supposed to be a subset of Ada, so even if the above is feasible from the SPARK point of view, it should compile as regular Ada as well and compilers are not required to do this level of static analysis. So, SPARK does not do it, because Ada might not be able to keep the pace.
What are your thoughts on this?
I think it is logical and correct. How would a compiler be able to determine the range of E if your precondition was more complex?

I would change the case statement into something like this:

case E is
when A => null;
when B => null;
when C => raise Impossible; -- or maybe Pragma Assert (False)
end case;

Note that you can use raise statements in SPARK as long as the program is still in SPARK i.e. the raise statement will never be executed.

Regards,

Mark L
Bob Duff
2015-10-09 14:53:49 UTC
Permalink
Post by Mark Lorenzen
I think it is logical and correct. How would a compiler be able to determine
the range of E if your precondition was more complex?
Well, the fact that compilers cannot prove ALL truthful things (see
halting problem ;-)) doesn't mean they shouldn't be required to prove
some simple things.

- Bob
S***@uni-weimar.de
2015-10-09 12:28:21 UTC
Permalink
Post by Maciej Sobczak
type Enum is (A, B, C);
procedure Test (E : in Enum)
with Pre => E /= C
is
begin
case Thingsome(Something(E)) is -- this was "case E is"
Post by Maciej Sobczak
when A => null;
when B => null;
end case;
end Test;
with some functions Thingsome and Something (X: Enum) return Enum.
Post by Maciej Sobczak
The Pre contract says that C is never used as a value for E. Still,
GNATProve complains about missing case value C in the case statement.
The compiler complains, too.
Well, your example is a triviality to prove.

But if Ada where required to deal with your example, why should it not
also be required to deal with my example?

On the other hand, assume the program is technically correct. I.e., for
all E /= C, the property

Thingsome(Something(E)) /=C

actually holds. Do you really expect the Ada compiler to prove this?

SPARK should prove this, in principle. But, for sufficiently complicated
functions Something and Thingsome, SPARKs success on proving this may
depend on your settings (which theorem provers and how much time for
proving you set). The legality of an Ada program should never depend on
such settings. Everything else would kill portability.

And allowing SPARK to compile formally illegal Ada programs would very
regrettably break the compability between SPARK and Ada -- even if there
acutally where any "pure-SPARK-compilers" at all.

So long

Stefan


-------- I love the taste of Cryptanalysis in the morning! --------
www.uni-weimar.de/de/medien/professuren/mediensicherheit/people/stefan-lucks
----Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universität Weimar, Germany----
Bob Duff
2015-10-09 14:39:01 UTC
Permalink
Post by Maciej Sobczak
type Enum is (A, B, C);
procedure Test (E : in Enum)
with Pre => E /= C
is
begin
case E is
when A => null;
when B => null;
end case;
end Test;
That's illegal Ada, as you noted. And illegal SPARK.

But this works:

type Enum is (A, B, C);
subtype A_C is Enum with Predicate => A_C /= B;

procedure Test (E : in A_C) is
begin
case E is
when A => null;
-- "when B" is not needed.
when C => null;
end case;
end Test;

And that has the advantage that A_C need not be a subrange;
it can have holes.

I find that predicates are often better than preconditions,
because the same precondition often applies to many parameters,
and also to local variables. The predicate allows you to avoid
repetition.

("Predicate =>" is a GNAT-specific extension. In Ada, you need to
say "Static_Predicate =>". IMHO the "Static_" part is just noise,
but I couldn't convince the rest of ARG.)

- Bob
Dmitry A. Kazakov
2015-10-09 15:10:18 UTC
Permalink
Post by Maciej Sobczak
type Enum is (A, B, C);
subtype A_C is Enum with Predicate => A_C /= B;
procedure Test (E : in A_C) is
begin
case E is
when A => null;
-- "when B" is not needed.
when C => null;
end case;
end Test;
And that has the advantage that A_C need not be a subrange;
it can have holes.
I find that predicates are often better than preconditions,
because the same precondition often applies to many parameters,
and also to local variables. The predicate allows you to avoid
repetition.
Because the above is a proper contract, while precondition is a land mine.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
Bob Duff
2015-10-09 15:22:40 UTC
Permalink
Post by Dmitry A. Kazakov
Because the above is a proper contract, while precondition is a land mine.
Why do you think preconditions are dangerous?

- Bob
Dmitry A. Kazakov
2015-10-09 15:34:34 UTC
Permalink
Post by Bob Duff
Post by Dmitry A. Kazakov
Because the above is a proper contract, while precondition is a land mine.
Why do you think preconditions are dangerous?
Even when statically checked they may cause issues as presented. And it
trivially follows from the basic SW design principle of weakening
preconditions. The weakest possible precondition is True, i.e. none.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
G.B.
2015-10-09 16:20:32 UTC
Permalink
Post by Dmitry A. Kazakov
Because the above is a proper contract, while precondition is a land mine.
A land mine has a very proper contract.
Dmitry A. Kazakov
2015-10-09 16:35:31 UTC
Permalink
Post by G.B.
Post by Dmitry A. Kazakov
Because the above is a proper contract, while precondition is a land mine.
A land mine has a very proper contract.
Certainly so. But there is a huge semantic and language difference between
IS and HAS.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
Georg Bauhaus
2015-10-09 20:29:21 UTC
Permalink
Post by Dmitry A. Kazakov
Post by G.B.
Post by Dmitry A. Kazakov
Because the above is a proper contract, while precondition is a land mine.
A land mine has a very proper contract.
Certainly so. But there is a huge semantic and language difference between
IS and HAS.
Right, a land mine cannot be stated as a precondition.
A precondition states conditionality of proper execution.

(To me, it seems improper to narrow contract based design to what
seem to be expressions of disbelief in anything mathematical truth
before the fact. Static_Predicate says less than Predicate, and
less is less practical, as of now, I think.)
Dmitry A. Kazakov
2015-10-09 21:01:33 UTC
Permalink
Post by Georg Bauhaus
A precondition states conditionality of proper execution.
You said that. Proper execution should be unconditional to the program
state. Otherwise it is called 'bug'. Ergo, precondition, especially a
dynamic one, is a method of introducing bugs. I called it a mine because
these bugs are well hidden, disguised as something appearing useful and
improving program design...
Post by Georg Bauhaus
(To me, it seems improper to narrow contract based design to what
seem to be expressions of disbelief in anything mathematical truth
before the fact. Static_Predicate says less than Predicate, and
less is less practical, as of now, I think.)
No idea what this was supposed to mean.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
Randy Brukardt
2015-10-10 06:44:50 UTC
Permalink
...
Post by Dmitry A. Kazakov
Post by Georg Bauhaus
(To me, it seems improper to narrow contract based design to what
seem to be expressions of disbelief in anything mathematical truth
before the fact. Static_Predicate says less than Predicate, and
less is less practical, as of now, I think.)
No idea what this was supposed to mean.
I'm happy to see it was not just me... :-)

Randy.
Georg Bauhaus
2015-10-10 09:10:48 UTC
Permalink
Post by Dmitry A. Kazakov
Post by Georg Bauhaus
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 …!".
Post by Dmitry A. Kazakov
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.(*)
Post by Dmitry A. Kazakov
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.
Post by Dmitry A. Kazakov
Post by Georg Bauhaus
[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.
Dmitry A. Kazakov
2015-10-10 10:00:08 UTC
Permalink
Post by Georg Bauhaus
Post by Dmitry A. Kazakov
Post by Georg Bauhaus
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...
Post by Georg Bauhaus
Post by Dmitry A. Kazakov
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.(*)
Post by Dmitry A. Kazakov
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...
Post by Georg Bauhaus
preconditions usually being checked.
Yes, the aircraft shattered into pieces and burned down, check!
Post by Georg Bauhaus
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.
Post by Georg Bauhaus
Post by Dmitry A. Kazakov
Post by Georg Bauhaus
[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.
Post by Georg Bauhaus
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.
Post by Georg Bauhaus
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...
Post by Georg Bauhaus
(*) "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
Georg Bauhaus
2015-10-10 14:19:31 UTC
Permalink
Post by Dmitry A. Kazakov
Post by Georg Bauhaus
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.
Post by Dmitry A. Kazakov
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 by Dmitry A. Kazakov
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.)
Post by Dmitry A. Kazakov
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.
Post by Dmitry A. Kazakov
Post by Georg Bauhaus
Post by Dmitry A. Kazakov
Post by Georg Bauhaus
[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.
Post by Dmitry A. Kazakov
Post by Georg Bauhaus
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.
Post by Dmitry A. Kazakov
The compiler knows the language, nothing else, nothing more.
The rest is bad philosophy.
Post by Georg Bauhaus
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.
Post by Dmitry A. Kazakov
Post by Georg Bauhaus
(*) "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.
Post by Dmitry A. Kazakov
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.
Dmitry A. Kazakov
2015-10-11 09:49:34 UTC
Permalink
Post by Georg Bauhaus
Post by Dmitry A. Kazakov
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 by Georg Bauhaus
Post by Dmitry A. Kazakov
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.
Post by Georg Bauhaus
Post by Dmitry A. Kazakov
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.
Post by Georg Bauhaus
Post by Dmitry A. Kazakov
Post by Georg Bauhaus
Post by Dmitry A. Kazakov
Post by Georg Bauhaus
[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.
Post by Georg Bauhaus
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.
Post by Georg Bauhaus
Post by Dmitry A. Kazakov
Post by Georg Bauhaus
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.
Post by Georg Bauhaus
Post by Dmitry A. Kazakov
The compiler knows the language, nothing else, nothing more.
The rest is bad philosophy.
Post by Georg Bauhaus
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...
Post by Georg Bauhaus
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.
Post by Georg Bauhaus
Post by Dmitry A. Kazakov
Post by Georg Bauhaus
(*) "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?
Post by Georg Bauhaus
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.
Post by Georg Bauhaus
Post by Dmitry A. Kazakov
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.
Post by Georg Bauhaus
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.
Post by Georg Bauhaus
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.
Post by Georg Bauhaus
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.
Post by Georg Bauhaus
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
Continue reading on narkive:
Loading...