Re: Assertions

Re: Assertions

[Marin David Condic]

J & A Richardson wrote:
> 
> I have looked through the RM and can not find any refference to
> assertions, pre conditions, or post conditions.
> 
> It was my understanding that Ada 95 used assertions.
> 
> I have also looked through a couple of webpages.
> 
> Does Ada 95 use exceptions to work as assertions?  Or am I missing
> something?
> 
That depends on exactly what will count as an "assertion". If parameters
to a procedure are of data types that have meaningful constraints
(ranges for which the subprogram is valid) then this counts as a kind of
primitive assertion. Violation of the assertion will raise an exception.

But I don't think that is what you mean. The sort of assertions that
would allow you to check for, say, relationships between parameters as
well as valid ranges, etc., are not a standard part of Ada. However, the
GNAT compiler for Ada95 has the pragma Assert which allows you to
include logical expressions which can be turned on and off with compiler
directives. This lets you accomplish the same thing as a direct language
feature in creating preconditions, postconditions, etc. I won't swear to
it, but I think the "pragma Assert" got enough attention that other
compiler vendors have implemented it as well, so it is becoming a common
- if not standard - feature of the language. I'd expect to see it in
some future revision of the ARM.

MDC
-- 
Marin David Condic
Real Time & Embedded Systems, Propulsion Systems Analysis
United Technologies, Pratt & Whitney, Large Military Engines
M/S 731-95, P.O.B. 109600, West Palm Beach, FL, 33410-9600
***To reply, remove "bogon" from the domain name.***

Visit my web page at: http://www.flipag.net/mcondic

Assertions

[J & A Richardson]

I have looked through the RM and can not find any refference to
assertions, pre conditions, or post conditions.

It was my understanding that Ada 95 used assertions.

I have also looked through a couple of webpages.

Does Ada 95 use exceptions to work as assertions?  Or am I missing
something?

Please help.


James

Re: Assertions

[Nick Roberts]

Well I've done a quick search on DN and nothing much came up (maybe it's too
far back).  I would be grateful if you would post a quick reprise of the
arguments.

-------------------------------------
Nick Roberts
-------------------------------------

Re: Assertions

[Robert Dewar]

In article <37383efd@eeyore.callnetuk.com>,
  "Nick Roberts" <nickroberts@callnetuk.com> wrote:
> Well I've done a quick search on DN and nothing much came up
> (maybe it's too far back).  I would be grateful if you would
> post a quick reprise of the arguments.

Here are some questions to answer:

1. Is an assertion a post condition that the compiler can
   rely on?

2. Can assertions have side effects

3. If assertions are off, are there still static semantic
   restrictions on assertions.

There are others, but this is enough :-)



--== Sent via Deja.com http://www.deja.com/ ==--
---Share what you know. Learn what you don't.---

Re: Assertions

[Robert Dewar]

In article <3736F549.E3DDCDEB@pwfl.com>,
  diespammer@pwfl.com wrote:
>but I think the "pragma Assert" got enough attention that other
> compiler vendors have implemented it as well, so it is
> becoming a common
> - if not standard - feature of the language. I'd expect to see
> it in some future revision of the ARM.

I would not! I do not see that the fundamental problems that
caused Assert not to make it into the Ada 95 RM have been
solved. For a discussion of these problems, consult the archives
(we have had that thread at least once, probably more than once
in recent memory).


--== Sent via Deja.com http://www.deja.com/ ==--
---Share what you know. Learn what you don't.---

Re: Assertions

[Dale Stanbrough]

Robert Dewar wrote:

"Here are some questions to answer:
 
 1. Is an assertion a post condition that the compiler can
    rely on?
 
 2. Can assertions have side effects
 
 3. If assertions are off, are there still static semantic
    restrictions on assertions."


One solution to the first questions (as suggested before) is to
have two types of assertions. One is the

   "please check this condition at run time and don't do
    any optimisations based on what you may be able to 
    deduce from this assert"


and the other is

   "I know this condition is true, please use it to the
    fullest to provide any further optimisations that you
    can".


The latter is of course used as a supplement to the type
system. I'm not sure which of these Eiffel supports, but 
probably Anna (the Ada83 annotation toolkit) would fall into
the 1st category.


I view Q2 as being very much like the question "should functions
have side effects". I would tend to say no for assertions, but
obviously this would be hard for a compiler to check (and of
course assertions have timing side effects, which could cause
problems in a time critical program).


Dale

Re: Assertions

[Robert Dewar]

In article <37397272.4B2FC372@praxis-cs.co.uk>,
  Peter Amey <pna@praxis-cs.co.uk> wrote:
> The SPARK Ada subset

Hmmm! I am very careful not to refer to SPARK as an Ada subset,
since really it is a language in its own right, and I thought
that was something Praxis liked to stress :-)

> has assertions in the form of pre/post conditions, loop
> invaraints etc. which are used to generate verification
> conditions (proof obligations) allowing partial
> correctness to be established.
> These are not checks which are monitiored at run time.

Indeed, this is yet a third view of assertions quite different
from the other two (run time checks, or assertions for the
compiler optimizer). I should have included this case in my
summary questions.

Assert is one of these things everyone thinks is

a) a good thing
b) straightforward

till you begin to discuss it, and realize that different
people have very different notions about what an assertion is!



--== Sent via Deja.com http://www.deja.com/ ==--
---Share what you know. Learn what you don't.---

Re: Assertions

[Tucker Taft]

Robert Dewar wrote:
> 
> In article <3736F549.E3DDCDEB@pwfl.com>,
>   diespammer@pwfl.com wrote:
> >but I think the "pragma Assert" got enough attention that other
> > compiler vendors have implemented it as well, so it is
> > becoming a common
> > - if not standard - feature of the language. I'd expect to see
> > it in some future revision of the ARM.
> 
> I would not! I do not see that the fundamental problems that
> caused Assert not to make it into the Ada 95 RM have been
> solved. For a discussion of these problems, consult the archives
> (we have had that thread at least once, probably more than once
> in recent memory).

