Problems with SPARK 2015 and XMLAda

Problems with SPARK 2015 and XMLAda

[Serge Robyns]

Hi,

I'm trying to use Spark on my little project.
I managed to make it work on some other toy but here it chokes on what seems to be references to XMLAda in my project.  However, the file I'm analyzing is not using any XML feature (others does).

I've no idea how to fix this.

Here is the excerpt of the command line execution.

Phase 1 of 2: generation of Global contracts ...
gprbuild --config=T:\SPARK\2015\share\spark\config\frames.cgpr -P ../test.
gpr -c -v --subdirs=gnatprove --restricted-to-languages=ada --no-object-check test-accounts.adb -cargs:Ada -gnatc -gnates=T:\Documents\Development\Test\obj\gnatprove\\35e4eb76.tmp
GPRBUILD GPL 2015 (20150428) (i686-pc-mingw32)
Copyright (C) 2004-2015, Free Software Foundation, Inc.
 102 lines: No errors
Checking configuration T:\SPARK\2015\share\spark\config\frames.cgpr
Setting the default project search directories
   Adding directory "T:\SPARK\2015\libexec\spark\x86-windows\lib\gnat"
   Adding directory "T:\SPARK\2015\libexec\spark\x86-windows\share\gpr"
   Adding directory "T:\SPARK\2015\libexec\spark\share\gpr"
   Adding directory "T:\SPARK\2015\libexec\spark\lib\gnat"

==============Error messages for project file: T:\Documents\Development\Test\test.gpr
    11.    Library_Type : Xmlada_Kind_Type := external ("LIBRARY_TYPE");
           1                                  2
        >>> no value defined for "library_type"
        >>> warning: undefined external reference

    14.    Xmlada_Build : Build_Kind := external ("XMLADA_BUILD");
           1                            2
        >>> no value defined for "xmlada_build"
        >>> warning: undefined external reference

 102 lines: 2 errors, 2 warnings
gprbuild: "../test.gpr" processing failed
gnatprove: error during generation of Global contracts

Re: Problems with SPARK 2015 and XMLAda

[Simon Wright]

Serge Robyns <serge.robyns@gmail.com> writes:

>     11.    Library_Type : Xmlada_Kind_Type := external ("LIBRARY_TYPE");
>            1                                  2
>         >>> no value defined for "library_type"
>         >>> warning: undefined external reference

I would expect the required value to be "static" or "dynamic" (perhaps
"relocatable").

'external ("FOO")' means 'look for a scenario variable[1] "FOO" and take
its value; fail if not found'.

You can define a scenario variable either as an environment variable
(export LIBRARY_TYPE=static, for bash) or on the command line,

   $ gprbuild -P prj -XLIBRARY_TYPE=static

but you might find it easier to define a default value,

   Library_Type : Xmlada_Kind_Type := external ("LIBRARY_TYPE", "static");

>     14.    Xmlada_Build : Build_Kind := external ("XMLADA_BUILD");
>            1                            2
>         >>> no value defined for "xmlada_build"
>         >>> warning: undefined external reference

xmlada.gpr & friends say e.g.

   library project XmlAda_Dom is
      type BUILD_KIND is ("static", "relocatable");
      BUILD : BUILD_KIND := external("XMLADA_BUILD", "static");


[1] http://docs.adacore.com/gprbuild-docs/html/share/gnat_project_manager.html#scenarios-in-projects

Re: Problems with SPARK 2015 and XMLAda

[Serge Robyns]

Hi Simon,

Manually editing the grp file as suggested did the trick.

Sadly I quickly abandoned SPARK as it barked on me for using bounded strings.  I intend to use a DB with my application and bounded strings seems to be the way to go, even if I do find them a pain to use.  For every type of string I've to instantiate the generic package as I want to have strong typing on the usage of these strings throughout the program and this is one of my drivers to use Ada.

And I know many other things SPARK doesn't like, like exceptions (not used (yet)) or access types.  So I guess it must dislike the standard containers too.

