Re: The future of Spark . Spark 2014 : a wreckage

["Randy Brukardt" <randy@rrsoftware.com>]

<Stefan.Lucks@uni-weimar.de> wrote in message 
news:alpine.DEB.2.10.1307120950410.10151@debian...
On Thu, 11 Jul 2013, Randy Brukardt wrote:
>>> Who said, catch all bugs? I didn't.
>>
>> You want to catch this very unlikely bug, and add a giant pile of extra 
>> junk
>> annotations for this purpose. My contention is that it won't catch enough
>> bugs by itself to be worth the complication.
>
>Firstly, whatever data flow annotations are, they are not "junk".
>
>Secondly, there is no "giant pile" of data flow annotations. Actually,
>they usually take a lot less lines of "anno-code" than writing pre- and
>postconditions. So even if you consider the data flow annotations as
>redundant, their overhead is small.

I called them "junk" because they're redundant (certainly in well-designed 
code). The OP complained that the proposed annotations for Spark 2014, and I 
agree with him on that. But I find it irrelevant because they're redundant.

And I'm strongly opposed to putting redundant information in specifications 
or anywhere else. I've learned by painful experience over the years that 
redundant information -- in type declarations, a compiler symboltable, or a 
programming language standard -- always ends up out of sync with the 
original infomation. That's especially true if it cannot be automatically 
checked (I'm dubious that "Depends" could be checked that way given the 
information available to an Ada compiler). So, I want to eliminate as much 
as possible of that information.

Clearly, we're not getting rid of parameter modes. Clearly, we need 
preconditions and postconditions, they can't be done any other way. That 
makes "Depends" the redundant information that we should not have in a 
specification.

Moreover, I really don't see what value they could possibly have. A 
subprogram has a number of "in" parameters and a number of "out" parameters 
(and possibly, but hopefully not some input globals and output globals, and 
treating a function result as a "out" parameter for this discussion). All of 
the "in" parameters should somehow effect the "out" parameters (and it is 
best if there is only one output).

Routines that don't have this structure are already dubious. It sometimes 
can't be avoided, but it should be extremely rare. So, already, the extra 
information gained by this "flow" information is minimal. On top of that, 
"out" parameters that don't depend on some parameters are likely to be 
obvious in the postcondition for that parameter.

The point is that there isn't much information to be gained from such an 
annotation; the vast majority of it is repeating the obvious (inputs affect 
outputs). I realize that there are a lot of badly designed subprograms out 
there, but I wouldn't want a significant language feature just for badly 
designed subprograms -- especially when we still need lots of support for 
*well* designed subprograms!

...
>> Your experience seems to have been on annotating existing code,
>
>Not at all! (Well, I tried once to SPARKify existing Ada code -- but I got
>rid of that disease very very quickly. Turning naturally-written Ada into
>proper SPARK is a pain in the you-know-where!)

The reason I said that if you design new code, you write the preconditions 
and postconditions along with the subprogram specification (many in the form 
of predicates, I would hope, as those are a lot easier than repeating large 
pre- and post-). (And you surely don't write subprograms where only some of 
the inputs affect some of the outputs.) Before you write anything else (like 
bodies or even descriptions of the purpose of the routine). I've never heard 
of any experienced Ada programmer writing subprogram specifications without 
considering the proper subtypes of the parameters immediately! So I don't 
see how you could get just "Depends" annotations. I grant that you might 
"beef up" the preconditions and postconditions later, to provide a more 
complete description, but you're almost always going to start with some.

>One real life example (simplified for the purpose of posting this) is the
>implementation an authenticated encryption scheme. Consider two byte
>strings X and Y of the same length, X being the message and being Y the
>"key stream". There is additional authentication key K. The output of the
>authenticated encryption is the ciphertext (X xor Y), followed by a
>cryptographic checksum(*) of X under the key K.

This sounds like precisely the bad sort of subprogram that typically should 
be avoided. Multiple outputs, and a strange non-dependence of some of the 
outputs on some of the inputs. I grant this can be unavoidable in some 
cases, but it should be rare. I don't see any point of an annotation that 
only provides extra information for such rare cases.

Probably a more sensible annotation here would be the negative: that is, 
declare which inputs a particular output does *not* depend upon. That 
normally should be a null list, in the rare case where it is non-null the 
information could be given.

But, as I said, this is not information useful to an Ada compiler (while the 
other annotations will improve code quality).

                        Randy.