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.3 required=5.0 tests=BAYES_00,INVALID_MSGID autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: f891f,9d58048b8113c00f X-Google-Attributes: gidf891f,public X-Google-Thread: 101deb,b20bb06b63f6e65 X-Google-Attributes: gid101deb,public X-Google-Thread: 10cc59,9d58048b8113c00f X-Google-Attributes: gid10cc59,public X-Google-Thread: 1014db,9d58048b8113c00f X-Google-Attributes: gid1014db,public X-Google-Thread: 103376,2e71cf22768a124d X-Google-Attributes: gid103376,public From: ag129@ucs.cam.ac.uk (A. Grant) Subject: Re: next "big" language?? (disagree) Date: 1996/06/26 Message-ID: #1/1 X-Deja-AN: 162256036 references: organization: University of Cambridge newsgroups: comp.lang.pascal,comp.lang.c,comp.lang.misc,comp.lang.pl1,comp.lang.ada Date: 1996-06-26T00:00:00+00:00 List-Id: In article djohnson@tartarus.ucsd.edu (Darin Johnson) writes: >How about "Assert"!!! That's exactly what this means in English, >despite the fact that Ada changed its meaning. "Assert" and >"assertion" in English in no way mean "check that this is true". If someone says something is true, don't you check it? There are all sorts of implicit assertions made by programmers which the compiler doesn't have to believe. F(A,B(5),C/D) implicitly asserts that F takes three parameters, that 5 is not out of bounds for B, and that D is non-zero. It is necessary for correct execution of the program (assuming we aren't relying on trapping exceptions for the moment) that these be correct, so if they can't be checked statically they should be checked dynamically. Explicit assertions are just a way of doing the same for more complicated algorithms where the compiler is unable to determine for itself that some condition must be met for an algorithm to function correctly, or is unable to propagate implicit assertions backwards far enough to make the test as efficient as it could be. The only situation where an assertion test is unnecessary is when an assertion is guaranteed to be true by a proof that is too complex for the program. For example FUNCTION EXP(X) ... some polynomial ... EXP = ... RETURN where you may want to assert in the published interface to EXP that its result is positive. I would suggest that any language environment which supports this kind of unproved assertion must have linguistic support (i.e. not just a comment) for reference to an external proof, e.g. a full record of the developer who made the assertion and any references they supply. Again this is just like real life - if you can't see the truth of someone's assertion, you have to see their evidence, and if you don't understand it, but it is from a reputable source, you remember what it is in case you act on the assertion and get challenged. Or you at least get enough paperwork so that if the assertion turns out to be wrong and your rocket explodes, they get sued, not you.