I guess I'll uninstall SPARK, as so far it hasn't been so helpful for me.
For example in another small toy (a little game) I'm using the following construct.

      Count1      : Natural range 0 .. Number_Of_Columns;
      Count2      : Natural range 0 .. Number_Of_Columns;
      The_Score   : Integer := 0;
      J           : Columns;

      --  To speed up, the value is calculated as a delta
      --  from the previous value.
      --  This is the less good code of this game (I'm not proud).
   begin
      --
      --  Horizontal
      --
      Count1 := 0;
      if Column > Columns'First then
         for J in reverse Columns'First .. Columns'Pred (Column)
         loop
            exit when The_Board.Board (Row, J) /= Player;
            Count1 := Count1 + 1;
            pragma Loop_Invariant ( Count1 <= Number_Of_Columns - Integer (Columns'First - Columns'Pred (Column)));
            pragma Loop_Variant ( Increases => Count1 );
            pragma Loop_Variant ( Decreases => J );
         end loop;
      end if;
      Count2 := 0;
      if Column < Columns'Last then
      for J in Columns'Succ (Column) .. Columns'Last
      loop
         exit when The_Board.Board (Row, J) /= Player;
         Count2 := Count2 + 1;
         pragma Loop_Invariant ( Count2 < Number_Of_Columns );
         pragma Loop_Variant ( Increases => Count2 );
         pragma Loop_Variant ( Increases => J );
      end loop;
   end if;

SPARK warns about potential range errors on Count1 and Count2 while I've put a lot of safeguards and tried two different Loop_Invariant constructs to tell SPARK to be happy.  For every construct attempt I get a different error.

I'm not going to waste my time fighting SPARK and put my trust in the standard ADA features and testing.  To bad not being able to proof.

Serge

Re: Problems with SPARK 2015 and XMLAda

[Jacob Sparre Andersen]

Serge Robyns wrote:

> Sadly I quickly abandoned SPARK [...]

> And I know many other things SPARK doesn't like, like exceptions [...]

One important purpose of SPARK is to avoid exceptions completely, so
yes.

> or access types.

Yes.  Proving a program using access types to be correct is rather
difficult.

> So I guess it must dislike the standard containers too.

Yes, but there are containers for SPARK too.

In general, you can't use much of the *Ada* standard libraries with
SPARK, as they aren't annotated for correctness proofs.

If you want to program in SPARK, you shouldn't try to write Ada, and
then just run a tool, when you're done.  You should read the SPARK LRM
(or a textbook on SPARK), and understand the language.

Greetings,

Jacob
-- 
"I have no prejudice except against Pakistanis, which is normal."

Re: Problems with SPARK 2015 and XMLAda

[Mark Lorenzen]

On Thursday, August 20, 2015 at 9:10:46 AM UTC+2, Jacob Sparre Andersen wrote:

> If you want to program in SPARK, you shouldn't try to write Ada, and
> then just run a tool, when you're done.  You should read the SPARK LRM
> (or a textbook on SPARK), and understand the language.

This is a very good advice! A SPARK program isn't just an Ada program with annotations. SPARK programs must be designed from the ground up with the SPARK restrictions in mind.

Regards,

Mark

Re: Problems with SPARK 2015 and XMLAda

[Shark8]

On Wednesday, August 19, 2015 at 3:22:44 PM UTC-6, Serge Robyns wrote:
> 
> I'm not going to waste my time fighting SPARK and put my trust in the standard ADA features and testing.  To bad not being able to proof.

How you've worded this makes me think that perhaps you think of SPARK as an extension of Ada [as superset], and that'll get you into a lot of headaches because SPARK is a subset of Ada [along w/ tools].

As others have said, SPARK is about avoiding exceptions completely (because the relevant properties are proved) and therefore having exceptions in your SPARK code is not allowed.

Do you /NEED/ SPARK? Maybe, maybe not. But there are certain properties of software built with formal methods that are desirable -- like the aforementioned absence of exceptions.

Re: Problems with SPARK 2015 and XMLAda

[Peter Chapin]

On Thu, 20 Aug 2015, Shark8 wrote:

> As others have said, SPARK is about avoiding exceptions completely 
> (because the relevant properties are proved) and therefore having 
> exceptions in your SPARK code is not allowed.

To clarify, SPARK 2014 does allow raise statements in programs. However, 
each Raise statement carries with it a proof obligation that it will never 
execute. What's the point of that? It allows you to use raise statements 
to document "impossible" situations and then have the tools attempt to 
prove that those situations are, indeed, impossible.

SPARK 2014 does not allow exception handlers, however.

Peter

Re: Problems with SPARK 2015 and XMLAda

[Jeffrey R. Carter]

On 08/20/2015 11:42 AM, Peter Chapin wrote:
> 
> To clarify, SPARK 2014 does allow raise statements in programs. However, each
> Raise statement carries with it a proof obligation that it will never execute.
> What's the point of that? It allows you to use raise statements to document
> "impossible" situations and then have the tools attempt to prove that those
> situations are, indeed, impossible.

SPARK is usually discussed in the context of complete programs, in which you
prove both that a subprogram is correct if the caller meets the precondition,
and that all calls meet the precondition.

However, in the case of a library unit that may be called by multiple programs,
it may be desirable to be able to prove the correctness of the unit without
being able to prove that all calls will be correct. In such cases, having
assertion checking catch the precondition violation and raise an exception is
the best solution should the unit be misused.

Also, some preconditions are very expensive to check; consider the "N is prime"
example discussed here in another thread. In such a case, it may be that the
normal processing allows detecting a precondition violation much more cheaply
than checking the precondition at the time of the call. In that case, a
conditional raise statement, which the condition being provably false if the
precondition is met. Then the unit can be proven correct if the precondition is
met, execute without the expensive precondition check in the case where the call
is not proven correct, and still raise an exception if it is called with the
precondition not met.

So it does seem there are cases where this feature may be useful.

-- 
Jeff Carter
"I've seen projects fail miserably for blindly
applying the Agile catechism: we're Agile, we
don't need to stop and think, we just go ahead
and code!"
Bertrand Meyer
150

Re: Problems with SPARK 2015 and XMLAda

[Serge Robyns]

On Thursday, 20 August 2015 18:38:18 UTC+2, Shark8  wrote:

> Do you /NEED/ SPARK? Maybe, maybe not. But there are certain properties of software built with formal methods that are desirable -- like the aforementioned absence of exceptions.

From the discussion it is clear I don't need SPARK for my application.  The application will consume data from external possibly unreliable sources.  It will work with systems that can fail, etc.  My attempt with SPARK was to be able to prove correctness of major portions of the code.  However, it is not a live critical software component.  Yes, I was wrong with my assumptions about SPARK.

With regards to exceptions I haven't any but XMLAda does raise them when failing to validate the XML file.  I'm using a few access variables where my *current* design pushes me to do so (there is an older post about it by me in this group) but when reading the GNAT container packages I do see they are used there too.  Exceptions are nice to handle certain kinds of failure without requiring to burden complex error handling everywhere.  In a database application it is perfectly acceptable to rollback the transaction in such case.

Thanks for sharing your thoughts.

Re: Problems with SPARK 2015 and XMLAda

[Randy Brukardt]

"Shark8" <onewingedshark@gmail.com> wrote in message 
news:9d3dc132-4e1a-4e9c-bcd4-82a42a73745f@googlegroups.com...
...
> As others have said, SPARK is about avoiding exceptions completely 
> (because
> the relevant properties are proved) and therefore having exceptions in 
> your SPARK
>  code is not allowed.

One use of exceptions is to signal errors with the parameters of a 
routine -- essentially the failure of a precondition. Clearly, it is better 
that such things are proved impossible, and thus such exceptions are not 
needed in SPARK.

But another use of exceptions is to signal things that cannot be known at 
compile time. How can you tell in advance whether the file Foobar.Txt exists 
on your disk? Even a pretesting it is unreliable (it could be deleted 
between the test and the usage); one has to report the error at runtime.

SPARK forces such errors to be reported as error codes, and that's pure 
evil. The problems with using error codes rather than exceptions to report 
unlikely but possible errors are well-known, and forcing one to use that is 
essentially junking decades of programming experience.

The lack of access types is similar; one has to emulate them using arrays in 
SPARK, which is a 1950s programming technique. It's the sort of thing that 
one uses Ada to get way from.

At least the SPARK team is aware of these limitations and considering ways 
to mitigate them in future versions of SPARK. What I hate is people spinning 
these as "features" rather than just a limitation of prover technology (and 
to me, an indication that SPARK tries to do too much).

                            Randy.
 

Re: Problems with SPARK 2015 and XMLAda

[Shark8]

On Thursday, August 20, 2015 at 2:36:09 PM UTC-6, Randy Brukardt wrote:
> "Shark8" wrote in message 
> news:9d3dc132-4e1a-4e9c-bcd4-82a42a73745f...
> ...
> > As others have said, SPARK is about avoiding exceptions completely 
> > (because
> > the relevant properties are proved) and therefore having exceptions in 
> > your SPARK
> >  code is not allowed.
> 
> One use of exceptions is to signal errors with the parameters of a 
> routine -- essentially the failure of a precondition. Clearly, it is better 
> that such things are proved impossible, and thus such exceptions are not 
> needed in SPARK.

This sort of exception is what I was thinking of.

> 
> But another use of exceptions is to signal things that cannot be known at 
> compile time. How can you tell in advance whether the file Foobar.Txt exists 
> on your disk? Even a pretesting it is unreliable (it could be deleted 
> between the test and the usage); one has to report the error at runtime.
> 
> SPARK forces such errors to be reported as error codes, and that's pure 
> evil. The problems with using error codes rather than exceptions to report 
> unlikely but possible errors are well-known, and forcing one to use that is 
> essentially junking decades of programming experience.

I *really* despise error-codes -- Though with Ada you can make it a bit nicer by having an actual enumeration, throwing the function-call into a case-statement, and letting the compiler smack you when you forget to cover one of the codes.

> 
> The lack of access types is similar; one has to emulate them using arrays in 
> SPARK, which is a 1950s programming technique. It's the sort of thing that 
> one uses Ada to get way from.

Yes, it is.
I wasn't aware of this 'feature' of SPARK.

> 
> At least the SPARK team is aware of these limitations and considering ways 
> to mitigate them in future versions of SPARK. What I hate is people spinning 
> these as "features" rather than just a limitation of prover technology (and 
> to me, an indication that SPARK tries to do too much).

I am hoping the SPARK team fixes some of those and it looks like they have been doing so -- just look at type-predicates: http://www.spark-2014.org/entries/detail/spark-2014-rationale-type-predicates

Re: Problems with SPARK 2015 and XMLAda

[Stefan.Lucks]

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

On Thu, 20 Aug 2015, Randy Brukardt wrote:

> SPARK forces such errors to be reported as error codes, and that's pure
> evil.

There are two cases against error codes, a strong one and a weak one.

The strong case that programmers just tend to forget handling them, or 
even intentionally ignore them. This is why error codes are evil.

But this is a non-issue for SPARK: If the postconditions of a subprogramm 
allow error codes, the caller cannot ignore the error and still prove its 
own postconditions (at least for any sort of useful postconditions).

The weak case is about readability. It is a reason why error codes are 
bad, but not quite evil. And it actually is an issue for SPARK:

Source code with well-used exception handlers at the bottom of a block are 
often better readable than programs where the error-handlers are 
distributed across the source code, with an error handler after every 
program call returning an error code.

> The lack of access types is similar; one has to emulate them using 
> arrays in SPARK, which is a 1950s programming technique. It's the sort 
> of thing that one uses Ada to get way from.

Agreed!

Unfortunately, the state of static verification in general is that proving 
properties for pointer-hopping programs is almost hopeless. There is some 
recent work in this direction, e.g., by Bertrand Mayer, but this only goes 
so far.

> At least the SPARK team is aware of these limitations and considering 
> ways to mitigate them in future versions of SPARK. What I hate is people 
> spinning these as "features" rather than just a limitation of prover 
> technology

Agreed!

> (and to me, an indication that SPARK tries to do too much).

SPARK tries to do as much as possible with current static verification 
technologies. Which is actually quite cool.

Actually, you can use access types in SPARK programs, as long as you 
encapsulate them away from the prover. Encapsulating access types is what 
you have proposed in another thread, actually.

More precisely, you can write SPARK specifications (no access types!) 
claiming postconditions, exception freedom and the like, for your 
subprograms. Now you implement your packages/subprograms in pure Ada (no 
SPARK) with access types used internally, if needed. The correctness of 
such packages is an unproven assumption. But can "with" your subprograms 
in your own SPARK bodies.

If you stick to your promises (your postconditions hold if the 
preconditions are statisfied), i.e., if the unproven assumptions are 
correct, then the full program is correct.

Of course, you would like to prove *everything* -- at least, I would like 
to do so. But mixing full Ada with SPARK is, IMHO, the best approach to 
provably correct programs possible with today's technology.

Stefan

--------  I  love  the  taste  of  Cryptanalysis  in  the morning!  --------
www.uni-weimar.de/de/medien/professuren/mediensicherheit/people/stefan-lucks
----Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universität Weimar, Germany----

Re: Problems with SPARK 2015 and XMLAda

[Dmitry A. Kazakov]

On Fri, 21 Aug 2015 08:26:53 +0200, Stefan.Lucks@uni-weimar.de wrote:

> On Thu, 20 Aug 2015, Randy Brukardt wrote:
> 
>> SPARK forces such errors to be reported as error codes, and that's pure
>> evil.
> 
> There are two cases against error codes, a strong one and a weak one.
> 
> The strong case that programmers just tend to forget handling them, or 
> even intentionally ignore them. This is why error codes are evil.
> 
> But this is a non-issue for SPARK: If the postconditions of a subprogramm 
> allow error codes, the caller cannot ignore the error and still prove its 
> own postconditions (at least for any sort of useful postconditions).
> 
> The weak case is about readability. It is a reason why error codes are 
> bad, but not quite evil. And it actually is an issue for SPARK:
> 
> Source code with well-used exception handlers at the bottom of a block are 
> often better readable than programs where the error-handlers are 
> distributed across the source code, with an error handler after every 
> program call returning an error code.

No, it is not about readability or dangers of not testing the return code. 

The main reason is that exceptions indicate states which usually cannot be
handled on the caller's context. (All other applications, e.g. to indicate
bugs are illegitimate)

