GNAT packages in Linux distributions
in [ADA]
|
From: Dmitry A. Kazakov on 13 May 2010 04:39 On Thu, 13 May 2010 04:03:38 +0200, Georg Bauhaus wrote: > All of these features of C have merits besides what else > they may have. But they sure don't warrant dismissing DbC? No. The point was about lack of substance in DbC as promoted by Eiffel. > Ada seems better here. But before the arrival of preconditions > etc. Ada didn't have that much to offer to programmers wanting > to state sets of permissible values, for example for subprogram > parameters. Ada has strong types. "A set of permissible values" does not look like that. > Ada subtypes, e.g. scalars, are poorly equipped for this style of > value set specification, AFAICS. They do establish two implicit > preconditions (>= S'First and <= S'Last). These are not preconditions, but invariants. > A Qi style type system could do more via types but is not to be in Ada > any time soon, is it? I don't know. If Ada designers will keep on driving Ada into a dynamically typed language, then probably never. > package P is > > type Number is range 1 .. 10; > function Compute (A, B: Number) return Number > with Precondition => A >= B; I don't understand this notation. > (Such specifications, if they were to be being static, would exclude > a test of A in relation to B at run time, You need not to specify anything you cannot check... As somebody said, do not check for bugs you aren't going to fix. (:-)) > A distinguishing property of DbC visible here is > that a programmer will *see* the contract (or part thereof). I do not accept "preconditions" in the operations, which are not statically true: function "/" (X, Y : Number) return Number -- Wrong! pre : Y /= 0.0; function "/" (X, Y : Number) return Number -- Right! post : result = X/Y or else Constraint_Error; >>> 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 >> >> If they can for *every* case, they are statically checkable, per >> definition. > > "Every case" cannot "reasonably be computed by the compiler". Either they can or cannot. You said they can, but then added "unreasonably can", or "reasonably cannot", whatever. Sound like Eiffel's contracts, x is even, not really even, we wanted it be even... (:-)) >>> (b) can guide the author of a client of a DbC component? >> >> I don't know what does it mean technically. > > Contractually, it means "do as the preconditions say." Like "do as comments say"? Note, since your "preconditions" are not static, how can you know *what* they say, in order to do as they do? Eiffel masters with easily. Its DbC is "do as you want, we'll see later." But I think that the honor of inventing this design principle by right belongs to C... > "Under no circumstances shall the body of a routine ever > test for the routine's precondition." -- OOCS2, p.343 > > IOW, no redundant checks. No, it would be *inconsistent* checks. No program can check itself. Eiffel pre- and postconditions fall into this category. Of course, I can imagine a compiler which would use a separate CPU core to check pre- and ponstconditions at tun-time. but that is beyond the point. >>> 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. >> >> char X [80]; // Don't use X[80], X[81], no matter etc. > > Yes, and don't use X[-200]. But you can. OTOH: > > function Access_Element (S: String_80; X: Index_80); > > function Careful (S: String_80; X: Index_80) > with Precondition => X rem 2 = 1; > > How would you write a statically checked version? Trivially: function Careful (S: String_80; X: Index_80) with Precondition True; with Postcondition <whatever> or Constraint_Error >>> (A DbC principle is that assertions are *not* a replacement >>> for checking input (at the client side).) >> >> Exactly. Assertion is not a check. You said this. > > What check means, exactly, is important. Error_Check (P) => P is incorrect other things you mentioned are control flow control statements. It is really simply: an error/correctness check is a statement about the program behavior. If-statement/exception etc is the program behavior. >>>>> What is "breach of contract" in your world? >>>> >>>> A case for the court. >>> >>> What's the court (speaking of programs)? >> >> A code revision. > > How do you become aware of a broken contract? > Statically? Dynamically? Me? I am not a part of the system. These terms do not apply to me. Before going any further, you should define the system under consideration. Note that your "DbC mindset" includes the programmer(s) into the system, delivered and deployed. Isn't that indicatory? (:-)) >>> 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. >> >> Mathematics has nothing to do with this. It is about a clear distinction >> between a contract and a condition, how undesirable it could be but >> nevertheless it is a condition, which you, as a programmer are obliged to >> consider as *possible*. Eiffel gives you an illusion of safety. > > No. Eiffel marketing claims that a fully proven DbC program > is 100% bug free. I can imagine Microsoft marketing doing same, if they didn't already... >> Simply consider >> the following rule: my program shall handle each exception I introduce. >> Objections? > > No objection. > >> Then consider exceptions from assertions. > > That is what Eiffel's rescue mechanism is about. And how do you rescue from: function "-" (X : Positive) return Positive; Note, if you handle an exception then it is same as if-statement. (I agree that if-statements could be better arranged, have nicer syntax etc. Is that the essence of Eiffel's DbC?) >>>>> 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? >> >> No, in Ada<constraint> is not required to be static. Example: >> >> procedure F (A : String) is >> subtype Span is Integer range A'Range; > > Is the constraint, not to be static, then part of the contractual > specification of subtype Even? The specification of includes all possible values of the constraint. When you assign -1 to Positive, it is not an error, it is a valid, well-defined program, which behavior is required to be Constraint_Error propagation. When you assign -1.0 to Positive, it is an error and the program is invalid. Where and how you are using these two mechanisms is up to you. A FORTRAN program can be written in Ada, of course... -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de
From: Dmitry A. Kazakov on 13 May 2010 05:09 On Thu, 13 May 2010 02:37:37 +0200, stefan-lucks(a)see-the.signature wrote: > On Wed, 12 May 2010, Dmitry A. Kazakov wrote: > >> On Wed, 12 May 2010 20:10:26 +0200, stefan-lucks(a)see-the.signature wrote: >> >>> 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. > > We clearly disagree on this point. > > Consider being new in a town, and asking how to go from, say, the railway > station to the market place. If we ask a guy who appears to be a local > person in our eyes, but is actually as foreing as we are, most people > would prefer an exception "sorry, I don't know the way" over the answer of > being directed into the wrong direction. If you think, the "sorry" is as > bad as the wrong direction, that is your problem, which I am not > interested in discussing any further. Consider another example. Let you have a word processor, which also calculates frequencies of some words. After typing dozen pages of the document, you remove a word (the last instance, occasionally), and the processor crashes on zero divide trying to calculate its new frequency. I bet you would prefer a rubbish frequency displayed. The bottom line, the effect of an error is undefined. You cannot define any reasonable action upon, UNLESS further information were available. Which is equivalent to *specification* of a behavior. Once the behavior is defined, it is no more an error, e.g. the frequency of an unused word is displayed as an empty string. It is a mere requirement. If you don't know the answer, say "I don't know", do not shoot. >> 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 exception may just as well be raised when checking the postcondition. or from an if-statement placed by the programmer. >> {Any Precondition} >> raise Program_Error; >> {Postcondition} > > Yes, that program is partially correct. I wouldn't consider it as such. > Well, Hoare did originally not bother with exceptions, BTW Hoare, wasn't it actually Edsger Dijkstra? >> The problem is that Program_Error does not satisfy postcondition. > >> 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. > > Now I see what you mean. You are asking for contracts which include > exception propagation. Yes, that would be nice to have. How could it be otherwise? > Then you should like Eiffel, because this is what Eiffel actually does. In > Eiffel, the formal postcondition > > require P; > > is a shortcut notation for the logical > > Postcondition: P or else (Postcondition_Violation propagating); > > (whatever the name of the exception is), which is the real postcondition > of an Eiffel program. If Eiffel checks P at the end of the program, and > raises that exception when the check fails, then > > Eiffel-programs are always correct! Yes. Therefore a lazy programmer could write raise Postcondition_Violation; and claim his salary. > You don't even need to perform any static analysis to ensure their > correctness. (But you must not turn of the checks!) Nice language, the program semantics depends on the compiler options. (We have this in some places in Ada too, unfortunately) > Of course the catch is that you would rather want to specify > postconditions which exclude exception propagation. Yep. > -> Eiffel is a very expressive programming language, > while SPARK is less expressive. > > -> The language for contracts in SPARK is more expressive > than the language for contracts in Eiffel. OK > That doesn't mean that the contracts you can express in Eiffel are > invalid, however. With the addition you made they are not. Once you remove Postcondition_Violation (which can be done by a compiler switch), they become invalid. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de
From: Georg Bauhaus on 14 May 2010 19:45 On 5/13/10 10:39 AM, Dmitry A. Kazakov wrote: >> Ada seems better here. But before the arrival of preconditions >> etc. Ada didn't have that much to offer to programmers wanting >> to state sets of permissible values, for example for subprogram >> parameters. > > Ada has strong types. "A set of permissible values" does not look like > that. Ada's strong types are not really strong enough to express a supplier library's ADT expectations in the sense of DbC. Subtypes (or the type system) would need to by more specific for that. One OOSC2 example is easily handled by Ada's subtypes, though. It also shows that DbC does *not* assume contracts should necessarily become a meaningful part of your executing program, i.e. have the program do assertion monitoring. On the contrary. function sqrt(x: REAL) return REAL; pragma Precondition (X >= 0.0); -- and something like pragma --- Postcondition (sqrt'Result * sqrt'Result = x); function Sqrt(x: REAL) return REAL is begin ... end Sqrt; (The requirement that X >= 0.0 on entry will actually be part of a translated *Ada* program if REAL above is defined as a subtype of some type that includes values below 0.0. The check is not necessarily part of a corresponding Eiffel program that has require X >= 0.0.) Anyway, wherever the Ada compiler sees that a value passed to Sqrt is < 0.0, it can warn at least. The following would *not* be a DbC style Sqrt: function Sqrt_Not_DbC (X: REAL) return REAL is begin if X < 0.0 then -- "Handle the error, somehow" else -- "Proceed with normal square root computation" end if; end Sqrt_Not_DbC; -- cf. OOSC2, p.343 Instead, supplier is supposed to write the program Sqrt as if X >= 0.0 on entry. Only if X >= 0.0 can client legitimately expect supplier's Sqrt to terminate in a state that satisfies the postcondition and INV. (INV is probably just True here.) >> Ada subtypes, e.g. scalars, are poorly equipped for this style of >> value set specification, AFAICS. They do establish two implicit >> preconditions (>= S'First and<= S'Last). > > These are not preconditions, but invariants. 'First and 'Last are invariants of the type and they express preconditions when reinterpreted in the normal DbC way. Again, can you produce a statically checked invariant for subtype Even? >> package P is >> >> type Number is range 1 .. 10; >> function Compute (A, B: Number) return Number >> with Precondition => A>= B; > > I don't understand this notation. It says that the client of Compute would have to provide A, B such that A >= B if client expects Compute to produce its postcondition; otherwise, the expectation is unjustified and Compute is not bound by the contract, i.e. may fail and produce whatever, including an exception. The contract here is this: I, client, give you, Compute, numbers A and B that are as you told me. I, Compute, will produce my Postcondition if you give me numbers A and B as I told you. > I do not accept "preconditions" in the operations, which are not statically > true: That's your choice then, but not DbC's, which is more inclusive (again, statically checked subtype Even vs. X rem 2 = 0). > function "/" (X, Y : Number) return Number -- Wrong! > pre : Y /= 0.0; > > function "/" (X, Y : Number) return Number -- Right! > post : result = X/Y or else Constraint_Error; The second "/" is a DbC one. There is a big warning sign in OOSC2 that says, / \ NO PRECONDITION TOO BIG OR TOO SMALL \ / While a matter of choice, there is one strict rule: "It is _never_ acceptable to deal with a correctness condition on both the client and supplier sides." >>>> 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 >>> >>> If they can for *every* case, they are statically checkable, per >>> definition. >> >> "Every case" cannot "reasonably be computed by the compiler". > > Either they can or cannot. You said they can, but then added "unreasonably > can", or "reasonably cannot", whatever. Sound like Eiffel's contracts, x > is even, not really even, we wanted it be even... (:-)) When I mentioned "not reasonably be computed by the compiler" early on, I meant that DbC should be a possible system that helps programmers. I did not want to theorize program analysis systems that are impossible to produce. I can think of a DbC program with assertion monitoring turned on and see it as a stepwise attempt at working out the correctness properties of the program. For example, I can see the program crash when a new change set makes some variable have a different value. This value no longer meets the stated requirements of some subprogram. That is shown then by the run-time and I can think again. Preferrably think about possible mistakes in my attempts at corectness lemmata, since otherwise this procedure will degrade into debugging things into some state. But DbC here yields more than dealing with exceptions and erroneous execution in some random fashion can possibly achieve! >>>> (b) can guide the author of a client of a DbC component? >>> >>> I don't know what does it mean technically. >> >> Contractually, it means "do as the preconditions say." > > Like "do as comments say"? Yes. Only, a DbC system can be quite helpful in checking my understanding of more formal "comments". > Note, since your "preconditions" are not static, > how can you know *what* they say, in order to do as they do? I can write my client code such that the preconditions are true. I know what a procondition says if I do not need to solve hard problems to know the meaning of a predicate. Note that DbC includes requirements that are stated in natural language. Of course, not even trying to write predicates defeats the purpose of contracting between client and supplier, assisted by the DbC system. E.g., I read a number from input, and another number from input. I know that subprogram P wants one number to be odd and the other number to be even. (Otherwise, it does not guarantee that it produces its postcondition.) These are easily tested conditions. I know what I have to test and I know how to test what. >> IOW, no redundant checks. > > No, it would be *inconsistent* checks. No program can check itself. DbC checks are not part of the (intended) program. Monitoring can be turned off and this should have no effect on program correctness. The proof obligation rests on us, the programmers. >>>> 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. >>> >>> char X [80]; // Don't use X[80], X[81], no matter etc. >> >> Yes, and don't use X[-200]. But you can. OTOH: >> >> function Access_Element (S: String_80; X: Index_80); >> >> function Careful (S: String_80; X: Index_80) >> with Precondition => X rem 2 = 1; >> >> How would you write a statically checked version? > > Trivially: > > function Careful (S: String_80; X: Index_80) > with Precondition True; > with Postcondition<whatever> or Constraint_Error This is legitimate I'd say, but is also is a destructive omission of what the precondition above does specify. Yours (True) does not tell the client programmer the conditions that by DbC will guarantee Postcondition. Without hardware failure or other occurrences that cannot be expected to be handled by the Careful algorithm, Careful must produce Postcondition provided odd Index_80 numbers are passed for X. But in your version, (a) there is nothing the programmer knows about valid Index_80 values (viz. the odd ones) (b) there is no debugging hook that can be turned on or off (monitoring the precondition X rem 2 = 1). > other things you mentioned are control flow control statements. It is > really simply: an error/correctness check is a statement about the program > behavior. If-statement/exception etc is the program behavior. Normal If-statements and exceptions cannot be turned off. > Note > that your "DbC mindset" includes the programmer(s) into the system, > delivered and deployed. Isn't that indicatory? (:-)) The programmer is the one ingredient that matters most in DbC, since programming is a human activity, and contracts are between clients and suppliers of software components (classes). > And how do you rescue from: > > function "-" (X : Positive) return Positive; > > Note, if you handle an exception then it is same as if-statement. (I agree > that if-statements could be better arranged, have nicer syntax etc. Is that > the essence of Eiffel's DbC?) I'm assuming this is not an input-sanitizing function. You don't handle the exception as part of the algorithm: minus: INTEGER require Current > 1 do Current := Current - 1 end ensure Current + 1 = old Current Where Ada requires "ifs" for bounds checking and raising an exception accordingly, DbC/Eiffel requires that you express the correctness properties of subprograms *and* that you choose whether or not you want the "if", and which ones. >>>>>> 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? >>> >>> No, in Ada<constraint> is not required to be static. Example: >>> >>> procedure F (A : String) is >>> subtype Span is Integer range A'Range; >> >> Is the constraint, not to be static, then part of the contractual >> specification of subtype Even? > > The specification of includes all possible values of the constraint. When > you assign -1 to Positive, it is not an error, it is a valid, well-defined > program, which behavior is required to be Constraint_Error propagation. > When you assign -1.0 to Positive, it is an error and the program is > invalid. Where and how you are using these two mechanisms is up to you. A > FORTRAN program can be written in Ada, of course... > This specifies that assigning -1 to a positive will raise an exception. It does not specify the possible values for Even (which would be constrained to include only even numbers).
From: Robert A Duff on 14 May 2010 20:17 Georg Bauhaus <rm.dash-bauhaus(a)futureapps.de> writes: > How would you specify > > subtype Even is ...; ? In Ada 2012, if AI-153 gets approved, you will be able to say: subtype Even is Integer with Predicate => (Even mod 2) = 0; ^^^^ refers to the "current instance" of the subtype That particular example isn't very useful, but this kind of thing is: type Color is (Red, Orange, Yellow, Green, Blue); subtype Primary_Color is Color with Predicate => Primary_Color in (Red, Green, Blue); By the way, I don't think "static" is a property of assertions. It's a property of how they're checked. If we have a precondition that "X > Y" (where X and Y are formal parameters), that's neither "static" nor "dynamic" in and of itself. One tool (e.g. an Ada compiler) might check it dynamically. A smarter tool (a proof checker, or a smarter compiler, or even a human being) might check it statically. It might even be checked statically at some call sites, but not others. - Bob
From: Dmitry A. Kazakov on 15 May 2010 05:30
On Sat, 15 May 2010 01:45:50 +0200, Georg Bauhaus wrote: > On 5/13/10 10:39 AM, Dmitry A. Kazakov wrote: > >>> Ada seems better here. But before the arrival of preconditions >>> etc. Ada didn't have that much to offer to programmers wanting >>> to state sets of permissible values, for example for subprogram >>> parameters. >> >> Ada has strong types. "A set of permissible values" does not look like >> that. > > Ada's strong types are not really strong enough to express > a supplier library's ADT expectations in the sense of DbC. No type system can express the program semantics. Otherwise you would need not program any bodies, only declarations. > Again, can you produce a statically checked invariant for > subtype Even? Yes, I can: type Even is private; -- No literals visible function To_Integer (X : Even) return Integer; function To_Even (X : Integer) return Even; private type Even is new Integer; -- Use literals as follows: 1 means 2 function To_Integer (X : Even) return Integer is begin return Integer (X * 2); end To_Integer; function To_Even (X : Integer) return Even is begin if X mod 2 = 0 then return Even (X / 2); else raise Constraint_Error; end if; end To_Even; >>> package P is >>> >>> type Number is range 1 .. 10; >>> function Compute (A, B: Number) return Number >>> with Precondition => A>= B; >> >> I don't understand this notation. > > It says that the client of Compute would have to provide > A, B such that A >= B if client expects Compute to produce > its postcondition; otherwise, Compute should have the contract: if the sequence A,B is sorted then ... else Constraint_Error propagated. And of course, A, B is just an interval [B, A], and should be declared as such: function Compute (X : Interval) return Number with Precondition => True; > Yes. Only, a DbC system can be quite helpful in checking > my understanding of more formal "comments". You say that Eiffel DbC is about writing structured comments? I do not object. >> Note, since your "preconditions" are not static, >> how can you know *what* they say, in order to do as they do? > > I can write my client code such that the preconditions are > true. Really? What about: pre : not HALT(p) There is a reason why they aren't static. >>> IOW, no redundant checks. >> >> No, it would be *inconsistent* checks. No program can check itself. > > DbC checks are not part of the (intended) program. Monitoring can be > turned off and this should have no effect on program correctness. and thus on program execution. q.e.d. >> Trivially: >> >> function Careful (S: String_80; X: Index_80) >> with Precondition True; >> with Postcondition<whatever> or Constraint_Error > > This is legitimate I'd say, but is also is a destructive omission of > what the precondition above does specify. Yours (True) does not tell > the client programmer the conditions that by DbC will guarantee > Postcondition. Without hardware failure or other occurrences > that cannot be expected to be handled by the Careful algorithm, > Careful must produce Postcondition provided odd Index_80 numbers > are passed for X. But in your version, > > (a) there is nothing the programmer knows about valid Index_80 > values (viz. the odd ones) They are *all* valid, that is the contract of Careful. > (b) there is no debugging hook that can be turned on > or off (monitoring the precondition X rem 2 = 1). Debugging hooks do not belong to code. >> other things you mentioned are control flow control statements. It is >> really simply: an error/correctness check is a statement about the program >> behavior. If-statement/exception etc is the program behavior. > > Normal If-statements and exceptions cannot be turned off. Come on. C has preprocessor! >> Note >> that your "DbC mindset" includes the programmer(s) into the system, >> delivered and deployed. Isn't that indicatory? (:-)) > > The programmer is the one ingredient that matters most in DbC, > since programming is a human activity, and contracts are between > clients and suppliers of software components (classes). That is what your car manufacturer will tell you next time, when the brake system will accelerate instead of braking... >> And how do you rescue from: >> >> function "-" (X : Positive) return Positive; >> >> Note, if you handle an exception then it is same as if-statement. (I agree >> that if-statements could be better arranged, have nicer syntax etc. Is that >> the essence of Eiffel's DbC?) > > I'm assuming this is not an input-sanitizing function. It was unary minus. > Where Ada requires "ifs" for bounds checking and raising an > exception accordingly, DbC/Eiffel requires that you express the > correctness properties of subprograms *and* that you choose > whether or not you want the "if", and which ones. Bounds are one kind of constraints. Eiffel has more of those. Ada goes in the same direction as Robert's response shows. I don't like it for two reasons: 1. Dynamic checks. This was discussed. Correctness checks shall be static, else it is a part of the behavior to be contracted as any other. 2. It is weakly/un-typed. The constraints you impose on input and output are specifications of a [sub]type. 2.a. This type is anonymous 2.b. This type mutates (precondition /= postcondition) 2.c. This type is inferred and structurally equivalent To me this is a deep breach with the core of Ada type system. > This specifies that assigning -1 to a positive will raise an exception. > It does not specify the possible values for Even (which would be > constrained to include only even numbers). You have to define "possible value": 1. Member of the type domain set. (3 is a member of the Even as a subtype of Integer) 2. Value of an initialized instance (3 cannot be a value of any Even object) (Considering Even an Ada subtype or a type inheriting to integer.) -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de |