In 8.1.4 Replace
A mapping operation is syntactically described by a
signature, a guard (a when clause), a mapping body, and a
postcondition (a where clause). Even if it is not explicitly
notated in the concrete syntax, a mapping operation is always
a refinement of an implicit relation that is the owner of the
when and where clauses.
by
A mapping operation is syntactically described by a
signature, a guard (a when clause) or precondition, a mapping
body, and a postcondition (a where clause). Even if it is not
explicitly notated in the concrete syntax, a mapping operation
is always a refinement of an implicit relation.
in 8.1.4 append
In strict invocation mode, a precondition (a when clause) is
executed as an assertion before any other execution. Failure
of the assertion causes a fatal execution failure. A
postcondition (a where clause) is similarly executed as an
assertion after all other execution has completed.
In 8.2.1.5 following
The when clause acts either as a pre-condition or as a guard,
depending on the invocation mode of the mapping operation. The
where clause always acts as a post-condition for the mapping
operation.
append
pre-conditions and post-conditions are assertions; any
execution failure is fatal.