Whatever the code is, unless indicating "success", some callers cannot do
anything with that and should pass it to their callers and maybe to the
caller's caller and so on.

The idea of exception is that the caller *cannot continue* when the callee
detected an exceptional state.

Since the callee shall not know its callers, which is one of the major
software design principles, there is no way how return code could be a
substitute to exception. You must rework the design and contaminate the
code of all callers up the calling chain until continuation were logically
possible.

Another reason is distributed overhead of testing return codes. Modern
compilers and processors have zero exception overhead when no exception
raised. Exceptions, when used properly, are rare, thus programs using
exceptions could be far more efficient.

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

Re: Problems with SPARK 2015 and XMLAda

[Stefan.Lucks]

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

On Fri, 21 Aug 2015, Dmitry A. Kazakov wrote:

I wrote:

>> The strong case that programmers just tend to forget handling them, or
>> even intentionally ignore them. This is why error codes are evil.
>>
>> But this is a non-issue for SPARK: If the postconditions of a subprogramm
>> allow error codes, the caller cannot ignore the error and still prove its
>> own postconditions (at least for any sort of useful postconditions).

Don't forget the two paragraphs above!

>> The weak case is about readability. It is a reason why error codes are
>> bad, but not quite evil. And it actually is an issue for SPARK:
>>
>> Source code with well-used exception handlers at the bottom of a block are
>> often better readable than programs where the error-handlers are
>> distributed across the source code, with an error handler after every
>> program call returning an error code.
>
> No, it is not about readability or dangers of not testing the return code.
>
> The main reason is that exceptions indicate states which usually cannot be
> handled on the caller's context. (All other applications, e.g. to indicate
> bugs are illegitimate)
>
> Whatever the code is, unless indicating "success", some callers cannot do
> anything with that and should pass it to their callers and maybe to the
> caller's caller and so on.

