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: 10cc59,9d58048b8113c00f X-Google-Attributes: gid10cc59,public X-Google-Thread: 1014db,9d58048b8113c00f X-Google-Attributes: gid1014db,public X-Google-Thread: 101deb,b20bb06b63f6e65 X-Google-Attributes: gid101deb,public From: ag129@ucs.cam.ac.uk (A. Grant) Subject: Re: next "big" language?? (disagree) Date: 1996/06/17 Message-ID: #1/1 X-Deja-AN: 160649174 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: University of Cambridge newsgroups: comp.lang.pascal,comp.lang.c,comp.lang.misc,comp.lang.pl1,comp.lang.ada Date: 1996-06-17T00:00:00+00:00 List-Id: In article dewar@cs.nyu.edu (Robert Dewar) writes: >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..." >It is certainly true that assertions can be used for compiler optimization, >but that's not what people want. What people want is for the compiler to do all the work, i.e. prove that all array subscripts are valid, that all dereferenced pointers are non-null, that all division denominators are non-zero etc. I think realistically, compilers can be helped by assertions which indicate stages in the proof, to do optimisations which they wouldn't otherwise be able to. Especially inter-procedural or inter-module optimisation where the assertion forms part of the interface. >When we discussed putting pragma Assert into the language Are you reading this in comp.lang.ada? I didn't mean to refer to any particular language. Why don't you like assertions enabling optimisation where the compiler can prove the correctness of the assertion, i.e. optimise it away? Then all you are doing is giving a hint to the compiler about an optimisation strategy, without altering the meaning of the program at all.