Re: OCL 2.0 FTF Issues: Satisfaction of Operation Specifications

Date view Thread view Subject view Author view Attachment view

From: Achim D. Brucker (
Date: Tue 04 Nov 2003 - 17:38:29 GMT

Dear all,

While supporting Hubert Baumeister's, Rolf Hennicker's and
Alexander Knapp's proposal in principle, we suggest a slight
modification from it for the following reasons:
- we would prefer to view a program as a special case of a
  specification, hence slightly generalize the notion of
  compliance to relations and bringing it closer to Spivey?s
  Notion of Operation Refinement (ZRM pp. 136)
- this paves the way for nondeterministic abstract programs
  occurring during formal development or in intermediate stages
  in MDA-Transformations
- we would like to simplify the notation. (No explicit ?graph?).

Description: Change Definition A.34 to allow the precondition to be

... as before ...

Therefore, we propose to replace Def. A.34 by:

operation specification with pre- and postconditions is satisfied by a
specification S if the restriction of S to the domain of R
(denoted S|_dom(R)) is included in R, i.e. S|_dom(R) \subseteq R.

This is equivalent to: \forall x, y. x:dom(R) & (x,y):S --> (x,y):R.

In particular, S may be a program, i.e. a computation function in the
sense of total correctness.

Achim D. Brucker ( and
Burkhart Wolff (
Achim D. Brucker, Information Security, IFW C 41.2, ETH Zentrum, 8092 Zurich
 Phone: +41/01 63 25217, Fax: +41/01 63 21172, E-Mail:

Date view Thread view Subject view Author view Attachment view