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: 1014db,9d58048b8113c00f X-Google-Attributes: gid1014db,public X-Google-Thread: 10cc59,9d58048b8113c00f X-Google-Attributes: gid10cc59,public X-Google-Thread: 101deb,b20bb06b63f6e65 X-Google-Attributes: gid101deb,public X-Google-Thread: 103376,2e71cf22768a124d X-Google-Attributes: gid103376,public From: dewar@cs.nyu.edu (Robert Dewar) Subject: Re: next "big" language?? (disagree) Date: 1996/06/26 Message-ID: #1/1 X-Deja-AN: 162414968 references: <4q707h$1r2@krusty.irvine.com> 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-26T00:00:00+00:00 List-Id: Brian says (regarding the possible interpretations of Assert): I'm not sure I see the complete distinction. Wouldn't it be possible for a compiler to eliminate any divide-by-zero check from the following code sequence: if not (X /= 0) then raise Assert_Error; end if; Q := 30 / X; The divide is unreachable when X = 0. Now this admittedly does cause a change in the generated code when an assertion is used. I'm trying to understand the "assertions should not affect things" camp. It's delicate, but let's extend the example: Q := 30 / X; assert X /= 0; Q := 30 / X; roughtly the three points of view are: 1. the assert has no effect on the code, so the semantics is exactly equivalent to what you would get by leaving out the assert, but the assert can be checked at run time. In this model it would be wrong for the compiler to leave out the second divide by zero check. Warning: this model is hard to define formally. 2. The assert is equivalent to an if. In this case the compiler can omit the second divide by zero check. This is what GNAT does, and is easy to define formally, since it is just an equivalent to the code that Brian quotes. 3. The assert does not correspond to executable code, but is an assertion that the compiler can use as an assumption in compiling code (in Ada terms you can almost think of this as saying that the semantics of the assert is that the execution is erroneous if the condition is false). In this interpretation the *first* of the divide by zero checks in the above example can be omitted. If this is not completely clear, that's not surprising, this is a messy area to be absolutely sure of what the other guy is talking about :-)