Robert is right that there were long discussions on this,
but I think they could still be resolved.  Many of the
Ada 95 compilers have an informally agreed-upon way of
supporing pragma Assert already.  It is often tough
to formalize these informal agreements, but it can be
done, especially when you have existing implementations,
and motivation to allow "reasonable" uses of the feature
to be portable.  

In any case, here is a strawman:

   pragma Assert(boolean_expression [, string_expression]);

This pragma may appear anywhere a declaration or a statement may
occur.  If the check Assertion_Check is suppressed, this pragma
has no effect.  If the check Assertion_Check is not suppressed,
this pragma's elaboration/execution is equivalent to the
execution of:

   if boolean_expression then
        System.Assertions.Raise_Assert_Failure([""|string_expression]);
   end if;

Anyway, this is a strawman, and I presume it will live up
to its name. ;-)

-- 
-Tucker Taft   stt@averstar.com   http://www.averstar.com/~stt/
Technical Director, Distributed IT Solutions  (www.averstar.com/tools)
AverStar (formerly Intermetrics, Inc.)   Burlington, MA  USA

Re: Assertions

[Marin David Condic]

Tucker Taft wrote:
> 
> In any case, here is a strawman:
> 
>    pragma Assert(boolean_expression [, string_expression]);
> 
<snip for brevity>
> 
I can imagine that there are any number of issues which might make it
difficult to write a rigorous definition for the pragma. That said, I
still don't think this is sufficient reason to leave it out of a future
standard. If a large number of compilers are including the pragma
anyway, then inclusion in the standard will at least mean *some* level
of safety as to what the feature means/does.

(Wait a minute! That sounds suspiciously like the argument for
legalizing drugs: "Well kids are going to do it anyway, so at least this
way we can make sure they are getting 'healthy' drugs!" I'm not so sure
I like being on this side of the argument! :-)

Where there are going to be difficult issues, there are always the
weasel words "Implementation Defined". Side effects of the boolean
expression? Implementation Defined! At least you'll have common syntax
and chances are that whatever semantic differences exist in theory, in
practice they will likely be "corner cases" or simply uncommon. (I've
seen endless discussion of parameter passing rules, for example, yet
never once encountered a situation in real-world code where it caused a
problem. Either the code never got ported to a different compiler where
behavior was different or, if it did get ported, the code was structured
in such a way as to not rely on the obscure side-effects. Is the
expression "a tempest in a teapot" relevant here?)

Anyway - I think your definition is fine, as long as the appropriate
"Implementation Defined" weasel words are thrown in when the objections
come up.

MDC
-- 
Marin David Condic
Real Time & Embedded Systems, Propulsion Systems Analysis
United Technologies, Pratt & Whitney, Large Military Engines
M/S 731-95, P.O.B. 109600, West Palm Beach, FL, 33410-9600
***To reply, remove "bogon" from the domain name.***

Visit my web page at: http://www.flipag.net/mcondic

Re: Assertions

[Larry Kilgallen]

In article <3739CECA.6A49865B@averstar.com>, Tucker Taft <stt@averstar.com> writes:

> In any case, here is a strawman:
> 
>    pragma Assert(boolean_expression [, string_expression]);
> 
> This pragma may appear anywhere a declaration or a statement may
> occur.  If the check Assertion_Check is suppressed, this pragma
> has no effect.  If the check Assertion_Check is not suppressed,
> this pragma's elaboration/execution is equivalent to the
> execution of:
> 
>    if boolean_expression then
>         System.Assertions.Raise_Assert_Failure([""|string_expression]);
>    end if;

I would have expected:

    if NOT boolean_expression then

since I would expect to say:

    pragma Assert(Expression_I_Expect_To_Be_True);

Larry Kilgallen

Re: Assertions

[Tucker Taft]

Larry Kilgallen wrote:

> ...
> I would have expected:
> 
>     if NOT boolean_expression then

So would I ;-).  Well, as I said, it was a strawman...

> since I would expect to say:
> 
>     pragma Assert(Expression_I_Expect_To_Be_True);

Yes, definitely, make that "if NOT boolean_expression then ..."

> Larry Kilgallen

-- 
-Tucker Taft   stt@averstar.com   http://www.averstar.com/~stt/
Technical Director, Distributed IT Solutions  (www.averstar.com/tools)
AverStar (formerly Intermetrics, Inc.)   Burlington, MA  USA

Re: Assertions

[Robert Dewar]

In article <dale-1205990834030001@dale.bu.cs.rmit.edu.au>,
  dale@cs.rmit.edu.au (Dale Stanbrough) wrote:

Just to be clear, I answered the request for a summary of
issues, but I really feel any detailed discussion is too
much of a rerun, so I won't post any further to this thread.
I really did not want to start this thread up again :-)


--== Sent via Deja.com http://www.deja.com/ ==--
---Share what you know. Learn what you don't.---

Re: Assertions

[Peter Amey]

J & A Richardson wrote:
> 
> I have looked through the RM and can not find any refference to
> assertions, pre conditions, or post conditions.
> 
> It was my understanding that Ada 95 used assertions.
> 
> I have also looked through a couple of webpages.
> 
> Does Ada 95 use exceptions to work as assertions?  Or am I missing
> something?
> 

The SPARK Ada subset has assertions in the form of pre/post conditions,
loop invaraints etc. which are used to generate verification conditions
(prrof obligations) allowing partial correctness to be established. 
These are not checks which are monitiored at run time.

Peter
 

-- 
---------------------------------------------------------------------------   
      __         Peter Amey, Product Manager
        )                    Praxis Critical Systems Ltd
       /                     20, Manvers Street, Bath, BA1 1PX
      / 0        Tel: +44 (0)1225 466991
     (_/         Fax: +44 (0)1225 469006
                 http://www.praxis-cs.co.uk/

--------------------------------------------------------------------------

Re: Assertions

[Nick Roberts]

I would suggest that a pragma Assert expands to something like the
following:

   if not boolean_expression then
      Ada.Exceptions.Raise_Exception(
         Ada.Assertions.Assert_Failure'Identity,
         "Test expression evaluated to False in a pragma Assert." & NL &
         "Page: " & Page & "Line: " & Line & NL &
         "File: " & Source_File_Name & NL &
         [""|string_expression]);
    end if;

where NL is the implementation's code for a line break. Then there should be
a package:

package Ada.Assertions is

   Assert_Failure: exception [renames lower_level_exception];

end;

I think it's also got to be made explicit that if a pragma Assert in the
place of a declaration---in the declarative region of a certain
block---raises an exception, that exception must be immediately propagated
out of the block (and can never be handled inside the block). I would also
suggest the following points.

1. There's no reason why the compiler should not be able to assume that any
assertion's condition holds true, regardless of whether assertion checking
is turned on or off. This would obviously be highly desirable, since, in
many cases, it would allow optimising compilers to make optimisations they
otherwise could not. The situation is analogous to other checks: if a check
is turned off, and consequently an exception fails to be raised, the
program's behaviour is undefined, and possibly highly erratic; if
Assertion_Check is on (the default) the failure of an assertion's condition
will always raise an exception (so the condition will certainly always hold
as a post condition).

2. I don't see why assertions should not be allowed to have side-effects.
Whether it would be wise, in practice, for an assertion to have side effects
is another matter (to be left to the 'wisdom' of the programmer ;-).

3. If Assertion_Check is turned off, but the compiler can nevertheless
detect (at compile time) that an assertion's condition will always fail (be
False), it should still be entitled to raise an exception. Again, this is
analogous to the other checks. In theory, the compiler should be entitled to
continue checking any assertions it fancies.

4. A pragma Assert must not be evaluated by the elaboration of a
preelaborated library unit.

-------------------------------------
Nick Roberts
-------------------------------------

Re: Assertions

[Dale Stanbrough]

Nick Roberts wrote:

" 1. There's no reason why the compiler should not be able to assume that any
  assertion's condition holds true"


But of course there is the rub - I certainly don't want this to be true
-all the time-. 

I want some assertions to be genuinely tested, while others to be used
as an adjunct to the type system (and thus the compiler can use it for
optimisation purposes).

E.g. an assertion that a cached bill-of-materials total cost is indeed
the sum of all it's line items is something i want checked, whereas an
assertion that "this pointer is a linear pointer type" (i think that's
the notation that Henry Baker uses to describe linear dynamic data
structures) would be a useful way to give info to the compiler, but 
extremely expensive (if indeed possible) to test.


Dale

Re: Assertions

[Richard D Riehle]

In article <3739CECA.6A49865B@averstar.com>,
	Tucker Taft <stt@averstar.com> wrote:

>In any case, here is a strawman:
>
>   pragma Assert(boolean_expression [, string_expression]);
>

    In one of my JOOP columns I proposed going a little further,
    coming closer to the Eiffel model,

    pragma Pre_condition  (boolean_expression [ ... ]);
    pragma Post_condition (boolean_expression [ ... ]);
    pragma Invariant      (boolean_expression [ ... ]);

   with the further suggestion that we adopt Require, Ensure, and
   Invariant from the Eiffel language.

   One must be careful with assertions as pragmas.  It is quite 
   possible to declare a non-sensical assertion that is never 
   detected by the compiler.  When declaring assertions for a 
   derivation class, one can construct a boolean expression that
   holds for the root of the class but fails for some derived type.
   
   This is a fundamental problem with assertions.  The more conservative
   approach of Ada, in which every type is invariant tends to be more
   appropriate for safety-critical software.  If there were some way
   to formally prove, through a software routine, that an assertion 
   did not resolve to some completely silly set of propositions during
   the derivation process, we might be more inclined to depend on them.
   As things stand now, assertion pragmas, while a good idea on the 
   surface, could easily create more problems than they solve.

   I think we need to proceed with some caution in this area.  SPARK 
   does take a very conservative approach with assertions.  However, 
   SPARK does not support extensible derivation classes.  This eliminates
   one of the potential dangers of relying on assertions.  Am I being too
   cautious here?

   Richard Riehle
   richard@adaworks.com
   http://www.adaworks.com

Re: Assertions

[Nick Roberts]

Could you give, please, one or two further examples, in a little more
detail?  I (if no-one else!) would appreciate this.

-------------------------------------
Nick Roberts
-------------------------------------

Dale Stanbrough wrote in message ...
[...]
|I want some assertions to be genuinely tested, while others to be used
|as an adjunct to the type system (and thus the compiler can use it for
|optimisation purposes).
[...]

Re: Assertions

[Nick Roberts]

Richard D Riehle wrote in message <7hqe7m$q7i@sjx-ixn1.ix.netcom.com>...
[...]
|    pragma Pre_condition  (boolean_expression [ ... ]);
|    pragma Post_condition (boolean_expression [ ... ]);


What would these actually do that Assert would not?

|    pragma Invariant      (boolean_expression [ ... ]);


This construct (I think) could be replaced by an Assert repeated in several
places.  Would it be so useful as to be worthwhile?  (Perhaps it would.)

|   with the further suggestion that we adopt Require, Ensure, and
|   Invariant from the Eiffel language.


For those of us Eiffel non-cognoscienti, what do these do, please?

|   One must be careful with assertions as pragmas.  It is quite
|   possible to declare a non-sensical assertion that is never
|   detected by the compiler.  When declaring assertions for a
|   derivation class, one can construct a boolean expression that
|   holds for the root of the class but fails for some derived type.

'Twas ever thus.  In all cases, the programmer must be as careful to put
something sensible into an Assert as into the code proper.

Assertions are certainly no panacea: sometimes the code to check up on a
piece of code would be more complex to write than the code it's checking;
sometimes there is no practical way to check up on it at all; M****y's L*w
ensures that bugs can get into the checking code as easily as they can get
into the code proper (and be just as much of a S*****g B****r to root out
;-).

|   This is a fundamental problem with assertions.  The more conservative
|   approach of Ada, in which every type is invariant tends to be more
|   appropriate for safety-critical software.  If there were some way
|   to formally prove, through a software routine, that an assertion
|   did not resolve to some completely silly set of propositions during
|   the derivation process, we might be more inclined to depend on them.
|   As things stand now, assertion pragmas, while a good idea on the
|   surface, could easily create more problems than they solve.


I would be grateful if you would expand a little on this, perhaps giving an
example or two.

I apologise to those who don't wish to retread this well-trodden ground, but
there some of us who missed the boat first time around, and need to retread
it.

-------------------------------------
Nick Roberts
-------------------------------------

Re: Assertions

[Richard D Riehle]

In article <3742eba6@eeyore.callnetuk.com>,
	"Nick Roberts" <nickroberts@callnetuk.com> wrote:

>Richard D Riehle wrote in message <7hqe7m$q7i@sjx-ixn1.ix.netcom.com>...
>[...]
>|    pragma Pre_condition  (boolean_expression [ ... ]);
>|    pragma Post_condition (boolean_expression [ ... ]);
>|    pragma Invariant      (boolean_expression [ ... ]);

>What would these actually do that Assert would not?

 A pre-condition test (Eiffel Require assertion) guarantees
 that a subprogram will not be entered unless the assertion is
 satisfied.  It can, in some environments, be applied at the
 class/type level, but is more often at the subprogram level.
 An example of this assertion is the "barrier" on a protected
 entry.  The barrier is a lot like a pre-condition since it also
 evaluates a boolean expression before we can begin execution of
 the routine.  The barrier is not precisely identical to a pre-
 condition, but it should give you the general idea.

 A post-condition (Eiffel Ensure) guarantees that a certain set
 of circumstances will be true before exiting a subprogram.  If
 the post-condition fails, an exception may be raised.  

 An invariant is much as it might seem to be from its name.  During
 the life of the entity given an invariant condition, the invariant
 must be true.  

 The Require, Ensure, and Invariant conditions may be applied to 
 a subprogram, a type, or a even some variable.  The designer of
 Eiffel (who did not invent these ideas but incorporated them into
 the design of his language), calls this "design by contract."  It
 is important to understand that this is a run-time contract.  Many
 safety-critical software practitioners feel this is the wrong place
 to evaluate assertions.  The SPARK language takes a more conservative
 approach to the same idea.  Ada probably needs an approach somewhere
 between SPARK and Eiffel.    

>This construct (I think) could be replaced by an Assert repeated in several
>places.  Would it be so useful as to be worthwhile?  (Perhaps it would.)

 The Require, Ensure, and Invariant are part of the contract and would
 appear in the package specification (in Ada) not in the code.  The Ada
 package specification can already be thought of as some kind of contract.
 Because of that, reinforcing the contract with publicly defined assertions
 would make sense.  The public assertions should state explicitly the
 place where the assertion applies.  Therefore, pre-condition or post-
 condition would be a clear indication to the client of the contract.

 Assertions are independent of the implementing code.  In Ada this would
 make especially good sense because of the full separation between the
 definition of what to do (specification) and implementing code to do
 it (body).  We may want to modify the assertions without touching the
 algorithms.  In fact, we probably want the assertions to be independent
 of the algorithms.  Therefore, it makes sense to differentiate between
 assertions required to enter the routine, those require for successful
 completion, and those required to remain unchanged for the life of each
 entity in the design.

 I hope this helps to clarify the thinking behind some of my earlier 
 points. Let me be clear that I am not interested in turning Ada into
 Eiffel.  I am interested in seeing Ada learn from other language designs.
 I know that Tucker explored this idea in great depth during the design
 of Ada 95 and understands the pros and cons.  He did not lightly dismiss
 the notion of pre-, post, and invariant conditions.  It was a decision
 seriously studied and excluded from Ada 95 for very good reasons.

 Richard Riehle
 richard@adaworks.com
 http://www.adaworks.com

Re: Assertions

[stimuli]

In article <7hv6bb$1l9@dfw-ixnews6.ix.netcom.com>,
  Richard D Riehle <laoXhai@ix.netcom.com> wrote:

>  The Require, Ensure, and Invariant conditions may be applied to
>  a subprogram, a type, or a even some variable.  The designer of
>  Eiffel (who did not invent these ideas but incorporated them into
>  the design of his language), calls this "design by contract."  It
>  is important to understand that this is a run-time contract.  Many
>  safety-critical software practitioners feel this is the wrong place
>  to evaluate assertions.  The SPARK language takes a more conservative
>  approach to the same idea.  Ada probably needs an approach somewhere
>  between SPARK and Eiffel.

This isn't entirely true, although I think I understand your point.
The Eiffel contract is not a run-time concept, it is a static property
of correct Eiffel systems (read: correct Eiffel programs). How an
Eiffel compiler goes about testing these is implementation dependant.
In fact, they needn't actually be checked as they have null semantics
within a correct program. It would be correct Eiffel for a compiler
to check the validity of the assertions at compile time and a correct
Eiffel program needn't check them at all. Now, given that a general
theorem checker for Eiffel is, in practical terms, very unlikely,
most Eiffel implementations perform runtime checks of the assertions.
This is a useful tool for testing and debugging, but it is not the
greater part of what assertions are.

--
Jeffrey L. Straszheim
stimuli@my-dejanews.com


--== Sent via Deja.com http://www.deja.com/ ==--
---Share what you know. Learn what you don't.---

Re: Assertions

[stimuli]

In article <3742eba6@eeyore.callnetuk.com>,
  "Nick Roberts" <nickroberts@callnetuk.com> wrote:

<snip adhoc ada versions of require/assure/invariant>

> For those of us Eiffel non-cognoscienti, what do these do, please?

These are the three main types of Eiffel assertions. For details,
see:

 http://www.eiffel.com/doc/manuals/technology/contract/index.html