If an exception cannot be handled in the caller's context, the caller 
cannot satisfy its own postconditions. See above!

> The idea of exception is that the caller *cannot continue* when the callee
> detected an exceptional state.

The idea of statically proven postconditions with error codes is to force 
the caller to return its own exception code.

> Since the callee shall not know its callers, which is one of the major
> software design principles, there is no way how return code could be a
> substitute to exception.

Hu?????? That does not make any sense to me!!!

Here is some code with exceptions:

   End_Error, Data_Error, Mode_Error, Layout_Error: exception;

   procedure Do_Something(Filename: String);
     -- may raise any of the above exceptions

Here is the same code with error codes substituting the exceptions:

   type Errors is (None, End_Error, Data_Error, Mode_Error, Layout_Error);

   procedure Do_Something(Filename: String; Error: out Errors);

The only thing that is not possible is for a caller to ignore or re-raise 
an exception. It must check the error codes of its callees and, in the 
exceptional case, return its own error code.

This is not necessarily a disadvantage for error codes!

One thing that is frightening about exceptions is that by not handling 
locally declared exceptions, some global caller's caller cannot handle 
that specific exception at all -- it can only use *the* *same* catch-all

   when others => ...;

exception handler for all such exceptions. For error codes, on the other 
hand, the Ada type system ensures that the caller will always know the 
callee's exception codes.

> Another reason is distributed overhead of testing return codes. Modern
> compilers and processors have zero exception overhead when no exception
> raised. Exceptions, when used properly, are rare, thus programs using
> exceptions could be far more efficient.

I doubt this makes any observable difference. The legitimate examples for 
exceptions that "signal things that cannot be known at compile time" (as 
Randy wrote) are usually related to input-output operations. Your machine 
is so much faster than such external devices that the overhead for a 
comparison like "if Error_Code /= None" would be negligible.

Stefan


--------  I  love  the  taste  of  Cryptanalysis  in  the morning!  --------
www.uni-weimar.de/de/medien/professuren/mediensicherheit/people/stefan-lucks
----Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universität Weimar, Germany----

Re: Problems with SPARK 2015 and XMLAda

[Dmitry A. Kazakov]

On Fri, 21 Aug 2015 10:19:50 +0200, Stefan.Lucks@uni-weimar.de wrote:

