Version 1.2 of ai05s/ai05-0274-1.txt

From: Erhard Ploedereder
Sent: Friday, November 11, 2011  5:49 PM

In 6.1.1 insert before 36/3:

It is a bounded error in a pre- or postcondition to invoke a subprogram that
alters the value of any variable *that is not locally declared in the
subprogram*. If the bounded error is detected, Program_Error is raised. If not
detected, execution proceeds normally, but values denoted by X'Old for any
prefix X may no longer denote the value denoted by X at the beginning of the
subprogram with the affected pre- or postcondition.

A better text for *...* would be *whose lifetime exceeds the duration of the
subprogram call", but I am not sure that the terminology is set up.

------------------
and in case this fails, and Steve deletes the first sentence of the definition
of 'Old, add a Note

If subprograms with side-effects are called inside pre- or postconditions, the
expectation that X'Old denotes the value of X at the beginning of the subprogram
is no longer justified.

and if Steve does not delete the first sentence:

If subprograms with side-effects are called inside pre- or postconditions, the
guarantee that X'Old denotes the value of X at the beginning of the subprogram
is voided.

****************************************************************

From: Robert Dewar
Sent: Friday, November 11, 2011  6:37 PM

> It is a bounded error in a pre- or postcondition to invoke a
> subprogram that alters the value of any variable *that is not locally
> declared in the subprogram*. If the bounded error is detected,
> Program_Error is raised. If not detected, execution proceeds normally,
> but values denoted by X'Old for any prefix X may no longer denote the
> value denoted by X at the beginning of the subprogram with the affected pre-
> or postcondition.

I don't like this being a bounded error, it forbids the use of memo functions in
pre and post conditions and that seems silly. Let's not go out of our way to
save people from themselves at the expense of hampering others!

****************************************************************

From: Erhard Ploedereder
Sent: Friday, November 11, 2011  6:55 PM

In 6.1.1 insert before 36/3:

It is a bounded error in a precondition to invoke a subprogram that alters the
value of any variable *that is not locally declared in the subprogram* so that
the value of the postcondition expression is affected. If the bounded error is
detected, Program_Error is raised. If the bounded error is not detected, values
denoted by X'Old for any prefix X might no longer denote the value denoted by X
at the beginning of the subprogram call with the affected postcondition.

****************************************************************

From: Erhard Ploedereder
Sent: Friday, November 11, 2011  7:12 PM

In 6.1.1 insert before 36/3:

It is a bounded error in a pre- or postcondition to invoke a subprogram that
alters the value of any variable *that is not locally declared in the
subprogram* so that the value of the postcondition expression is affected by the
altered variable. If the bounded error is detected, Program_Error is raised. If
the bounded error is not detected, values denoted by X'Old for any prefix X
might no longer denote the value denoted by X at the beginning of the subprogram
call with the affected postcondition.

****************************************************************

From: Erhard Ploedereder
Sent: Friday, November 11, 2011  7:32 PM

In 6.1.1 insert before 36/3:

It is a bounded error in a pre- or postcondition of subprogram S to invoke a
subprogram that alters the value of any variable *that is not locally declared
in the subprogram* and whose value affects the value of any pre- or
postcondition expression of subprogram S. If the bounded error is detected,
Program_Error is raised. Otherwise, execution proceeds normally with the
affected pre- or postcondition expressions.

One possible consequence of the bounded error is that the values denoted by
X'Old for any prefix X might no longer denote the value denoted by X at the
beginning of the subprogram call with the affected postcondition.

****************************************************************

From: Steve Baird
Sent: Friday, November 11, 2011  7:43 PM

If the value of an Old attribute_reference is not needed, then the
implementation is permitted to omit the declaration of the corresponding
implicitly-declared constant.

****************************************************************

From: Robert Dewar
Sent: Friday, November 11, 2011  7:48 PM

Ah, the old "is not needed" phrase, what exactly does that mean in this case,
for instance if some clever prover can prove that the postcondition is always
true, then you don't need the declaration right?

hmmmm ....

****************************************************************

From: Steve Baird
Sent: Friday, November 11, 2011  7:50 PM

As was noted in discussion here in Denver, it means the same thing that it has
meant for years in 10.2.1(18).

****************************************************************

From: Jean-Pierre Rosen
Sent: Saturday, November 12, 2011  6:37 AM

Small improvement, to my taste (because that's the one that really convinced
me):

Possible consequences of the bounded error include that a precondition that
evaluates to True might not be True anymore at the beginning of S, and that the
values denoted by X'Old for any prefix X might no longer denote the value
denoted by X at the beginning of the subprogram call with the affected
postcondition.

****************************************************************

From: Erhard Ploedereder
Sent: Saturday, November 12, 2011 12:04 PM

Sorry, fixed a few typos. Randy, thisis the version on the stick..

[Editor's note: This is, with a few corrections, version /02 of the AI. The
previous version, which was the same except with a few additional typos,
was discarded.]