--
Jeffrey L. Straszheim
stimuli@my-dejanews.com


--== Sent via Deja.com http://www.deja.com/ ==--
---Share what you know. Learn what you don't.---

Re: Assertions

[Ehud Lamm]

On Wed, 19 May 1999, Richard D Riehle wrote:

> I hope this helps to clarify the thinking behind some of my earlier 
> points. Let me be clear that I am not interested in turning Ada into
> Eiffel.  I am interested in seeing Ada learn from other language designs.
> I know that Tucker explored this idea in great depth during the design
> of Ada 95 and understands the pros and cons.  He did not lightly dismiss
> the notion of pre-, post, and invariant conditions.  It was a decision
> seriously studied and excluded from Ada 95 for very good reasons.
> 

Are there any documents about this design issue? I am very much interested
in DBC ("design by contract"), which I think is one of the nicest ideas in
SE. So why did Ada95 dismiss it?

Ehud Lamm     mslamm@pluto.mscc.huji.ac.il

Re: Assertions

[Richard D Riehle]

In article <7i2015$jut$1@nnrp1.deja.com>,
	stimuli@my-dejanews.com wrote:

>In article <7hv6bb$1l9@dfw-ixnews6.ix.netcom.com>,
>  Richard D Riehle <laoXhai@ix.netcom.com> wrote:
>
>>  The Require, Ensure, and Invariant conditions may be applied to
>>  a subprogram, a type, or a even some variable.  The designer of
>>  Eiffel (who did not invent these ideas but incorporated them into
>>  the design of his language), calls this "design by contract."  It
>>  is important to understand that this is a run-time contract.  Many
>>  safety-critical software practitioners feel this is the wrong place
>>  to evaluate assertions.  The SPARK language takes a more conservative
>>  approach to the same idea.  Ada probably needs an approach somewhere
>>  between SPARK and Eiffel.
>
>This isn't entirely true, although I think I understand your point.
>The Eiffel contract is not a run-time concept, it is a static property
>of correct Eiffel systems (read: correct Eiffel programs). 

 I agree that it is possible that some assertions might be checkable
 at compile time.  Most pre-conditions and post-conditions I have seen
 have not looked like something that could be strictly checked by the
 compiler -- such things as ensuring that a variable never has a value
 of zero at run-time.

 On the other hand, I realize that the Eiffel contract does give the
 compiler the ability to do conformance checking through assertions
 and other mechanisms of the contract.  This is part of the power of
 Bertrand's fundamental idea of "design by contract."

> It would be correct Eiffel for a compiler
>to check the validity of the assertions at compile time and a correct
>Eiffel program needn't check them at all. 

 Understood.  We agree on this.  

>Now, given that a general
>theorem checker for Eiffel is, in practical terms, very unlikely,
>most Eiffel implementations perform runtime checks of the assertions.

 Yes, this is true.  Moreover, we have not yet reached the level of
 sophistication in software practice where we can apply foolproof
 theorem checkers on large-scale computer programs.  Even Ada does not
 lend itself to this kind of validity checking.

>This is a useful tool for testing and debugging, but it is not the
>greater part of what assertions are.

 My earlier point was that, Assertions, when focused on run-time
 checking, are not sufficient for safety-critical software development.
 That is why SPARK put emphasis on assertions that are always 
 evaluated at compile time.  Also, it is possible to formulate an
 assertion that is flawed.  Granted, most assertions are simple boolean
 expressions.  Consider, though a post-condition such as,

   Ensure count = old count + 1 and (P) or (Y and Z) or not P;

Someone will find fault with this construct, but I am not interested
in absolute correctness of logic at the moment. Most Eiffel developers are  
careful not to create potentially self-cancelling assertions.  There is
always someone who will not be so careful.  Also, I would not be surprised
to see an inherited post-condition in conflict with some new post-condition.
Granted, Eiffel has a nice set of features for avoiding this kind of thing,
but the discussion concerned implementing assertions in Ada via a pragma.
I think it will take a pragma to set the assertions, as suggested, but it
might require a pragma to _undefine_ such a pragma to prevent conflicts
within a derivation class.

The addition of a general assertion mechanism to Ada would please me
greatly.  I wonder if it is not more complicated than simply adding a
few new pragmas.  For example, will the assertion pragma on type T be
inherited by every derivation in T'Class?  This question alone should
spawn a whole set of associated questions.  In Eiffel this has been
thought through carefully.  Even so, I not absolutely certain, with my
limited knowledge of Eiffel, that one cannot create the kind of errors
in Eiffel I suggested in my earlier paragraph.  I think this one reason
the SPARK devotees are taking such a conservative approach to this
subject.  I am told this was a concern that prevented a generalized
assertion feature from becoming part of the Ada 95 standard.  Someone
may correct me on this, but I recall a discussion with one of the
distinguished reviewers during which I was told as much.

I suppose the person with the best perspective on this is Tucker. It
would be interesting to hear his view on the why's and wherefore's of
excluding pre-, post, and invariant assertions from the Ada 95 standard.

Richard Riehle
richard@adaworks.com
http://www.adaworks.com

Re: Assertions

[Ehud Lamm]

On Fri, 21 May 1999, Robert Dewar wrote:

> But to think that Ada dismissed DBC just because it did not
> adopt the particular partial assertion language facilities
> of Eiffel misses the point I think.
> 
> 
Sure.

But still two points.
1) I was responding to a claim that the issue of DBC was dicussed in the
Ada95 design process. I just wondered whether any documents from this
dicussion may be available.

2) I think having language support for DBC is a good thing. (I am not
advoacting Eiffel, just the general claim.) It is much cleaner, more
readable and most reliable to declare some set of assertions as being the
invariant of an ADt, than to explicitly code a check for them at the end
(etc.) of each routine that updates the ADT. Don't you agree?
Sure, language support is not essential for DBC. But I think it has many
advantages.