> On Fri, 21 Aug 2015, Dmitry A. Kazakov wrote:
> 
> I wrote:
> 
>>> The strong case that programmers just tend to forget handling them, or
>>> even intentionally ignore them. This is why error codes are evil.
>>>
>>> But this is a non-issue for SPARK: If the postconditions of a subprogramm
>>> allow error codes, the caller cannot ignore the error and still prove its
>>> own postconditions (at least for any sort of useful postconditions).
> 
> Don't forget the two paragraphs above!
> 
>>> The weak case is about readability. It is a reason why error codes are
>>> bad, but not quite evil. And it actually is an issue for SPARK:
>>>
>>> Source code with well-used exception handlers at the bottom of a block are
>>> often better readable than programs where the error-handlers are
>>> distributed across the source code, with an error handler after every
>>> program call returning an error code.
>>
>> No, it is not about readability or dangers of not testing the return code.
>>
>> The main reason is that exceptions indicate states which usually cannot be
>> handled on the caller's context. (All other applications, e.g. to indicate
>> bugs are illegitimate)
>>
>> Whatever the code is, unless indicating "success", some callers cannot do
>> anything with that and should pass it to their callers and maybe to the
>> caller's caller and so on.
> 
> If an exception cannot be handled in the caller's context, the caller 
> cannot satisfy its own postconditions. See above!

Exactly! You cannot implement the caller and thus you must scrap all your
design (decomposition into modules like caller and callee).

Exceptions are here to make reasonable decomposition possible.

>> The idea of exception is that the caller *cannot continue* when the callee
>> detected an exceptional state.
> 
> The idea of statically proven postconditions with error codes is to force 
> the caller to return its own exception code.

Which is impossible to do, as we saw above.

>> Since the callee shall not know its callers, which is one of the major
>> software design principles, there is no way how return code could be a
>> substitute to exception.
> 
> Hu?????? That does not make any sense to me!!!

(Which "that"?)

> Here is some code with exceptions:
> 
>    End_Error, Data_Error, Mode_Error, Layout_Error: exception;
> 
>    procedure Do_Something(Filename: String);
>      -- may raise any of the above exceptions
> 
> Here is the same code with error codes substituting the exceptions:
> 
>    type Errors is (None, End_Error, Data_Error, Mode_Error, Layout_Error);
> 
>    procedure Do_Something(Filename: String; Error: out Errors);
> 
> The only thing that is not possible is for a caller to ignore or re-raise 
> an exception.

Yes. The difference is in the callers.

> It must check the error codes of its callees and, in the 
> exceptional case, return its own error code.

Yes, it must re-implement exception propagation throughout all caller,
existing and potential ones.

> This is not necessarily a disadvantage for error codes!

Massive distributed redesign of all client code base. Not a disadvantage,
indeed, it is a catastrophe.

> One thing that is frightening about exceptions is that by not handling 
> locally declared exceptions, some global caller's caller cannot handle 
> that specific exception at all -- it can only use *the* *same* catch-all
> 
>    when others => ...;

That is true for non-contracted exceptions only. Clearly Ada and SPARK must
have had exception contracts which would have statically prevented
unhandled exceptions, including the "when others =>" mess. E.g. Finialize
would have "not raising anything" in the contract, which would force you to
handle all exceptions.

>> Another reason is distributed overhead of testing return codes. Modern
>> compilers and processors have zero exception overhead when no exception
>> raised. Exceptions, when used properly, are rare, thus programs using
>> exceptions could be far more efficient.
> 
> I doubt this makes any observable difference. The legitimate examples for 
> exceptions that "signal things that cannot be known at compile time"

These are misuse of exceptions. States not known at compile time (design
time) are bugs. You cannot do anything with bugs in a running program. The
bug handler is you. Bug fixing is accomplished by typing some text in the
IDE, recompiling and deploying the program.

> (as Randy wrote) are usually related to input-output operations.

Wrong. I/O states are all known at compile time. You do know that you might
get a read error. Indeterminism of program's inputs has nothing to do with
compiler-time constants (or indeterminism of the program itself).

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

Re: Problems with SPARK 2015 and XMLAda

[G.B.]

On 21.08.15 11:37, Dmitry A. Kazakov wrote:
> Clearly Ada and SPARK must
> have had exception contracts which would have statically prevented
> unhandled exceptions,

Well, it seems a stricture on design to me, if it is to mean:
"If implementing my abstraction, though shalt raise but these
exceptions: A, B, and C".

Would He, the designer of exception contracts, by looking into
some crystal ball, then write the contract knowing of all
possible implementations of the contracted feature in advance?
Able to decide on which paths of unforeseen computation some
implementation might want to give up? Disallowing any other exception
known to both the implementer of the feature and the implementer
of the caller?

Or is it about exceptions written into the contract after knowing
all possible callers, and being able to adjust all source code
as necessary? (I.e., dismissing immutable software components?)

Re: Problems with SPARK 2015 and XMLAda

[Dmitry A. Kazakov]

On Fri, 21 Aug 2015 12:09:43 +0200, G.B. wrote:

> On 21.08.15 11:37, Dmitry A. Kazakov wrote:
>> Clearly Ada and SPARK must
>> have had exception contracts which would have statically prevented
>> unhandled exceptions,
> 
> Well, it seems a stricture on design to me, if it is to mean:
> "If implementing my abstraction, though shalt raise but these
> exceptions: A, B, and C".

The contract can be refined as necessary. E.g. between may and shall raise.
It is an important thing especially with contracts inherited from
overridden operations. And there must be transitive contracts, e.g. "*"
raises this and what "+" does.

> Would He, the designer of exception contracts, by looking into
> some crystal ball, then write the contract knowing of all
> possible implementations of the contracted feature in advance?

Certainly so. Because of separation of implementation and interface.

> Able to decide on which paths of unforeseen computation some
> implementation might want to give up?

It is not an implementation which does not fulfill the contract, per
definition of the term "implementation." Sorry about telling basic design
by contract stuff.

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

Re: Problems with SPARK 2015 and XMLAda

[G.B.]

