* Problems with SPARK 2015 and XMLAda @ 2015-08-19 15:58 Serge Robyns 2015-08-19 20:21 ` Simon Wright 0 siblings, 1 reply; 25+ messages in thread From: Serge Robyns @ 2015-08-19 15:58 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: Problems with SPARK 2015 and XMLAda 2015-08-19 15:58 Problems with SPARK 2015 and XMLAda Serge Robyns @ 2015-08-19 20:21 ` Simon Wright 2015-08-19 21:22 ` Serge Robyns 0 siblings, 1 reply; 25+ messages in thread From: Simon Wright @ 2015-08-19 20:21 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: Problems with SPARK 2015 and XMLAda 2015-08-19 20:21 ` Simon Wright @ 2015-08-19 21:22 ` Serge Robyns 2015-08-20 7:10 ` Jacob Sparre Andersen 2015-08-20 16:38 ` Shark8 0 siblings, 2 replies; 25+ messages in thread From: Serge Robyns @ 2015-08-19 21:22 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: Problems with SPARK 2015 and XMLAda 2015-08-19 21:22 ` Serge Robyns @ 2015-08-20 7:10 ` Jacob Sparre Andersen 2015-08-20 10:06 ` Mark Lorenzen 2015-08-20 16:38 ` Shark8 1 sibling, 1 reply; 25+ messages in thread From: Jacob Sparre Andersen @ 2015-08-20 7:10 UTC (permalink / raw) 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." ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: Problems with SPARK 2015 and XMLAda 2015-08-20 7:10 ` Jacob Sparre Andersen @ 2015-08-20 10:06 ` Mark Lorenzen 0 siblings, 0 replies; 25+ messages in thread From: Mark Lorenzen @ 2015-08-20 10:06 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: Problems with SPARK 2015 and XMLAda 2015-08-19 21:22 ` Serge Robyns 2015-08-20 7:10 ` Jacob Sparre Andersen @ 2015-08-20 16:38 ` Shark8 2015-08-20 18:42 ` Peter Chapin ` (2 more replies) 1 sibling, 3 replies; 25+ messages in thread From: Shark8 @ 2015-08-20 16:38 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: Problems with SPARK 2015 and XMLAda 2015-08-20 16:38 ` Shark8 @ 2015-08-20 18:42 ` Peter Chapin 2015-08-20 19:13 ` Jeffrey R. Carter 2015-08-20 20:00 ` Serge Robyns 2015-08-20 20:36 ` Randy Brukardt 2 siblings, 1 reply; 25+ messages in thread From: Peter Chapin @ 2015-08-20 18:42 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: Problems with SPARK 2015 and XMLAda 2015-08-20 18:42 ` Peter Chapin @ 2015-08-20 19:13 ` Jeffrey R. Carter 0 siblings, 0 replies; 25+ messages in thread From: Jeffrey R. Carter @ 2015-08-20 19:13 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: Problems with SPARK 2015 and XMLAda 2015-08-20 16:38 ` Shark8 2015-08-20 18:42 ` Peter Chapin @ 2015-08-20 20:00 ` Serge Robyns 2015-08-20 20:36 ` Randy Brukardt 2 siblings, 0 replies; 25+ messages in thread From: Serge Robyns @ 2015-08-20 20:00 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: Problems with SPARK 2015 and XMLAda 2015-08-20 16:38 ` Shark8 2015-08-20 18:42 ` Peter Chapin 2015-08-20 20:00 ` Serge Robyns @ 2015-08-20 20:36 ` Randy Brukardt 2015-08-20 23:21 ` Shark8 2015-08-21 6:26 ` Stefan.Lucks 2 siblings, 2 replies; 25+ messages in thread From: Randy Brukardt @ 2015-08-20 20:36 UTC (permalink / raw) "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. ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: Problems with SPARK 2015 and XMLAda 2015-08-20 20:36 ` Randy Brukardt @ 2015-08-20 23:21 ` Shark8 2015-08-21 6:26 ` Stefan.Lucks 1 sibling, 0 replies; 25+ messages in thread From: Shark8 @ 2015-08-20 23:21 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: Problems with SPARK 2015 and XMLAda 2015-08-20 20:36 ` Randy Brukardt 2015-08-20 23:21 ` Shark8 @ 2015-08-21 6:26 ` Stefan.Lucks 2015-08-21 7:30 ` Dmitry A. Kazakov 1 sibling, 1 reply; 25+ messages in thread From: Stefan.Lucks @ 2015-08-21 6:26 UTC (permalink / raw) [-- 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---- ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: Problems with SPARK 2015 and XMLAda 2015-08-21 6:26 ` Stefan.Lucks @ 2015-08-21 7:30 ` Dmitry A. Kazakov 2015-08-21 8:19 ` Stefan.Lucks 0 siblings, 1 reply; 25+ messages in thread From: Dmitry A. Kazakov @ 2015-08-21 7:30 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: Problems with SPARK 2015 and XMLAda 2015-08-21 7:30 ` Dmitry A. Kazakov @ 2015-08-21 8:19 ` Stefan.Lucks 2015-08-21 9:37 ` Dmitry A. Kazakov 2015-08-24 21:32 ` Randy Brukardt 0 siblings, 2 replies; 25+ messages in thread From: Stefan.Lucks @ 2015-08-21 8:19 UTC (permalink / raw) [-- 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---- ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: Problems with SPARK 2015 and XMLAda 2015-08-21 8:19 ` Stefan.Lucks @ 2015-08-21 9:37 ` Dmitry A. Kazakov 2015-08-21 10:09 ` G.B. 2015-08-21 10:43 ` Stefan.Lucks 2015-08-24 21:32 ` Randy Brukardt 1 sibling, 2 replies; 25+ messages in thread From: Dmitry A. Kazakov @ 2015-08-21 9:37 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: Problems with SPARK 2015 and XMLAda 2015-08-21 9:37 ` Dmitry A. Kazakov @ 2015-08-21 10:09 ` G.B. 2015-08-21 11:56 ` Dmitry A. Kazakov 2015-08-21 10:43 ` Stefan.Lucks 1 sibling, 1 reply; 25+ messages in thread From: G.B. @ 2015-08-21 10:09 UTC (permalink / raw) 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?) ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: Problems with SPARK 2015 and XMLAda 2015-08-21 10:09 ` G.B. @ 2015-08-21 11:56 ` Dmitry A. Kazakov 2015-08-21 13:46 ` G.B. 0 siblings, 1 reply; 25+ messages in thread From: Dmitry A. Kazakov @ 2015-08-21 11:56 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: Problems with SPARK 2015 and XMLAda 2015-08-21 11:56 ` Dmitry A. Kazakov @ 2015-08-21 13:46 ` G.B. 2015-08-21 14:45 ` brbarkstrom ` (2 more replies) 0 siblings, 3 replies; 25+ messages in thread From: G.B. @ 2015-08-21 13:46 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: Problems with SPARK 2015 and XMLAda 2015-08-21 13:46 ` G.B. @ 2015-08-21 14:45 ` brbarkstrom 2015-08-21 15:34 ` Dmitry A. Kazakov 2015-08-21 23:44 ` Bob Duff 2 siblings, 0 replies; 25+ messages in thread From: brbarkstrom @ 2015-08-21 14:45 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: Problems with SPARK 2015 and XMLAda 2015-08-21 13:46 ` G.B. 2015-08-21 14:45 ` brbarkstrom @ 2015-08-21 15:34 ` Dmitry A. Kazakov 2015-08-21 23:44 ` Bob Duff 2 siblings, 0 replies; 25+ messages in thread From: Dmitry A. Kazakov @ 2015-08-21 15:34 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: Problems with SPARK 2015 and XMLAda 2015-08-21 13:46 ` G.B. 2015-08-21 14:45 ` brbarkstrom 2015-08-21 15:34 ` Dmitry A. Kazakov @ 2015-08-21 23:44 ` Bob Duff 2015-08-22 6:22 ` Dmitry A. Kazakov 2 siblings, 1 reply; 25+ messages in thread From: Bob Duff @ 2015-08-21 23:44 UTC (permalink / raw) "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 ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: Problems with SPARK 2015 and XMLAda 2015-08-21 23:44 ` Bob Duff @ 2015-08-22 6:22 ` Dmitry A. Kazakov 0 siblings, 0 replies; 25+ messages in thread From: Dmitry A. Kazakov @ 2015-08-22 6:22 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: Problems with SPARK 2015 and XMLAda 2015-08-21 9:37 ` Dmitry A. Kazakov 2015-08-21 10:09 ` G.B. @ 2015-08-21 10:43 ` Stefan.Lucks 2015-08-21 12:35 ` Dmitry A. Kazakov 1 sibling, 1 reply; 25+ messages in thread From: Stefan.Lucks @ 2015-08-21 10:43 UTC (permalink / raw) [-- 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---- ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: Problems with SPARK 2015 and XMLAda 2015-08-21 10:43 ` Stefan.Lucks @ 2015-08-21 12:35 ` Dmitry A. Kazakov 0 siblings, 0 replies; 25+ messages in thread From: Dmitry A. Kazakov @ 2015-08-21 12:35 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: Problems with SPARK 2015 and XMLAda 2015-08-21 8:19 ` Stefan.Lucks 2015-08-21 9:37 ` Dmitry A. Kazakov @ 2015-08-24 21:32 ` Randy Brukardt 1 sibling, 0 replies; 25+ messages in thread From: Randy Brukardt @ 2015-08-24 21:32 UTC (permalink / raw) <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. ^ permalink raw reply [flat|nested] 25+ messages in thread
end of thread, other threads:[~2015-08-24 21:32 UTC | newest] Thread overview: 25+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2015-08-19 15:58 Problems with SPARK 2015 and XMLAda Serge Robyns 2015-08-19 20:21 ` Simon Wright 2015-08-19 21:22 ` Serge Robyns 2015-08-20 7:10 ` Jacob Sparre Andersen 2015-08-20 10:06 ` Mark Lorenzen 2015-08-20 16:38 ` Shark8 2015-08-20 18:42 ` Peter Chapin 2015-08-20 19:13 ` Jeffrey R. Carter 2015-08-20 20:00 ` Serge Robyns 2015-08-20 20:36 ` Randy Brukardt 2015-08-20 23:21 ` Shark8 2015-08-21 6:26 ` Stefan.Lucks 2015-08-21 7:30 ` Dmitry A. Kazakov 2015-08-21 8:19 ` Stefan.Lucks 2015-08-21 9:37 ` Dmitry A. Kazakov 2015-08-21 10:09 ` G.B. 2015-08-21 11:56 ` Dmitry A. Kazakov 2015-08-21 13:46 ` G.B. 2015-08-21 14:45 ` brbarkstrom 2015-08-21 15:34 ` Dmitry A. Kazakov 2015-08-21 23:44 ` Bob Duff 2015-08-22 6:22 ` Dmitry A. Kazakov 2015-08-21 10:43 ` Stefan.Lucks 2015-08-21 12:35 ` Dmitry A. Kazakov 2015-08-24 21:32 ` Randy Brukardt
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox