SPARK: missing case value

SPARK: missing case value

[Maciej Sobczak]

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

Re: SPARK: missing case value

[Stefan.Lucks]

[-- Attachment #1: Type: text/plain, Size: 1745 bytes --]

On Fri, 9 Oct 2015, Maciej Sobczak wrote:

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

>         when A => null;
>         when B => null;
>      end case;
>   end Test;

with some functions Thingsome and Something (X: Enum) return Enum.

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

Re: SPARK: missing case value

[Mark Lorenzen]

On Friday, October 9, 2015 at 1:38:35 PM UTC+2, Maciej Sobczak wrote:
> 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

Re: SPARK: missing case value

[Bob Duff]

Mark Lorenzen <mark.lorenzen@gmail.com> writes:

> 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

Re: SPARK: missing case value

[Bob Duff]

Maciej Sobczak <see.my.homepage@gmail.com> writes:

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

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

Re: SPARK: missing case value

[Dmitry A. Kazakov]

On Fri, 09 Oct 2015 10:39:01 -0400, Bob Duff wrote:

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

Because the above is a proper contract, while precondition is a land mine.

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

Re: SPARK: missing case value

[Bob Duff]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:

> Because the above is a proper contract, while precondition is a land
> mine.

Why do you think preconditions are dangerous?

- Bob

Re: SPARK: missing case value

[Dmitry A. Kazakov]

On Fri, 09 Oct 2015 11:22:40 -0400, Bob Duff wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> 
>> 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

Re: SPARK: missing case value

[G.B.]

On 09.10.15 17:10, Dmitry A. Kazakov wrote:
> Because the above is a proper contract, while precondition is a land mine.

A land mine has a very proper contract.

Re: SPARK: missing case value

[Dmitry A. Kazakov]

On Fri, 9 Oct 2015 18:20:32 +0200, G.B. wrote:

> On 09.10.15 17:10, Dmitry A. Kazakov wrote:
>> 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

Re: SPARK: missing case value

[Georg Bauhaus]

On 09.10.15 18:35, Dmitry A. Kazakov wrote:
> On Fri, 9 Oct 2015 18:20:32 +0200, G.B. wrote:
>
>> On 09.10.15 17:10, Dmitry A. Kazakov wrote:
>>> 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.)

Re: SPARK: missing case value

[Dmitry A. Kazakov]

On Fri, 9 Oct 2015 22:29:21 +0200, Georg Bauhaus wrote:

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

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

Re: SPARK: missing case value

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:8ea6wfytssdg.1ake0jrn1irc8.dlg@40tude.net...
> On Fri, 9 Oct 2015 22:29:21 +0200, Georg Bauhaus wrote:
...
>> (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.

Re: SPARK: missing case value

[Georg Bauhaus]

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.

Re: SPARK: missing case value

[Dmitry A. Kazakov]

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

Re: SPARK: missing case value

[Georg Bauhaus]

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.

Re: SPARK: missing case value

[Dmitry A. Kazakov]

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