false or null = null? [message #1754038] |
Tue, 14 February 2017 00:23  |
Eclipse User |
|
|
|
Hi
I'm trying to understand semantics of the OCL. According to Table A.2 of the OCL Specification:
false or null = null
null or null = null
But it seems that Eclipse OCL returns invalid for the both cases:
transformation Semantics();
main() {
log('false or null = ' + str(false or null));
log('null or false = ' + str(null or false));
log('b() or null = ' + str(b() or null));
}
query b() : Boolean = null;
query str(s : OclAny) : String =
if s.oclIsInvalid() then '<Invalid>'
else if s.oclIsUndefined() then 'null' else s.repr() endif endif;
Here is the output:
false or null = <Invalid>
null or false = <Invalid>
b() or null = <Invalid>
Is it a bug in the Eclipse OCL?
|
|
|
Re: false or null = null? [message #1754046 is a reply to message #1754038] |
Tue, 14 February 2017 02:15   |
Eclipse User |
|
|
|
Hi
No and Yes.
The new Pivot-based Eclipse OCL that prototypes solutions to many specification problems is correct. It has a JUnit sub-test:
ocl.assertQueryNull(null, "let b : Boolean = null in false or b");
The classic Eclipse OCL that has a number of issues that are too hard to resolve has:
assertResultInvalid("let b : Boolean = null in false or b");
Unfortunately migration to the new Pivot OCL is a still an aspiration for QVTo, which is I think what you are using.
This is an area that changed as a consequence of the observation by the Isabelle researchers that OCL Boolean operations were not idempotent for null. i.e "X = not not X" should be true. OCL 2.4 Boolean is consistently 4-valued, whereas OCL 2.3 Boolean was 3.5-valued, results were always 3-valued, although the inputs could be 4-valued; there was no difference between null/invalid as input; hence I call it 3.5-valued. IMHO the 3.5-valued seems slightly better, although it seems that in practice code that actually uses this corner is dangerous. When I've tried to have a logic that re-uses Boolean to handle explicitly-true, explicitly-false, unspecified, I find that I need to implement logic explicitly.
Regards
Ed Willink
|
|
|
|
|
|
|
|
Re: false or null = null? [message #1754339 is a reply to message #1754274] |
Thu, 16 February 2017 08:46  |
Eclipse User |
|
|
|
Hi
QVTd is already based on the Pivot OCL.
Unless someone volunteers to do it for me, I guess QVTo migration might be a year or two away.
In principle a next OMG OCL could be based on auto-generation from the same models from which Eclipse OCL is auto-generated. But there is a lot of work to remove Eclipse-isms and bad design decisions before the models can sensibly be part of a neutral standard.
Unfortunately, I am practically the only person working on OMG OCL, OMG QVT, Eclipse OCL, Eclipse QVTd, so my progress is consistently disappointing.
Regards
Ed Willink
|
|
|
Powered by
FUDForum. Page generated in 0.03074 seconds