From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: a07f3367d7,23c0de5a42cf667e X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news2.google.com!news3.google.com!feeder3.cambriumusenet.nl!feed.tweaknews.nl!193.201.147.68.MISMATCH!feeder.news-service.com!newsfeed.straub-nv.de!news2.arglkargh.de!news.n-ix.net!news.belwue.de!newsfeed.arcor.de!newsspool3.arcor-online.net!news.arcor.de.POSTED!not-for-mail Date: Sat, 15 May 2010 01:45:50 +0200 From: Georg Bauhaus User-Agent: Mozilla/5.0 (Macintosh; U; Intel Mac OS X 10.5; en-US; rv:1.9.1.10) Gecko/20100512 Thunderbird/3.0.5 MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: GNAT packages in Linux distributions References: <87mxw9x7no.fsf@ludovic-brenta.org> <16bz9kvbqa8y9$.155ntpwpwl29d.dlg@40tude.net> <4be97bea$0$2966$ba4acef3@reader.news.orange.fr> <1p87qdlnjbufg.127laayhrw9x3$.dlg@40tude.net> <4j73xhgimt6r$.pu55kne2p2w5$.dlg@40tude.net> <4beaeeed$0$6888$9b4e6d93@newsspool2.arcor-online.net> <1c8dan2pi7bm9.1os0h56b9fukv$.dlg@40tude.net> <4beaf93a$0$6875$9b4e6d93@newsspool2.arcor-online.net> <1u6ficvfjfreg$.16cmwyau8jkd9.dlg@40tude.net> <4beb5dfa$0$6883$9b4e6d93@newsspool2.arcor-online.net> <1qvxyz4nolwsi.1fth5xpxi2m3t.dlg@40tude.net> In-Reply-To: <1qvxyz4nolwsi.1fth5xpxi2m3t.dlg@40tude.net> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Message-ID: <4bede0af$0$6883$9b4e6d93@newsspool2.arcor-online.net> Organization: Arcor NNTP-Posting-Date: 15 May 2010 01:45:51 CEST NNTP-Posting-Host: be95e591.newsspool2.arcor-online.net X-Trace: DXC=3M@:_GI8SGd^Y=RbYBPl4`A9EHlD;3Ycb4Fo<]lROoRa8kFejVhOTITCmQ]`KfB55Ckmg:Qgk X-Complaints-To: usenet-abuse@arcor.de Xref: g2news2.google.com comp.lang.ada:11624 Date: 2010-05-15T01:45:51+02:00 List-Id: 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 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 is ; >>>> >>>> What will static and static be for subtype Even? >>> >>> No, in Ada 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).