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: 103376,2e71cf22768a124d X-Google-Attributes: gid103376,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 From: dewar@cs.nyu.edu (Robert Dewar) Subject: Re: next "big" language?? (disagree) Date: 1996/06/12 Message-ID: #1/1 X-Deja-AN: 160275024 references: <4p1l65$35qi@info4.rus.uni-stuttgart.de> <4p60nk$imd@euas20.eua.ericsson.se> <4p8lmq$oq7@goanna.cs.rmit.edu.au> <4pj8p7$h9r@goanna.cs.rmit.EDU.AU> organization: Courant Institute of Mathematical Sciences newsgroups: comp.lang.pascal,comp.lang.c,comp.lang.misc,comp.lang.pl1,comp.lang.ada Date: 1996-06-12T00:00:00+00:00 List-Id: A. Grant said "The point of assertions is not to print messages for the programmer. You can use them to allow the compiler to optimise safely, provide a contractual interface between modules, and for preconditions, postconditions, loop invariants etc. when proving the correctness of programs." Actually that is a very controversial statement. What most people want is non-intrusive assertions that do NOT affect the generated code. That's not 100% possible, but it is something you can aim at. It is certainly true that assertions can be used for compiler optimization, but that's not what people want. When we discussed putting pragma Assert into the language (i.e. into the standard), it was this point that tripped us up, and resulted in it being left out. We could not figure out how to formally define the notion that the compiler should NOT be allowed to use the assertion for optimization purpoes. Other kinds of pragmas than Assert are what is appropriate for performing the kind of optimization related and contract and correctness related aspects (e.g. a pragma that says that a procedure is non-recursive).