The future of Spark . Spark 2014 : a wreckage

The future of Spark . Spark 2014 : a wreckage

[vincent.diemunsch]

Have you heard of the new Spark 2014 initiative by AdaCore ?
http://docs.adacore.com/spark2014-docs/html/ug/language_subset.html

Spark 2014 aims at replacing Spark annotations by Ada 2012 aspects, at replacing proof functions by expression functions, and at using the Frama-C
tools (Alt-Ergo and why3 language) for automatic proof. At the beginning I thought this was a good idea, but the more I get into the subject, the more it seems for me that they are going wrong.

First ASPECTS : Let's take an example, that is given in the Spark Reference Manual.

- their syntax is clumsy and error prone : 

Spark 2005 :
   procedure Swap;
   --# global in out X, Y;
   --# derives X from Y &
   --#         Y from X;
  
Same specification in Spark 2014 :
   procedure Swap
      with Global  => (In_Out => (X, Y)),
           Depends => (X => Y,   -- to be read as "X depends on Y"
                       Y => X);  -- to be read as "Y depends on X"

How are we supposed to guess that "X => Y" means X depends on Y, if the arrow goes from X to Y ? In the literature, Flow analysis use always Information Flow where arrows follows the real move of information. See for instance "SPARK the proven approach of High Integrity Software" from John Barn page 311 or the "Dragon Book" (Compilers : principles, techniques and tools).

- the syntax makes a complete confusion between a precondition and a test : Preconditions are SPECIFICATIONS that insures that the runtime tests that the Ada compiler puts in the code will pass. What's the use of testing at the entry of a procedure what will be tested in the procedure ? Doing the test twice won't impove correctness ! That is why proconditions and postconditions must stay as comments.


Second EXPRESSION FUNCTIONS :

Expressions functions break the Ada Specification, by allowing the programmer to give the body of a function into the specification of a package. For what purpose ? To allow the runtime testing of pre and post conditions...

But Spark had logical functions that could be declared in the package specification, for expressing pre/postconditions, for instance : 
   --# type StackType is abstract;
   --# function Count_of(S: StackType) return Natural;
   --# function Substack(S1: StackType; S2: StackType) return Boolean;

The problem with Spark was that one had to use an old language : FDL to express
what these functions meant. So the only thing that is required here for an improvement of Spark is to be able to write IN THE PACKAGE BODY the logical function as, for instance : 

package body Stack
--# own State is Ptr, Vector;

is
   type Ptrs       is range 0..MaxStackSize;
   subtype Indexes is Ptrs range 1..Ptrs'Last;
   type Vectors    is array (Indexes) of Integer;

   Ptr      : Ptrs    := 0;
   Vector   : Vectors := Vectors'(Indexes => 0);
   
   --# function Count_of(S: StackType) return Natural is Ptr;
   --# function Substack(S1: StackType; S2: StackType) return Boolean is
   --#    (for all X in 1 .. S1.Ptr => S1.Vector(X) = S2.Vector(X));

This is much, much better than the Spark 2014 solution because :
- a proof function like Substack is not supposed to be called at runtime, because it compares to states of the same unique stack, not two real stacks ! so it should not appear in the compilable code. But Spark 2014 would transform this into a runtime comparison...
- it allows to do in the body a refinement of the abstract type Stacktype that represents the package state, which is not possible with expression functions in the specification. It seems that the people of Spark 2014 didn't get that point.

I realy hope that Spark users will say to AdaCore that they aro going wrong and that AdaCore will really try to make a better future for Spark.

Vincent DIEMUNSCH

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

[Simon Wright]

vincent.diemunsch@gmail.com writes:

> Same specification in Spark 2014 :
>    procedure Swap
>       with Global  => (In_Out => (X, Y)),
>            Depends => (X => Y,   -- to be read as "X depends on Y"
>                        Y => X);  -- to be read as "Y depends on X"
>
> How are we supposed to guess that "X => Y" means X depends on Y, if
> the arrow goes from X to Y ? In the literature, Flow analysis use
> always Information Flow where arrows follows the real move of
> information. See for instance "SPARK the proven approach of High
> Integrity Software" from John Barn page 311 or the "Dragon Book"
> (Compilers : principles, techniques and tools).

Maybe, but a UML dependency would be read the way that you have quoted.
I don't expect users would guess, I expect they'd RTFM.

> - the syntax makes a complete confusion between a precondition and a
> test : Preconditions are SPECIFICATIONS that insures that the runtime
> tests that the Ada compiler puts in the code will pass. What's the use
> of testing at the entry of a procedure what will be tested in the
> procedure ? Doing the test twice won't impove correctness ! That is
> why proconditions and postconditions must stay as comments.

I assume that after one has done a successful proof of correctness with
SPARK 2014 one will build with a configuration that says that assertions
and predicates are to be ignored (ARM 11.4.2). I suspect that for many
real-time systems you'd need to do this to get timely operation anyway;
nice if the compiler could ensure the Note, "Normally, the boolean
expression in a pragma Assert should not call functions that have
significant side effects when the result of the expression is True, so
that the particular assertion policy in effect will not affect normal
operation of the program.", but that's probably equivalent to the
halting problem.

I wonder whether the same consideration should apply to predicates?

> Expressions functions break the Ada Specification

Expression functions are *in* the Ada Specification! (assuming you mean
the ARM?)

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

[Florian Weimer]

* vincent diemunsch:

> Same specification in Spark 2014 :
>    procedure Swap
>       with Global  => (In_Out => (X, Y)),
>            Depends => (X => Y,   -- to be read as "X depends on Y"
>                        Y => X);  -- to be read as "Y depends on X"
>
> How are we supposed to guess that "X => Y" means X depends on Y, if
> the arrow goes from X to Y ? In the literature, Flow analysis use
> always Information Flow where arrows follows the real move of
> information. See for instance "SPARK the proven approach of High
> Integrity Software" from John Barn page 311 or the "Dragon Book"
> (Compilers : principles, techniques and tools).

This is nothing new.  Boolean implication p → q is already written as
P <= Q in Ada.

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

[Randy Brukardt]

<vincent.diemunsch@gmail.com> wrote in message 
news:d84b2eb2-eab3-4dec-917c-0498473c1e93@googlegroups.com...
>Have you heard of the new Spark 2014 initiative by AdaCore ?
>http://docs.adacore.com/spark2014-docs/html/ug/language_subset.html
>
>Spark 2014 aims at replacing Spark annotations by Ada 2012 aspects, at 
>replacing
>proof functions by expression functions, and at using the Frama-C tools 
>(Alt-Ergo
>and why3 language) for automatic proof. At the beginning I thought this was 
>a good
>idea, but the more I get into the subject, the more it seems for me that 
>they are going wrong.

I have nothing to do with AdaCore or this Spark update, so what follows is 
personal opinion.

I think existing Spark is evil, in that it funnels off effort best applied 
to the entire Ada language (or at least, a much larger subset). Computers 
are now powerful enough that the excuses for avoiding proofs of exceptions, 
dynamic memory allocation, and the like no longer are valid.

Thus I like what AdaCore is trying to do, because they are bringing Spark 
closer to Ada itself. Which makes it much more likely that the effort that 
goes into Spark can be applied to the full Ada language as well.

>First ASPECTS : Let's take an example, that is given in the Spark Reference 
>Manual.
>
>- their syntax is clumsy and error prone :
>
>Spark 2005 :
>   procedure Swap;
>   --# global in out X, Y;
>   --# derives X from Y &
>   --#         Y from X;

You're certainly right that this is clumsy and makes little sense. :-) A 
routine that modifies global variables in this way shouldn't pass any code 
review, so it's pretty much irrelevant what the annotations would look like.

>
>Same specification in Spark 2014 :
>   procedure Swap
>      with Global  => (In_Out => (X, Y)),
>           Depends => (X => Y,   -- to be read as "X depends on Y"
>                       Y => X);  -- to be read as "Y depends on X"
>
>How are we supposed to guess that "X => Y" means X depends on Y, if the 
>arrow goes
>from X to Y ? In the >literature, Flow analysis use always Information Flow 
>where arrows
>follows the real move of information. See for instance "SPARK the proven 
>approach of
>High Integrity Software" from John Barn page 311 or the "Dragon Book" 
>(Compilers :
>principles, techniques and tools).

I don't know, nor care, because I don't see any reason or value to "Depends" 
information in the first place. Routines shouldn't be modifying globals in 
this sort of way, IMHO, so there is no need to proof them. (Any globals 
should be hidden in package bodies and not exposed to clients.)

The Globals notation is much more important. We tried to design such a 
notation for Ada 2012, but it became too much work to complete and there was 
a lot of concern about getting it wrong. So we left this for the "experts". 
It appears that the experts are working on it, which is good, because we 
still want this capability in the next version of Ada (whenever that will 
be). And for that to be the case, we'll need it to have proper Ada syntax 
using aspects.

>- the syntax makes a complete confusion between a precondition and a test : 
>Preconditions
>are SPECIFICATIONS that insures that the runtime tests that the Ada 
>compiler puts in the
>code will pass. What's the use of testing at the entry of a procedure what 
>will be tested in
>the procedure ? Doing the test twice won't impove correctness ! That is why 
>proconditions
>and postconditions must stay as comments.

If you're doing the test twice, you are completely misusing Ada 2012 (not to 
mention Spark!). The whole point is that the *only* test is in the 
precondition (or predicates). If a proof tool (or better yet, the compiler - 
I believe these proofs need to be part of normal compilation), has proven 
that the precondition can't fail, the compiler is not going to generate any 
test anywhere.

I suppose Spark (which is a separate tool) won't be able to tell the 
compiler to not make the check. But since there will only be one check in 
the code, you certainly won't be getting redundant checks. (The entire point 
of adding raise expressions was that we failed to provide proper mechanisms 
for setting the exception raised in these checks; that's necessary to be 
able to eliminate the existing hand-coded checks in existing code. That's 
why raise expressions were added as a "bug fix" to Ada 2012 and thus are 
required of all Ada 2012 implementations.)

>Second EXPRESSION FUNCTIONS :
>
>Expressions functions break the Ada Specification, by allowing the 
>programmer to
>give the body of a function into the specification of a package. For what 
>purpose ?
>To allow the runtime testing of pre and post conditions...

No, to allow *compile-time* analysis of pre and post conditions. An Ada 
compiler cannot look into the body of a package to see what is there, and 
without expression functions, almost no compile-time analysis could be 
accomplished. (We also need globals annotations for similar reasons.) The 
real end-game here ought to be compile-time proof (that is, proofs that are 
created as part of the normal compilation of Ada code).

>But Spark had logical functions that could be declared in the package 
>specification, for
>expressing pre/postconditions, for instance :
>   --# type StackType is abstract;
>   --# function Count_of(S: StackType) return Natural;
>   --# function Substack(S1: StackType; S2: StackType) return Boolean;
>
>The problem with Spark was that one had to use an old language : FDL to 
>express
>what these functions meant. So the only thing that is required here for an 
>improvement
>of Spark is to be able to write IN THE PACKAGE BODY the logical function 
>as, for instance :

Proofs of any kind should never, ever depend on anything in the package body 
(other than the one being proved, of course):

(1) Body dependence greatly increases coupling;
(2) Proofs should be able to be created for partially created programs 
(doing proofs as an afterthought will never work); no body ought to be 
required or even exist. (This is also is important so that propietary code 
can be used and still included in proofs.)
(3) If body dependencies are eliminated, proofs remain valid so long as no 
specification is changed. The only unit that needs reproofing when a body is 
changed is that body itself.

(2) is necessary to use proof tools on large systems. Full source is almost 
never available, and if it is, it isn't available until very late in a 
project. (3) is necessary so that work doesn't have to be done over and over 
and over.

...
>- it allows to do in the body a refinement of the abstract type Stacktype 
>that
> represents the package state, which is not possible with expression 
> functions
> in the specification. It seems that the people of Spark 2014 didn't get 
> that point.

The expression functions go in the private part, where you can have 
visibility onto anything that you need, without exposing it to clients. 
Perhaps you missed that part.

> I realy hope that Spark users will say to AdaCore that they aro going 
> wrong
> and that AdaCore will really try to make a better future for Spark.

Spark users are on a certain dead-end, IMHO. The future is getting proof 
into the hands of all programmers, as a normal part of their day-to-day 
programming. That requires that proofs aren't necessarily complete, that 
they use whatever information is available, and most of all, that they only 
depend on the specifications of packages (never, ever, on the contents of a 
body).

It sounds like this is the direction that Spark 2014 is taking, which means 
IMHO that we'll all benefit, not just a few that can live with draconian 
limitations that turns Ada into a form of Fortran 77.

Just my $1 worth (inflation, you know).

                                  Randy.


Vincent DIEMUNSCH

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

[Peter C. Chapin]

On 07/08/2013 01:56 PM, vincent.diemunsch@gmail.com wrote:

>     procedure Swap
>        with Global  => (In_Out => (X, Y)),
>             Depends => (X => Y,   -- to be read as "X depends on Y"
>                         Y => X);  -- to be read as "Y depends on X"
>
> How are we supposed to guess that "X => Y" means X depends on Y, if the arrow goes from X to Y ?

Well the phrase "X depends on Y" has X on the left and Y on the right 
just as X => Y does. So it reads fairly naturally to me. I understand 
there is value in being consistent with existing notations although I 
get the impression there is already conflicting practice in that area.

More significantly, though, I think you may be assigning too much 
semantic weight to the '=>' token in this case. In the aspect syntax it 
is used more as a separator than anything else. Consider

   Pre => X < 0

Nobody would say that there is information flowing from "Pre" to the 
expression 'X < 0' or visa-versa. The SPARK 2014 syntax extends this 
notion of "arrow as separator" to the subcomponents of the aspects. Thus

   Depends => (X => Y)

The "inner" arrow just separates X from Y syntactically. It's not really 
related to information flow... although its easy to see why someone 
would assume that it was considering the semantics of the Depends aspect 
overall.

Peter

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

[Dmitry A. Kazakov]

On Mon, 8 Jul 2013 16:32:21 -0500, Randy Brukardt wrote:

>> I realy hope that Spark users will say to AdaCore that they aro going 
>> wrong and that AdaCore will really try to make a better future for Spark.
> 
> Spark users are on a certain dead-end, IMHO. The future is getting proof 
> into the hands of all programmers, as a normal part of their day-to-day 
> programming. That requires that proofs aren't necessarily complete,

Rather the programmer should announce what to prove and that proof must be
complete.

> that 
> they use whatever information is available, and most of all, that they only 
> depend on the specifications of packages (never, ever, on the contents of a 
> body).

There are obviously goals which cannot be proven without the bodies. Proofs
about specifications are important but far not all. Consider LSP as an
example. You cannot prove substitutability from interfaces. It simply does
not work. Same with almost everything else, because proving something in
general is much more harder, even impossible, than proving things about a
concrete instance, e.g. body.

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

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

[Stefan.Lucks]