On 21.08.15 13:56, Dmitry A. Kazakov wrote:
> On Fri, 21 Aug 2015 12:09:43 +0200, G.B. wrote:
>
>> On 21.08.15 11:37, Dmitry A. Kazakov wrote:
>>> Clearly Ada and SPARK must
>>> have had exception contracts which would have statically prevented
>>> unhandled exceptions,
>>
>> Well, it seems a stricture on design to me, if it is to mean:
>> "If implementing my abstraction, though shalt raise but these
>> exceptions: A, B, and C".
>
> The contract can be refined as necessary. E.g. between may and shall raise.
> It is an important thing especially with contracts inherited from
> overridden operations. And there must be transitive contracts, e.g. "*"
> raises this and what "+" does.

O.K.

>> Would He, the designer of exception contracts, by looking into
>> some crystal ball, then write the contract knowing of all
>> possible implementations of the contracted feature in advance?
>
> Certainly so. Because of separation of implementation and interface.

You mean, the designer of contracts with exceptions only needs
to know all possible implementations trivially, correct?
Thus excluding all designs of the feature he might not
have *not* thought of, and need not, due to this formal restriction
banning a choice of exceptions. "You don't need these, my boy!" This has 
consequences.

Like, the consequence
  "You cannot implement the caller and thus you must scrap all your
   design"
does not start from more real
  "You have implemented the caller and thus you cannot scrap all your
   design"

I don't personally need much variability of exceptions, I'd like to
have them in contracts, I use "raises" annotations all the time.
But! Few. Assertion_Error is one.
I also know that exceptions requires adaptable software; I imagine
that programmers will place exception information that is disallowed
by the contract into specially formalized message strings, insofar
as their design requires some handling, but elsewhere.

Or they go "enterprise" and say "An error has occurred".

Uses of contracted exceptions as deplorable as these may outweigh
any advantages.
This is when I'd like exceptions as non-extensible, yet derived
things:

    Drought : exception is new End_Error;

This way, when handling something more specific than End_Error,
"when others =>" could be replaced with a kind of "class-wide"
handler, the class essentially covering related names.

>> Able to decide on which paths of unforeseen computation some
>> implementation might want to give up?
>
> It is not an implementation which does not fulfill the contract, per
> definition of the term "implementation." Sorry about telling basic design
> by contract stuff.

Design by Contract™, which wasn't defined by your or me, has
the "retry" facility as part of the "rescue"(*); both, exceptions as
assertion failures and exceptions as other failures are parts of
the definitions surrounding DbC. But not in the way imagined
here. I'm sure that this imagination of "design by contract" has
somehow definitions of something quite reasonable. It would be
nice, though, if the number of naming conflicts could be small.

It is the possibility of computing possible implementations that
I thought I'd question: designing contracts is a process that
leads to decisions. I am not convinced that shifting responsibility
of handling every non-contracted failure to the implementer
(so as to stay within the allowances of the contract) is going
to be acceptable. Or if so, it will be worked around as outlined
above.

You have reminded us frequently of HALT in connection with
how to predict things in contracts. Do you think that the
*choice* of exceptions is an exception?

__
(*) an older view:
http://se.ethz.ch/~meyer/publications/methodology/exceptions.pdf

Re: Problems with SPARK 2015 and XMLAda

[brbarkstrom]

An alternative to SPARK may be TLA+ and its associated
tools.  TLA+ has a lot of work put in by Leslie Lamport,
who won last year's ACM Turing prize.  The April issue
of Comm. ACM has a report from Amazon Web Service developers
about using TLA+ and its tools to provide formal methods
of proving that programs are correct:

Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M.,
and Dearduff, M., 2015: How Amazon Web Services Uses Formal
Methods, Comm. ACM, 58, No. 4, 66-73.

The tools are available using an Eclipse environment, which 
suggests that the tool developers are being supported by an IBM
contingent of developers.

I've not delved deeply into TLA+, which has a pretty
massive amount of hypertext documentation, see

Lamport, L., 2015: The TLA Home Page, <http:research.microsoft.com/
en-us/um/people/lamport/tla/tla.html>

Thus, I don't know how much of an advance these tools make 
over SPARK.  I can't say whether they support exceptions, access 
variables, or task hierarchies.  On the other hand, TLA+ is probably one 
generation beyond SPARK and Lamport has a very high reputation 
for his math.  It is clear that TLA+ and its tools support
preconditions and postconditions for assisting proofs.
Merging TLA+ with Ada is probably at about the same level
of difficulty as merging SPARK with Ada.  According to the
article on the Amazon experience, TLA+ is fairly easy to
learn.

Bruce B.

Re: Problems with SPARK 2015 and XMLAda

[Dmitry A. Kazakov]

On Fri, 21 Aug 2015 15:46:58 +0200, G.B. wrote:

> On 21.08.15 13:56, Dmitry A. Kazakov wrote:
>> On Fri, 21 Aug 2015 12:09:43 +0200, G.B. wrote:
>>
>>> Would He, the designer of exception contracts, by looking into
>>> some crystal ball, then write the contract knowing of all
>>> possible implementations of the contracted feature in advance?
>>
>> Certainly so. Because of separation of implementation and interface.
> 
> You mean, the designer of contracts with exceptions only needs
> to know all possible implementations trivially, correct?

The designer of the exceptions contract needs to know what he wants to
impose on the implementations to make client design robust.

> Thus excluding all designs of the feature he might not
> have *not* thought of, and need not, due to this formal restriction
> banning a choice of exceptions.

He must, because the clients will rely on the contract. He would avoid too
rigid contracts, sure.

> Like, the consequence
>   "You cannot implement the caller and thus you must scrap all your
>    design"
> does not start from more real
>   "You have implemented the caller and thus you cannot scrap all your
>    design"

That is not such a big problem as it appears. The designer of the contract
can include may raise Constraint_Error or Data_Error. This would not weaken
the design of the implementation, which, still, can strengthen the
post-condition to "I don't raise Constraint_Error." The prover will use the
*concrete* client contract of the implementation, to see that the client
does not need to handle Constraint_Error when it does not pass it further.

