GNAT packages in Linux distributions
in [ADA]
|
From: Dmitry A. Kazakov on 12 May 2010 13:48 On Wed, 12 May 2010 20:10:26 +0200, stefan-lucks(a)see-the.signature wrote: > On Wed, 12 May 2010, Dmitry A. Kazakov wrote: > >> Any program is partially correct, if otherwise has not been observed. I >> fail to see how Eiffel is different from C or Assembler in that respect. > > In C, if I try to compute the factorial of a (natural) number, I'll always > get an answer (assuming a decent program, which can be written by a > first-year computer science student, and a normal C-compiler). > may be right or wrong. If the input is too large, the answer actually is > wrong (our first-year student stores the result in an int variable, and > 100! is too large). But I still get an answer, even if it is wrong. > > In Eiffel, I'll either get an answer, or the program will tell that at > some point of time when computing, say, the factorial of 100, a certain > exception has been raised. (I didn't try out Eiffel, but that is what I > would expect.) But if I get an answer, I can be sure it is the right one. > That is partial correctness. 1. Wrong answer is no more/less incorrect as an exception. Otherwise you have to introduce some scale of correctness, which is called accuracy. A program can yield more or less accurate results staying correct. 2. It is unrelated to error checks. The programmer did not use any. That Eiffel possibly checks for integer overflow and C does not is irrelevant to the issue. >> The point is that run-time checks contribute nothing to correctness either >> partial or not. Because a partially incorrect program remains partially >> incorrect independently on whether you check that or not: > > Technically, any program of the form > > {Any Precondition} > Statements; > if not Postcondition then > raise Program_Error; > end if; > {Postcondition} > > is partially correct, even if "Statements;" are semantic nonsense (as long > as the whole thing compiles at all), regardless of "{Any Precondition}". No. If Statements were irrelevant, you could take this: {Any Precondition} raise Program_Error; {Postcondition} The problem is that Program_Error does not satisfy postcondition. > Perhaps you don't like raising an exception? I don't like any action upon a failed check, if that was a check. To self checks are clearly infeasible. > OK, we can stick with the original approach from Hoare from 1969, who > didn't know (or didn't care) about exceptions. His approach, which I greatly appreciate, is perfectly compatible with exceptions. Exception propagation is a part of the program behavior to be checked as anything else. E.g. pre : x = 1 if x = 1 then raise Foo; end if; post : Foo propagating This program were be incorrect if it would not raise Foo. > The following program is > partially correct, regardless of the "Statements;" and "{Any > Precondition}": > > {Any Precondition} > Statements; > while not Postcondition loop > null; > end loop; > {Postcondition} Hmm, I would consider it totally incorrect => not partially incorrect, because in no state it satisfies the postcondition. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de
From: Georg Bauhaus on 12 May 2010 14:09 On 12.05.10 19:24, Dmitry A. Kazakov wrote: > On Wed, 12 May 2010 18:06:16 +0200, Yannick Duchêne (Hibou57) wrote: > >> Well, I've noted you do not like runtime-check because it is not [formal] >> proof of anything, but no one said it is formal proof, this is just better >> to catch error the sooner and understand why this was an error. > > Yes, it is better but that is not the point. Being better is precisely the point (of DbC). DbC talks about proof obligations, not about provability. > there is no > substantial difference between Eiffel precondition and C's if statement > beyond syntax sugar, and that if-statement is less misleading. "If" is - much more flexible and - totally unspecific and - not integrated with, e.g. rescue clauses; - needs bodies You can emulate anything with "if" or write assembler, though ... . >> About expression now, although understandability of a source does not >> provide proof, this help to at least make partial assertions and discover >> what's wrong. > > No more than an appropriately placed if-statement, tracing call, debugging > break point etc. You cannot place an "if" in a specification. If you say Precondition: Has-Such-And-Such; then this is effectively raise when not Has-Such-And-Such; Except that smart tools do not need to understand the full program including its bodies in order to infer a precondition. >> It is best to >> face an error like “this class invariant was violated” than “this access >> to this memory address failed”. > > The text used in error message is up to the programmer. My objection is not > that what Eiffel offers is useless. The objection is that it has nothing to > do with contracts (in its normal meaning) or with design by. These are no > more than *debugging* tools. Using the terms pre-, postcondition, invariant > is also misleading. What is "breach of contract" in your world? Anything that is not yielding a full proof of everything is a debugging tool. So what? Should we therefore bend the normal, worldly definition of "contract" to mean something that can never be had? > What Ada lacks is better contracts specified by the programmer only when he > wishes to. E,g, exception contracts, statements about purity of a function, > upper bound of stack use etc. Raising of exceptions is an integral part of DbC specs. Purity: postcondition: interesting_1 = interesting_1'old and interesting_2 = interesting_2'old and ...; Stack usage: precondition: avail = max_avail - 140; > Ada had dynamic constraints long before Eiffel. If one wished to extend > this feature, it is welcome. Just do not call it "error check", when you > use the subtype Positive. Tie it to subtypes. How would you specify subtype Even is ...; ?
From: Georg Bauhaus on 12 May 2010 14:15 On 12.05.10 19:24, Dmitry A. Kazakov wrote: > On Wed, 12 May 2010 18:06:16 +0200, Yannick Duchêne (Hibou57) wrote: > >> Well, I've noted you do not like runtime-check because it is not [formal] >> proof of anything, but no one said it is formal proof, this is just better >> to catch error the sooner and understand why this was an error. > > Yes, it is better but that is not the point. Which is there is no > substantial difference between Eiffel precondition and C's if statement > beyond syntax sugar, and that if-statement is less misleading. Another important difference between a simple "if" and DbC assertions: The routine conditions must be consistent along the inheritance chain. It seems silly to have the programmer walk up and down the chain and make sure that substitutability isn't violated by manual "if" style preconditions. Hence, Eiffel's require else and ensure then for overriding routines.
From: Dmitry A. Kazakov on 12 May 2010 14:33 On Wed, 12 May 2010 20:09:49 +0200, Georg Bauhaus wrote: > On 12.05.10 19:24, Dmitry A. Kazakov wrote: >> On Wed, 12 May 2010 18:06:16 +0200, Yannick Duchêne (Hibou57) wrote: >> >>> Well, I've noted you do not like runtime-check because it is not [formal] >>> proof of anything, but no one said it is formal proof, this is just better >>> to catch error the sooner and understand why this was an error. >> >> Yes, it is better but that is not the point. > > Being better is precisely the point (of DbC). > DbC talks about proof obligations, not about provability. Who is obliged to whom in what? >> there is no >> substantial difference between Eiffel precondition and C's if statement >> beyond syntax sugar, and that if-statement is less misleading. > > "If" is > - much more flexible and > - totally unspecific and > - not integrated with, e.g. rescue clauses; > - needs bodies > > You can emulate anything with "if" or write assembler, though ... . Yes, but all above is not substantial. >>> About expression now, although understandability of a source does not >>> provide proof, this help to at least make partial assertions and discover >>> what's wrong. >> >> No more than an appropriately placed if-statement, tracing call, debugging >> break point etc. > > You cannot place an "if" in a specification. The answer was in my post. You have skipped out. OK, it was that exceptions from declarations is not a good idea. And considering it more deeply, Eiffel cannot do it either, because specifications are static things. What you meant is actually "if" in declarations elaboration, which is quite possible. >>> It is best to >>> face an error like “this class invariant was violated” than “this access >>> to this memory address failed”. >> >> The text used in error message is up to the programmer. My objection is not >> that what Eiffel offers is useless. The objection is that it has nothing to >> do with contracts (in its normal meaning) or with design by. These are no >> more than *debugging* tools. Using the terms pre-, postcondition, invariant >> is also misleading. > > What is "breach of contract" in your world? A case for the court. >> What Ada lacks is better contracts specified by the programmer only when he >> wishes to. E,g, exception contracts, statements about purity of a function, >> upper bound of stack use etc. > > Raising of exceptions is an integral part of DbC specs. And buffer overflow is an integral part of C... I meant static contracts, statically checked, if that was not clear. It don't need a shortcut for if-then-raise. >> Ada had dynamic constraints long before Eiffel. If one wished to extend >> this feature, it is welcome. Just do not call it "error check", when you >> use the subtype Positive. Tie it to subtypes. > > How would you specify > > subtype Even is ...; ? Ada's syntax is: subtype <name> is <name> <constraint>; -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de
From: Georg Bauhaus on 12 May 2010 14:53
On 12.05.10 20:33, Dmitry A. Kazakov wrote: >> Being better is precisely the point (of DbC). >> DbC talks about proof obligations, not about provability. > > Who is obliged to whom in what? By being a programmer subscribing to the principles of DbC, you are obliged to show that the components of your system obey the components' contracts. The compiler and run-time try to help you achieving this goal. >>>> About expression now, although understandability of a source does not >>>> provide proof, this help to at least make partial assertions and discover >>>> what's wrong. >>> >>> No more than an appropriately placed if-statement, tracing call, debugging >>> break point etc. >> >> You cannot place an "if" in a specification. > > The answer was in my post. You have skipped out. OK, it was that exceptions > from declarations is not a good idea. And considering it more deeply, > Eiffel cannot do it either, because specifications are static things. Which set of "specifications" has only static things in it? Why exclude conditionals whose results cannot reasonably be computed by the compiler but (a) can be computed for every single case occuring in the executing program (b) can guide the author of a client of a DbC component? For example, assume that Is_Prime(N) is a precondition of sub P. Furthermore, TIME(Is_Prime(N)) >> PERMISSIBLE_TIME. Then, still, PRE: Is_Prime (N) expresses an obligation, part of a contract: Don't call P unless N is prime, no matter whether or not assertion checking is in effect. (A DbC principle is that assertions are *not* a replacement for checking input (at the client side).) >> What is "breach of contract" in your world? > > A case for the court. What's the court (speaking of programs)? >>> What Ada lacks is better contracts specified by the programmer only when he >>> wishes to. E,g, exception contracts, statements about purity of a function, >>> upper bound of stack use etc. >> >> Raising of exceptions is an integral part of DbC specs. > > And buffer overflow is an integral part of C... I meant static contracts, > statically checked, if that was not clear. It wasn't clear to me that you wanted a mathematically closed structure to be the only legitimate substance of "contract". I'm a programmer. If I "design" anything, it is a program whose parts need to interact in a way that meets some almost entirely non-mathematical specification. I try to add some formality to the whole thing. This helps. I wish I had static type checking for a start! >> How would you specify >> >> subtype Even is ...; ? > > Ada's syntax is: > > subtype <name> is <name> <constraint>; What will static <name> and static <constraint> be for subtype Even? |