Re: OCL 2.0 FTF Issues: Satisfaction of Operation Specifications



Date view Thread view Subject view Author view Attachment view

From: Achim D. Brucker (brucker@informatik.uni-freiburg.de)
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
weakened

Rationale:
... as before ...


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

DEFINITION A.34 (SATISFACTION OF OPERATION SPECIFICATIONS) An
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 (brucker@inf.ethz.ch) and
Burkhart Wolff (wolff@informatik.uni-freiburg.de)
-- 
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: brucker@inf.ethz.ch

Date view Thread view Subject view Author view Attachment view