The important thing is that the prover deals with actual contracts, unless
it is generic programming (sets of implementations).

> I don't personally need much variability of exceptions, I'd like to
> have them in contracts, I use "raises" annotations all the time.
> But! Few. Assertion_Error is one.
> I also know that exceptions requires adaptable software; I imagine
> that programmers will place exception information that is disallowed
> by the contract into specially formalized message strings, insofar
> as their design requires some handling, but elsewhere.
> 
> Or they go "enterprise" and say "An error has occurred".

Programmers misuse language features. A good language design is to prevent
them doing this.

> Uses of contracted exceptions as deplorable as these may outweigh
> any advantages.
> This is when I'd like exceptions as non-extensible, yet derived
> things:
> 
>     Drought : exception is new End_Error;
> 
> This way, when handling something more specific than End_Error,
> "when others =>" could be replaced with a kind of "class-wide"
> handler, the class essentially covering related names.

This is another discussion: whether exception is a value of an indefinite
type (Ada) or of a type hierarchy (C++). Both have advantages and
disadvantages. Contracted exceptions would gravitate to the former.

>>> Able to decide on which paths of unforeseen computation some
>>> implementation might want to give up?
>>
>> It is not an implementation which does not fulfill the contract, per
>> definition of the term "implementation." Sorry about telling basic design
>> by contract stuff.
> 
> Design by Contract™, which wasn't defined by your or me,

I don't care about trade marks. I do about the meanings.

> It is the possibility of computing possible implementations that
> I thought I'd question: designing contracts is a process that
> leads to decisions. I am not convinced that shifting responsibility
> of handling every non-contracted failure to the implementer
> (so as to stay within the allowances of the contract) is going
> to be acceptable. Or if so, it will be worked around as outlined
> above.

A contract that is not fulfilled is not a contract. Of course you can
redesign any contract during the software developing cycle, that is no
problem, except for the costs. But no implementation exists prior the
contract and no code is an implementation if it breaches the contract.
Simple, isn't?

> You have reminded us frequently of HALT in connection with
> how to predict things in contracts. Do you think that the
> *choice* of exceptions is an exception?

No.

Contract is not an implementation. A contract is a constraint put on the
set of possible implementations. Halting problem equivalence is a handy
tool to illustrate that the set of implementations cannot be reduced to a
singleton instance. Which is why contract /= implementation.

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

Re: Problems with SPARK 2015 and XMLAda

[Bob Duff]

"G.B." <bauhaus@futureapps.invalid> writes:

> Design by Contract™, which wasn't defined by your or me, has
> the "retry" facility as part of the "rescue"(*); ...

Eiffel is a pretty good language design, but "retry" is probably my
least favorite feature of that language.  It's just a disguised "goto".
I'm not 100% opposed to goto's in all cases, but they should normally be
avoided, and this is the worst kind of goto -- a goto that jumps
backward, thus forming a loop.

Meyer's examples have kludgy flags to indicate "how did I get here?"
As in "If I got here from the exception handler, then do the exceptional
case, else do the normal case".  He even has examples where there's a
counter of the number of times the exception handler was entered.
Yuck.

And the disguised goto is worse than a goto, because there's no label
saying "beware!, somebody jumps here from elsewhere!".

In Ada syntax, this seems clear enough:

procedure P (...) is
begin
   Do_Something;
exception
   when Some_Error =>
      Do_Something_Else;
end P;

But Meyer prefers this:

procedure P (...) is
   Flag : Boolean := False;
begin
   <<Retry>>
   if Flag then
      Do_Something_Else;
   else
      Do_Something;
   end if;
exception
   when Some_Error =>
      Flag := True;
      goto Retry; -- Illegal in Ada, for good reason!
end P;

Except the label is implicit in Eiffel, and the "goto Retry" is just
"retry".  (Oh, and the initialization to False is also implicit in
Eiffel -- another bad design decision, but unrelated to "retry".)

His complaint about the first version of P is that Do_Something_Else
might violate contracts (because at that time, Ada didn't have any way
to express contracts).  But the second version of P has the same
problem, for the same reason (Ada didn't have any way to express
contracts).

It boils down to "Ada exception handlers might have bugs".  Well, yeah,
but any code might have bugs.  Moving the bugs from the handler to
the main body of code doesn't prevent bugs.

>...both, exceptions as
> assertion failures and exceptions as other failures are parts of
> the definitions surrounding DbC. But not in the way imagined
> here. I'm sure that this imagination of "design by contract" has
> somehow definitions of something quite reasonable. It would be
> nice, though, if the number of naming conflicts could be small.

- Bob

Re: Problems with SPARK 2015 and XMLAda

[Dmitry A. Kazakov]

On Fri, 21 Aug 2015 19:44:12 -0400, Bob Duff wrote:

> It boils down to "Ada exception handlers might have bugs".  Well, yeah,
> but any code might have bugs.  Moving the bugs from the handler to
> the main body of code doesn't prevent bugs.

Yes. That is why there is no such thing as handing bugs, handling contract
violations, dynamic contract checks. Why repeating other's errors?

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

Re: Problems with SPARK 2015 and XMLAda

[Stefan.Lucks]

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

On Fri, 21 Aug 2015, Dmitry A. Kazakov wrote:

>> If an exception cannot be handled in the caller's context, the caller
>> cannot satisfy its own postconditions. See above!
>
> Exactly! You cannot implement the caller and thus you must scrap all your
> design (decomposition into modules like caller and callee).

That is Ada. The caller needs to "with" the package where the callee is 
defined, anyway.

>>> Since the callee shall not know its callers, which is one of the major
>>> software design principles, there is no way how return code could be a
>>> substitute to exception.
>>
>> Hu?????? That does not make any sense to me!!!
>
> (Which "that"?)