------
!standard 6.1.1
!standard 11.4.2
!standard 7.3.2
!class binding interpretation
!status received
!priority Medium
!difficulty Easy
!qualifier Omission
!subject Fixes to assertion evaluation semantics

!summary

1. Wording for the Assertion_Policy is updated to extend its effects to pre- and
   postconditions and type invariants.

2. The bounded error situations that apply to pre- and postconditions are moved
   to the section on assertion policy, since they should apply to type
   invariants and all other assertions as well.

3. Calls on functions with side-effects within assertions that affect the value
   of the assertion of the same subprogram are a bounded error.

4. Calls on functions with side-effects within pre- and post-conditions that
   affect the value of any other pre- or postcondition of the same subprogram
   are a bounded error.

5. An implementation permission is added that allows omissions of function calls
   that do not contribute to the value of an assertion, regardless of
   side-effects of the function.

!question

Should Assertion_Policy really only apply to Assert pragmas? (No.)

'Old should be the value at the beginning of a subprogram, not something else
(non-deterministically) in the presence of side-effects? (Yes.)

Should assertion-affecting side-effects be allowed in assertions? (No.)

Should unneeded function calls in assertions be evaluated regardless? (No).

!recommendation

(See summary and wording.)

!wording

Change 11.4.2 1/2 (old version:)

Pragma Assert is used to assert the truth of a Boolean expression at any point
within a sequence of declarations or statements. Pragma Assertion_Policy is used
to control whether such assertions are to be ignored by the implementation,
checked at run-time, or handled in some implementation-defined manner.

to read:

Pragma Assert is used to assert the truth of a Boolean expression at any point
within a sequence of declarations or statements.

Assert pragmas, pre- and postconditions (see 6.1.1), and type invariants (see
7.3.2) are collectively referred to as assertions; their boolean expressions are
referred to as assertion expressions.

Pragma Assertion_Policy is used to control whether assertions are to be ignored
by the implementation, checked at run-time, or handled in some
implementation-defined manner.

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

  1. Delete 6.1.1. 36/3. (replicated below)
  2. Insert the following in 11.4.3 after 23/2.

Bounded (Run-Time) Errors

It is a bounded error to invoke a potentially blocking operation (see 9.5.1)
during the evaluation of an assertion expression. If the bounded error is
detected, Program_Error is raised. If not detected, execution proceeds normally,
but if it is invoked within a protected action, it might result in deadlock or a
(nested) protected action.

It is a bounded error in an assertion expression to alter the value of any
variable that affects the value of the assertion expression. If the bounded
error is detected, Program_Error is raised. Otherwise, execution proceeds
normally with the affected assertion, but the assertion expression need not hold
after the assertion.

It is a bounded error in a pre- or postcondition of subprogram P to alter the
value of any variable that affects the value of any pre- or postcondition
expression of subprogram P. If the bounded error is detected, Program_Error is
raised. Otherwise, execution proceeds normally with the affected pre- or
postcondition expressions. Possible consequence of the bounded error are that
the values denoted by X'Old for any prefix X might no longer denote the value
denoted by X at the beginning of the subprogram call with the affected
postcondition or that a condition that evaluated to true is no longer true after
evaluation of the affected pre- or postcondition.

---------
Add an implementation permission in 11.4.2

If the result of a function call in an assertion is not needed to determine the
value of the assertion expression, the function call need not be executed. This
permission applies even if the function not only returns a value but has
additional effects.

<<< The following is for discussion >>>

In addition, the implementation may omit a call on such a subprogram and simply
reuse  the results produced by an earlier call on the same subprogram, provided
that none of the parameters nor any object accessible via  access values from
the parameters have any part that is of a type  whose full type is an immutably
limited type, and the addresses and  values of all by-reference actual
parameters, the values of all  by-copy-in actual parameters, and the values of
all objects  accessible via access values from the parameters, are the same as
they were at the earlier call. This permission applies even if the subprogram
produces other side effects when called.


!discussion

1. Wording for the Assertion_Policy is updated to extend its effects to pre- and
   postconditions and type invariants.

This is a simple fix. The old words made the Pragma apply only the Assert
pragmas, not to pre/postconditions or invariants.

2. The bounded error situations that apply to pre- and postconditions are moved
   to the section on assertion policy, since they should apply to type
   invariants and all other assertions as well.

The reasons are obvious for type invariants. Might as well fix it for
assertions, too, where the same issue applies.

3. Calling on functions with side-effects within assertions that affect the
   value of the assertion of the same subprogram are a bounded error.

We decided this for pre- and postconditions at the Denver meeting. It should be
true for invariants and general assertions as well. Note that the rules do not
preclude anything that isn't outright dangerous. Memo-functions are legitimate,
as long as the memo-state is not queried by the 'Old attribute.

4. Calling on functions with side-effects within pre- and post-conditions that
   affect the value of any other pre- or postcondition of the same subprogram
   are a bounded error.

We decided this at the Denver meeting.

5. An implementation permission is added that allows omissions of function calls
   that do not contribute to the value of an assertion, regardless of
   side-effects of the function.

We decided this at the Denver meeting.

****************************************************************