[-- Attachment #1: Type: TEXT/PLAIN, Size: 2463 bytes --]

On Mon, 8 Jul 2013, Peter C. Chapin wrote:

> On 07/08/2013 01:56 PM, vincent.diemunsch@gmail.com wrote:
>
>>     procedure Swap
>>        with Global  => (In_Out => (X, Y)),
>>             Depends => (X => Y,   -- to be read as "X depends on Y"
>>                         Y => X);  -- to be read as "Y depends on X"
>> 
>> How are we supposed to guess that "X => Y" means X depends on Y, if the 
>> arrow goes from X to Y ?
>
> Well the phrase "X depends on Y" has X on the left and Y on the right just as 
> X => Y does. So it reads fairly naturally to me. I understand there is value 
> in being consistent with existing notations although I get the impression 
> there is already conflicting practice in that area.
>
> More significantly, though, I think you may be assigning too much semantic 
> weight to the '=>' token in this case. In the aspect syntax it is used more 
> as a separator than anything else. Consider
>
>  Pre => X < 0

Fair enough! The "=>" is not an arrow, it is just a syntactic token to 
separate two other tokens.

Unfortunately, this token greatly (and certainly intentionally, at the 
early days of Ada) resembles an arrow. And this is relly confusing in 
situations where an arrow would make sense, but where the "=>" goes into 
the wrong direction. "Pre =>" isn't an issue, but X => Y above is.

Actually, this has been irritating me when using named notation for out 
parameters, since I have learned Ada. If Y is an out parameter, it should 
be Do_Something (X <= Y), shouldn't it?

This isn't such a big issue that Ada will actually need another separator 
token, such as "<=" ... we'll have to live with "=>". But maybe, one could 
turn this "bug" into a feature, by defining an alternative to the Depends 
annotation^H^H^H^H^H^H^H^H^H^H aspect, where the "=>" points into the 
correct direction, e.g.:

      procedure Swap
         with Global           => (In_Out => (X, Y)),
              Information_Flow => (Y => X,   -- "X depends on Y"
                                   X => Y);  -- "Y depends on X"

as a legal replacement for the usage of "Depends". That would be a lot 
more intuitive!

Alas, it is probably too late for SPARK 2014 ... sigh!


------  I  love  the  taste  of  Cryptanalysis  in  the morning!  ------
     <http://www.uni-weimar.de/cms/medien/mediensicherheit/home.html>
--Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universität Weimar, Germany--

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

[Dmitry A. Kazakov]

On Mon, 08 Jul 2013 22:59:30 +0200, Florian Weimer wrote:

> * vincent diemunsch:
> 
>> Same specification in Spark 2014 :
>>    procedure Swap
>>       with Global  => (In_Out => (X, Y)),
>>            Depends => (X => Y,   -- to be read as "X depends on Y"
>>                        Y => X);  -- to be read as "Y depends on X"
>>
>> How are we supposed to guess that "X => Y" means X depends on Y, if
>> the arrow goes from X to Y ? In the literature, Flow analysis use
>> always Information Flow where arrows follows the real move of
>> information. See for instance "SPARK the proven approach of High
>> Integrity Software" from John Barn page 311 or the "Dragon Book"
>> (Compilers : principles, techniques and tools).
> 
> This is nothing new.  Boolean implication p → q is already written as
> P <= Q in Ada.

Where?

It would be plain wrong, because logical implication (not P or Q) must be
denoted as P => Q.

   http://en.wikipedia.org/wiki/Material_conditional

BTW, there is a difference between implication (Boolean operation) and
consequence like

   P |= Q

   http://en.wikipedia.org/wiki/Logical_consequence#Semantic_consequence

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

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

[Stefan.Lucks]

[-- Attachment #1: Type: TEXT/PLAIN, Size: 4281 bytes --]

On Mon, 8 Jul 2013, Randy Brukardt wrote:

> I think existing Spark is evil, in that it funnels off effort best applied
> to the entire Ada language (or at least, a much larger subset). Computers
> are now powerful enough that the excuses for avoiding proofs of exceptions,
> dynamic memory allocation, and the like no longer are valid.

Agreed! Well, "evil" is a bit harsh -- existing SPARK fills a gap that Ada 
until recently has left wide open, which was a good thing at its time. But 
Ada 2012 has narrowed that gap a lot, and it is a good thing that Ada and 
SPARK are now evolving together.

>> Spark 2005 :
>>   procedure Swap;
>>   --# global in out X, Y;
>>   --# derives X from Y &
>>   --#         Y from X;
>
> You're certainly right that this is clumsy and makes little sense. :-) A
> routine that modifies global variables in this way shouldn't pass any code
> review, so it's pretty much irrelevant what the annotations would look like.

Randy, here you are really throwing out the child with the bath. Sure, a 
procedure to swap two globals is is a silly example -- but the topic here 
is the syntax for information flow analysis, and the example has the 
benefit of being very simple. The following doesn't use globals and might 
pass a code review:

Spark 2005 :
    procedure Swap(X, Y: in out T);
    --# derives X from Y &
    --#         Y from X;


Same specification in Spark 2014 :
    procedure Swap(X, Y: in out T);
       with Depends => (X => Y,   -- to be read as "X depends on Y"
                        Y => X);  -- to be read as "Y depends on X"

>> How are we supposed to guess that "X => Y" means X depends on Y, if the
>> arrow goes from X to Y ? In the >literature, Flow analysis use always 
>> Information Flow where arrows follows the real move of information. 
[...]

> I don't know, nor care, because I don't see any reason or value to "Depends"
> information in the first place.

So you think, information flow analysis is completely worthless? (I mean, 
for building and verifying correct systems -- as a compiler writer you 
will not question the usage of information flow analysis inside the 
compiler or optimiser).

> Routines shouldn't be modifying globals in
> this sort of way, IMHO, so there is no need to proof them. (Any globals
> should be hidden in package bodies and not exposed to clients.)

Agreed. The OP has been using an example with modifying globals, mine 
doesn't, the issue raised by the OP remains.

>> - the syntax makes a complete confusion between a precondition and a 
>> test : Preconditions are SPECIFICATIONS that insures that the runtime 
>> tests that the Ada compiler puts in the code will pass. What's the use 
>> of testing at the entry of a procedure what will be tested in the 
>> procedure ? Doing the test twice won't impove correctness ! That is why 
>> proconditions and postconditions must stay as comments.
>
> If you're doing the test twice, you are completely misusing Ada 2012 (not to
> mention Spark!). The whole point is that the *only* test is in the
> precondition (or predicates). If a proof tool (or better yet, the compiler -
> I believe these proofs need to be part of normal compilation), has proven
> that the precondition can't fail, the compiler is not going to generate any
> test anywhere.

Agreed! Many people seem to confuse this like the OP: Ada 2012 is about 
*specifying* contracts. It *allows* to prove them or to check them at run 
time if proving them has not been possible. A good toolset would not 
generate code checking conditions that have been proven.

> Spark users are on a certain dead-end, IMHO.

That is a bit unfair, IMHO. SPARK users have a real head start when it 
comes to applying the really innovative features of Ada 2012.

> It sounds like this is the direction that Spark 2014 is taking, which means
> IMHO that we'll all benefit, not just a few that can live with draconian
> limitations that turns Ada into a form of Fortran 77.

Agreed!

------  I  love  the  taste  of  Cryptanalysis  in  the morning!  ------
     <http://www.uni-weimar.de/cms/medien/mediensicherheit/home.html>
--Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universität Weimar, Germany--

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

[Georg Bauhaus]

On 09.07.13 09:40, Dmitry A. Kazakov wrote:
> On Mon, 08 Jul 2013 22:59:30 +0200, Florian Weimer wrote:
>
>> * vincent diemunsch:
>>
>>> Same specification in Spark 2014 :
>>>     procedure Swap
>>>        with Global  => (In_Out => (X, Y)),
>>>             Depends => (X => Y,   -- to be read as "X depends on Y"
>>>                         Y => X);  -- to be read as "Y depends on X"
>>>
>>> How are we supposed to guess that "X => Y" means X depends on Y, if
>>> the arrow goes from X to Y ? In the literature, Flow analysis use
>>> always Information Flow where arrows follows the real move of
>>> information. See for instance "SPARK the proven approach of High
>>> Integrity Software" from John Barn page 311 or the "Dragon Book"
>>> (Compilers : principles, techniques and tools).
>>
>> This is nothing new.  Boolean implication p → q is already written as
>> P <= Q in Ada.
>
> Where?

In Boolean expressions. With obvious, I think, abbreviations
and referring to ordering of (False, True), and (0, 1),

p q | p → q   (p <= q)
-----------------------
1 1 |   1       True
1 0 |   0       False
0 1 |   1       True
0 0 |   1       True

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

[Dmitry A. Kazakov]

On Tue, 09 Jul 2013 10:30:59 +0200, Georg Bauhaus wrote:

> On 09.07.13 09:40, Dmitry A. Kazakov wrote:
>> On Mon, 08 Jul 2013 22:59:30 +0200, Florian Weimer wrote:
>>
>>> * vincent diemunsch:
>>>
>>>> Same specification in Spark 2014 :
>>>>     procedure Swap
>>>>        with Global  => (In_Out => (X, Y)),
>>>>             Depends => (X => Y,   -- to be read as "X depends on Y"
>>>>                         Y => X);  -- to be read as "Y depends on X"
>>>>
>>>> How are we supposed to guess that "X => Y" means X depends on Y, if
>>>> the arrow goes from X to Y ? In the literature, Flow analysis use
>>>> always Information Flow where arrows follows the real move of
>>>> information. See for instance "SPARK the proven approach of High
>>>> Integrity Software" from John Barn page 311 or the "Dragon Book"
>>>> (Compilers : principles, techniques and tools).
>>>
>>> This is nothing new.  Boolean implication p → q is already written as
>>> P <= Q in Ada.
>>
>> Where?
> 
> In Boolean expressions. With obvious, I think, abbreviations
> and referring to ordering of (False, True), and (0, 1),
> 
> p q | p → q   (p <= q)
> -----------------------
> 1 1 |   1       True
> 1 0 |   0       False
> 0 1 |   1       True
> 0 0 |   1       True

This is p=>q

    p=>q  =def=  not p or q
/= q=>p  =def=  not q or p

p<=q = q=>p is

p q | p<=q
----------
1 1 | 1
1 0 | 1
0 1 | 0
0 0 | 1

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

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

[G.B.]

On 09.07.13 10:58, Dmitry A. Kazakov wrote:
> On Tue, 09 Jul 2013 10:30:59 +0200, Georg Bauhaus wrote:
> 
>> On 09.07.13 09:40, Dmitry A. Kazakov wrote:
>>> On Mon, 08 Jul 2013 22:59:30 +0200, Florian Weimer wrote:

>>>> This is nothing new.  Boolean implication p → q is already written as
>>>> P <= Q in Ada.
>>>
>>> Where?
>>
>> In Boolean expressions. With obvious, I think, abbreviations
>> and referring to ordering of (False, True), and (0, 1),
>>
>> p q | p → q   (p <= q)
>> -----------------------
>> 1 1 |   1       True
>> 1 0 |   0       False
>> 0 1 |   1       True
>> 0 0 |   1       True
> 
> This is p=>q
>
>      p=>q  =def=  not p or q

"Boolean implication p → q is already written as
 P <= Q in Ada."

As shown above. "=>" has no "Boolean" meaning in Ada.
(It has, in Prolog.) In implementation defined aspects,
GNAT is free to assign "depends" to "=>", UML style.

I guess we need to adapt to even many overloadings
if symbolophobia is part of Ada culture.

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

[G.B.]

On 09.07.13 10:58, Dmitry A. Kazakov wrote:
> On Tue, 09 Jul 2013 10:30:59 +0200, Georg Bauhaus wrote:
> 
>> On 09.07.13 09:40, Dmitry A. Kazakov wrote:
>>> On Mon, 08 Jul 2013 22:59:30 +0200, Florian Weimer wrote:
>>>
>>>> * vincent diemunsch:
>>>>
>>>>> Same specification in Spark 2014 :
>>>>>      procedure Swap
>>>>>         with Global  => (In_Out => (X, Y)),
>>>>>              Depends => (X => Y,   -- to be read as "X depends on Y"
>>>>>                          Y => X);  -- to be read as "Y depends on X"
>>>>>
>>>>> How are we supposed to guess that "X => Y" means X depends on Y, if
>>>>> the arrow goes from X to Y ? In the literature, Flow analysis use
>>>>> always Information Flow where arrows follows the real move of
>>>>> information. See for instance "SPARK the proven approach of High
>>>>> Integrity Software" from John Barn page 311 or the "Dragon Book"
>>>>> (Compilers : principles, techniques and tools).
>>>>
>>>> This is nothing new.  Boolean implication p → q is already written as
>>>> P <= Q in Ada.
>>>
>>> Where?
>>
>> In Boolean expressions. With obvious, I think, abbreviations
>> and referring to ordering of (False, True), and (0, 1),
>>
>> p q | p → q   (p <= q)
>> -----------------------
>> 1 1 |   1       True
>> 1 0 |   0       False
>> 0 1 |   1       True
>> 0 0 |   1       True
> 
> This is p=>q

"Boolean implication p → q is already written as
 P <= Q in Ada."

As shown above. "=>" has no "Boolean" meaning in Ada.
(It has, in Prolog.) In implementation defined aspects,
GNAT is free to assign "depends" to "=>", UML style.

I guess we need to adapt to even more overloadings,
since symbolophobia is part of Ada culture.

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

[Simon Wright]

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

> On Mon, 8 Jul 2013 16:32:21 -0500, Randy Brukardt wrote:

>> that they use whatever information is available, and most of all,
>> that they only depend on the specifications of packages (never, ever,
>> on the contents of a body).
>
> There are obviously goals which cannot be proven without the
> bodies. Proofs about specifications are important but far not
> all. Consider LSP as an example. You cannot prove substitutability
> from interfaces. It simply does not work. Same with almost everything
> else, because proving something in general is much more harder, even
> impossible, than proving things about a concrete instance, e.g. body.

I think what Randy meant (and may even have said) was that in

   with A;
   package B is ...

it shouldn't be necessary to look at the body of A to prove the body of
B. Of course the body of A will have to be proved ... but not right now.

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

[Dmitry A. Kazakov]

On Tue, 09 Jul 2013 12:29:03 +0100, Simon Wright wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> 
>> On Mon, 8 Jul 2013 16:32:21 -0500, Randy Brukardt wrote:
> 
>>> that they use whatever information is available, and most of all,
>>> that they only depend on the specifications of packages (never, ever,
>>> on the contents of a body).
>>
>> There are obviously goals which cannot be proven without the
>> bodies. Proofs about specifications are important but far not
>> all. Consider LSP as an example. You cannot prove substitutability
>> from interfaces. It simply does not work. Same with almost everything
>> else, because proving something in general is much more harder, even
>> impossible, than proving things about a concrete instance, e.g. body.
> 
> I think what Randy meant (and may even have said) was that in
> 
>    with A;
>    package B is ...
> 
> it shouldn't be necessary to look at the body of A to prove the body of
> B. Of course the body of A will have to be proved ... but not right now.

Yes this is how I understood him and what I objected to.

You cannot rely on the contracts when it comes to correctness.

OK, for the sake on the argument, you could contract proofs about A's body,
so that these proofs could be used in the proofs of the body B. But the
problem with that is exactly what Randy wanted to avoid - tight coupling
and doing things in advance which nobody would ever needed.

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

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

[Adam Beneschan]

On Tuesday, July 9, 2013 12:40:55 AM UTC-7, Dmitry A. Kazakov wrote:

> > This is nothing new.  Boolean implication p → q is already written as
> > P <= Q in Ada.
> 
> Where?

It's an accident, really.  <= means "less than or equal to", and it works for implication just because it so happens that p → q is true except when p=TRUE and q=FALSE, which just happens to be the same behavior as p <= q.  Treating <= as an arrow was sort of a joke, I think.

                               -- Adam

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

[Adam Beneschan]

On Tuesday, July 9, 2013 12:34:59 AM UTC-7, Stefan...@uni-weimar.de wrote:

> Actually, this has been irritating me when using named notation for out 
> parameters, since I have learned Ada. If Y is an out parameter, it should 
> be Do_Something (X <= Y), shouldn't it?

<= already has another meaning, so that wouldn't work.  As some of us have pointed out before, an early version of Ada did have different symbols; instead of the arrow, =>, it used =: for IN parameters, := for OUT parameters, :=: for IN OUT parameters.  I don't really know why this idea was dropped before Ada 83 was finalized.  I'm beginning to think it should have been left in.  Especially now that [IN] OUT parameters are allowed in function calls; I've been big on the idea of providing some syntax for a function call that would let the reader know that the call might be changing one of the parameters.

                            -- Adam

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

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:1vc73wjwkqmnl$.gx86xaqy60u4$.dlg@40tude.net...
> On Mon, 8 Jul 2013 16:32:21 -0500, Randy Brukardt wrote:
>
>>> I realy hope that Spark users will say to AdaCore that they aro going
>>> wrong and that AdaCore will really try to make a better future for 
>>> Spark.
>>
>> Spark users are on a certain dead-end, IMHO. The future is getting proof
>> into the hands of all programmers, as a normal part of their day-to-day
>> programming. That requires that proofs aren't necessarily complete,
>
> Rather the programmer should announce what to prove and that proof must be
> complete.

Right. And that should be an integral part of compilation: no proof, no 
compilation.

>> that
>> they use whatever information is available, and most of all, that they 
>> only
>> depend on the specifications of packages (never, ever, on the contents of 
>> a
>> body).
>
> There are obviously goals which cannot be proven without the bodies. 
> Proofs
> about specifications are important but far not all. Consider LSP as an
> example. You cannot prove substitutability from interfaces. It simply does
> not work. Same with almost everything else, because proving something in
> general is much more harder, even impossible, than proving things about a
> concrete instance, e.g. body.

My contention is such things are not worth proving. With strong enough 
contracts (including class-wide contracts for dispatching calls, and 
contracts on subprogram types :-), important properties of code can be 
proven. What's too hard shouldn't be bothered with, because we've lived just 
fine with no proofs at all for programming up to this point. Proofs should 
be an aid to debugging, not the be-all, end-all. I want to add proof 
technology incrementally so that everyone can use a little of it, benefit 
from it, and then use more of it. It's how most Ada programmers learned to 
use types and constraints, and its the way to get proofs into the 
mainstream. Not by stand-alone tools and subsets with weird rules.

                                   Randy.


                                            Randy.

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

[Randy Brukardt]

<Stefan.Lucks@uni-weimar.de> wrote in message 
news:alpine.DEB.2.10.1307090935310.23845@debian...
On Mon, 8 Jul 2013, Randy Brukardt wrote:

...
>> I don't know, nor care, because I don't see any reason or value to 
>> "Depends"
>> information in the first place.
>
>So you think, information flow analysis is completely worthless? (I mean,
>for building and verifying correct systems -- as a compiler writer you
>will not question the usage of information flow analysis inside the
>compiler or optimiser).

Information flow *within* a subprogram is important. Information flow 
*between* subprograms is completely defined by the subprogram's interfaces 
and calls. Other information ought to be irrelevant (no one should be 
depending upon what the body of Swap does, other than whatever is specified 
in the postcondition).

Janus/Ada does not do any inter-procedural optimizations, and I doubt that 
it would ever do any beyond inlining and parameter elimination -- neither of 
which have anything to do with flow analysis.

I realize that one can prove additional properties with this additional 
information, but my contention is that trying to do so is harmful (it adds a 
lot of coupling to a program) and isn't valuable to the vast majority of 
users. That is where Spark mostly went wrong, IMHO.

                Randy.

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

[Robert A Duff]

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

> On Mon, 08 Jul 2013 22:59:30 +0200, Florian Weimer wrote:
>> This is nothing new.  Boolean implication p → q is already written as
>> P <= Q in Ada.
>
> Where?
> 
> It would be plain wrong, ...

Less-or-equal on Booleans is indeed equivalent to implication.
But that's a hack.  Considering Booleans as ordered is questionable --
I never heard of such a thing in mathematical logic.

>...because logical implication (not P or Q) must be
> denoted as P => Q.

It must be?  In Eiffel, it is denoted by the "implies" keyword.
In Ada 2012, one writes "(if P then Q)", which is shorthand for
"(if P then Q else True)".

- Bob

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

[Dmitry A. Kazakov]

On Tue, 09 Jul 2013 18:51:36 -0400, Robert A Duff wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> 
>> On Mon, 08 Jul 2013 22:59:30 +0200, Florian Weimer wrote:
>>> This is nothing new.  Boolean implication p → q is already written as
>>> P <= Q in Ada.
>>
>> Where?
>> 
>> It would be plain wrong, ...
> 
> Less-or-equal on Booleans is indeed equivalent to implication.
> But that's a hack.  Considering Booleans as ordered is questionable --
> I never heard of such a thing in mathematical logic.

Truth values are ordered in some logics. In others they are not.

>>...because logical implication (not P or Q) must be
>> denoted as P => Q.
> 
> It must be?

Yes, if logical implication is indeed meant here, of which I am not sure.

> In Eiffel, it is denoted by the "implies" keyword.
> In Ada 2012, one writes "(if P then Q)", which is shorthand for
> "(if P then Q else True)".

But this is not an implication (Boolean operation). It is a rule based on
implication. E.g. Modus ponens:

P, P=>Q
------------
Q

So "implies" and "if-then" are correct, while P->Q looks wrong even when
spelled correctly as P=>Q.

If there should be a symbol, I think,

   P |= Q  or P |- Q

would be more appropriate.

Why had we introduced Unicode? After all, there is a code point for this:

  P ⊧ Q    U+22A7  Logical consequence

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

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

[Stefan.Lucks]

On Tue, 9 Jul 2013, Randy Brukardt wrote:

> <Stefan.Lucks@uni-weimar.de> wrote:

>> So you think, information flow analysis is completely worthless? (I mean,
>> for building and verifying correct systems -- as a compiler writer you
>> will not question the usage of information flow analysis inside the
>> compiler or optimiser).
>
> Information flow *within* a subprogram is important. Information flow
> *between* subprograms is completely defined by the subprogram's interfaces
> and calls.

Firstly, for current Ada (i.e., Ada 2012) this is completely wrong 
whenever a program manipulates global variables. Even specifying pre- and 
postconditions doesn't guarantee the absence of any other (side-)effects.
(You are right, however, a proper "global" annotation would seem to catch 
this.)

Secondly, Ada's "in", "out", and "in out" information give only a cursory 
view of what is going on. Even *without* pre- and postcondition, verifying 
a SPARK-like specification of, say,

    procedure Count_Vote(Vote: Vote_Type;
                         Count_A, Count_B, Invalid: out Natural)
 	with Depends (Count_A => Vote, Count_A,
                       Count_B => Vote, Count_B,
                       Invalid => Vote, Invalid);

give a great deal of assurance -- a lot more than the same specification 
without the Depends Aspect.

Now consider the following not-quite-complete contract with pre- and 
postconditions:

    procedure Count_Vote(Vote: Vote_Type;
                         Count_A, Count_B, Invalid: out Natural)
 	with Pre => ((Count_A <= Natural'Last) and
 	             (Count_B <= Natural'Last) and
                      (Count_C <= Natural'Last)),
              Post => ((Count_A >= Count_A'Old) and
                       (Count_B >= Count_B'Old) and
                       (Invalid >= Invalid'Old) and
                       (Count_A + Count_B + Invalid =
 	              (Count_A + Count_B + Invalid)'Old +1);

At a first look, this may appear to be more precise. Each vote will 
increase exactly one counter, either Count_A or Count_B or Invalid. All 
what is left open is how does Count_Vote decide about which counter to 
increase.

However, a correct (up to the specification) implementation could do the 
following:

    procedure Count_Vote(Vote: Vote_Type;
                         Count_A, Count_B, Invalid: out Natural) is
    begin
       if (Vote = 'A') or (Vote='a') then
 	Count_A := Count_A + 1;
       elsif (Vote = 'B') or (Vote='b') then
         if (Count_A + Count_B < 1000) or else
            Count_B < Count_A then
             Count_B := Count_B + 1;
         else
             Count_A := Count_A + 1;
             -- Make sure A wins, assuming more than 2000 valid votes.
         end if;
       else
         Invalid := Invalid + 1;
       end if;
    end Count_Vote;

Without "Depends", your cool analysis tool verifying all pre- and 
postconditions will not catch this bug. And yes, I am aware that another 
implementation could cheat without violating the "Depends" clause. But 
ensuring an "innocent" result (a marginal lead for A where the real result 
would be a marginal lead for B) would be a lot more difficult, if not 
impossible.

The above is a malicious example, but the "frame problem" is a big issue 
for program analysis in general. It appears to be fairly difficult to 
write pre- and postconditions such that you can be sure nothing else is 
going on. "Global" and "Depends" allow to make "nothing else" claims that 
analysis tools can actually verify and use for their subsequent analysis, 
and where "Depends" is a lot more specific than "Global".

> Other information ought to be irrelevant (no one should be
> depending upon what the body of Swap does, other than whatever is specified
> in the postcondition).

I agree that no one should depend on what the body of some Subprogram 
does. But then, information flow analysis is actually useful!




------  I  love  the  taste  of  Cryptanalysis  in  the morning!  ------
     <http://www.uni-weimar.de/cms/medien/mediensicherheit/home.html>
--Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universität Weimar, Germany--

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

[Georg Bauhaus]

On 10.07.13 09:49, Dmitry A. Kazakov wrote:
> On Tue, 09 Jul 2013 18:51:36 -0400, Robert A Duff wrote:

>>> ...because logical implication (not P or Q) must be
>>> denoted as P => Q.
>>
>> It must be?
>
> Yes, if logical implication is indeed meant here, of which I am not sure.
>
>> In Eiffel, it is denoted by the "implies" keyword.
>> In Ada 2012, one writes "(if P then Q)", which is shorthand for
>> "(if P then Q else True)".
>
> But this is not an implication (Boolean operation). It is a rule based on
> implication. E.g. Modus ponens:
>
> P, P=>Q
> ------------
> Q
>
> So "implies" and "if-then" are correct, while P->Q looks wrong even when
> spelled correctly as P=>Q.
>
> If there should be a symbol, I think,
>
>     P |= Q  or P |- Q
>
> would be more appropriate.

Appropriate even though semantic and syntactic entailment resp.
are not usually considered part of the language governing P and Q?

Wouldn't we rather be writing computable expressions and
feed them to mechanical testing of satisfiability? (Which
means, right now, we have just formulae, but not any language
for speaking about arguments or about consistent sets.)

What's your plan?

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

[Dmitry A. Kazakov]

On Tue, 9 Jul 2013 15:37:10 -0500, Randy Brukardt wrote:

>> There are obviously goals which cannot be proven without the bodies. Proofs
>> about specifications are important but far not all. Consider LSP as an
>> example. You cannot prove substitutability from interfaces. It simply does
>> not work. Same with almost everything else, because proving something in
>> general is much more harder, even impossible, than proving things about a
>> concrete instance, e.g. body.
> 
> My contention is such things are not worth proving. With strong enough 
> contracts (including class-wide contracts for dispatching calls, and 
> contracts on subprogram types :-), important properties of code can be 
> proven.

No, that is the problem. You want to overburden the contracts with stuff
that does not belong there. This would make the design fragile.

Consider as an example stack use. Do you want to contract all subprograms
to maximum stack use, or let the compiler to estimate stack use of a
concrete body?

Another example is a mathematical function like sine. In order to prove its
correctness you would need an extremely elaborated apparatus of contract
specification which itself will be a source of countless bugs due to its
complexity. This is a typical over-specification. Only if somebody wanted
to verify an implementation of sine, he would have to look into the body.
Most people never will.

Contracts should not define semantics, only most general properties of. Yet
semantics should sometimes be proven. The provider does not know when. It
is up to the user. In that case he have to look into the body.

> What's too hard shouldn't be bothered with, because we've lived just 
> fine with no proofs at all for programming up to this point.

We didn't. Accessibility checks and constraint errors are a permanent
headache in Ada.

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

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

[vincent.diemunsch]

Hello Randy,

> I think existing Spark is evil, in that it funnels off effort best applied 
> to the entire Ada language (or at least, a much larger subset). Computers 
> are now powerful enough that the excuses for avoiding proofs of exceptions, 
> dynamic memory allocation, and the like no longer are valid.

Spark imposes static memory allocation to be able to prove total correctness,
which means that the program will always do what is expected, which is required
by embedded softwares... 


> The Globals notation is much more important. We tried to design such a 
> notation for Ada 2012, but it became too much work to complete and there was 
> a lot of concern about getting it wrong. So we left this for the "experts". 
> It appears that the experts are working on it, which is good, because we 
> still want this capability in the next version of Ada (whenever that will 
> be). And for that to be the case, we'll need it to have proper Ada syntax 
> using aspects.

Ada has been designed so as to let global variables be freely accessed. Only a pragma was used to specify that a function is Pure (of side effects) and can be skipped for optimisation. Therefore it is now almost impossible to change that and that is probably the reason why you had so much difficulties to define the global annotation, which is trivial, because how will you deal with a procedure that have no annotation, but still uses global variables ? A simple warning at compile time ? Refuse to compile ?

Aspects syntax is ugly. It is simply the return of a kind of primitive language like LISP, done with words and arrows. It shows clearly that it is simply a workaround.


> No, to allow *compile-time* analysis of pre and post conditions. An Ada 
> compiler cannot look into the body of a package to see what is there, and 
> without expression functions, almost no compile-time analysis could be 
> accomplished. (We also need globals annotations for similar reasons.) The 
> real end-game here ought to be compile-time proof (that is, proofs that are 
> created as part of the normal compilation of Ada code).

A proof can't be generated at compile time ! The proof must be written independently, based on formal specification, and checked by an analyser, that may or may not be the compiler.


> Proofs of any kind should never, ever depend on anything in the package body 

As others told you, a proof is a proof that the implementation respects the specification, therefore it needs to make an interpretation of the package body.

> Spark users are on a certain dead-end, IMHO. The future is getting proof 
> into the hands of all programmers, as a normal part of their day-to-day 
>  programming. That requires that proofs aren't necessarily complete, that 
> hey use whatever information is available, and most of all, that they only 
> depend on the specifications of packages (never, ever, on the contents of a 
>  body).

But you seem to make also the confusion between a test and a proof, and that is exactly what AdaCore is doing now : they simply write the tests as post-
conditions and uses symbolic interpretation during compile time. I think that is what you mention by "into the hands of all programmers", ie even those with very few theoretical background.

It's a nice feature to sell and great fun for compiler writers but it's far from a mathematical proof and what Spark was able to do. But mathematical proof requires formal specification and that is far from the "all programmers" knowledge. The problem is that recent books on Spark completly forgot to speak of the necessary formal specifications (like Z for instance).


To conclude here is my vision of Spark and Ada :
- use Ada for things that are necessary for the compiler to produce the code and to express the semantic of the program.
- use Pragmas only as compiler directives, for specific implementation or optimisation (InLine, Ravenscar, Remote-Call-Interface...). Not for assertion, tests or whatever.
- everything that is related to formal verification should stay as comment in
the code. These comments can then be verified by external tools. There can be different levels of verification, not only the Spark vision.
- formal specifications are necessary for formal verification, therefore Spark should be able to make the link between formal annotations and formal specification.
- tests can be put either as comments or as external files, but please not as aspects. It is ugly to write the detail of a procedure in the spec.


Forget Aspects and worst expression functions : they are simply an error.
Mixing testing, specification and proofs as pragma or aspects or a combination of both of them will result in a too complicated language lacking of abstraction and a proper syntax.

Regards 

Vincent

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

[Simon Wright]

Stefan.Lucks@uni-weimar.de writes:

>    procedure Count_Vote(Vote: Vote_Type;
>                         Count_A, Count_B, Invalid: out Natural)
> 	with Depends (Count_A => Vote, Count_A,
>                       Count_B => Vote, Count_B,
>                       Invalid => Vote, Invalid);

We'd hope this would fail verification because eg Count_A is an out
parameter and therefore the result can't depend on the original value!

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

[Simon Wright]

vincent.diemunsch@gmail.com writes:

> Spark imposes static memory allocation to be able to prove total
> correctness, which means that the program will always do what is
> expected, which is required by embedded softwares...

Not at all sure that's true! Safety-related, security-related: probably,
other fields, not so much.

I just saw the Tony Hoare quote from 1995 (3rd quotation of [1]):

   "Ten years ago, researchers into formal methods (and I was the most
   mistaken among them) predicted that the programming world would
   embrace with gratitude every assistance promised by formalisation to
   solve the problems of reliability that arise when programs get large
   and more safety-critical. Programs have now got very large and very
   critical -- well beyond the scale which can be comfortably tackled by
   formal methods. There have been many problems and failures, but these
   have nearly always been attributable to inadequate analysis of
   requirements or inadequate management control. It has turned out that
   the world just does not suffer significantly from the kind of problem
   that our research was originally intended to solve."

[1] http://en.wikipedia.org/wiki/Tony_Hoare#Quotations

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

[Randy Brukardt]

<Stefan.Lucks@uni-weimar.de> wrote in message 
news:alpine.DEB.2.10.1307100904530.27942@debian...
On Tue, 9 Jul 2013, Randy Brukardt wrote:
> <Stefan.Lucks@uni-weimar.de> wrote:

>>> So you think, information flow analysis is completely worthless? (I 
>>> mean,
>>> for building and verifying correct systems -- as a compiler writer you
>>> will not question the usage of information flow analysis inside the
>>> compiler or optimiser).
>>
>> Information flow *within* a subprogram is important. Information flow
>> *between* subprograms is completely defined by the subprogram's 
>> interfaces
>> and calls.
>
>Firstly, for current Ada (i.e., Ada 2012) this is completely wrong
>whenever a program manipulates global variables. Even specifying pre- and
>postconditions doesn't guarantee the absence of any other (side-)effects.
>(You are right, however, a proper "global" annotation would seem to catch
>this.)

I'm always presuming a proper globals annotation. You really can't do 
anything without it (Janus/Ada does almost no optimizations across 
subprogram calls precisely because Ada doesn't have this information in its 
contracts).

>Secondly, Ada's "in", "out", and "in out" information give only a cursory
>view of what is going on.

Of course. But that and the postcondition is all you ought to be depending 
upon. If you're depending on more, your program is more fragile than it 
ought to be.

... (detailed and possibly interesting examples of Depends removed)

 ...
>Without "Depends", your cool analysis tool verifying all pre- and
>postconditions will not catch this bug.

Sure, but so what? It's a fools game to try to catch all bugs, it not even a 
worthwhile goal. (That's essentially where Spark goes wrong, in my view.)

If you had some magic annotations that could specify a totally bug-free 
program, then there no longer is any need for the program at all. Just 
execute the annotations, and forget the error-prone Ada code!

What I care about is extending what Ada already does well: catch the 
low-hanging fruit of bugs. There are always going to be a few really tough 
bugs that aren't going to be detectable automatically -- the goal should be 
to reduce that number in practical programs (no matter how large), not to 
eliminate all bugs in a barely usable subset of tiny programs.

Think about all of the "bugs" that we Ada programmers don't really have to 
deal with, because the compiler or runtime has already automatically 
detected it. That's not just type errors and array indexes out of range, but 
also dereferencing null pointers, accessing the wrong variant in a record, 
and many more. (I don't think Janus/Ada would have ever worked reliably 
without the variant check -- the early versions always had weird stability 
problems that disappeared as soon as we implemented the variant checks [and 
spent months eliminating all of the errors that turned up]).

What I think is important is bringing that level of ability to user-defined 
properties (think Is_Open and Mode for Text_IO files), and detecting more of 
these problems at compile-time (which is always better then runtime).

It's not being able to detect every possible bug.

My main point is that I think people are trying to solve the wrong problem, 
and that leads to having over-elaborate contracts.

>I agree that no one should depend on what the body of some Subprogram
>does. But then, information flow analysis is actually useful!

...in very marginal cases. I don't think it's worth trying to cover every 
possible base, certainly not before compilers even do a passible job on the 
easy cases. Once every Ada compiler does basic proof using 
pre/post/globals/exception contracts, we can revisit.

                                                    Randy.

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

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:6pqhcwi0wuop.15v6h3g7gkto4.dlg@40tude.net...
> On Tue, 9 Jul 2013 15:37:10 -0500, Randy Brukardt wrote:
>
>>> There are obviously goals which cannot be proven without the bodies. 
>>> Proofs
>>> about specifications are important but far not all. Consider LSP as an
>>> example. You cannot prove substitutability from interfaces. It simply 
>>> does
>>> not work. Same with almost everything else, because proving something in
>>> general is much more harder, even impossible, than proving things about 
>>> a
>>> concrete instance, e.g. body.
>>
>> My contention is such things are not worth proving. With strong enough
>> contracts (including class-wide contracts for dispatching calls, and
>> contracts on subprogram types :-), important properties of code can be
>> proven.
>
> No, that is the problem. You want to overburden the contracts with stuff
> that does not belong there. This would make the design fragile.
>
> Consider as an example stack use. Do you want to contract all subprograms
> to maximum stack use, or let the compiler to estimate stack use of a
> concrete body?

As I said, these sorts of things aren't worth proving. Certainly not until 
proof of simple concepts is already a widely used feature of Ada; then 
expanding it further might make sense. But we have to walk before we can 
run, and we're barely crawling right now.

> Another example is a mathematical function like sine. In order to prove 
> its
> correctness you would need an extremely elaborated apparatus of contract
> specification which itself will be a source of countless bugs due to its
> complexity. This is a typical over-specification. Only if somebody wanted
> to verify an implementation of sine, he would have to look into the body.
> Most people never will.

There is no reason to prove such things. For things like Sine, the best one 
can do is copy an implementation from a cookbook -- it makes no sense to 
even imagine trying to create a new one. (That makes as much sense as 
creating a new sort.) Even the simplest tests will detect any implementation 
errors (and we're never going to be able to live without testing).

...
>> What's too hard shouldn't be bothered with, because we've lived just
>> fine with no proofs at all for programming up to this point.
>
> We didn't. Accessibility checks and constraint errors are a permanent
> headache in Ada.

Constraint_Errors a headache? They're a blessing, because the alternative is 
zillions of impossible to find bugs. (I lived with those in the early days 
of Janus/Ada; I'll never go back.) It will never, ever be possible to detect 
every runtime failure at compile-time, nor is it possible to pre-test 
because of the possiblity of race conditions, so we have to have 
Constraint_Error.

It's annoying that one can't tell between specification errors that should 
be contracted and proved away and those that are truly runtime (that is, a 
normal part of the implementation); Ada does conflate these things and 
that's probably annoying to a purist. (You can't seem to see the difference, 
which leads to bizarre conclusions.) But it's far from fatal.

                                          Randy.

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

[Randy Brukardt]

<vincent.diemunsch@gmail.com> wrote in message 
news:7ebe0439-fa4c-4374-a6c7-365ac78e6e39@googlegroups.com..., replying to 
me

>> I think existing Spark is evil, in that it funnels off effort best 
>> applied
>> to the entire Ada language (or at least, a much larger subset). Computers
>> are now powerful enough that the excuses for avoiding proofs of 
>> exceptions,
>> dynamic memory allocation, and the like no longer are valid.
>
>Spark imposes static memory allocation to be able to prove total 
>correctness,
>which means that the program will always do what is expected, which is 
>required
>by embedded softwares...

The idea of "total correctness" is exactly what I object to. It's a false 
promise that only works on tiny, toy programs. Real Spark programs almost 
always interface to "regular" Ada code to do stuff that Spark can't handle, 
and once you've done that, you've lost your "total correctness".

In any case, static memory allocation is not necessary to prove correctness. 
All that's needed is a discipline in manging dynamically allocated memory 
(as happens inside of the containers, for instance). Ada already has strong 
typing of pointers, so the only problem to be avoided that affects 
correctness is premature destruction. Moreover, in Ada, you can use pools to 
keep the memory "theaters" separate, so you can avoid problems with 
fragmentation. (Although those are way overblown, they're very unlikely to 
occur in practice.)

It's certainly true that a tiny minority of systems cannot have any 
possibility of downtime, and those probably may have to stick with static 
allocation (although they could still use pools as an alternative). But it 
is silly to describe that as any sort of mainstream need.

>> The Globals notation is much more important. We tried to design such a
>> notation for Ada 2012, but it became too much work to complete and there 
>> was
>> a lot of concern about getting it wrong. So we left this for the 
>> "experts".
>> It appears that the experts are working on it, which is good, because we
>> still want this capability in the next version of Ada (whenever that will
>> be). And for that to be the case, we'll need it to have proper Ada syntax
>> using aspects.

>Ada has been designed so as to let global variables be freely accessed. 
>Only a
>pragma was used to specify that a function is Pure (of side effects) and 
>can be
>skipped for optimisation. Therefore it is now almost impossible to change 
>that

Right, we'd never change that.

>and that is probably the reason why you had so much difficulties to define 
>the
>global annotation, which is trivial,

It's not remotely trivial, because you have to deal with global variables 
that you don't have visibility onto and thus must not name (those in package 
bodies, especially), you have to deal intelligently with storage pools and 
access types, and you have to deal with generic units. Spark ignores almost 
all of these issues by not allowing the constructs, which is a non-starter 
for a construct for the full Ada language. We also required checking that 
the annotations were accurate, and that too is a fairly complex issue.

>because how will you deal with a procedure that have no annotation, but 
>still
>uses global variables ? A simple warning at compile time ? Refuse to 
>compile ?

No annotation means "uses anything", of course. You have to specify that a 
routine does NOT use globals. Perhaps that's backwards of what we would do 
if starting from scratch, but we're not starting from scratch. This is the 
same way we dealt with "overriding" and "limited" and lots of other things.

>Aspects syntax is ugly. It is simply the return of a kind of primitive 
>language like LISP,
>done with words and arrows. It shows clearly that it is simply a 
>workaround.

It's ten times better than using pragmas. Pragmas are the worst possible way 
to do anything. The rest is just Ada expression syntax, which has the 
distinct advantage that programmers don't have to learn anything new to use 
it. If you don't believe that Ada syntax is far superior to any other 
language's syntax, go back to curly bracket hell. :-) The barrier to using 
Spark is far too high, because it's a completely new syntax.

I agree with you that the Depends syntax is ugly, but that's mainly because 
Depends is a stupid thing that should not exist, and thus does not fit at 
all into the Ada model.

>> No, to allow *compile-time* analysis of pre and post conditions. An Ada
>> compiler cannot look into the body of a package to see what is there, and
>> without expression functions, almost no compile-time analysis could be
>> accomplished. (We also need globals annotations for similar reasons.) The
>> real end-game here ought to be compile-time proof (that is, proofs that 
>> are
>> created as part of the normal compilation of Ada code).

>A proof can't be generated at compile time ! The proof must be written
>independently, based on formal specification, and checked by an analyser,
>that may or may not be the compiler.

Wow, what an elitist attitude! *Every* compiler, for every language, uses 
proof techniques when it does optimizations and code generation. "I can 
prove that V always has value 5 here, because every path to here either 
fails to modify V or sets it to 5." Why shouldn't Ada programmers have 
access to that sort of checking?

Moreover, only a very small number of people/projects are willing to spend 
extra time to prove a working program. Schedules and the like make those 
sorts of extras the first thing to go. If we want more people to use these 
sorts of tools, they have to be integrated into the compiler so that using 
them is just as automatic as getting type and range checks.

>> Proofs of any kind should never, ever depend on anything in the package 
>> body
[other than the subprogram that you are proving, of course.]

>As others told you, a proof is a proof that the implementation respects the 
>specification,
>therefore it needs to make an interpretation of the package body.

If the one, single package body that it is currently proving. Looking into 
any *other* package body adds additional dependencies.

>> Spark users are on a certain dead-end, IMHO. The future is getting proof
>> into the hands of all programmers, as a normal part of their day-to-day
>>  programming. That requires that proofs aren't necessarily complete, that
>> hey use whatever information is available, and most of all, that they 
>> only
>> depend on the specifications of packages (never, ever, on the contents of 
>> a
>>  body).

>But you seem to make also the confusion between a test and a proof, and 
>that is
>exactly what AdaCore is doing now : they simply write the tests as post-
>conditions and uses symbolic interpretation during compile time. I think 
>that is
>what you mention by "into the hands of all programmers", ie even those with
>very few theoretical background.

Right; no one should need to understand the details in order to get the 
benefits. Do you understand how your Ada compiler does code selection or 
optimization? Of course not, but you still get the benefits.

And the entire point is that there is a strong correlation between test and 
proof. The programmer writes a "test" (as you put it; Ada 2012 calls it an 
assertion), and the compiler uses proof to verify that it is true (including 
all of the optimization tricks that compiler writers have been using for 
decades. If the proof is true, the "test" is eliminated from the generated 
code; if the proof fails, the "test" is generated, and the programmer gets a 
warning or error (depending on switches).

>It's a nice feature to sell and great fun for compiler writers but it's far 
>from a mathematical
>proof and what Spark was able to do. But mathematical proof requires formal 
>specification
>and that is far from the "all programmers" knowledge. The problem is that 
>recent books on
>Spark completly forgot to speak of the necessary formal specifications 
>(like Z for instance).

This is a case of the tail wagging the dog. (It's not surprising though, 
people often get so wrapped up in something that they forget why they 
started to do it in the first place.)

The goal here is to reduce the number of bugs in programs. No one cares how 
that is accomplished. "Formal mathematical proof" is one such tool, but it's 
almost completely inaccessible to the average programmer and project. And no 
project manager cares about a formal proof; they only care that their 
project is finished on time with a minimal number of bugs.

>To conclude here is my vision of Spark and Ada :
>- use Ada for things that are necessary for the compiler to produce the 
>code and to
>  express the semantic of the program.
>- use Pragmas only as compiler directives, for specific implementation or 
>optimisation
> (InLine, Ravenscar, Remote-Call-Interface...). Not for assertion, tests or 
> whatever.
Pragmas shouldn't be used for anything, IMHO. Maybe other that global 
properties; certainly nothing specific to an entity.
>- everything that is related to formal verification should stay as comment 
>in
>the code. These comments can then be verified by external tools. There can 
>be
>different levels of verification, not only the Spark vision.
>- formal specifications are necessary for formal verification, therefore 
>Spark
>should be able to make the link between formal annotations and formal 
>specification.
>- tests can be put either as comments or as external files, but please not 
>as aspects.
>It is ugly to write the detail of a procedure in the spec.

>Forget Aspects and worst expression functions : they are simply an error.
>Mixing testing, specification and proofs as pragma or aspects or a 
>combination
>of both of them will result in a too complicated language lacking of 
>abstraction and
>a proper syntax.

Too late, Ada 2012 was standardized in December and couldn't be recinded if 
we wanted to. Far too much code already exists. You should have come to the 
ARG and made these comments 3 years ago. Of course, it's unlikely that they 
would have changed anything -- we had comments from members of the formal 
methods community and they were taken very seriously. And we decided to go 
with aspects, expression functions and the like. Now that the path has been 
set, it's likely that most will follow along.

You of course don't have to follow the path -- you can stay with Ada 2005 
and Spark 2005 (which I'm sure will continue to be supported for a long time 
to come). But if you want to stay at the bleeding edge, then you're going to 
have to adopt Ada 2012, and everything that comes with it.

It's fairly clear that you have a real problem with the Ada model of 
specification (as it has existed forever), because there is no mixing here: 
assertions, proofs, and specifications are all different aspects (sorry 
about the pun) of the same whole; what's artifical is separating them in the 
first place.

The truly formal stuff shouldn't be in the Ada source code at all (I'd go so 
far as to say it shouldn't *exist* at all, but who am I to prevent people 
from wasting their time).

Anyway, good luck, no matter how you decide to proceed with Ada. I hope of 
course, that you will get over your initial reaction to Ada 2012 and join us 
in a better future way of programming, but if not, good luck wasting time. 
:-)

                               Randy.

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

[Simon Wright]

"Randy Brukardt" <randy@rrsoftware.com> writes:

> problems with fragmentation. (Although those are way overblown,
> they're very unlikely to occur in practice.)

That depends on the capabilities of your OS's memory manager! In our
VxWorks 5.5/Ada 95 system, it didn't take long for the heap to become so
fragmented that the system couldn't meet real-time constraints (such as
failing to kick the watchdog timer).

It was a fairly straightforward job to provide our own version of GNAT's
System.Memory to use preallocated binary-sized bins (we instrumented it
to determine the maximum number of blocks for each bin and allocated
that number at startup, with the ability to allocate further blocks at
run time if the measured maximum requirement grew).

I don't remember why use of Ada storage pools wasn't the right solution;
maybe the some of the allocations were by the runtime without the option
to use a user-defined storage pool? (things like task control blocks).

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

[Dmitry A. Kazakov]

On Wed, 10 Jul 2013 18:21:33 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:6pqhcwi0wuop.15v6h3g7gkto4.dlg@40tude.net...

>> Another example is a mathematical function like sine. In order to prove its
>> correctness you would need an extremely elaborated apparatus of contract
>> specification which itself will be a source of countless bugs due to its
>> complexity. This is a typical over-specification. Only if somebody wanted
>> to verify an implementation of sine, he would have to look into the body.
>> Most people never will.
> 
> There is no reason to prove such things. For things like Sine, the best one 
> can do is copy an implementation from a cookbook -- it makes no sense to 
> even imagine trying to create a new one.

Do you have Hankel function in your cookbook? How do you know that the copy
you made is authentic? What is about the accuracy of the implementation?

>>> What's too hard shouldn't be bothered with, because we've lived just
>>> fine with no proofs at all for programming up to this point.
>>
>> We didn't. Accessibility checks and constraint errors are a permanent
>> headache in Ada.
> 
> Constraint_Errors a headache? They're a blessing, because the alternative is 
> zillions of impossible to find bugs.

No, the alternative is to prove that the constraint is not violated.

You can do this only at the client side. Which is why it cannot be
contracted for the callee. When you move from instances to universally
holding contracts you frequently lose provability.

Note how accessibility checks attempted in the form of a contract became
more problem than solution. In order to have it provable you must
strengthen it. Probably every Ada programmer was annoyed by silly "must be
statically deeper" messages about pointers. It cannot be handled at the
level of contracts. Yet in most cases it is no problem to see that a
*given* pointer is never dangling.

> It's annoying that one can't tell between specification errors that should 
> be contracted and proved away and those that are truly runtime (that is, a 
> normal part of the implementation);

That was ARG's decision for Ada 2012, wasn't it?

> Ada does conflate these things and 
> that's probably annoying to a purist. (You can't seem to see the difference, 
> which leads to bizarre conclusions.) But it's far from fatal.

It is fatal, because inconsistent. Error /= bug.

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

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

[vincent.diemunsch]

> 
> The idea of "total correctness" is exactly what I object to. It's a false 
> promise that only works on tiny, toy programs. Real Spark programs almost 
> always interface to "regular" Ada code to do stuff that Spark can't handle, 
> and once you've done that, you've lost your "total correctness".
> 

Ok one can't prove everything, only a subset of the logic, an abstraction of the system. But total correctness is vital for :
- distributed or concurrent programs, that can't be "debugged" the usual way because they are not determinist
- embedded systems because errors means lost of lives, and it is simply not possible to test everyting : the number of tests is to high.

> In any case, static memory allocation is not necessary to prove correctness. 
Maybe, but it is easier to prove with it :-).


> It's not remotely trivial, because you have to deal with global variables 
> that you don't have visibility onto and thus must not name (those in package 
> bodies, especially), you have to deal intelligently with storage pools and 
> access types, and you have to deal with generic units. Spark ignores almost 
> all of these issues by not allowing the constructs, which is a non-starter 
> for a construct for the full Ada language. We also required checking that 
> the annotations were accurate, and that too is a fairly complex issue.
 
> No annotation means "uses anything", of course. You have to specify that a 
> routine does NOT use globals. Perhaps that's backwards of what we would do 
> if starting from scratch, but we're not starting from scratch. This is the 
> same way we dealt with "overriding" and "limited" and lots of other things.
It is easy to specify that : simply use pragma Pure.

But what I like with Spark is that they took the problem from scratch and created own annotations with abstract states and inherit clauses. It won't
be possible to do it in Ada without these abstractions, and I don't see the
point of adding these without a deep rethinking of Ada encapsulation... Because
visibility of state and data flow is nice but it is a heavy burden that not everyone wants to deal with, thus the very existence of global variables.


There is another point on which I disagree : the fact that compilers make proofs for optimisation. Compilers do symbolic computation, and this computation includes propositional calculus. Sometimes the result of a symbolic computation is called a proof, but it is not a mathematical proof in fact. A proof is the very essence of mathematics and it is a human activity. Proving programs is a human activity exactly like conception.

Spark syntax needs to be different from Ada syntax because they manipulate different things : Ada manipulates types like boolean, integers. Spark annotations manipulates propositions based on abstraction of types (that I call categories). For instance where Ada sees : 
X : Positive; 
Spark Sees :
X : root_integer;
X >= 0;
X < Integer'Last;
So it is a nonsense to keep the Ada syntax for annotations and to allow them to be transformed as tests, because in doing so one looses abstraction.

> If you don't believe that Ada syntax is far superior to any other 
> language's syntax, go back to curly bracket hell. :-)
I like the Ada syntax, and also the Spark syntax :-)


> Wow, what an elitist attitude!
Ada must be better than C or Java otherwise it will disappear.


> Moreover, only a very small number of people/projects are willing to spend 
> extra time to prove a working program. Schedules and the like make those 
> sorts of extras the first thing to go. 
Right. Spark is for the elite, trying to sell it to everybody will result in a big disappointement.


> Too late, Ada 2012 was standardized in December and couldn't be recinded if 
> we wanted to. Far too much code already exists. You should have come to the 
> ARG and made these comments 3 years ago. 
I wish I could.

> Of course, it's unlikely that they would have changed anything -- we had 
> comments from members of the formal methods community and they were taken 
> very seriously. And we decided to go with aspects, expression functions 
> and the like. Now that the path has been set, it's likely that most will 
> follow along.
 
> You of course don't have to follow the path -- you can stay with Ada 2005 
> and Spark 2005 (which I'm sure will continue to be supported for a long time 
> to come). But if you want to stay at the bleeding edge, then you're going to 
> have to adopt Ada 2012, and everything that comes with it.

I will use Ada 2012, except annotations and expression functions, and Spark 2005. I think that Spark 2014 will be a dilemna for many people, and it will divide the little community in two : those who follow and those who stay with comment annotations. Since all tools are OpenSource, the second may try to make an evolution of the annotations, as I proposed.

> Anyway, good luck, no matter how you decide to proceed with Ada. I hope of 
> course, that you will get over your initial reaction to Ada 2012 and join us 
> in a better future way of programming, but if not, good luck wasting time. 
> :-)

I hope that it won't be a total waste of time, because I think that the error of AdaCore is that they thought they could use the tools and techniques from Frama-C. According to some researcher, Frama-C tools are better than Spark tools (more advanced, but more reliable ?), but the ACSL language is not at all as good as Spark. The trick is that while improving the tools, which was their job, they thought they could change the language and make it like ACSL (E-ACSL, the new version they created). But in doing so they lost the very specificity of Spark : not only its clear syntax, but its higher abstraction level, just as Ada has higher abstraction level as C or Java.

Regards,

Vincent

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

[Dmitry A. Kazakov]

On Thu, 11 Jul 2013 03:10:51 -0700 (PDT), vincent.diemunsch@gmail.com
wrote:

> Spark syntax needs to be different from Ada syntax because they manipulate
> different things : Ada manipulates types like boolean, integers. Spark
> annotations manipulates propositions based on abstraction of types (that I
> call categories).

Yes this is a crucial point. These are two different languages where one
(Ada) is a subject of another (SPARK). Statements in these languages should
be visually distinct.

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

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

[Stefan.Lucks]

[-- Attachment #1: Type: TEXT/PLAIN, Size: 1783 bytes --]

On Wed, 10 Jul 2013, Randy Brukardt wrote:

>> Secondly, Ada's "in", "out", and "in out" information give only a cursory
>> view of what is going on.
>
> Of course. But that and the postcondition is all you ought to be depending
> upon. If you're depending on more, your program is more fragile than it
> ought to be.

Your program can depend on whatever has been specified (and hopefully 
proven) in the specification. Which is one reason why "Depends" is 
actually useful -- you are allowed to make more specific contracts.

> ... (detailed and possibly interesting examples of Depends removed)
>
> ...
>> Without "Depends", your cool analysis tool verifying all pre- and
>> postconditions will not catch this bug.
>
> Sure, but so what? It's a fools game to try to catch all bugs, it not even a
> worthwhile goal. (That's essentially where Spark goes wrong, in my view.)

Who said, catch all bugs? I didn't.

> What I care about is extending what Ada already does well: catch the
> low-hanging fruit of bugs.

By my own experience, having worked occasionally with SPARK, information 
flow analysis actually catches a lot of errors -- even without having 
specified any pre- or postconditions. In other words, SPARK's information 
flow analysis actually gives you the low-hanging fruits you mention.

The fruits (well, bugs) you catch by employing pre- and postconditions are 
a bit higher, actually. At least, that is what I gather from my own 
experience YMMV. Did you ever actually work with SPARK?

So long

Stefan


------  I  love  the  taste  of  Cryptanalysis  in  the morning!  ------
     <http://www.uni-weimar.de/cms/medien/mediensicherheit/home.html>
--Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universität Weimar, Germany--

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

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:1s6sw93u97355$.1n0205ucj6251.dlg@40tude.net...
> On Wed, 10 Jul 2013 18:21:33 -0500, Randy Brukardt wrote:
>
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>> news:6pqhcwi0wuop.15v6h3g7gkto4.dlg@40tude.net...
>
>>> Another example is a mathematical function like sine. In order to prove 
>>> its
>>> correctness you would need an extremely elaborated apparatus of contract
>>> specification which itself will be a source of countless bugs due to its
>>> complexity. This is a typical over-specification. Only if somebody 
>>> wanted
>>> to verify an implementation of sine, he would have to look into the 
>>> body.
>>> Most people never will.
>>
>> There is no reason to prove such things. For things like Sine, the best 
>> one
>> can do is copy an implementation from a cookbook -- it makes no sense to
>> even imagine trying to create a new one.
>
> Do you have Hankel function in your cookbook?

Don't know what it is, so I'd never try to write one.

> How do you know that the copy you made is authentic? What is about the 
> accuracy of the implementation?

That's easily determinable by unit tests (which are needed in any case - 
testing and proof are not exclusive, you need both because it's real easy to 
prove the wrong thing). If you screw up copying a cookbook function, you'll 
get results that are obviously wrong, and that's easy to detect.

>>>> What's too hard shouldn't be bothered with, because we've lived just
>>>> fine with no proofs at all for programming up to this point.
>>>
>>> We didn't. Accessibility checks and constraint errors are a permanent
>>> headache in Ada.
>>
>> Constraint_Errors a headache? They're a blessing, because the alternative 
>> is
>> zillions of impossible to find bugs.
>
> No, the alternative is to prove that the constraint is not violated.

That's completely impractical.

> You can do this only at the client side. Which is why it cannot be
> contracted for the callee. When you move from instances to universally
> holding contracts you frequently lose provability.

...of things that aren't worth proving in the first place. You get rid of 
constraint_errors from bodies by writing good preconditions, predicates, 
constraints, and exclusions in the first place. Have constraint_error from 
dereferencing a null pointer? Use an exclusion (or a pre-test). Same with 
ranges or with user properties.

If for whatever reason you can't do this, then yes you lose proveability. 
But that's the price of lowering coupling, and excessive coupling is the 
cause of almost all software inflexibility.

> Note how accessibility checks attempted in the form of a contract became
> more problem than solution. In order to have it provable you must
> strengthen it. Probably every Ada programmer was annoyed by silly "must be
> statically deeper" messages about pointers. It cannot be handled at the
> level of contracts. Yet in most cases it is no problem to see that a
> *given* pointer is never dangling.

"No problem"? Informally, sure. It's impossible to prove in any real case; 
there is too much going on. (Claw, for instance, prevents it by design, but 
I don't think there is any way to formally describe that design -- certainly 
not in systems like Spark which ignore the effects of finalization [which is 
how Claw guarentees non-dangling]).

>> It's annoying that one can't tell between specification errors that 
>> should
>> be contracted and proved away and those that are truly runtime (that is, 
>> a
>> normal part of the implementation);
>
> That was ARG's decision for Ada 2012, wasn't it?

No, it was an effect of Ada 83, which conflated those uses of exceptions. We 
had to formalize existing practice (we need the ability to add these 
specifications to existing code without changing any behavior). It would be 
better for exceptions that we would want to "prove-away" (like Status_Error 
and Mode_Error in Text_IO) to be strictly separated from those that are 
purely runtime behavior (like End_Error and Device_Error).

One thing we had to do is to make these things work is to allow existing 
compilers to use runtime checks, with the hope that more will become proved 
over time. Compiler technology isn't quite ready for mandatory proof 
requirements (maybe next time).

>> Ada does conflate these things and
>> that's probably annoying to a purist. (You can't seem to see the 
>> difference,
>> which leads to bizarre conclusions.) But it's far from fatal.
>
> It is fatal, because inconsistent. Error /= bug.

We can only agree to disagree on that.

                      Randy.

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

[Randy Brukardt]

"Simon Wright" <simon@pushface.org> wrote in message 
news:lyppupvcs3.fsf@pushface.org...
> "Randy Brukardt" <randy@rrsoftware.com> writes:
>
>> problems with fragmentation. (Although those are way overblown,
>> they're very unlikely to occur in practice.)
>
> That depends on the capabilities of your OS's memory manager! In our
> VxWorks 5.5/Ada 95 system, it didn't take long for the heap to become so
> fragmented that the system couldn't meet real-time constraints (such as
> failing to kick the watchdog timer).

I suppose I should know better than to presume most programmers are 
competent. ;-)

My personal experience is that fragmentation is rare at best. We had a bit 
of trouble with it in our MS-DOS compilers, that mainly came from allocating 
lots of objects, each one slightly larger than the last (pretty much the 
worst case for heap use). Changing to a quadradic size increase (rather than 
a linear one) got rid of that problem (as did moving some tiny objects to 
their own manager [allocated once and never freed back to the main heap] - 
today I'd use a custom pool for that).

I was very worried that the long running web server and spam filter would 
suffer from fragmentation, but I've never seen any evidence of that, even 
after running two months and having processed a half a million requests. 
Apparently, the Windows heap manager is smart enough to prevent it, as the 
fragmentation goes up a bit in the first few hours after the servers get 
started and then stays pretty constant after that.

> It was a fairly straightforward job to provide our own version of GNAT's
> System.Memory to use preallocated binary-sized bins (we instrumented it
> to determine the maximum number of blocks for each bin and allocated
> that number at startup, with the ability to allocate further blocks at
> run time if the measured maximum requirement grew).
>
> I don't remember why use of Ada storage pools wasn't the right solution;
> maybe the some of the allocations were by the runtime without the option
> to use a user-defined storage pool? (things like task control blocks).

Obviously, the best solution is to replace a bad heap by a good one. Won't 
work in every circumstance, but it will in 98% of them.

                          Randy. 

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

[Shark8]

On Wednesday, July 10, 2013 6:36:42 PM UTC-6, Randy Brukardt wrote:
> 
> The idea of "total correctness" is exactly what I object to. It's a false 
> promise that only works on tiny, toy programs. Real Spark programs almost 
> always interface to "regular" Ada code to do stuff that Spark can't handle, 
> and once you've done that, you've lost your "total correctness".

Interesting sentiment, I'm not sure I agree with you -- though I can see what you're saying -- as a counter-example there's IRONSIDES, a DNS server that is "provably exception-free, contains no data flow errors, and terminates only in the ways that its programmers explicitly say that it can."

http://ironsides.martincarlisle.com/


I think we DO need "total correctness" in the lower levels of our software-stacks. Specifically OSes and compilers; I, for one, would love to see a proved Ada OS (no *nix, please) developed on a proved Ada compiler. -- I don't *know* if that would be "in demand" by the industry (but then, the industry is embracing C-style languages and ramming their heads on the walls built by those misdesigns).

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

[Randy Brukardt]

<vincent.diemunsch@gmail.com> wrote in message 
news:a20ef22c-36f0-4c04-8d79-6aaadabb8fa6@googlegroups.com, replying to me:

>> The idea of "total correctness" is exactly what I object to. It's a false
>> promise that only works on tiny, toy programs. Real Spark programs almost
>> always interface to "regular" Ada code to do stuff that Spark can't 
>> handle,
>> and once you've done that, you've lost your "total correctness".
>
>
>Ok one can't prove everything, only a subset of the logic, an abstraction 
>of the system.
> But total correctness is vital for :
>- distributed or concurrent programs, that can't be "debugged" the usual 
>way because
> they are not determinist
>- embedded systems because errors means lost of lives, and it is simply not 
>possible
> to test everyting : the number of tests is to high.

I'm pretty amazed to find out that I can't debug concurrent programs, 
because I've been doing it for decades. On top of that, unit tests almost 
never involve any concurrency (just like proofs rarely do), so that it 
irrelevant for the vast majority of debugging (and the sorts of things that 
you would prove with Spark).

...
>> No annotation means "uses anything", of course. You have to specify that 
>> a
>> routine does NOT use globals. Perhaps that's backwards of what we would 
>> do
>> if starting from scratch, but we're not starting from scratch. This is 
>> the
>> same way we dealt with "overriding" and "limited" and lots of other 
>> things.

>It is easy to specify that : simply use pragma Pure.

Nope. First of all, pragma Pure allows the use of lots of kinds of globals - 
just do a dereference somewhere in the package. Secondly, pragma Pure only 
works on packages. It's extremely difficult to find any package that could 
have pragma Pure applied, because that means that there is no I/O, no access 
types, no clock/timers. I've never found any package of mine that could use 
it (almost all of my private types include a way to trace themselves, which 
you can't do in a pure package).

Moreover, do you know that adding pragma Pure to a package could make it 
erroneous (even if it is legal and compiles correctly)? Pure has a number of 
holes that make a program that uses it potentially less safe than one that 
does not. Because of this, I'm surprised that a safety-critical program 
would allow it to be used at all.

GNAT has a pragma Pure_Function which can be used on a single function. This 
isn't in Ada because it is just an assumption; there is no checks at all 
whether it is true. In that case, any mistake in the function would make a 
program calling it erroneous (because the compiler is allowed to assume the 
function is pure, even if it isn't). It can only be made safe if it is 
combined with a proof that there are no side-effects, in which case it 
surely should never be separated from that proof -- but pragmas are *always* 
separated from the thing they apply to. As such, they are never appropriate 
for setting properties of single entities.

>But what I like with Spark is that they took the problem from scratch and
> created own annotations with abstract states and inherit clauses. It won't
>be possible to do it in Ada without these abstractions, and I don't see the
>point of adding these without a deep rethinking of Ada encapsulation...

The point is very simple: Ada *compilers* can generate better code if they 
have this additional information. It isn't just useful for proofs. (And that 
has nothing to do with other annotations, either; it's unrelated to 
assertions like preconditions.) And there is no way that we're ever going to 
put anything significant to Ada compilers (and Ada programmers) into 
comments.

Ada encapuslation is one of the things Ada gets better than other 
languages -- there is no reason to rethink anything. There is a need to 
allow people who want to to give additional information to both readers and 
the Ada compiler.

> Because visibility of state and data flow is nice but it is a heavy burden
>that not everyone wants to deal with, thus the very existence of global
> variables.

Quite right, which is why the default has to be to live without that 
information. If you want to add it, you'll get more error detection at 
compile-time, possibly better code (even with all checking turned off), and 
provide more information for tools like Spark. A win-win in my mind.

>There is another point on which I disagree : the fact that compilers make
>proofs for optimisation. Compilers do symbolic computation, and this
>computation includes propositional calculus. Sometimes the result of a
>symbolic computation is called a proof, but it is not a mathematical proof
>in fact. A proof is the very essence of mathematics and it is a human
>activity. Proving programs is a human activity exactly like conception.

I agree that your definition of proof is wildly different than mine. What 
you're interested in I find not only irrelevant but actively harmful. The 
last thing we need (in any field!) is more human activities. Humans make 
mistakes; the more the computer does of the checking the better. And we 
absolutely do not need any additional tasks in programming; the pressure to 
take short-cuts is already very high and anything "extra" is very liable to 
be cut.

>Spark syntax needs to be different from Ada syntax because they manipulate 
>different
>things : Ada manipulates types like boolean, integers. Spark annotations 
>manipulates
>propositions based on abstraction of types (that I call categories). For 
>instance where
>Ada sees :
>X : Positive;
>Spark Sees :
>X : root_integer;
>X >= 0;
I hope Spark sees
X >= 1
else it isn't even proving the right thing. ;-)
>X < Integer'Last;
Well, an Ada compiler sees:
X : root_integer;
Check X in 1 .. Integer'Last.
This is not materially different.
>So it is a nonsense to keep the Ada syntax for annotations and to allow 
>them
>to be transformed as tests, because in doing so one looses abstraction.

Only if you don't understand Ada semantics. Having two different ways to 
write the same thing doesn't add any abstraction!

>> If you don't believe that Ada syntax is far superior to any other
>> language's syntax, go back to curly bracket hell. :-)
>I like the Ada syntax, and also the Spark syntax :-)

Fine, then stick with it.

>> Wow, what an elitist attitude!
>Ada must be better than C or Java otherwise it will disappear.

It already is. And this has nothing to do with Spark.

>> Moreover, only a very small number of people/projects are willing to 
>> spend
>> extra time to prove a working program. Schedules and the like make those
>> sorts of extras the first thing to go.
>Right. Spark is for the elite, trying to sell it to everybody will result 
>in a
>big disappointement.

Then, IMHO, it's not worth having. We need more customers for Ada as a 
whole, not a series of fractionated subsets. And to do that, we need *Ada* 
to be better.
...
>I will use Ada 2012, except annotations and expression functions, and Spark 
>2005.

Since aspects (and especially precondition and postcondition aspects) are 
pretty much the only new feature in Ada 2012 of significance (pretty much 
everything else was designed to support them, other than some of the 
containers related things), you'll end up using Ada 2005 plus if 
expressions. That's hardly counts as using Ada 2012.

I certainly would not call any code that uses an entity-specific pragma Ada 
2012 code. (I'd also call it evil, but that's just me.)

...

                                            Randy.

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

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:2bvcgf0jmjcv$.79izri1n5n9r.dlg@40tude.net...
> On Thu, 11 Jul 2013 03:10:51 -0700 (PDT), vincent.diemunsch@gmail.com
> wrote:
>
>> Spark syntax needs to be different from Ada syntax because they 
>> manipulate
>> different things : Ada manipulates types like boolean, integers. Spark
>> annotations manipulates propositions based on abstraction of types (that 
>> I
>> call categories).
>
> Yes this is a crucial point. These are two different languages where one
> (Ada) is a subject of another (SPARK). Statements in these languages 
> should
> be visually distinct.

The problem here is that there is a strong overlap in these annotations. If 
you make them completely distinct, you'll have to write most of them twice 
(especially globals contracts, which you'll want for the optimization/code 
generation benefits, and preconditions and predicates, because they expose 
what otherwise are checks buried in subprogram bodies [where they never can 
be eliminated] to the compiler [which can then eliminate them from the call 
site - no matter whether you are using proofs or not]). These to me are a 
code quality issue, and items intended for the Ada compiler have to be in 
the Ada syntax.) And I agree that you don't want to make them completely the 
same either (Ada has no use for the "depends" annotation that I can see; Ada 
code shouldn't have items in it that are of no use to an Ada compiler).

Which leaves us with a problem that isn't obvious to solve. AdaCore is 
trying.

Anyway, I've said enough on this topic.

                                Randy.

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

[Randy Brukardt]

<Stefan.Lucks@uni-weimar.de> wrote in message 
news:alpine.DEB.2.10.1307112112110.8707@debian...
On Wed, 10 Jul 2013, Randy Brukardt wrote:

...
>> ... (detailed and possibly interesting examples of Depends removed)
>>
>> ...
>>> Without "Depends", your cool analysis tool verifying all pre- and
>>> postconditions will not catch this bug.
>>
>> Sure, but so what? It's a fools game to try to catch all bugs, it not 
>> even a
>> worthwhile goal. (That's essentially where Spark goes wrong, in my view.)
>
>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.

>> What I care about is extending what Ada already does well: catch the
>> low-hanging fruit of bugs.
>
>By my own experience, having worked occasionally with SPARK, information
>flow analysis actually catches a lot of errors -- even without having
>specified any pre- or postconditions. In other words, SPARK's information
>flow analysis actually gives you the low-hanging fruits you mention.

Preconditions (and constraints) come first. You write them before you write 
any bodies, before you write any comments even - they're an integral part of 
the specification of a subprogram. So the situation you speak of isn't even 
possible.

Moreover, the vast majority of the information in "Depends" is already in 
the Ada subprogram specification (once you include its pre and 
postconditions). The question is how much it adds to already properly 
annotated subprograms, not what happens when the tools are misused.

I don't care at all about "after-the-fact" addition of these things. Hardly 
anyone is going to be adding annotations to existing packages (it's not 
clear whether we're ever going to do that for the language-defined 
packages).

>The fruits (well, bugs) you catch by employing pre- and postconditions are
>a bit higher, actually. At least, that is what I gather from my own
>experience YMMV.

Your experience seems to have been on annotating existing code, and doing it 
backwards ("depends" first). I can see why you might have annotated existing 
code that way, but that's not a goal or concern of mine. I'm only interested 
in new code, and code that's written properly (that is, the parameter modes 
tell one the data flow).

>Did you ever actually work with SPARK?

No, there wasn't a free version when I was interested. And now that there is 
a free version, I'm no longer interested because it is too restricted to be 
useful in any of my code. And it tries to do too much as well.

                                     Randy.

Slow? Ada??

[Bill Findlay]

I was amused to read this ...

On 11/07/2013 00:21, in article krkq9u$fo9$1@loke.gir.dk, "Randy Brukardt"
<randy@rrsoftware.com> wrote:
...
> For things like Sine, the best one can do is copy an implementation from a
> cookbook -- it makes no sense to even imagine trying to create a new one.

...for reasons nothing to do with that controversy.

When debugging Whetstone Algol under my KDF9 emulator I looked at the KDF9
assembly code programming of the arctan function and was completely baffled
by it, so I asked my former colleague, Michael Jamieson to investigate.
He successfully reconstructed the mathemetics behind it, which are very
non-obvious (to put it mildly).

A couple of days ago I idly wondered how well this 50 years old algorithm
would compare with modern implementations, so I wrote a test program to race
it against GNAT GPL 2013's arctan.  I expected to find that 2013 would spank
1963's botty.  To my astonishment, the old algorithm was faster.

Digging down, I found that Ada.Numerics.Long_Elementary_Functions.arctan
does quite a bit of argument range reduction and result error checking, but
finally invokes the "fpatan" opcode of the x86_64 CPU.

The 1963 algorithm, expressed in Ada 2012 but compiled with aggressive
optimization, is only 17% slower than that single CPU opcode!

Note also that, although it was designed for a machine with 48-bit floating
point, it gets the same accuracy as the hardware method on a machine with
64-bit floating point.

Here is the code, with the observed results included as commentary:

with Ada.Numerics.Long_Elementary_Functions;
with Ada.Text_IO;
with CPU_Timing;
with System.Machine_Code;

use  Ada.Numerics.Long_Elementary_Functions;
use  Ada.Text_IO;
use  CPU_Timing;
use  System.Machine_Code;

procedure arctan_test64 is

   -- typical output:
   -- R = 100000000 evaluations
   -- checksum = 5.00000005000000E+07, loop   time per repetition = 6 ns
   -- checksum = 4.38824577044418E+07, P51V15 time per evaluation = 49 ns
   -- checksum = 4.38824577044418E+07, arctan time per evaluation = 53 ns
   -- checksum = 4.38824577044418E+07, fpatan time per evaluation = 41 ns

   -- P51V15 is the KDF9 algorithm used in Whetstone Algol, ca. 1963
   -- See http://www.findlayw.plus.com/KDF9/Arctan%20Paper.pdf

   type vector is array (0..5) of Long_Float;

   V : constant vector := (  28165298.0 / 1479104550.0,
                             28165300.0 / 1479104550.0,
                             56327872.0 / 1479104550.0,
                            113397760.0 / 1479104550.0,
                            179306496.0 / 1479104550.0,
                           1073741824.0 / 1479104550.0);

   function P51V15 (x : Long_Float) return Long_Float with Inline;

   function P51V15 (x : Long_Float)
   return Long_Float is
      A : Long_Float := 1.0;
      S : Long_Float := V(0);
      B : vector;
   begin
       B(0) := sqrt(x*x + 1.0);
       -- 4 AGM (Arithmetic-Geometric Mean) cycles give a set of values ...
       for i in 0..3 loop
          A := (A+B(i)) * 0.5;
          B(i+1) := sqrt(A*B(i));
       end loop;
       -- ... that is subjected to a convergence acceleration process:
       for i in 1..5 loop
          S := S + V(i)*B(i-1);
       end loop;
       return x / S;
   end P51V15;

   -- this is the hardware arctan function of the x86_64 Core i7 CPU
   function fpatan (X : Long_Float) return Long_Float with Inline;

   function fpatan (X : Long_Float)
   return Long_Float is
      Result  : Long_Float;
   begin
      Asm(Template  => "fld1"
                     & Character'Val(10) -- LF
                     & Character'Val(9)  -- HT
                     & "fpatan",
          Outputs   => Long_Float'Asm_Output ("=t", Result),
          Inputs    => Long_Float'Asm_Input  ("0", X));
      return Result;
   end fpatan;

   R : constant := 1e8; -- number of loop repetitions

   function ns_per_rep (c : CPU_Usage_in_Microseconds)
   return Natural is
   begin
      return Natural(c * 1e3 / R);
   end ns_per_rep;

   x : Long_Float;
   c : CPU_Timer;
   l : CPU_Usage_in_Microseconds;
   t : CPU_Usage_in_Microseconds;

begin
   Put_Line("R =" & Integer'Image(R) & " evaluations");

   -- determine the fixed overhead time
   x := 0.0;
   Reset_Timer(c);
   for i in 1..R loop
      x := x + Long_Float(i)/Long_Float(R);
   end loop;
   l := User_CPU_Time_Since(c);
   Put_Line("checksum =" & x'Img & ", "
          & "loop   time per repetition ="
          & Natural'Image(ns_per_rep(l)) & " ns");

   x := 0.0;
   Reset_Timer(c);
   for i in 1..R loop
      x := x + P51V15(Long_Float(i)/Long_Float(R));
   end loop;
   t := User_CPU_Time_Since(c) - l;
   Put_Line("checksum =" & x'Img & ", "
          & "P51V15 time per evaluation ="
          & Natural'Image(ns_per_rep(t)) & " ns");

   x := 0.0;
   Reset_Timer(c);
   for i in 1..R loop
      x := x + arctan(Long_Float(i)/Long_Float(R));
   end loop;
   t := User_CPU_Time_Since(c) - l;
   Put_Line("checksum =" & x'Img & ", "
          & "arctan time per evaluation ="
          & Natural'Image(ns_per_rep(t)) & " ns");

   x := 0.0;
   Reset_Timer(c);
   for i in 1..R loop
      x := x + fpatan(Long_Float(i)/Long_Float(R));
   end loop;
   t := User_CPU_Time_Since(c) - l;
   Put_Line("checksum =" & x'Img & ", "
          & "fpatan time per evaluation ="
          & Natural'Image(ns_per_rep(t)) & " ns");

end arctan_test64;

The difference in time between Ada.Numerics.Long_Elementary_Functions.arctan
and  the fpatan function above is due to the afore-mentioned range reduction
and checking.  The KDF9 programmers in 1963 were less punctillious about
such matters than we rightly expect Ada to be nowadays.

-- 
Bill Findlay
with blueyonder.co.uk;
use  surname & forename;

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

[Simon Wright]

"Randy Brukardt" <randy@rrsoftware.com> writes:

> GNAT has a pragma Pure_Function which can be used on a single
> function. This isn't in Ada because it is just an assumption; there is
> no checks at all whether it is true. In that case, any mistake in the
> function would make a program calling it erroneous (because the
> compiler is allowed to assume the function is pure, even if it
> isn't). It can only be made safe if it is combined with a proof that
> there are no side-effects, in which case it surely should never be
> separated from that proof -- but pragmas are *always* separated from
> the thing they apply to. As such, they are never appropriate for
> setting properties of single entities.

GNAT supports Pure_Function as an aspect; so you can write

   package Pf is
      function F (X : Integer) return Integer with Pure_Function;
   end Pf;

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

[Dmitry A. Kazakov]

On Thu, 11 Jul 2013 17:28:31 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:1s6sw93u97355$.1n0205ucj6251.dlg@40tude.net...

>> How do you know that the copy you made is authentic? What is about the 
>> accuracy of the implementation?
> 
> That's easily determinable by unit tests (which are needed in any case - 
> testing and proof are not exclusive, you need both because it's real easy to 
> prove the wrong thing).

Firstly, you propose to replace proofs with tests, which automatically
disqualifies the answer.

Secondly, it does not work anyway. One famous example was given by Forsythe
in his book on numerical methods. It is solving quadratic equation using
school formula. In some cases (when roots are close to each other) the
accuracy catastrophically drops for one root and increases for another. You
*cannot* catch such stuff through tests. Only analysis can, and analysis is
equivalent to proofs.

>>>>> What's too hard shouldn't be bothered with, because we've lived just
>>>>> fine with no proofs at all for programming up to this point.
>>>>
>>>> We didn't. Accessibility checks and constraint errors are a permanent
>>>> headache in Ada.
>>>
>>> Constraint_Errors a headache? They're a blessing, because the alternative 
>>> is zillions of impossible to find bugs.
>>
>> No, the alternative is to prove that the constraint is not violated.
> 
> That's completely impractical.

You *always* can do on the client's side:

exception
   when Constraint_Error =>
       Put_Line ("Oops!');
end;

Which is the point, things are much simpler on instances of use compared to
universal usage.

>> You can do this only at the client side. Which is why it cannot be
>> contracted for the callee. When you move from instances to universally
>> holding contracts you frequently lose provability.
> 
> ...of things that aren't worth proving in the first place. You get rid of 
> constraint_errors from bodies by writing good preconditions, predicates, 
> constraints, and exclusions in the first place.

Really? You can start writing preconditions for +,-,*,/,** defined in the
package Standard and continue to user defined types and subtypes. If
anything is totally impractical then the idea to move Constraint_Error from
post to pre-condition. It is wrong and will never work for anything beyond
trivial examples.

> If for whatever reason you can't do this, then yes you lose proveability.

Nope. See above. I can prove that Constraint_Error is handled by given
client. Which is what Ada programmers really want, because unhandled
Constraint_Error is by far the most common bug.
 
>> Note how accessibility checks attempted in the form of a contract became
>> more problem than solution. In order to have it provable you must
>> strengthen it. Probably every Ada programmer was annoyed by silly "must be
>> statically deeper" messages about pointers. It cannot be handled at the
>> level of contracts. Yet in most cases it is no problem to see that a
>> *given* pointer is never dangling.
> 
> "No problem"? Informally, sure. It's impossible to prove in any real case; 
> there is too much going on. (Claw, for instance, prevents it by design, but 
> I don't think there is any way to formally describe that design -- certainly 
> not in systems like Spark which ignore the effects of finalization [which is 
> how Claw guarentees non-dangling]).

Most real cases are about downward closures and stuff when pointer is
aliased argument. For the latter you need the body.

>>> It's annoying that one can't tell between specification errors that should
>>> be contracted and proved away and those that are truly runtime (that is, 
>>> a normal part of the implementation);
>>
>> That was ARG's decision for Ada 2012, wasn't it?
> 
> No, it was an effect of Ada 83, which conflated those uses of exceptions. We 
> had to formalize existing practice (we need the ability to add these 
> specifications to existing code without changing any behavior). It would be 
> better for exceptions that we would want to "prove-away" (like Status_Error 
> and Mode_Error in Text_IO) to be strictly separated from those that are 
> purely runtime behavior (like End_Error and Device_Error).

This has nothing with that.

Status_Error and Mode_Error are there because file type as designed does
not reflect its mode:

   type Read_File_Type is ...
   type Write_File_Type is ...
   type Readwrite_File_Type is Read_File_Type and Write_File_Type is ...

Done.

> One thing we had to do is to make these things work is to allow existing 
> compilers to use runtime checks, with the hope that more will become proved 
> over time. Compiler technology isn't quite ready for mandatory proof 
> requirements (maybe next time).

This is a conflation of its worst.

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

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

[Stefan.Lucks]

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.

Thirdly, maybe my example has been too artificial. Below, I'll briefly 
describe one real-world example.

>> The fruits (well, bugs) you catch by employing pre- and postconditions are
>> a bit higher, actually. At least, that is what I gather from my own
>> experience YMMV.
>
> 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!)

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.

Specifying and proving the first part of the output (X xor Y) was easy. 
But specifying and proving the checksum part turned out to be tough. So I 
stopped trying it -- concentrating on the low-hanging fruits, as you put 
it.

However, I still had the flow annotations in my spec. (I use to write the 
flow annotations first, then the pre- and postconditions, and then the 
implementation.) The flow annotations specified the flow from X and K to 
Z. And that actually caught my error of using (X xor Y) instead of X in 
the implementation.

>> Did you ever actually work with SPARK?
>
> No, there wasn't a free version when I was interested. And now that there is
> a free version, I'm no longer interested because it is too restricted to be
> useful in any of my code. And it tries to do too much as well.

Agreed! Well, certainly there are people who require as much assurance as 
SPARK 05 provides, but I did find the work with old SPARK rather tedious, 
and I don't need that amount of assurance.


-----------------
(*) The correct terminology would be "message authentication code" or 
"MAC", rather than "checksum".



------  I  love  the  taste  of  Cryptanalysis  in  the morning!  ------
     <http://www.uni-weimar.de/cms/medien/mediensicherheit/home.html>
--Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universität Weimar, Germany--

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

[Robert A Duff]

"Randy Brukardt" <randy@rrsoftware.com> writes:

> I'm pretty amazed to find out that I can't debug concurrent programs, 
> because I've been doing it for decades.

Are you done yet?

- Bob

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

[Randy Brukardt]

"Simon Wright" <simon@pushface.org> wrote in message 
news:lyd2qoutno.fsf@pushface.org...
> "Randy Brukardt" <randy@rrsoftware.com> writes:
>
>> GNAT has a pragma Pure_Function which can be used on a single
>> function. This isn't in Ada because it is just an assumption; there is
>> no checks at all whether it is true. In that case, any mistake in the
>> function would make a program calling it erroneous (because the
>> compiler is allowed to assume the function is pure, even if it
>> isn't). It can only be made safe if it is combined with a proof that
>> there are no side-effects, in which case it surely should never be
>> separated from that proof -- but pragmas are *always* separated from
>> the thing they apply to. As such, they are never appropriate for
>> setting properties of single entities.
>
> GNAT supports Pure_Function as an aspect; so you can write
>
>   package Pf is
>      function F (X : Integer) return Integer with Pure_Function;
>   end Pf;

Right, but the semantics are still (arguably) wrong. We (the ARG) eventually 
concluded that Ada can't use the name Pure_Function because we didn't want 
to interfere with the existing GNAT implementation, and doing it without any 
checking at all is just a non-starter.

                                      Randy.

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

[Randy Brukardt]

"Robert A Duff" <bobduff@shell01.TheWorld.com> wrote in message 
news:wcck3kvdfgg.fsf@shell01.TheWorld.com...
> "Randy Brukardt" <randy@rrsoftware.com> writes:
>
>> I'm pretty amazed to find out that I can't debug concurrent programs,
>> because I've been doing it for decades.
>
> Are you done yet?

I presume this is supposed to be a joke of some kind (but without a 
emoticon, can't be sure), and I'm not sure what the joke is supposed to be, 
either.

So, the serious answer: The servers appear to work properly, without 
deadlocks or other problems. There can't be 100% certainty of that, but 
hardly anyone requires that sort of certainty. I'd like a form of 
correctness-by-construction for concurrent programs, but that appears beyond 
the state of the art. I don't see proof tools adding much in this area, the 
main problem is ensuring that bad things are avoided (about the only place 
that proof might help would be in preventing livelock, but that's way down 
the list of problems).

                       Randy.

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

[Randy Brukardt]

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

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

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:1lhsyg46iz9jj.8jrvydqxt8l6.dlg@40tude.net...
> On Thu, 11 Jul 2013 17:28:31 -0500, Randy Brukardt wrote:
>
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>> news:1s6sw93u97355$.1n0205ucj6251.dlg@40tude.net...
>
>>> How do you know that the copy you made is authentic? What is about the
>>> accuracy of the implementation?
>>
>> That's easily determinable by unit tests (which are needed in any case -
>> testing and proof are not exclusive, you need both because it's real easy 
>> to
>> prove the wrong thing).
>
> Firstly, you propose to replace proofs with tests, which automatically
> disqualifies the answer.

True enough. I'm saying that we need to replace the impractical ("proofs") 
with the possible.

> Secondly, it does not work anyway. One famous example was given by 
> Forsythe
> in his book on numerical methods. It is solving quadratic equation using
> school formula. In some cases (when roots are close to each other) the
> accuracy catastrophically drops for one root and increases for another. 
> You
> *cannot* catch such stuff through tests. Only analysis can, and analysis 
> is
> equivalent to proofs.

If your "cookbook" is full of bad algorithms, then of course you'll get 
garbage. And I certainly agree you can't test accuracy. The problem is that 
even if you prove that your algorithm is too inaccurate, what can you do? 
You don't have any other way to implement it (because you already did the 
research to find the best algorithm available -- if you didn't do at least 
that, "proof" is the LEAST of your problems).

I was presuming that you were starting with a cookbook implementation of 
appropriate accuracy, and the only need for testing is to prove that the 
algorithm was in fact implemented properly.

If you're starting with a blank sheet of paper, there is no technique that 
is likely to be available in my lifetime that is reaally going to help.

...
>>> No, the alternative is to prove that the constraint is not violated.
>>
>> That's completely impractical.
>
> You *always* can do on the client's side:
>
> exception
>   when Constraint_Error =>
>       Put_Line ("Oops!');
> end;

That doesn't prove that the constraint is not violated -- that's proving 
that you covered it up! Supposedly, it's the worst side-effect of exception 
contracts in Java, is that programmers write handlers to swallow exceptions 
without knowing or caring why they're doing so.

You've got to prevent the exceptions at the source, and the main way you do 
that for Constraint_Error is to use proper range constraints and null 
exclusions on parameters. Then your proof is actually possible because we 
moved it from inside of the body to the call site.

> Which is the point, things are much simpler on instances of use compared 
> to
> universal usage.

Which of course is what I've been saying: you move these requirements into 
the contract for a subprogram so you can prove them at the call-site. It's 
impossible to prove anything in the body of a subprogram if all of the 
parameters are type Integer.

>>> You can do this only at the client side. Which is why it cannot be
>>> contracted for the callee. When you move from instances to universally
>>> holding contracts you frequently lose provability.
>>
>> ...of things that aren't worth proving in the first place. You get rid of
>> constraint_errors from bodies by writing good preconditions, predicates,
>> constraints, and exclusions in the first place.
>
> Really? You can start writing preconditions for +,-,*,/,** defined in the
> package Standard and continue to user defined types and subtypes. If
> anything is totally impractical then the idea to move Constraint_Error 
> from
> post to pre-condition. It is wrong and will never work for anything beyond
> trivial examples.

Which is amazing because it works for most examples. (It doesn't work for 
overflow of "*" very well, but that's the only real issue.) And in any case, 
there is no point in moving it for language-defined operators -- both the 
compiler and any provers know exactly what they do. It's only for 
user-defined subprograms that you need to do so.

...
>>>> It's annoying that one can't tell between specification errors that 
>>>> should
>>>> be contracted and proved away and those that are truly runtime (that 
>>>> is,
>>>> a normal part of the implementation);
>>>
>>> That was ARG's decision for Ada 2012, wasn't it?
>>
>> No, it was an effect of Ada 83, which conflated those uses of exceptions. 
>> We
>> had to formalize existing practice (we need the ability to add these
>> specifications to existing code without changing any behavior). It would 
>> be
>> better for exceptions that we would want to "prove-away" (like 
>> Status_Error
>> and Mode_Error in Text_IO) to be strictly separated from those that are
>> purely runtime behavior (like End_Error and Device_Error).
>
> This has nothing with that.
>
> Status_Error and Mode_Error are there because file type as designed does
> not reflect its mode:
>
>   type Read_File_Type is ...
>   type Write_File_Type is ...
>   type Readwrite_File_Type is Read_File_Type and Write_File_Type is ...
>
> Done.

Huh? This makes no sense for this problem. You can't do that in any version 
of Ada (or any other sensible language), because it would require that the 
type of a file object could change in response to operations. And in such a 
language, it would be impossible to do any static checks (you can't know if 
Open is going to succeed, for instance, so afterwards, the file is going to 
have one of several possible types). Which would defeat the purpose.

Ada doesn't allow changing the type of an object for any reason, and to 
change that would require designing a new language. I realize that you have 
a fantasy that such a radical redesign could be made to work compatibly, but 
that's highly unlikely.

>> One thing we had to do is to make these things work is to allow existing
>> compilers to use runtime checks, with the hope that more will become 
>> proved
>> over time. Compiler technology isn't quite ready for mandatory proof
>> requirements (maybe next time).
>
> This is a conflation of its worst.

Carried over from Ada 83. Ada will never be a language that requires much in 
the way of proof, it would be way too disruptive to existing 
implementations. (And we definitely want more than one implementation!). It 
could only be changed in a new Ada-like language, but that seems unlikely 
right now.

                                         Randy.

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

[Dmitry A. Kazakov]

On Fri, 12 Jul 2013 16:16:36 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:1lhsyg46iz9jj.8jrvydqxt8l6.dlg@40tude.net...

>> Secondly, it does not work anyway. One famous example was given by 
>> Forsythe
>> in his book on numerical methods. It is solving quadratic equation using
>> school formula. In some cases (when roots are close to each other) the
>> accuracy catastrophically drops for one root and increases for another. 
>> You
>> *cannot* catch such stuff through tests. Only analysis can, and analysis 
>> is
>> equivalent to proofs.
> 
> If your "cookbook" is full of bad algorithms, then of course you'll get 
> garbage. And I certainly agree you can't test accuracy. The problem is that 
> even if you prove that your algorithm is too inaccurate, what can you do?

This is a different question. The first one how do I prove things about
accuracy. And the answer is that I need bodies to do that and specifying
accuracy through contracts would be extremely difficult.

Answering the question, if you know that the aircraft will crash, you don't
board it.

> You don't have any other way to implement it (because you already did the 
> research to find the best algorithm available -- if you didn't do at least 
> that, "proof" is the LEAST of your problems).

There is practically never the best algorithm. In any case in order to take
a decision one needs evidences. The only reliable evidence is a proof.

>>>> No, the alternative is to prove that the constraint is not violated.
>>>
>>> That's completely impractical.
>>
>> You *always* can do on the client's side:
>>
>> exception
>>   when Constraint_Error =>
>>       Put_Line ("Oops!');
>> end;
> 
> That doesn't prove that the constraint is not violated

It handles violation, which cannot be prevented otherwise.

> You've got to prevent the exceptions at the source, and the main way you do 
> that for Constraint_Error is to use proper range constraints and null 
> exclusions on parameters.

No. Dynamic constraints cannot prevent anything. They are a part of
defining semantics so that violation could be handled elsewhere.

Only static constraints can serve prevention. If you let Constraint_Error
propagation, you already gave up with static constraints and with
provability on the whole class of all instances.

You still can have it provable on per instance basis and this is the
client's side.

> Then your proof is actually possible because we 
> moved it from inside of the body to the call site.

Yes. Bodies are needed.
 
>>>> You can do this only at the client side. Which is why it cannot be
>>>> contracted for the callee. When you move from instances to universally
>>>> holding contracts you frequently lose provability.
>>>
>>> ...of things that aren't worth proving in the first place. You get rid of
>>> constraint_errors from bodies by writing good preconditions, predicates,
>>> constraints, and exclusions in the first place.
>>
>> Really? You can start writing preconditions for +,-,*,/,** defined in the
>> package Standard and continue to user defined types and subtypes. If
>> anything is totally impractical then the idea to move Constraint_Error from
>> post to pre-condition. It is wrong and will never work for anything beyond
>> trivial examples.
> 
> Which is amazing because it works for most examples. (It doesn't work for 
> overflow of "*" very well, but that's the only real issue.) And in any case, 
> there is no point in moving it for language-defined operators -- both the 
> compiler and any provers know exactly what they do. It's only for 
> user-defined subprograms that you need to do so.

How are you going to do that for user-defined subprograms using
language-defined operations, which are all user-defined subprograms?

>>>>> It's annoying that one can't tell between specification errors that 
>>>>> should
>>>>> be contracted and proved away and those that are truly runtime (that 
>>>>> is,
>>>>> a normal part of the implementation);
>>>>
>>>> That was ARG's decision for Ada 2012, wasn't it?
>>>
>>> No, it was an effect of Ada 83, which conflated those uses of exceptions. We
>>> had to formalize existing practice (we need the ability to add these
>>> specifications to existing code without changing any behavior). It would be
>>> better for exceptions that we would want to "prove-away" (like 
>>> Status_Error
>>> and Mode_Error in Text_IO) to be strictly separated from those that are
>>> purely runtime behavior (like End_Error and Device_Error).
>>
>> This has nothing with that.
>>
>> Status_Error and Mode_Error are there because file type as designed does
>> not reflect its mode:
>>
>>   type Read_File_Type is ...
>>   type Write_File_Type is ...
>>   type Readwrite_File_Type is Read_File_Type and Write_File_Type is ...
>>
>> Done.
> 
> Huh? This makes no sense for this problem. You can't do that in any version 
> of Ada (or any other sensible language),

Of course I can. It is MI. Even in Ada it is partially possible with
interfaces, just a bit more clumsy than it should be. It is trivial to
statically ensure that Write will never be called on Read_File_Type. It has
no such operation.

> because it would require that the 
> type of a file object could change in response to operations.

Never.

>>> One thing we had to do is to make these things work is to allow existing
>>> compilers to use runtime checks, with the hope that more will become 
>>> proved over time. Compiler technology isn't quite ready for mandatory proof
>>> requirements (maybe next time).
>>
>> This is a conflation of its worst.
> 
> Carried over from Ada 83. Ada will never be a language that requires much in 
> the way of proof, it would be way too disruptive to existing 
> implementations.

I don't see how adding optional exception contracts should disrupt
anything.

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

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

[Georg Bauhaus]

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

> I don't see how adding optional exception contracts should disrupt
> anything.

Aren't exceptions already part of contracts? Implied, though.

procedure Op (x : in out T)
  with Post => Foo(x) or else False;

For clarity, 

  C_E: Boolean renames False;

procedure Op (x : in out T)
  with Post => Foo(x) or else C_E;


Or, if there seems no way of telling clients about
preventive measures, but they should
nevertheless be aware of exceptions,

procedure Op (x : in out T)
  with Post => Random or else C_E;

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

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:1d4tuwlfdnz2j$.18l68s96x3vjj.dlg@40tude.net...
> On Fri, 12 Jul 2013 16:16:36 -0500, Randy Brukardt wrote:
...
>> You've got to prevent the exceptions at the source, and the main way you 
>> do
>> that for Constraint_Error is to use proper range constraints and null
>> exclusions on parameters.
>
> No. Dynamic constraints cannot prevent anything. They are a part of
> defining semantics so that violation could be handled elsewhere.

Sorry, you definitely can prove that dynamic constraints can't be violated. 
Ada compilers do it all the time. The issue is letting the programmer have 
access to that information.

> Only static constraints can serve prevention. If you let Constraint_Error
> propagation, you already gave up with static constraints and with
> provability on the whole class of all instances.

If you don't want Constraint_Error to propagate (and generally one does 
not), then you don't put that into the exception contract for the routine. 
Hardly ever would you want that in the contract.

> You still can have it provable on per instance basis and this is the
> client's side.

No, that's making a lot more complicated that it needs to be, and I don't 
think it's possible in any useful generality.

In any case, going that route completely takes the compiler out of the 
equation. Once you do that, only an extremely limited number of users would 
care, and there will be no effect on normal programs.

...
>>>>> You can do this only at the client side. Which is why it cannot be
>>>>> contracted for the callee. When you move from instances to universally
>>>>> holding contracts you frequently lose provability.
>>>>
>>>> ...of things that aren't worth proving in the first place. You get rid 
>>>> of
>>>> constraint_errors from bodies by writing good preconditions, 
>>>> predicates,
>>>> constraints, and exclusions in the first place.
>>>
>>> Really? You can start writing preconditions for +,-,*,/,** defined in 
>>> the
>>> package Standard and continue to user defined types and subtypes. If
>>> anything is totally impractical then the idea to move Constraint_Error 
>>> from
>>> post to pre-condition. It is wrong and will never work for anything 
>>> beyond
>>> trivial examples.
>>
>> Which is amazing because it works for most examples. (It doesn't work for
>> overflow of "*" very well, but that's the only real issue.) And in any 
>> case,
>> there is no point in moving it for language-defined operators -- both the
>> compiler and any provers know exactly what they do. It's only for
>> user-defined subprograms that you need to do so.
>
> How are you going to do that for user-defined subprograms using
> language-defined operations, which are all user-defined subprograms?

Why is there a problem? Every Ada compiler (and pretty much every other 
compiler as well) does it already. The only issue is that programmers can't 
harness it for their own purposes. I would hope that exception contracts 
would be defined in order to do that.

...
>> Huh? This makes no sense for this problem. You can't do that in any 
>> version
>> of Ada (or any other sensible language),
>
> Of course I can. It is MI. Even in Ada it is partially possible with
> interfaces, just a bit more clumsy than it should be. It is trivial to
> statically ensure that Write will never be called on Read_File_Type. It 
> has
> no such operation.

But you can't know when you declare a file object what mode it will have, or 
even if it will get one. That's determined dynamically because by the result 
of Open.

>> because it would require that the
>> type of a file object could change in response to operations.
>
> Never.

You've never explained how you supposely static approach would work in the 
face of failing Opens, among other things. That's because it wouldn't work 
at all.

>>>> One thing we had to do is to make these things work is to allow 
>>>> existing
>>>> compilers to use runtime checks, with the hope that more will become
>>>> proved over time. Compiler technology isn't quite ready for mandatory 
>>>> proof
>>>> requirements (maybe next time).
>>>
>>> This is a conflation of its worst.
>>
>> Carried over from Ada 83. Ada will never be a language that requires much 
>> in
>> the way of proof, it would be way too disruptive to existing
>> implementations.
>
> I don't see how adding optional exception contracts should disrupt
> anything.

It wouldn't, and I hope we'll do that. But that doesn't have a darn thing to 
do with our discussion; I'm assuming such contracts (and global contracts) 
exist -- else absolutely nothing can be done. Everything I've been talking 
about for weeks is for Ada 202x, which certainly will have exception 
contracts if I have anything to do about it.

But you are insisting on more than that, and I think that's actively harmful 
to programming in general. You seem to insist on access to bodies even with 
such contracts, but that would prevent all compile-time checking -- the only 
kind that would benefit most programmers. I want each subprogram to be 
checked in isolation (subject its contracts), because in that case there is 
no coupling between calls and bodies.

                                     Randy.

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

[Randy Brukardt]

"Georg Bauhaus" <rm-host.bauhaus@maps.arcor.de> wrote in message 
news:984821833395507830.672948rm-host.bauhaus-maps.arcor.de@news.arcor.de...
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote:
>
>> I don't see how adding optional exception contracts should disrupt
>> anything.
>
> Aren't exceptions already part of contracts? Implied, though.

Yes, but only for inbound contracts (preconditions and predicates). We need 
them for outbound contracts as well, without having to guess. And I agree 
with Dmitry that those need to be compile-time checked in the subprogram 
bodies. (Exactly how that's done has to be worked out, of course).

procedure Op (x : in out T)
  with Post => Foo(x),
         Exception => Constraint_Error when not Foo(x);

or something like that.

                            Randy.




                                                Randy.

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

[Dmitry A. Kazakov]

On Mon, 15 Jul 2013 19:13:24 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:1d4tuwlfdnz2j$.18l68s96x3vjj.dlg@40tude.net...
>> On Fri, 12 Jul 2013 16:16:36 -0500, Randy Brukardt wrote:
> ...
>>> You've got to prevent the exceptions at the source, and the main way you 
>>> do that for Constraint_Error is to use proper range constraints and null
>>> exclusions on parameters.
>>
>> No. Dynamic constraints cannot prevent anything. They are a part of
>> defining semantics so that violation could be handled elsewhere.
> 
> Sorry, you definitely can prove that dynamic constraints can't be violated.

Only in some cases. For proofs it must be all or nothing.

> Ada compilers do it all the time. The issue is letting the programmer have 
> access to that information.

This is upside down. The programmer should manifest his intention for a
constraint to hold and the compiler should verify that. The manifest must
be syntactically visible. Conflation such declaration with dynamic
constraints is a bad idea.

>> Only static constraints can serve prevention. If you let Constraint_Error
>> propagation, you already gave up with static constraints and with
>> provability on the whole class of all instances.
> 
> If you don't want Constraint_Error to propagate (and generally one does 
> not), then you don't put that into the exception contract for the routine.

This would make the routine non-implementable, because, again, you cannot
do that on the callee side. It is a halting problem.

>> You still can have it provable on per instance basis and this is the
>> client's side.
> 
> No, that's making a lot more complicated that it needs to be, and I don't 
> think it's possible in any useful generality.

SPARK does this already. Moreover historically the concept of correctness
proofs was explicitly about instances. Only later, with the dawn of generic
programming, it was expanded onto contracts and behavior in general (e.g.
LSP). The latter is much more difficult and frequently impossible in hard
mathematical sense (undecidable).

> In any case, going that route completely takes the compiler out of the 
> equation. Once you do that, only an extremely limited number of users would 
> care, and there will be no effect on normal programs.

I disagree. I trust that most Ada programmers will enjoy trying it in their
program and gradually relaxing requirements on the proofs as they see what
can and what cannot be proved.

This process would be extremely useful for deeper understanding and
evaluation of how the given implementation works and how software
components interact each other in the concrete case (AKA software
integration).

>>>>>> You can do this only at the client side. Which is why it cannot be
>>>>>> contracted for the callee. When you move from instances to universally
>>>>>> holding contracts you frequently lose provability.
>>>>>
>>>>> ...of things that aren't worth proving in the first place. You get rid 
>>>>> of constraint_errors from bodies by writing good preconditions, 
>>>>> predicates, constraints, and exclusions in the first place.
>>>>
>>>> Really? You can start writing preconditions for +,-,*,/,** defined in the
>>>> package Standard and continue to user defined types and subtypes. If
>>>> anything is totally impractical then the idea to move Constraint_Error 
>>>> from post to pre-condition. It is wrong and will never work for anything 
>>>> beyond trivial examples.
>>>
>>> Which is amazing because it works for most examples. (It doesn't work for
>>> overflow of "*" very well, but that's the only real issue.) And in any case,
>>> there is no point in moving it for language-defined operators -- both the
>>> compiler and any provers know exactly what they do. It's only for
>>> user-defined subprograms that you need to do so.
>>
>> How are you going to do that for user-defined subprograms using
>> language-defined operations, which are all user-defined subprograms?
> 
> Why is there a problem? Every Ada compiler (and pretty much every other 
> compiler as well) does it already.

How do you prove that this does not raise Constraint_Error

   function Geometric_Mean (A, B : Float) return Float is
   begin
       return sqrt (A * B);
   end Geometric_Mean;

> The only issue is that programmers can't 
> harness it for their own purposes. I would hope that exception contracts 
> would be defined in order to do that.

Yes. But they will only help if used on the client side and when bodies are
looked into.

1. You will not prove that sqrt never raises Constraint_Error. You will do
that in *your* calls to sqrt it never does.

2. In a great number of cases you won't be able to contract *when*
Constraint_Error is to be raised. Consider this:

   function Sum (A : Float_Array) return Float;

You cannot spell the contract when Sum must raise Constraint_Error and when
not. Such a contract would much more complex (=> error prone) than the
implementation itself. This is why when the caller of Sum contracts itself
not to raise Constraint_Error, you will have to look into the body of Sum
in order to prove that. Otherwise, you will end up with Java's exception
contracts mess and brainless catch-all handlers.

>>> Huh? This makes no sense for this problem. You can't do that in any 
>>> version of Ada (or any other sensible language),
>>
>> Of course I can. It is MI. Even in Ada it is partially possible with
>> interfaces, just a bit more clumsy than it should be. It is trivial to
>> statically ensure that Write will never be called on Read_File_Type. It 
>> has no such operation.
> 
> But you can't know when you declare a file object what mode it will have, or 
> even if it will get one. That's determined dynamically because by the result 
> of Open.

Nope. Open must be a primitive operation of file type. Readonly file Open
/= write-only Open/Create.

>>> because it would require that the
>>> type of a file object could change in response to operations.
>>
>> Never.
> 
> You've never explained how you supposely static approach would work in the 
> face of failing Opens, among other things.

It is supposed to work with Read and Write.

Maybe I didn't understand your point. I didn't say that Open should not
raise Status_Error. I did that Read should not.

Opening readonly file for writing is not a bug it is an error, a legitime
state of the program which must be handled. Writing a file opened as
readonly is a bug. Bug /= error. Errors are handled, bugs are fixed.

> But you are insisting on more than that, and I think that's actively harmful 
> to programming in general. You seem to insist on access to bodies even with 
> such contracts, but that would prevent all compile-time checking -- the only 
> kind that would benefit most programmers.

I don't see how allowing correctness checks involving the bodies should
prevent correctness checks involving the specifications.

> I want each subprogram to be 
> checked in isolation (subject its contracts), because in that case there is 
> no coupling between calls and bodies.

This will be too weak to be useful. It was attempted long ago by LSP.

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

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

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:1rjye7dyn3vgk.66fbcca9y4zd.dlg@40tude.net...
> On Mon, 15 Jul 2013 19:13:24 -0500, Randy Brukardt wrote:
>
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>> news:1d4tuwlfdnz2j$.18l68s96x3vjj.dlg@40tude.net...
>>> On Fri, 12 Jul 2013 16:16:36 -0500, Randy Brukardt wrote:
>> ...
>>>> You've got to prevent the exceptions at the source, and the main way 
>>>> you
>>>> do that for Constraint_Error is to use proper range constraints and 
>>>> null
>>>> exclusions on parameters.
>>>
>>> No. Dynamic constraints cannot prevent anything. They are a part of
>>> defining semantics so that violation could be handled elsewhere.
>>
>> Sorry, you definitely can prove that dynamic constraints can't be 
>> violated.
>
> Only in some cases. For proofs it must be all or nothing.
>
>> Ada compilers do it all the time. The issue is letting the programmer 
>> have
>> access to that information.
>
> This is upside down. The programmer should manifest his intention for a
> constraint to hold and the compiler should verify that. The manifest must
> be syntactically visible. Conflation such declaration with dynamic
> constraints is a bad idea.

Yes, that's precisely what I'm talking about - some sort of exception 
contract. But those don't depend on the kind of constraint.

>>> Only static constraints can serve prevention. If you let 
>>> Constraint_Error
>>> propagation, you already gave up with static constraints and with
>>> provability on the whole class of all instances.
>>
>> If you don't want Constraint_Error to propagate (and generally one does
>> not), then you don't put that into the exception contract for the 
>> routine.
>
> This would make the routine non-implementable, because, again, you cannot
> do that on the callee side. It is a halting problem.

As you showed a couple of days ago, it's trivial on the callee side (just 
stick in a handler). The hope is to use proof techniques to reduce the cases 
where that's required, but I see no important reason to worry about 
eliminating that.

>>> You still can have it provable on per instance basis and this is the
>>> client's side.
>>
>> No, that's making a lot more complicated that it needs to be, and I don't
>> think it's possible in any useful generality.
>
> SPARK does this already.

Exactly my point! :-)

> Moreover historically the concept of correctness
> proofs was explicitly about instances. Only later, with the dawn of 
> generic
> programming, it was expanded onto contracts and behavior in general (e.g.
> LSP). The latter is much more difficult and frequently impossible in hard
> mathematical sense (undecidable).

Certainly, there is lots of stuff that's not worth proving that's not 
provable. So what? We've lived for decades without general proof and there 
is absolutely no evidence that general proof would do anything to improve 
the quality and timelyness of software. (Software that takes longer to 
develop isn't viable no matter how much better quality it actualy is.)

>> In any case, going that route completely takes the compiler out of the
>> equation. Once you do that, only an extremely limited number of users 
>> would
>> care, and there will be no effect on normal programs.
>
> I disagree. I trust that most Ada programmers will enjoy trying it in 
> their
> program and gradually relaxing requirements on the proofs as they see what
> can and what cannot be proved.

No one is going to run extra tools beyond compilation; they simply don't 
have the time. The "win" with Ada is that the extra correctness brought by 
the language comes for "free", it's an integrated part of the development 
process. (Your program cannot be run if it doesn't compile.) Extra tools 
never will have that level force behind them, and people like me would never 
run them.

...
>> Why is there a problem? Every Ada compiler (and pretty much every other
>> compiler as well) does it already.
>
> How do you prove that this does not raise Constraint_Error
>
>   function Geometric_Mean (A, B : Float) return Float is
>   begin
>       return sqrt (A * B);
>   end Geometric_Mean;

You can't, because it does. :-) Your contract is not strong enough, which is 
not surprising: you have unbounded types here -- you can prove nothing about 
such types.

But that's OK, there is no point in proving everything about everything. 
Moreover, if you made this an expression function (meaning that you are 
merely giving a name to "sqrt (A*B)", you could plug it in without any 
effect on your proof. Enjoy.

>> The only issue is that programmers can't
>> harness it for their own purposes. I would hope that exception contracts
>> would be defined in order to do that.
>
> Yes. But they will only help if used on the client side and when bodies 
> are
> looked into.

You might be right, but in that case we're wasting our time even thinking 
about proof, because any technology that requires programmer-visble access 
to bodies is evil. ("Evil" here being a shorthand for "has a bunch of bad 
properties", which I've previously outlined.) And you may say that many Ada 
compilers have such features, and I repeat that pragma Inline and 
macro-expanded generics are evil, if they have any programmer-visible 
effect. Those sorts of things are only acceptable if they are completely 
semantically invisible, and that is rarely true.



> 1. You will not prove that sqrt never raises Constraint_Error. You will do
> that in *your* calls to sqrt it never does.

You don't have to. A properly written Sqrt has a precondition, and that 
precondition raises Constraint_Error when it fails. Sqrt itself never raises 
any exception. You then prove at the call site that the precondition is met.

> 2. In a great number of cases you won't be able to contract *when*
> Constraint_Error is to be raised. Consider this:
>
>   function Sum (A : Float_Array) return Float;
>
> You cannot spell the contract when Sum must raise Constraint_Error and 
> when
> not. Such a contract would much more complex (=> error prone) than the
> implementation itself. This is why when the caller of Sum contracts itself
> not to raise Constraint_Error, you will have to look into the body of Sum
> in order to prove that. Otherwise, you will end up with Java's exception
> contracts mess and brainless catch-all handlers.

Yup, if you think that *everything* can be contracted and should be 
contracted, the only possible result is Java's mess. That's perfectly clear, 
because I certainly agree with you that you can't explain why exceptions are 
raised formally in many cases. And that's actually OK, because the point is 
to get rid of the exceptions (with smart use of constraints, predicates, and 
preconditions). If you can't do that, there's really nothing to prove and 
nothing to be gained from the contracts.

...
>> You've never explained how you supposely static approach would work in 
>> the
>> face of failing Opens, among other things.
>
> It is supposed to work with Read and Write.
>
> Maybe I didn't understand your point. I didn't say that Open should not
> raise Status_Error. I did that Read should not.

I agree with that, that's the precondition's job.

> Opening readonly file for writing is not a bug it is an error, a legitime
> state of the program which must be handled. Writing a file opened as
> readonly is a bug. Bug /= error. Errors are handled, bugs are fixed.

You claim that you can use the file type to eliminate Status_Error and 
Mode_Error. But that's impossible, because an Open that fails leaves the 
file unopened; and you have to be able to fall back and open a different 
file (or create one instead) on such a condition. It's not practical to have 
a single Open operation as an initializer -- so your scheme means that the 
file type has to change dynamically during it's lifetime. That's the purpose 
of a subtype, not of a type (in Ada terms, at least).

>> But you are insisting on more than that, and I think that's actively 
>> harmful
>> to programming in general. You seem to insist on access to bodies even 
>> with
>> such contracts, but that would prevent all compile-time checking -- the 
>> only
>> kind that would benefit most programmers.
>
> I don't see how allowing correctness checks involving the bodies should
> prevent correctness checks involving the specifications.

Because you can't have "correctness checks" involving bodies that don't 
exist. And having them depend on bodies is "evil", because it means that a 
change to a body can make a call in someone else's code fail. That's 
completely unacceptable - it would be impossible to write any reusable code 
in such an environment.

>> I want each subprogram to be
>> checked in isolation (subject its contracts), because in that case there 
>> is
>> no coupling between calls and bodies.
>
> This will be too weak to be useful. It was attempted long ago by LSP.

LSP is a dynamic thingy, completely uncheckable at compile-time.

And you may be right, in which case any sort of proof is worthless, because 
violating encapsulation instantly causes all of the bad effects that Ada 
have been designed to avoid -- changing an unrelated thing (and every body 
is unrelated in Ada terms) never makes someone else's code illegal.

                                Randy.

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

[Shark8]

On Monday, July 15, 2013 6:16:56 PM UTC-6, Randy Brukardt wrote:
> "Georg Bauhaus" <rm-host.bauhaus@maps.arcor.de> wrote in message 
> news:984821833395507830.672948rm-host.bauhaus-maps.arcor.de@news.arcor.de...
> > "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote:
> >
> >> I don't see how adding optional exception contracts should disrupt
> >> anything.
> >
> > Aren't exceptions already part of contracts? Implied, though.
> 
> Yes, but only for inbound contracts (preconditions and predicates). We need 
> them for outbound contracts as well, without having to guess. And I agree 
> with Dmitry that those need to be compile-time checked in the subprogram 
> bodies. (Exactly how that's done has to be worked out, of course).
> 
> procedure Op (x : in out T)
>   with Post => Foo(x),
>          Exception => Constraint_Error when not Foo(x);
> or something like that.
> 
>                             Randy.

I think you and I talked about that idea (basically sets of exceptions) and I like the idea a lot (though not the particular syntax you were using, which is ok) -- I really like the idea you have for renaming the violation exception, in retrospect that would have been very desirable for constraint-aspect violations (pre-/post-conditions, particularly).

The one drawback from your proposal is that it makes you reiterate the condition, but with a negation, this could be a source of bugs. Even though it's a little less straightforward the following would circumvent that problem:

 procedure Op (x : in out T)
   with Post => (Constraint_Error at [not?] Foo(x));

which would reuse the keyword(s) AT [and NOT] in addition to preventing the unnecessary duplication. {The use of parenthesis could also be mandated that way the clauses [which are different constitutions] could be made/forced-distinct when they are to raise differing exceptions on violation.}

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

[Dmitry A. Kazakov]

On Tue, 16 Jul 2013 17:13:43 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:1rjye7dyn3vgk.66fbcca9y4zd.dlg@40tude.net...
>> On Mon, 15 Jul 2013 19:13:24 -0500, Randy Brukardt wrote:

>>> Ada compilers do it all the time. The issue is letting the programmer 
>>> have access to that information.
>>
>> This is upside down. The programmer should manifest his intention for a
>> constraint to hold and the compiler should verify that. The manifest must
>> be syntactically visible. Conflation such declaration with dynamic
>> constraints is a bad idea.
> 
> Yes, that's precisely what I'm talking about - some sort of exception 
> contract. But those don't depend on the kind of constraint.

But they do, exception contract is a static constraint.

It is no matter what is constrained, but how. Dynamically (=>code) vs.
statically (=>proof).
 
>>> In any case, going that route completely takes the compiler out of the
>>> equation. Once you do that, only an extremely limited number of users 
>>> would care, and there will be no effect on normal programs.
>>
>> I disagree. I trust that most Ada programmers will enjoy trying it in their
>> program and gradually relaxing requirements on the proofs as they see what
>> can and what cannot be proved.
> 
> No one is going to run extra tools beyond compilation; they simply don't 
> have the time. The "win" with Ada is that the extra correctness brought by 
> the language comes for "free",

They aren't free as they rely on careful choice of types. This is indeed
frustrating for must programmers with C and "everything is int" background.
But Ada programmers are different, otherwise they weren't Ada programmers.

> it's an integrated part of the development 
> process. (Your program cannot be run if it doesn't compile.) Extra tools 
> never will have that level force behind them, and people like me would never 
> run them.

I always was for SPARK being integrated into Ada.

>>> Why is there a problem? Every Ada compiler (and pretty much every other
>>> compiler as well) does it already.
>>
>> How do you prove that this does not raise Constraint_Error
>>
>>   function Geometric_Mean (A, B : Float) return Float is
>>   begin
>>       return sqrt (A * B);
>>   end Geometric_Mean;
> 
> You can't, because it does. :-) Your contract is not strong enough, which is 
> not surprising: you have unbounded types here -- you can prove nothing about 
> such types.
> 
> But that's OK, there is no point in proving everything about everything. 
> Moreover, if you made this an expression function (meaning that you are 
> merely giving a name to "sqrt (A*B)", you could plug it in without any 
> effect on your proof. Enjoy.

But you could prove that with concrete ranges of A and B at the client
side. Which is the whole point. You want to discard a whole class of
proofs. Especially the ones crucial for exception contracts. How are you
going to prove the caller's contract not to raise? You could not without
non-sensual handlers. It would be like the idiotic "function must have a
return statement rule."

>>> The only issue is that programmers can't
>>> harness it for their own purposes. I would hope that exception contracts
>>> would be defined in order to do that.
>>
>> Yes. But they will only help if used on the client side and when bodies are
>> looked into.
> 
> You might be right, but in that case we're wasting our time even thinking 
> about proof, because any technology that requires programmer-visble access 
> to bodies is evil. ("Evil" here being a shorthand for "has a bunch of bad 
> properties", which I've previously outlined.)

Yes of course. Just like Churchill's remark about democracy, it is evil,
but anything else is much worse.

Correctness proof has the nature similar to optimization, most powerful on
concrete instances and close to damaging in general.

>> 1. You will not prove that sqrt never raises Constraint_Error. You will do
>> that in *your* calls to sqrt it never does.
> 
> You don't have to. A properly written Sqrt has a precondition, and that 
> precondition raises Constraint_Error when it fails. Sqrt itself never raises 
> any exception.

In most cases the precondition cannot be spelled or is more complex than
the implementation itself. It is just a wrong (and not working) way to do
this.

>> Opening readonly file for writing is not a bug it is an error, a legitime
>> state of the program which must be handled. Writing a file opened as
>> readonly is a bug. Bug /= error. Errors are handled, bugs are fixed.
> 
> You claim that you can use the file type to eliminate Status_Error and 
> Mode_Error. But that's impossible, because an Open that fails leaves the 
> file unopened;

This is another issue, i.e. construction and initialization. You should not
be able to create unopened instances of file type.

> and you have to be able to fall back and open a different 
> file (or create one instead) on such a condition. It's not practical to have 
> a single Open operation as an initializer

Why? I certainly want it exactly this way.

>> I don't see how allowing correctness checks involving the bodies should
>> prevent correctness checks involving the specifications.
> 
> Because you can't have "correctness checks" involving bodies that don't 
> exist.

Yes, it certainly will require some consideration of how to deal with
opaque libraries. The model is already a bit leaky in GNAT which requires
*.ali files. Maybe checks involving the bodies should be performed rather
by the binder and the information required for that stored in the *.ali
files or equivalent.

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

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

[Randy Brukardt]

"Shark8" <onewingedshark@gmail.com> wrote in message 
news:e7de5753-5819-41a4-a40f-3d80c101bf03@googlegroups.com...
...
>The one drawback from your proposal is that it makes you reiterate the 
>condition,
>but with a negation, this could be a source of bugs. Even though it's a 
>little less
>straightforward the following would circumvent that problem:

> procedure Op (x : in out T)
>   with Post => (Constraint_Error at [not?] Foo(x));

I didn't mean this to be a real example. An example like the one given 
probably would have been better written as a precondition (depending on 
exactly what Foo does):

  procedure Op (x : in out T)
     with Pre => Foo(x) or else raise Constraint_Error,
            Post => Foo(x);

which is just normal Ada 2012 code (using the raise expression, which we 
added 'after the fact' to support this usage).

I don't think most exception contracts would have an associated 
postcondition (that is, cause); what would the postcondition be for 
Use_Error, for instance? It's just an optional help in a few circumstances.

                                                Randy.

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

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:1awbjaens2vca$.1asmpnthmmycl.dlg@40tude.net...
> On Tue, 16 Jul 2013 17:13:43 -0500, Randy Brukardt wrote:
>
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>> news:1rjye7dyn3vgk.66fbcca9y4zd.dlg@40tude.net...
>>> On Mon, 15 Jul 2013 19:13:24 -0500, Randy Brukardt wrote:
>
>>>> Ada compilers do it all the time. The issue is letting the programmer
>>>> have access to that information.
>>>
>>> This is upside down. The programmer should manifest his intention for a
>>> constraint to hold and the compiler should verify that. The manifest 
>>> must
>>> be syntactically visible. Conflation such declaration with dynamic
>>> constraints is a bad idea.
>>
>> Yes, that's precisely what I'm talking about - some sort of exception
>> contract. But those don't depend on the kind of constraint.
>
> But they do, exception contract is a static constraint.
>
> It is no matter what is constrained, but how. Dynamically (=>code) vs.
> statically (=>proof).

Ah, you've redefined Ada's terms again. "Static" is defined in RM 4.9, and 
that's how I'm using it. "Proof", which is not an Ada concept, is not 
relevant to it's description.

By your twisted definition, everything is static (including dynamic 
constraints!) if sufficient information is known at compile-time to reason 
about them.

It would be nice to have a discussion where you didn't change the 
terminology from that accepted by Ada (this is, after all, an Ada group).

...
>> it's an integrated part of the development
>> process. (Your program cannot be run if it doesn't compile.) Extra tools
>> never will have that level force behind them, and people like me would 
>> never
>> run them.
>
> I always was for SPARK being integrated into Ada.

Nothing that has body dependencies can be integrated into Ada.

...
>> But that's OK, there is no point in proving everything about everything.
>> Moreover, if you made this an expression function (meaning that you are
>> merely giving a name to "sqrt (A*B)", you could plug it in without any
>> effect on your proof. Enjoy.
>
> But you could prove that with concrete ranges of A and B at the client
> side. Which is the whole point. You want to discard a whole class of
> proofs.

Absolutely. The sorts of proofs you want would absolutely kill program 
maintenance, making it impossible to have the sort of reusable libraries 
that Ada makes so easy. The contract represented by the interface can be the 
*only* thing that clients depend upon. If they depend on anything else, 
changes to the body will break otherwise correct calls, and that's 
unacceptable. This property if absolutely required to build large programs 
with large and distributed teams -- otherwise, "proof" remains solely the 
provence of small, toy-sized programs.

> Especially the ones crucial for exception contracts. How are you
> going to prove the caller's contract not to raise? You could not without
> non-sensual handlers. It would be like the idiotic "function must have a
> return statement rule."

You can only provide exception contracts if you have strong preconditions 
and constraints on the parameters. In the absense of that, you shouldn't be 
*allowed* to prove anything, because in doing so you force a strong coupling 
to the contents of the body.

...
>>> Opening readonly file for writing is not a bug it is an error, a 
>>> legitime
>>> state of the program which must be handled. Writing a file opened as
>>> readonly is a bug. Bug /= error. Errors are handled, bugs are fixed.
>>
>> You claim that you can use the file type to eliminate Status_Error and
>> Mode_Error. But that's impossible, because an Open that fails leaves the
>> file unopened;
>
> This is another issue, i.e. construction and initialization. You should 
> not
> be able to create unopened instances of file type.

Nice theory, impossible to do in practice. Next suggestion...

>> and you have to be able to fall back and open a different
>> file (or create one instead) on such a condition. It's not practical to 
>> have
>> a single Open operation as an initializer
>
> Why? I certainly want it exactly this way.

It's impractical to have an Open that somehow encodes every possible 
sequence of Open-fall back-Open-Create that might come up. In the absense of 
that, you have to resort to complex program structures (it's not possible to 
declare objects with the right scope easily) or worse, lots of allocated 
objects. (A major cause of "allocator mania" is certain other languages is 
that they don't have sufficiently powerful ways to create stack objects.)

In any case, we're talking about Ada here, and the form of Ada's I/O is 
fixed. The question is what proof techniques we can bring to these existing 
libraries, not how they could be designed in some hypothetical and 
unimplementable language.

                                         Randy.

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

[Dmitry A. Kazakov]

On Wed, 17 Jul 2013 18:08:17 -0500, Randy Brukardt wrote:

> "Shark8" <onewingedshark@gmail.com> wrote in message 
> news:e7de5753-5819-41a4-a40f-3d80c101bf03@googlegroups.com...
> ...
>>The one drawback from your proposal is that it makes you reiterate the 
>>condition, but with a negation, this could be a source of bugs. Even though it's a 
>>little less straightforward the following would circumvent that problem:
> 
>> procedure Op (x : in out T)
>>   with Post => (Constraint_Error at [not?] Foo(x));
> 
> I didn't mean this to be a real example. An example like the one given 
> probably would have been better written as a precondition (depending on 
> exactly what Foo does):
> 
>   procedure Op (x : in out T)
>      with Pre => Foo(x) or else raise Constraint_Error,
>             Post => Foo(x);
> 
> which is just normal Ada 2012 code (using the raise expression, which we 
> added 'after the fact' to support this usage).

Yep, and also highlights the inconvenient truth, that the "precondition" is
not a precondition but rather a chunk of executable code pushed in front of
the body.

Why not to honestly call it Prologue?

> I don't think most exception contracts would have an associated 
> postcondition (that is, cause); what would the postcondition be for 
> Use_Error, for instance?

If proper post-condition meant then:

   ensure Foo (X) or Raised (Constraint_Error); -- Weak contract

The issue you mentioned is strong exception contract telling when the
exception has to propagate and when not. That would be:

   ensure Foo (X) xor Raised (Constraint_Error); -- Explicit contract

If not Foo (X) then exception.

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

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

[Dmitry A. Kazakov]

On Wed, 17 Jul 2013 18:26:31 -0500, Randy Brukardt wrote:

> By your twisted definition, everything is static (including dynamic 
> constraints!) if sufficient information is known at compile-time to reason 
> about them.

Yes.
 
> Absolutely. The sorts of proofs you want would absolutely kill program 
> maintenance, making it impossible to have the sort of reusable libraries 
> that Ada makes so easy.

Maybe. But remember that other proofs will be useless beyond toy cases.

>> Especially the ones crucial for exception contracts. How are you
>> going to prove the caller's contract not to raise? You could not without
>> non-sensual handlers. It would be like the idiotic "function must have a
>> return statement rule."
> 
> You can only provide exception contracts if you have strong preconditions 
> and constraints on the parameters. In the absense of that, you shouldn't be 
> *allowed* to prove anything, because in doing so you force a strong coupling 
> to the contents of the body.

As I said. Useless. 

>>>> Opening readonly file for writing is not a bug it is an error, a  legitime
>>>> state of the program which must be handled. Writing a file opened as
>>>> readonly is a bug. Bug /= error. Errors are handled, bugs are fixed.
>>>
>>> You claim that you can use the file type to eliminate Status_Error and
>>> Mode_Error. But that's impossible, because an Open that fails leaves the
>>> file unopened;
>>
>> This is another issue, i.e. construction and initialization. You should 
>> not be able to create unopened instances of file type.
> 
> Nice theory, impossible to do in practice.

Even if as "practice" you mean broken limited return, it is still quite
possible.

>>> and you have to be able to fall back and open a different
>>> file (or create one instead) on such a condition. It's not practical to 
>>> have a single Open operation as an initializer
>>
>> Why? I certainly want it exactly this way.
> 
> It's impractical to have an Open that somehow encodes every possible 
> sequence of Open-fall back-Open-Create that might come up. In the absense of 
> that, you have to resort to complex program structures (it's not possible to 
> declare objects with the right scope easily) or worse,

It won't be any more complex than it is when handling exceptions
propagating out of Open. In fact it will be much simpler because you forgot
the issue of closing the file on subsequent errors.

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

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

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:17i525dc26pat$.1octlzd41c8zm.dlg@40tude.net...
> On Wed, 17 Jul 2013 18:26:31 -0500, Randy Brukardt wrote:
...
>>> Especially the ones crucial for exception contracts. How are you
>>> going to prove the caller's contract not to raise? You could not without
>>> non-sensual handlers. It would be like the idiotic "function must have a
>>> return statement rule."
>>
>> You can only provide exception contracts if you have strong preconditions
>> and constraints on the parameters. In the absense of that, you shouldn't 
>> be
>> *allowed* to prove anything, because in doing so you force a strong 
>> coupling
>> to the contents of the body.
>
> As I said. Useless.

Then proof is beyond useless, it's downright dangerous. If you're right, no 
one should even think about it.

...
>> It's impractical to have an Open that somehow encodes every possible
>> sequence of Open-fall back-Open-Create that might come up. In the absense 
>> of
>> that, you have to resort to complex program structures (it's not possible 
>> to
>> declare objects with the right scope easily) or worse,
>
> It won't be any more complex than it is when handling exceptions
> propagating out of Open. In fact it will be much simpler because you 
> forgot
> the issue of closing the file on subsequent errors.

I've never had the slightest "issue" with closing the file at the end. And 
certainly, there aren't "subsequent errors", because either the file gets 
opened eventually, or the whole routine is aborted (usually, the entire 
program is halted at the point, since failure to be able to write results --  
no one needs to calculate results if you can't save them).

                             Randy.

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

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:15q73x8g743d.solfjve1fywf$.dlg@40tude.net...
> On Wed, 17 Jul 2013 18:08:17 -0500, Randy Brukardt wrote:
...
>> I didn't mean this to be a real example. An example like the one given
>> probably would have been better written as a precondition (depending on
>> exactly what Foo does):
>>
>>   procedure Op (x : in out T)
>>      with Pre => Foo(x) or else raise Constraint_Error,
>>             Post => Foo(x);
>>
>> which is just normal Ada 2012 code (using the raise expression, which we
>> added 'after the fact' to support this usage).
>
> Yep, and also highlights the inconvenient truth, that the "precondition" 
> is
> not a precondition but rather a chunk of executable code pushed in front 
> of
> the body.

Well, it's special in the sense that the compiler will try hard to eliminate 
it, and generally, I think a compiler should generate a warning if it 
*can't* remove the precondition. (That might be hard to accomplish 
initially, mainly  because the removal code happens after the stage where 
warnings can easily be given.) In that sense, it's executable in name only.

> Why not to honestly call it Prologue?

I presume people wanted to match common usage (as in Eiffel, for instance).

                       Randy.

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

[Dmitry A. Kazakov]

On Thu, 18 Jul 2013 23:32:57 -0500, Randy Brukardt wrote:

>> It won't be any more complex than it is when handling exceptions
>> propagating out of Open. In fact it will be much simpler because you 
>> forgot the issue of closing the file on subsequent errors.
> 
> I've never had the slightest "issue" with closing the file at the end. And 
> certainly, there aren't "subsequent errors", because either the file gets 
> opened eventually, or the whole routine is aborted (usually, the entire 
> program is halted at the point, since failure to be able to write results --  
> no one needs to calculate results if you can't save them).

I meant I/O errors and more elaborated cases like sockets. If you open a
socket file you should bind it, set options which may fail as well. Code
that does not use controlled wrappers look very ugly.

It is *always* a much better design when the object maintains a state
invariant (e.g. file is open). Provability of such code is a nice
byproduct.

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

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

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:w30s4q4tdrue$.1q2ek7n0im2ba$.dlg@40tude.net...
> On Thu, 18 Jul 2013 23:32:57 -0500, Randy Brukardt wrote:
>
>>> It won't be any more complex than it is when handling exceptions
>>> propagating out of Open. In fact it will be much simpler because you
>>> forgot the issue of closing the file on subsequent errors.
>>
>> I've never had the slightest "issue" with closing the file at the end. 
>> And
>> certainly, there aren't "subsequent errors", because either the file gets
>> opened eventually, or the whole routine is aborted (usually, the entire
>> program is halted at the point, since failure to be able to write 
>> results --
>> no one needs to calculate results if you can't save them).
>
> I meant I/O errors and more elaborated cases like sockets. If you open a
> socket file you should bind it, set options which may fail as well. Code
> that does not use controlled wrappers look very ugly.
>
> It is *always* a much better design when the object maintains a state
> invariant (e.g. file is open). Provability of such code is a nice
> byproduct.

But isn't that impossible, practically? If the USB drive is unplugged, it's 
impossible to get to the file. Same with sockets. If you mean that it's 
required to propagate an exception out of scope so that it's impossible to 
access a file object that's not open, that's going to make a lot of trouble 
because of overlapping file lifetimes. (Imagine copying data from one file 
to another with a transformation: if one of the files has an I/O error, you 
no longer can clean up the other one (you might be able to use nesting to 
get it to work one way, but not either way).

In any case, this seems like solving a non-problem, as closing files and the 
like is trivially handled by finalization. (I don't much care about people 
who refuse to use the tools they're given.)

Anyway, I think the problem with your scheme is on the initialization end. 
Initialization (as you seemed to acknowledge above) is just too complex for 
many of these objects to do it as part of the object declaration.

Indeed, we (briefly) tried to use a scheme like the one you are suggesting 
for the Claw packages. We immediately ran into problems with too many 
parameters (especially for discriminants). And there were further problems 
with the interrelationships between the objects; we would have had to 
extensively use access types, which would have greatly compromised the 
ease-of-use and especially the bulletproof-ness goals that we had for Claw.

So, I don't think it works outside of the simplest cases.

                                       Randy.

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

[Dmitry A. Kazakov]

On Sat, 20 Jul 2013 00:32:44 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:w30s4q4tdrue$.1q2ek7n0im2ba$.dlg@40tude.net...
>> On Thu, 18 Jul 2013 23:32:57 -0500, Randy Brukardt wrote:
>>
>>>> It won't be any more complex than it is when handling exceptions
>>>> propagating out of Open. In fact it will be much simpler because you
>>>> forgot the issue of closing the file on subsequent errors.
>>>
>>> I've never had the slightest "issue" with closing the file at the end. 
>>> And
>>> certainly, there aren't "subsequent errors", because either the file gets
>>> opened eventually, or the whole routine is aborted (usually, the entire
>>> program is halted at the point, since failure to be able to write 
>>> results --
>>> no one needs to calculate results if you can't save them).
>>
>> I meant I/O errors and more elaborated cases like sockets. If you open a
>> socket file you should bind it, set options which may fail as well. Code
>> that does not use controlled wrappers look very ugly.
>>
>> It is *always* a much better design when the object maintains a state
>> invariant (e.g. file is open). Provability of such code is a nice
>> byproduct.
> 
> But isn't that impossible, practically? If the USB drive is unplugged, it's 
> impossible to get to the file. Same with sockets. If you mean that it's 
> required to propagate an exception out of scope so that it's impossible to 
> access a file object that's not open, that's going to make a lot of trouble 
> because of overlapping file lifetimes.

I think it is a consequence of your approach that leads to conflating
states of a file, of its descriptor, of the Ada's proxy to that descriptor
and all OSI levels from top to the bottom into one big mess. Yes, if you do
that it will never be possible to check.

My approach is to identify states which can be statically determined and
make them invariant. A file being opened or a socket created is such a
state. Non-opened file has no use. Similarly a bound socket is an invariant
for another type, and a connected socket is for yet another.

When a connection gets closed by the peer pending I/O should propagate an
I/O error exception for opened-bound-connected socket. This exception has
nothing to do with attempting to read fron a non-existing file description.
Because the latter is a bug to me, which shall be prevented statically.

> Anyway, I think the problem with your scheme is on the initialization end. 
> Initialization (as you seemed to acknowledge above) is just too complex for 
> many of these objects to do it as part of the object declaration.

My answer is that even talking about complexity is breaking abstraction. It
is irrelevant how complex an opaque operation is.

> Indeed, we (briefly) tried to use a scheme like the one you are suggesting 
> for the Claw packages. We immediately ran into problems with too many 
> parameters (especially for discriminants). And there were further problems 
> with the interrelationships between the objects; we would have had to 
> extensively use access types, which would have greatly compromised the 
> ease-of-use and especially the bulletproof-ness goals that we had for Claw.

These problems are mostly language problems, namely lack of proper
constructors and encapsulation of initialization/finalization.

Your and others opposition to fixing constructors in Ada is to large extent
based on flawed design patterns like you described.

> So, I don't think it works outside of the simplest cases.

On the contrary, it is the flawed "first construct then initialize"
pattern, which is simple only on paper. In practice it is becomes a huge
maintenance and testing problem because it shoulders all the burden on the
clients => distributed overhead.

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

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

[Paul Rubin]

Stefan.Lucks@uni-weimar.de writes:
> the implementation an authenticated encryption scheme.... The
> output of the authenticated encryption is the ciphertext (X xor Y),
> followed by a cryptographic checksum(*) of X under the key K. ...
> The flow annotations specified the flow from X
> and K to Z. And that actually caught my error of using (X xor Y)
> instead of X in the implementation.

Surely you wanted to authenticate the ciphertext and not the plaintext?
Authenticating the plaintext can leak information about it.