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.1 required=5.0 tests=BAYES_00, PP_MIME_FAKE_ASCII_TEXT autolearn=no autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!mx05.eternal-september.org!feeder.eternal-september.org!nntp-feed.chiark.greenend.org.uk!ewrotcd!reality.xs3.de!news.jacob-sparre.dk!loke.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail From: "Jacob Sparre Andersen news" Newsgroups: comp.lang.ada Subject: Re: SPARK Question Date: Tue, 7 May 2013 15:44:12 -0500 Organization: Jacob Sparre Andersen Research & Innovation Message-ID: References: <0efb385b-279a-49b7-8289-86b0e99e7930@googlegroups.com> <5188b317$0$6555$9b4e6d93@newsspool4.arcor-online.net> NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: loke.gir.dk 1367959453 17609 69.95.181.76 (7 May 2013 20:44:13 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Tue, 7 May 2013 20:44:13 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-RFC2646: Format=Flowed; Response X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157 Xref: news.eternal-september.org comp.lang.ada:15412 Date: 2013-05-07T15:44:12-05:00 List-Id: "Georg Bauhaus" wrote in message news:5188b317$0$6555$9b4e6d93@newsspool4.arcor-online.net... > On 07.05.13 08:59, Yannick Duchêne (Hibou57) wrote: >> Le Wed, 01 May 2013 15:35:20 +0200, Phil Thornley >> a écrit: >>> Assuming you are using the latest version of SPARK, the simplest way to >>> do this is to also include the proof function Vec_Length in the body, >>> and give it a return annotation. So in the spec put: >>> >>> --# function Vec_Length (The_Vector : in Basic_Vector) >>> --# return Positive; >>> >>> function Get_Value >>> (The_Vector : in Basic_Vector; >>> At_Position : in Positive) >>> return Basis_Type; >>> --# PRE At_Position in Array_Range'First .. Vec_Length(The_Vector); >>> >> >> That's exactly the kind of thing I miss with Ada 2012's Pre/Post: ability >> to define something for use in pre/post only, without injecting it in the >> real program. That's finally what the above do. >> > > In practical cases, contract-only predicates might well vanish > during optimization phases in compilers, I think, in case the > programmers decide that assertion checking can be turned off. I agree. Compilers do not include dead code in programs, regardless of why that code is dead. So there is little practical difference between having some sort of contract-only predicate functions and having them generally available. Moreover, I'm very skeptical that having contract-only functions is a good idea, especially for preconditions. For a precondition, the caller is supposed to ensure that the precondition is true before making the call. How can a programmer do this if the predicate is not available to them? For instance, it's common to have code like: if Is_Open (Log_File) then Put_Line (Log_File, ...); -- else don't log, file has failed for some reason. end if; where the precondition on Put_Line includes "Is_Open (File)". If the programmer can't write Is_Open in their code, they cannot avoid the failure nor program around it. All they can do is handle the exception, which is often the worst way to handle the situation. Similarly, postconditions often include conditions that hold true after the call, and it's quite common for those conditions to feed into following preconditions (as in Post => Is_Open(File) after a call to Open). So, as much as possible, postconditions should use the same functions that are used in preconditions. (The more that's done, the more likely that the compiler can completely eliminate the pre- and post- condition checks even when they're turned on.) Randy.