That := "Since the callee ... to exception.";

> Yes, it must re-implement exception propagation throughout all caller,
> existing and potential ones.

Wait a minute -- why did you write "re-implement", rather than 
"implement"?

Trying to convert an existing big Ada implementation into SPARK would be a 
very tedious pice of work, regardless of exceptions versus error codes. I 
am inclined to say, this would be futile from the very beginning.

A fresh project, starting from the scratch, would be entirely different.

> Massive distributed redesign of all client code base. Not a disadvantage,
> indeed, it is a catastrophe.

Agreed! If you have a big code base in Ada, translating it into SPARK 
would be the highway to hell, or at least mental insanity.

>> One thing that is frightening about exceptions is that by not handling
>> locally declared exceptions, some global caller's caller cannot handle
>> that specific exception at all -- it can only use *the* *same* catch-all
>>
>>    when others => ...;
>
> That is true for non-contracted exceptions only. Clearly Ada and SPARK must
> have had exception contracts which would have statically prevented
> unhandled exceptions, including the "when others =>" mess. E.g. Finialize
> would have "not raising anything" in the contract, which would force you to
> handle all exceptions.

Unfortunately, Ada doesn't have contracted exceptions, today.

> Wrong. I/O states are all known at compile time.

My point was that the overhead for handling error codes is neglible for 
these cases.

Stefan


--------  I  love  the  taste  of  Cryptanalysis  in  the morning!  --------
www.uni-weimar.de/de/medien/professuren/mediensicherheit/people/stefan-lucks
----Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universität Weimar, Germany----

Re: Problems with SPARK 2015 and XMLAda

[Dmitry A. Kazakov]

On Fri, 21 Aug 2015 12:43:53 +0200, Stefan.Lucks@uni-weimar.de wrote:

> On Fri, 21 Aug 2015, Dmitry A. Kazakov wrote:
> 
>>> If an exception cannot be handled in the caller's context, the caller
>>> cannot satisfy its own postconditions. See above!
>>
>> Exactly! You cannot implement the caller and thus you must scrap all your
>> design (decomposition into modules like caller and callee).
> 
> That is Ada. The caller needs to "with" the package where the callee is 
> defined, anyway.

Not the callee, only the interface (contract) of.

>>>> Since the callee shall not know its callers, which is one of the major
>>>> software design principles, there is no way how return code could be a
>>>> substitute to exception.
>>>
>>> Hu?????? That does not make any sense to me!!!
>>
>> (Which "that"?)
> 
> That := "Since the callee ... to exception.";

Does not make sense #1 decoupling of callee from callers or that #2 this is
a major design principle?

>> Yes, it must re-implement exception propagation throughout all caller,
>> existing and potential ones.
> 
> Wait a minute -- why did you write "re-implement", rather than 
> "implement"?

Because with exceptions all this will be implemented by the compiler.

> Trying to convert an existing big Ada implementation into SPARK would be a 
> very tedious pice of work, regardless of exceptions versus error codes. I 
> am inclined to say, this would be futile from the very beginning.

That is true, because contracts and proofs, presently, cannot be gradually
refined. And because the contracts of the core Ada are too weak or absent
(as in the case of exceptions). The must be work done to refine
Constraint_Error, Storage_Error, Program_Error contracts.

> A fresh project, starting from the scratch, would be entirely different.

Yes, and this situation must be changed because contracts and proofs are
too valuable to be ignored.

>> Massive distributed redesign of all client code base. Not a disadvantage,
>> indeed, it is a catastrophe.
> 
> Agreed! If you have a big code base in Ada, translating it into SPARK 
> would be the highway to hell, or at least mental insanity.

SPARK must be an integral part of Ada.

>>> One thing that is frightening about exceptions is that by not handling
>>> locally declared exceptions, some global caller's caller cannot handle
>>> that specific exception at all -- it can only use *the* *same* catch-all
>>>
>>>    when others => ...;
>>
>> That is true for non-contracted exceptions only. Clearly Ada and SPARK must
>> have had exception contracts which would have statically prevented
>> unhandled exceptions, including the "when others =>" mess. E.g. Finialize
>> would have "not raising anything" in the contract, which would force you to
>> handle all exceptions.
> 
> Unfortunately, Ada doesn't have contracted exceptions, today.

But it could have them tomorrow.

>> Wrong. I/O states are all known at compile time.
> 
> My point was that the overhead for handling error codes is neglible for 
> these cases.

Really? When reading character by character you must check the code for
each single character. Actually, if honestly implemented, the approach
requires checking after each single language statement for error codes for
memory access violation, stack overflow, integer overflow, floating point
overflow, it is probably an infinite list, which is self-recursive because
check is a statement as well. This is semantically impossible because
checks involve invariants of higher abstractions, e.g. objects, groups of
objects, invariants which can hold in some context and do not hold in
others etc. Error code contradicts to basic principles of software
decomposition.

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

Re: Problems with SPARK 2015 and XMLAda

[Randy Brukardt]

<Stefan.Lucks@uni-weimar.de> wrote in message 
news:alpine.DEB.2.20.1508210948320.23241@debian...
...
> I doubt this makes any observable difference. The legitimate examples for
> exceptions that "signal things that cannot be known at compile time" (as
> Randy wrote) are usually related to input-output operations.

You really should say "external environment" rather than I/O. Anything that 
the target OS (or hardware!) provides is in that category -- environment 
variables (what if some other program adds/deletes a variable?), command 
lines, memory management (allocating too much memory), clocks, GUI (what if 
the user of the program manually closes a window? That can happen at any 
time.)

Not all of these things are slow in the sense of external I/O devices. The 
difference between exceptions and error codes (particularly as keeping OS 
error codes task safe adds an expense) may be more significant.

(But clearly the main issues are readability, locality, and the requirement 
to handle them.)

                                 Randy.