Re: InOut Variables (Operations' Semantics)



Date view Thread view Subject view Author view Attachment view

From: Andreas Awenius (andreas.awenius@empowertec.de)
Date: Fri 28 Jan 2005 - 20:15:54 GMT


Hello all,

> It is a major deficiency of OCL not to offer means to express
> what you have in mind. In JML  e.g.there
> is something called the "assignable clause" attached to a method
> specification, where you can give a list of expression e1,..,en,
> (Java expression in this case) with the intented meaning that
> the method changes at most these expression.
> So you could add to your triangleKind specification an empty
> assignable clause to express that you do not whish
> the values of si to be changed.

The latter effect could also be achieved in OCL by defining the operations result as an expression of type 'body'.
I'd say, setting 'result' in a postcondition to define the operations result is deprecated.

Kind regards,
Andreas
--
Andreas Awenius
EmPowerTec AG
Taubenweg 20
85238 Petershausen
Fon: +49 8137 80 98 81
Fax: +49 8137 80 98 82


> regards  Peter


> Percy Pari Salas wrote:
>> Hello all,
>>
>>>
>>> What Percy meant is probably: "attributes can be read and modified in
>>> an OCL expression"?
>>> If that is what he meant, the answer could be complemented with "No,
>>> because OCL expressions may not alter an objects state. They would be
>>> of kind 'in', if the kind would apply to attributes.".
>>>
>>> Kind regards,
>>> Andreas
>>>
>> Andreas is almost right, but what I exactly mean is the following:
>> suppose we have a Class Triangle with integer attributes s1,s2,s3
>> (representing the sides of the triangle). I model an operation
>> triangleKind as
>>
>> context Triangle::triangleKind():String
>> Post: if s1=s2 and s2=s3 then result = "equilateral" else (result =
>> "isosceles" or result = "scalene")
>>  (I'm just simplifying the specification)
>>
>> Well, look that I am not saying anything about the pre-state, I am just
>> restricting the output (result) by evaluating the values of the
>> post-state. The question is... it can be safely assumed that this
>> specification ensures (for example) that s1=s1@pre ???  Moreover, if I
>> have an IMPLEMENTATION of triangleKind that before evaluating the values
>> and deciding the output assigns new (random) values to s1,s2,s3 and
>> after that satisfies the postcondition; this implementation still
>> conforms the OCL specification (even when   NOT s1=s1@pre  or   NOT
>> s2=s2@pre  ... )
>>
>> Thanks for your answers,
>>
>>  Percy Pari Salas
>> UNU-IIST Fellow
>> Macau SAR - China
>>
>>>
>>> --
>>> Andreas Awenius
>>> EmPowerTec AG
>>> Taubenweg 20
>>> 85238 Petershausen
>>> Fon: +49 8137 80 98 81
>>> Fax: +49 8137 80 98 82
>>>
>>>
>>>
>>>
>>> To remove yourself from this list please mail
>>> puml-list-request@cs.york.ac.uk
>>> with a message containing the word "unsubscribe".
>>>
>>>
>>
>>
>>
>>
>>
>> To remove yourself from this list please mail
>> puml-list-request@cs.york.ac.uk
>> with a message containing the word "unsubscribe".
>>

> --
> Prof.Dr.P.H.Schmitt
> Fakultät für Informatik
> Universität Karlsruhe




> To remove yourself from this list please mail
> puml-list-request@cs.york.ac.uk
> with a message containing the word "unsubscribe".

Date view Thread view Subject view Author view Attachment view