!standard  6.1.1(0)                              11-11-11    AI05-0274-1/01
!class Amendment 11-11-11
!status work item 11-11-11
!status received 11-11-11
!priority Low
!difficulty Medium
!subject Side-effects during assertion evaluation

!summary

Define side-effects in a pre/postcondition to be a bounded error.

!problem

Calling a function that has some side effect from a precondition or
postcondition can have some unusual effects.

For instance, if F is a function that increments I, then in
   F'Old + I'Old
the value of I might not be the value that it had when the subprogram was
entered.

!proposal

(See summary.)

!wording

Add before 6.1.1(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.

!discussion

!example

(See problem.)

!corrigendum 6.1.1(0)

@dinsc

Force a conflict; the real text is found in the conflict file.


!ACATS Test

ACATS tests could be constructed to see if the bounded error is detected, but these
would have minimal value.

!ASIS


!appendix

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.

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