Ehud Lamm     mslamm@pluto.mscc.huji.ac.il

Re: Assertions

[Tucker Taft]

Ehud Lamm wrote:
> 
> On Fri, 21 May 1999, Robert Dewar wrote:
> 
> > But to think that Ada dismissed DBC just because it did not
> > adopt the particular partial assertion language facilities
> > of Eiffel misses the point I think.
> >
> >
> Sure.
> 
> But still two points.
> 1) I was responding to a claim that the issue of DBC was dicussed in the
> Ada95 design process. I just wondered whether any documents from this
> dicussion may be available.

We discussed associating assertions with types.  We didn't "dismiss"
them, but rather decided at the time they were too complex for the
perceived benefit.  We came quite close to standardizing on a
pragma Assert, and in fact most Ada 95 compilers have implemented
such a pragma.  Whether we can get it officially standardized over
the next few years, or just "de facto" standardized remains to be seen.

> 2) I think having language support for DBC is a good thing. (I am not
> advoacting Eiffel, just the general claim.) It is much cleaner, more
> readable and most reliable to declare some set of assertions as being the
> invariant of an ADt, than to explicitly code a check for them at the end
> (etc.) of each routine that updates the ADT. Don't you agree?
> Sure, language support is not essential for DBC. But I think it has many
> advantages.

Bertrand Meyer has a very specific definition of design by contract
which he associates closely with the Eiffel assertions/invariants.

Ada certainly has linguistic support for design by contract in 
general, though not in the same way as Eiffel.  In particular, every
subtype constraint in Ada is a contract that is enforced at run-time.
In addition, the fact that Ada physically separates spec from body,
and visible part from private part, creates a number of very well-defined
and configuration-manageable "contracts" that are compiler enforced.
Personally, I find one of the greatest weaknesses of Eiffel (and Java) is
that classes do not provide this physical separation into spec and body.
The notion that you "extract" the spec from a class is counter to the
idea that you have a well-defined contract.  The contract is much stronger
if it is physically separate from the implementation.  In a business
contract, I would never allow the supplier to be the "keeper" of the
contract, where I would have to ask the supplier to "extract" the
contract from the current implementation.

None of the above is meant to say I don't see the value in assertions
and invariants.  However, I think in practice, the support that Ada
already has for contracts is in many ways more valuable on a "day-to-day"
basis, because the range constraints (and other constraints) are ubiquitous
in a typical Ada program, providing contract enforcement on a line-by-line
basis and at every subprogram call, and the physical separation of
spec and body is valuable in every package. I would certainly 
not want to trade Ada's existing support for "contracts" for just 
having the explicit assertions provided by Eiffel.  
I would want both.  The pragma Assert generally available
in Ada compilers already provides a good portion of the power of
explicit assertions and invariants. 

> Ehud Lamm     mslamm@pluto.mscc.huji.ac.il

-- 
-Tucker Taft   stt@averstar.com   http://www.averstar.com/~stt/
Technical Director, Distributed IT Solutions  (www.averstar.com/tools)
AverStar (formerly Intermetrics, Inc.)   Burlington, MA  USA

Re: Assertions

[Robert Dewar]

In article <7i27tt$hn@dfw-ixnews11.ix.netcom.com>,
  Richard D Riehle <laoXhai@ix.netcom.com> wrote:
> I agree that it is possible that some assertions might be
> checkable at compile time.

That misses the point, Eiffel assertions are not about
checking (either at compile time or at run time). They
are formalized comments stating certain static properties
of the program. If one of these comments lies, this is a bug
in the program.

One of course wants to debug programs, so mechanisms like
testing assertions at run time etc are useful for debugging
the assertions (as well as the rest of the code).

But you really have to get out of the habit of thinking of
them as having much to do with the check-this-assertion-at
run-time type gizmo which is what most of this thread has
been discussing.

As I said earlier, assertions mean many different things to
different people :-)


--== Sent via Deja.com http://www.deja.com/ ==--
---Share what you know. Learn what you don't.---

Re: Assertions

[Robert Dewar]

In article
<Pine.A41.3.96-heb-2.07.990520114314.161678A-100000@pluto.mscc.h
uji.ac.il>,
  Ehud Lamm <mslamm@mscc.huji.ac.il> wrote:
> Are there any documents about this design issue? I am very
> much interested in DBC ("design by contract"), which I think
> is one of the nicest ideas in
> SE. So why did Ada95 dismiss it?

DBC is a methodology, which of course you can adopt in any
language, and indeed Ada is quite well suited for this purpose.
The issue of whether specific language features should be
designed into the language to support DBC is a different
one. It is of COURSE not the case that all elements of a
DBC approach can be captured by Eiffel assert statements
(as soon as you constrain the syntax and semantics of such
assertions, you limit their applicability).

Obviously some level of support for design contracts seems
like a good idea. FOr example, an Ada package spec is exactly
an interface contract.

Are assertions a la Eiffel the right form?
Not clear the answer is yes.
There are MANY other similar constructions and a lot of
 design room here.

But to think that Ada dismissed DBC just because it did not
adopt the particular partial assertion language facilities
of Eiffel misses the point I think.


--== Sent via Deja.com http://www.deja.com/ ==--
---Share what you know. Learn what you don't.---

Re: Assertions

[Dale Stanbrough]

Nick Roberts wrote:

" Could you give, please, one or two further examples, in a little more
  detail?  I (if no-one else!) would appreciate this."

in response to my statement...

  |I want some assertions to be genuinely tested, while others to be used
  |as an adjunct to the type system (and thus the compiler can use it for
  |optimisation purposes).


For an assertion that I would like tested...


   procedure Insert (Root : in out Tree; Item : Element) is
   --  insert into a binary search tree
   begin
      -- insertion code.
      ...

      pragma Assert (Balanced (Root));
          -- test this, die if it fails

   end Insert;


This assertion would cause an exception if the assertion failed 
(i.e. the semantics that Tucker Taft recently described). The
compiler would not take advantage of this assertion to make any
optimisations.


