GNAT packages in Linux distributions
in [ADA]
|
From: Dmitry A. Kazakov on 15 May 2010 05:40 On Fri, 14 May 2010 20:17:30 -0400, Robert A Duff wrote: > 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. It becomes static or dynamic when you define of which language the formula "X > Y" is. If it is of the "language of Ada bodies," e.g. compiled into a run-time code, then it is dynamic. If it is of the "language of Ada specifications" (compiled into compiler messages), then it is static. Ada, at least in its earlier years, tried to segregate these. > One tool (e.g. an Ada compiler) might check it dynamically. That would be true C... -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de
From: Georg Bauhaus on 15 May 2010 14:39 On 5/15/10 11:30 AM, Dmitry A. Kazakov wrote: > No type system can express the program semantics. OK, lets keep this in mind. > 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; OK, I guess we'd have a To_Interval (A, B) function raising constraint_error in case the programmer improperly passes A < B. Which he has learned not to do from some comment that states contractual obligations of client wishing to call To_Interval? >>> 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) This is why I mentioned "not solve hard problems". I want to keep making sense in my preconditions/comments. > There is a reason why they aren't static. Practically, yes, there is a reason why normal programming cannot hope to rely on static analysis. >>>> 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. The programs (with or without monitoring) are not too different and hence will lead to a useful program construction process. (Better exceptions.) >> (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. I guess we disagree here: I think that a "programming into exceptions" style leads to the universally applicable precondition True, but otherwise keeps the programmer in the dark about how to not make a subprogram raise. OTOH, being more specific (trying to explain additional "constraints") seems helpful. Here I recall "No type system can express the program semantics." Until Ada has a type system that can express expectations better than predicates, I'll rather have stupid, weakly typed predicates, supported by tools, than nothing. loop begin P(X); exit; exception when constraint_error => X := find_another_x; end; end loop; >> (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. I guess my wording was too unspecific. Call it tracing automatism or whatever. > You have to define "possible value": In the sense of DbC: values that client can pass without violating the DbC contract.
From: Dmitry A. Kazakov on 15 May 2010 16:33 On Sat, 15 May 2010 20:39:46 +0200, Georg Bauhaus wrote: > On 5/15/10 11:30 AM, Dmitry A. Kazakov wrote: > >> 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; > > OK, I guess we'd have a To_Interval (A, B) function raising > constraint_error in case the programmer improperly passes A < B. > Which he has learned not to do from some comment that states > contractual obligations of client wishing to call To_Interval? He learned that from the semantics of intervals, when he uses intervals he supposed to know what they are. When you write a precondition you use some premises. Consider primitive operations of the type T. You cannot describe T in terms of T. I.e. + cannot refer to +. So interval must be known to the programmer. >> There is a reason why they aren't static. > > Practically, yes, there is a reason why normal programming > cannot hope to rely on static analysis. If it could, you would not need program anything. E.g. the result would be obtained statically. >>>>> 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. > > The programs (with or without monitoring) are not too different > and hence will lead to a useful program construction process. How do you measure the difference? >>> (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. > > I guess we disagree here: I think that a "programming into > exceptions" style leads to the universally applicable precondition > True, but otherwise keeps the programmer in the dark about > how to not make a subprogram raise. This is what programming in Ada all about. Since the rest of the language is by large safe, the main problem is debugging exceptions. I would like Ada having contracted exceptions rather than run-time assertions producing more exceptions than we already have. >>> (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. > > I guess my wording was too unspecific. Call it tracing > automatism or whatever. Nope, the key feature of tracing is that it does not change the program's behavior. Assertions with handled exceptions do change it. It is a very poor debugging tool. I would prefer a decent debugger to run-time assertions. Make it remember the break conditions between runs. That would be helpful and consistent. >> You have to define "possible value": > > In the sense of DbC: values that client can pass without > violating the DbC contract. And contract is of course a predicate of that set of values? Nice circular definitions. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de
From: Yannick Duchêne (Hibou57) on 25 May 2010 16:40 Le Mon, 10 May 2010 03:26:56 +0200, Ludovic Brenta <ludovic(a)ludovic-brenta.org> a écrit: > PS. If you are jobless, you might try working on known compiler bugs and > eventually join AdaCore :) But you aren't an AdaCore member yourself, aren't you ? So, with due respect, how can I believe this supposition ? -- There is even better than a pragma Assert: a SPARK --# check.
From: Yannick Duchêne (Hibou57) on 25 May 2010 16:45
Le Wed, 12 May 2010 19:24:11 +0200, Dmitry A. Kazakov <mailbox(a)dmitry-kazakov.de> a écrit: > 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. There is a major difference : Eiffel's pre/cond on methods are inherited by derived class. With C, or even with Ada' pragma Assert, this have to be done manually. Side note: I'm not talking about pre/cond in Ada 2012/2015, which will be closer to that of Eiffel. However, as SPARK already has this and do it better from my point of view (because of static checking and proofs), I am not waiting for Ada 2012/2015 for that. -- There is even better than a pragma Assert: a SPARK --# check. |