Re: OCL 2.0 FTF Issues: Satisfaction of Operation Specifications



Date view Thread view Subject view Author view Attachment view

From: Hubert Baumeister (baumeist@informatik.uni-muenchen.de)
Date: Wed 05 Nov 2003 - 15:41:06 GMT


Dear Achim and Burckhard,

we don't agree with your proposal. In contrast, we think that one should separate operations from
their specifications and the notion of when an operation satisfies an operation specification from
the notion of when an operation specification satisfies (better: refines) another one. (cf.
<http://www.pst.informatik.uni-muenchen.de/veroeffentlichungen/hennicker-knapp-baumeister:2003.pdf>)

In any case the words "specification S" should be replaced by "relation S" and "S may be a program"
should be replaced by "S may represent the semantics of a program".

Greetings,
	Hubert

Achim D. Brucker wrote:
> 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)


-- 
Dr. Hubert Baumeister, Institut für Informatik, Universität München
mailto:baumeist@informatik.uni-muenchen.de
http://www.informatik.uni-muenchen.de/~baumeist
phone (x49-89)2180-9375  * fax -9175

Date view Thread view Subject view Author view Attachment view