For an assertion that could be used by the compiler to optimise
the code


   pragma Enforce (X in 1..9 or X in 20..29);

   case X is
      when  1..10 => Something;
      when 20..29 => Something_Else;
      when others => Put_Line ("Whoops!");
   end case;


In this example, the compiler could remove the others clause.
The "Enforce" (I don't think this is a good name, but I can't
think of anything better) is used to extend the type system.

One problem with the name "Assert" is that people have 
different views about what it actually means. Robert Dewar
considers that "Assert" _should_ be able to be used for
optimisation purposes.


Dale

Re: Assertions

[Robert Dewar]

In article <dale-2205990829190001@r1021c-20.ppp.cs.rmit.edu.au>,
  dale@cs.rmit.edu.au (Dale Stanbrough) wrote:
> Nick Roberts wrote:
> One problem with the name "Assert" is that people have
> different views about what it actually means. Robert Dewar
> considers that "Assert" _should_ be able to be used for
> optimisation purposes.

No! Not at all! I said nothing of the kind, go back and check
my posts. I merely pointed out that there were many possible
interpretations of Assert, and mentioned that this was an
issue. I have been VERY careful in this thread not to express
opinions, other than that it is not clear what Assert should
do!

Robert Dewar

P.S. in fact I don't think it is easy, or even possible, to
specify precisely what this means ("use for optimization
purposes"), so someone would have to define it for me, before
I could tell you whether it made sense to me or not!


--== Sent via Deja.com http://www.deja.com/ ==--
---Share what you know. Learn what you don't.---

Re: Assertions

[Ray Blaak]

I would suggest the name "Verify" for assertions intended to be runtime
checks, and "Assume" for assertions intended to give info to the compiler.

dale@cs.rmit.edu.au (Dale Stanbrough) writes:
> For an assertion that I would like tested...
[...]
>       pragma Assert (Balanced (Root));
>           -- test this, die if it fails
[...]
> For an assertion that could be used by the compiler to optimise
> the code
>    pragma Enforce (X in 1..9 or X in 20..29);
[...]
> The "Enforce" (I don't think this is a good name, but I can't
> think of anything better) is used to extend the type system.
> 
> One problem with the name "Assert" is that people have 
> different views about what it actually means. Robert Dewar
> considers that "Assert" _should_ be able to be used for
> optimisation purposes.

-- 
Cheers,                                        The Rhythm is around me,
                                               The Rhythm has control.
Ray Blaak                                      The Rhythm is inside me,
blaak@infomatch.com                            The Rhythm has my soul.

Re: Assertions

[Robert Dewar]

In article <ur9o9f95c.fsf@infomatch.com>,
  Ray Blaak <blaak@infomatch.com> wrote:
>
> I would suggest the name "Verify" for assertions intended to
> be runtime checks, and "Assume" for assertions intended to
> give info to the compiler.

In any case, this thread should have adequately demonstrated
that

(a) this is quite a tricky subject
(b) it is not easy to propose a solution that gets any kind of
    consensus agreement.

This has always been the case when this issue has been
discussed, so it is hardly surprising to see it happening again
:-)



--== Sent via Deja.com http://www.deja.com/ ==--
---Share what you know. Learn what you don't.---

Re: Assertions

[Nick Roberts]

Dale Stanbrough wrote ...
[...]
|For an assertion that I would like tested...
|
|   procedure Insert (Root : in out Tree; Item : Element) is
|   --  insert into a binary search tree
|   begin
|      -- insertion code.
|      ...
|
|      pragma Assert (Balanced (Root));
|          -- test this, die if it fails
|
|   end Insert;
|
|This assertion would cause an exception if the assertion failed
|(i.e. the semantics that Tucker Taft recently described). The
|compiler would not take advantage of this assertion to make any
|optimisations.


Supposing we had, at some other point in your code:

   Order_Pudding(Cherry_Pie);
   Insert(Cocktail,Umbrella);
   if not Balanced(Cocktail) then
      Have_Another(Cherry_Pie);
   end if;

[I'm also going to assume the program has no tasks (other than the main
task), and no volatile objects.]

The compiler could decide, at compile time, to forego the second serving of
pudding at this point.  It would still have to call Balanced; but only once,
as part of the assertion inside the body of Insert.

Of course, if suppression of assertions is allowed inside the body of
Insert, AND the compiler decides to comply with this suppression, then the
condition in the if...then here would have to be tested (and two cherry pies
are a theoretical possibility).  [Assuming the waiter is never clumsy (and
always balances the cocktail after inserting an umbrella into it), the
second pie will never happen, in practice, but the compiler probably can't
know this.]

I do not see how this kind of optimisation---based on an assertion---could
ever be a problem.  (Am I wrong?)

-------------------------------------
Nick Roberts
-------------------------------------

PS: I would like to take the opportunity here to thank the people who
responded to my questions in this thread.  I have found the discussion
illuminating and stimulating.

Re: Assertions

[Nick Roberts]

Robert Dewar wrote in message <7i7ei9$93v$1@nnrp1.deja.com>...
|In article <ur9o9f95c.fsf@infomatch.com>,
|  Ray Blaak <blaak@infomatch.com> wrote:
|>
|> I would suggest the name "Verify" for assertions intended to
|> be runtime checks, and "Assume" for assertions intended to
|> give info to the compiler.
|
|In any case, this thread should have adequately demonstrated
|that
|
|(a) this is quite a tricky subject
|(b) it is not easy to propose a solution that gets any kind of
|    consensus agreement.
|
|This has always been the case when this issue has been
|discussed, so it is hardly surprising to see it happening again
|:-)


Robert is absolutely right on both points, of course.  However, I don't
actually recall anybody actually suggesting anything to the contrary.  I,
for one, never expected otherwise.

Of course it's a tricky subject!  Of course consensus is not going to be
handed to us on a plate!  However, I would suggest that we can,
nevertheless, attempt to negotiate this tricky subject, and to persue a
sufficient consensus.  If people hadn't taken this attitude towards almost
all aspects of the development of the Ada standard, there would never have
been an Ada language at all.

