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=-0.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD, FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,78447032bdbeb343,start X-Google-Attributes: gid103376,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII Path: g2news1.google.com!postnews.google.com!b1g2000hsg.googlegroups.com!not-for-mail From: =?ISO-8859-1?Q?Santiago_Urue=F1a?= Newsgroups: comp.lang.ada Subject: Proposal: pragma Assumption Date: Sun, 25 May 2008 11:59:07 -0700 (PDT) Organization: http://groups.google.com Message-ID: <30917be5-1446-417c-8a4e-18b2f9a1f420@b1g2000hsg.googlegroups.com> NNTP-Posting-Host: 83.52.230.105 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: posting.google.com 1211741947 30738 127.0.0.1 (25 May 2008 18:59:07 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Sun, 25 May 2008 18:59:07 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: b1g2000hsg.googlegroups.com; posting-host=83.52.230.105; posting-account=Lcd2wAoAAAADW2SqWO5AWY55Q-jjpVWU User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/5.0 (X11; U; Linux i686; es-ES; rv:1.9b5) Gecko/2008050509 Firefox/3.0b5,gzip(gfe),gzip(gfe) Xref: g2news1.google.com comp.lang.ada:344 Date: 2008-05-25T11:59:07-07:00 List-Id: Hi everybody, I'm thinking in sending the following proposal to the ARG, but I'd like to present it here first to have more opinions about it usefulness, and probably to refine it a bit with your comments... It is based on a 2004 paper of Tony Hoare (from the book 'From Object- orientation To Formal Methods') where he describes different types of assertions used by (C/C++) developers in production code, including this one: SYMPLIFYING_ASSUMPTION (strlen(input) > MAX_PATH, "not yet checking for overflow"); 'SYMPLIFYING_ASSUMPTION' is a macro very similar to the C 'assert', also checking at run-time a boolean condition and aborting the program if it evaluates to false. But if an 'assert' is valid during the whole life of the application, the 'SYMPLIFYING_ASSUMPTION' is used by the programmer just *during the coding phase* to document those cases that aren't coded yet (probably edge cases). The difference is when compiling the program _not_ in debug mode (NDEBUG defined): the 'assert' macros are eliminated by the preprocessor whereas it is a compilation error if any 'SYMPLIFYING_ASSUMPTION' remains in the sources. That is, a SYMPLIFYING_ASSUMPTION is like those 'TODO:' or 'FIXME:' annotations used to remind the programmer what should be modified in the code, but it is recognized by the compiler instead of being just a comment, and therefore cannot be ignored by accident. So the proposal whould be adding to the next Ada revision two new pragmas: pragma Assumption ([Check =3D>] boolean_expression[, [Message =3D>] string_expression]); pragma Assumption_Policy (policy_identifier); -- Error, Check Which behave exactly like Assert and Assertion_Policy (also raising Assertion_Error, but with a different message), except that by default it is a compilation error to find any pragma Assumption in the sources unless when explicitly allowed using a compilation flag or the 'Check' policy. Probably better names can be chosen for those pragmas, so feel free to propose more adequate identifiers. Also, maybe in this case the Message string should be required, anyway it is a documentation pragma (in pragma Assert the second parameter is optional). IMHO this pragma is not a complete replacement for the TODO or FIXME comments, and in many cases it is better to code the whole functionality at once than just the more common cases. However, sometimes it will be a good approach to code just some cases documenting the assumptions, run the testsuite (raising an exception if any of those missing cases are triggered), and to code the rest in the future. But now, even if you forget to add that code, the compiler will remind you about those missing cases when trying to compile the final executable (following the "programmers make faults" Ada philosophy). Do you think it is an useful addition to Ada 2015? Would you use this feature? Do you know of any means to achieve the same effect in Ada 2005? Thanks Cheers, -- Santiago Urue=F1a-Pascual Technical University of Madrid (UPM)