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: 103376,2e71cf22768a124d
X-Google-Attributes: gid103376,public
From: Simon Read <s.read@cranfield.ac.uk>
Subject: Re: next "big" language?? (disagree)
Date: 1996/06/25
Message-ID: <4qom2s$9j7@yama.mcc.ac.uk>#1/1
X-Deja-AN: 162059279
references: <ag129.511.000A9CE9@ucs.cam.ac.uk> <dewar.834584250@schonberg>
      <JSA.96Jun15175541@organon.com> <4q707h$1r2@krusty.irvine.com>
 <JSA.96Jun19115535@organon.com> <dewar.835306677@schonberg>
 <DtIqn8.ADH@thomsoft.com>
content-type: text/plain; charset=us-ascii
organization: Serious Cybernetics Corporation
x-url: news:DtIqn8.ADH@thomsoft.com
mime-version: 1.0
newsgroups: comp.lang.ada
x-mailer: Mozilla 1.1N (X11; I; OSF1 V3.2 alpha)
Date: 1996-06-25T00:00:00+00:00
List-Id: <comp.lang.ada>


It's the difference between compiler directives and run-time code.
I'd have one construction for the compiler directive "Optimise if you
can using the following assumption" and one other construction
for the run-time code "Make sure the following is true; cause an
error signal if not."

in Robert Dewar's construction
    pragma Suppress(Assertion_Check);
    pragma Assert(...);

the "Suppress.." line modifies the run-time code.
The "Assert.." line is both run-time code AND compiler directive,
which is mixed, which is why I would not favour it.

Since most posters here seem to be using the word "check" or "checking"
as a verb to describe the run-time actions, why not use

    pragma Check (x)

as run-time code for "Check; Verify; ensure; cause error if wrong"

Also, assumptions don't hold for the entire program, or even in one
subroutine. Therefore:

   Begin assume (x)

     ...
     ...

   End assume (x)

should give the compiler plenty to think about.

These assumptions need not be nested tidily with loops and other
program control structures. They may overlap, but don't need to
nest entirely. These assumptions don't even need to nest with
other assumptions. They can overlap.
Since nesting is not obligatory, I think the assumptions
will probably need something like line labels to define start
and end points.

Simon