At this point, I think I can suggest five possible pragmas as candidates for
a future revision of the Ada standard (and perhaps for prior de facto
adoption):

============================================================

   pragma Assume (Condition);
   pragma Verify (Condition);

The Assume and Verify pragmas are allowed anywhere a declaration or a
statement is allowed.  When the pragma would be elaborated, if it were a
declaration, or executed, if it were a statement, the pragma is said to be
executed.

For execution of the  Assume pragma, the compiler is allowed, but not
required, to test the Condition, but in either case is allowed to assume
that the Condition is true for the purposes of optimisation.

For execution of the  Verify pragma, the compiler is required, unless
suppression of Verify_Check applies, to test the Condition is true. If the
suppression of Verify_Check applies, the compiler is allowed, but not
required, to omit this test.  In any case, the compiler is allowed to assume
that the Condition is true for the purposes of optimisation.

   pragma Verify_Before_Call (Subprogram,Condition);
   pragma Verify_Before_Return (Subprogram,Condition);

These two pragmas are allowed anywhere a declaration is allowed in the
public part of a package specification.  The Subprogram must be the name of
a subprogram declared before the pragma in the same specification.  The
condition may contain the names of any of the parameters of the subprogram,
as well as any entity that would normally be visible at the point of the
pragma (but not any entity in the body of the subprogram).  The
Verify_Before_Call pragma causes the execution, with the same Condition, of
an implicit Verify pragma just before the first declaration, or, if the
subprogram has no declarations, as the only declaration, of the subprogram.
The Verify_Before_Return pragma causes the execution, with the same
Condition, of an implicit Verify pragma just after the evaluation of the
return expression of a return statement in the subprogram, or just before
the execution of a return statement in the subprogram which has no return
expression.  For both these pragmas, the meanings of the names in the
Condition shall be interpreted at the place of the pragmas (not at the
places of their implicit execution).

For all four of these pragmas, if the test of the Condition is actually
done, and it fails (evaluates to False), the predefined exception
Program_Error is raised.  (If this exception is raised by a pragma which
takes the place of a declaration, the exception is immediately propagated
out the innermost enclosing block, and is never handled by an exception
handler inside this block.)

[There is a new check for the Suppress pragma, Verify_Check.]

   pragma Parallel_Loop [(Loop_Name)];

This pragma is allowed anywhere a statement is allowed, but must apply to
loop.  With no parameter, this pragma applies to the innermost enclosing
loop statement; otherwise this pragma applies to loop whose name is
Loop_Name.  The loop must have an iteration scheme of the 'for' variety, and
this iteration scheme must not include the reserved word 'reverse'.

The pragma Parallel_Loop allows the compiler to assume, for the purposes of
optimisation, that the loop it applies to has the following property:
execution of the iterations of the loop may be arbitrarily overlapping, and
in any order, without changing the effect of the loop.  The compiler is
allowed, but not required, to test that the loop actually has this property;
if such a test is done, and fails, the predefined exception Program_Error is
raised.

============================================================

It may well be better to use 'Assert' throughout rather than 'Verify'.
Comments please.

Does this count as a stoneman? :-)  I hope no-one objects to my throwing in
the last pragma, but it seemed reasonably appropriate.  Sorry, I must go
now, my mum is expecting her cup of tea ;-)

-------------------------------------
Nick Roberts
-------------------------------------

Re: Assertions

[Ray Blaak]

"Nick Roberts" <nickroberts@callnetuk.com> writes:
>    pragma Assume (Condition);
>    pragma Verify (Condition);

I would also allow optional description strings that would be part of the
raised exception, accessible via Ada.Exceptions. Most importantly, the strings
would be evaluated only if Condition is False:

    pragma Assume (Condition [, description]);
    pragma Verify (Condition [, description]);

This would eliminate once and for all code like:

  if Debug and not Condition then
    Verify (False, "complicated string that should be evaluated only "
                   & "when necessary: " & DescriptionOf (currentObject));
  end if;

> For all four of these pragmas, if the test of the Condition is actually
> done, and it fails (evaluates to False), the predefined exception
> Program_Error is raised.  (If this exception is raised by a pragma which
> takes the place of a declaration, the exception is immediately propagated
> out the innermost enclosing block, and is never handled by an exception
> handler inside this block.)

I would suggest another exception name, so that one can distinguish the fact
that a programmer-defined check failed, as opposed to a mistake in
general. Maybe: Assertion_Error, or both Verification_Error and
Assumption_Error.

> It may well be better to use 'Assert' throughout rather than 'Verify'.
> Comments please.

Well, "Assert" gives rise to discussions as to what it really means,
especially in comp.lang.ada :-). The idea is to side-step the issue by letting
the programmer decide which type of assertion is desired. Whatever names are
chosen should clearly reflect the intention.

-- 
Cheers,                                        The Rhythm is around me,
                                               The Rhythm has control.
Ray Blaak                                      The Rhythm is inside me,
blaak@infomatch.com                            The Rhythm has my soul.

Re: Assertions

[Dale Stanbrough]

Nick Roberts wrote:

"    pragma Parallel_Loop [(Loop_Name)];
  
  This pragma is allowed anywhere a statement is allowed, but must apply to
  loop.  With no parameter, this pragma applies to the innermost enclosing
  loop statement; otherwise this pragma applies to loop whose name is
  Loop_Name.  The loop must have an iteration scheme of the 'for' variety, and
  this iteration scheme must not include the reserved word 'reverse'."


This sounds good, but i really know next to nothing about this area.

I would certainly recommend anyone to read up on HPF (High Performance
Fortran) to get an idea on the issues that have been examined on this
topic.

I -think- from previous postings that there are some features in Ada
that may prevent the level of parallelisation (sp?) that Fortran can
achieve (specifically exceptions (and probably finalisation and Async
abort)).


Dale