Re: InOut Variables (Operations' Semantics)



Date view Thread view Subject view Author view Attachment view

From: Percy Pari Salas (percy@iist.unu.edu)
Date: Fri 28 Jan 2005 - 01:49:21 GMT


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".
>
> 

Date view Thread view Subject view Author view Attachment view