Re: InOut Variables (Operations' Semantics)



Date view Thread view Subject view Author view Attachment view

From: Prof. Dr. Peter H. Schmitt (pschmitt@ira.uka.de)
Date: Fri 28 Jan 2005 - 08:30:04 GMT


A post condition in OCL is always evaluated in the post state.
So, in your example, when the traingelKind method changes s1,s2,
or s3 then then the result depends on the new values NOT
on the values before calling the method.
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.


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

Date view Thread view Subject view Author view Attachment view