| Parser ignores @pre [message #1686710] |
Thu, 19 March 2015 06:10  |
Eclipse User |
|
|
|
Hi!
I have a short question about the following example:
class C {
op void addElem();
!ordered attr int[*] intSet;
}
context C::addElem():
post : self.intSet->size() = self.intSet->size@pre() + 1
post : self.intSet->size() = self.intSet@pre->size() + 1
I'm parsing the OCL file with the parse method from org.eclipse.ocl.OCL. When I'm printing the parsed constraints, I get the following result:
context addElem() : post: self.intSet->size().=(self.intSet@pre->size().+(1))
context addElem() : post: self.intSet->size().=(self.intSet->size().+(1))
After reading in the OMG OCL 2.4 spec, I've found the following snippet:
"The rule says that the @pre modifier may be applied to all operations, although, in general, not all operations do actually depend on a system state (for example, operations on data types). The result of these operations will be the same in all states. Operations that do depend on a system state are, e.g., attribute access and navigation operations."
For me ->size@pre works on the data from an attribute, such that I would expect that the parsed size is markedPre for the second post condition. Is my understanding here simply wrong?
If my understanding is wrong, I would like to know if there are any operations where an usage as in the example above is meaningful and would lead to different results, or must the result be always the same?
Regards,
Nils
|
|
|
| Re: Parser ignores @pre [message #1686830 is a reply to message #1686710] |
Thu, 19 March 2015 07:16  |
| Eclipse User |
|
|
|
Hi
Currently Eclipse OCL only provides parsing support for oclIsNew(),
@pre, preconditions and postconditions. They are completely ignored in
all execution scenarios.
AFAIK USE is the only OCL tool that makes any attempt at supporting more
than one system state. USE maintains all states, not just two.
The snippet you highlight from the OCL specification is not particularly
helpful; operation is used in a confusingly general PropertyCallExp or
OperationCallExp sense.
Looking a bit further: https://bugs.eclipse.org/bugs/show_bug.cgi?id=462552
Regards
Ed Willink
On 19/03/2015 10:10, Nils Przigoda wrote:
> Hi!
>
> I have a short question about the following example:
> class C {
> op void addElem();
> !ordered attr int[*] intSet;
> }
> context C::addElem():
> post : self.intSet->size() = self.intSet->size@pre() + 1
> post : self.intSet->size() = self.intSet@pre->size() + 1
>
> I'm parsing the OCL file with the parse method from
> org.eclipse.ocl.OCL. When I'm printing the parsed constraints, I get
> the following result:
> context addElem() : post:
> self.intSet->size().=(self.intSet@pre->size().+(1))
> context addElem() : post: self.intSet->size().=(self.intSet->size().+(1))
>
> After reading in the OMG OCL 2.4 spec, I've found the following snippet:
> "The rule says that the @pre modifier may be applied to all
> operations, although, in general, not all operations do actually
> depend on a system state (for example, operations on data types). The
> result of these operations will be the same in all states. Operations
> that do depend on a system state are, e.g., attribute access and
> navigation operations."
>
> For me ->size@pre works on the data from an attribute, such that I
> would expect that the parsed size is markedPre for the second post
> condition. Is my understanding here simply wrong?
>
> If my understanding is wrong, I would like to know if there are any
> operations where an usage as in the example above is meaningful and
> would lead to different results, or must the result be always the same?
>
> Regards,
> Nils
>
|
|
|
| Re: Parser ignores @pre [message #1687169 is a reply to message #1686830] |
Thu, 19 March 2015 10:37 |
| Eclipse User |
|
|
|
Thanks a lot, Ed!
But I'm still asking myself if there is any semantical difference between the evaluation of the two postconditions?
context C::addElem():
post : self.intSet->size() = self.intSet->size@pre() + 1
post : self.intSet->size() = self.intSet@pre->size() + 1
The evaluation in the background is conducted by my own tool, that's why I need to know how to handle such cases.
|
|
|
Powered by
FUDForum. Page generated in 0.05200 seconds
Home