Home » Modeling » OCL » Purpose of OCL precondition ?
| Purpose of OCL precondition ? [message #19468] |
Mon, 23 April 2007 02:55  |
Eclipse User |
|
|
|
Originally posted by: maiera.de.ibm.com
In 12.7 of the OCL 2.0 spec, it says:
"The purpose of a precondition is to specify the conditions that must
hold before the operation executes. A precondition consists of an OCL
expression of type Boolean. The expression must evaluate to true
whenever the operation starts executing, but only for the instance that
will execute the operation."
I'm not sure I agree to the unconditional requirement that the
precondition must hold whenever the operation starts executing.
I think what makes much more sense is to say that the precondition must
hold in order to enable the operation to succeed (in which case it must
ensure that the postconditions hold)
Is that what is meant ?
Andy
|
|
|
| Re: Purpose of OCL precondition ? [message #19605 is a reply to message #19468] |
Mon, 23 April 2007 13:11  |
| Eclipse User |
|
|
|
Originally posted by: cdamus.ca.ibm.com
Hi, Andy,
I'm not so sure. OCL constraints are absolute assertions. The language of
"must evaluate to true whenever the operation starts executing" is,
perhaps, too soft. I think "evaluates to true whenever..." is more
appropriate.
What I mean is that the constraint states that the pre-condition expression
is true at the time of the operation call. Evaluating to false isn't an
option, and the OCL specification doesn't say anything about the
consequences of violating a constraint. All that OCL says is that in a
correct implementation of the system, this expression evaluates to true at
such time. So, it doesn't matter whether the operation could attempt to
execute and possibly fail or not. It simply doesn't happen in the system
being modeled. Whether that system looks like what is actually implemented
is another question ...
Consider, also, that post-condition constraints are sometimes (often?) used
to specify what an operation does (esp. when message expressions are used).
In such cases, the purpose of the constraint isn't so much to check what an
operation execution has done as just to communicate (in the model) what it
is intended to do.
That's just my $0.02.
Cheers,
Christian
Andreas Maier wrote:
> In 12.7 of the OCL 2.0 spec, it says:
>
> "The purpose of a precondition is to specify the conditions that must
> hold before the operation executes. A precondition consists of an OCL
> expression of type Boolean. The expression must evaluate to true
> whenever the operation starts executing, but only for the instance that
> will execute the operation."
>
> I'm not sure I agree to the unconditional requirement that the
> precondition must hold whenever the operation starts executing.
>
> I think what makes much more sense is to say that the precondition must
> hold in order to enable the operation to succeed (in which case it must
> ensure that the postconditions hold)
>
> Is that what is meant ?
>
> Andy
|
|
|
| Re: Purpose of OCL precondition ? [message #19739 is a reply to message #19468] |
Tue, 24 April 2007 06:18 |
| Eclipse User |
|
|
|
Hi Andy,
If it helps, my comments below.
"Andreas Maier" <maiera@de.ibm.com> wrote in message
news:f0hl7s$tvd$1@build.eclipse.org...
> In 12.7 of the OCL 2.0 spec, it says:
>
> "The purpose of a precondition is to specify the conditions that must hold
> before the operation executes. A precondition consists of an OCL
> expression of type Boolean. The expression must evaluate to true whenever
> the operation starts executing, but only for the instance that will
> execute the operation."
>
> I'm not sure I agree to the unconditional requirement that the
> precondition must hold whenever the operation starts executing.
>
> I think what makes much more sense is to say that the precondition must
> hold in order to enable the operation to succeed (in which case it must
> ensure that the postconditions hold)
I agree that precondition must be true to make the operation to succeed.
Nevertheless, the postconditions expression has no relationship with the
preconditions. Of the same context, the modeler may specify multiple
preconditions without specifying any postconditions and vice versa. The
implication when the precondition evaluates to true, is that the model
behave like the specified requirement, which later the expectation to the
the real post conditions situation can be achieved.
> Is that what is meant ?
>
> Andy
Best regards,
Jibran
|
|
|
| Re: Purpose of OCL precondition ? [message #19783 is a reply to message #19739] |
Tue, 24 April 2007 09:18 |
| Eclipse User |
|
|
|
Hi Jibran,
As I understand it, there are two different interpretations of
"precondition" in the literature.
For those talking about Design-By-Contract, a precondition serves the
purpose of fielding the blame on one of (caller, callee) whenever the
operation does not complete as expected, in spite of the fact that the
precond evaluated to true. To me, the distinctive feature of this
interpretation is that no attempt is made at compile time to certify that
the operation, whenever invoked, will actually fulfill postconds after being
executed.
For those talking instead about Program Verification, then "precondition"
means what it means in Hoare logic: a formal analysis has been performed on
the statements that make up the operation, and the conclusion has been
reached (at compile time) that whenever the operation is invoked with valid
preconds, and the operation completes, it will be the case that the
postconds will hold.
I think the OCL standard just lets you pick an interpretation.
Miguel
|
|
|
| Re: Purpose of OCL precondition ? [message #19858 is a reply to message #19783] |
Wed, 25 April 2007 02:23 |
| Eclipse User |
|
|
|
Originally posted by: maiera.de.ibm.com
Thanks to all who responded.
We try to use OCL in CIM (Common Information Model, DMTF) where we do
care about things like failed method invocations. So I guess the bottom
line of this for us is that we need to define in our usage exactly those
things that OCL itself leaves open, i.e. exactly what a precondition
means to us, particularly when it is not satisfied.
Andy
Miguel Garcia wrote:
> Hi Jibran,
>
> As I understand it, there are two different interpretations of
> "precondition" in the literature.
>
> For those talking about Design-By-Contract, a precondition serves the
> purpose of fielding the blame on one of (caller, callee) whenever the
> operation does not complete as expected, in spite of the fact that the
> precond evaluated to true. To me, the distinctive feature of this
> interpretation is that no attempt is made at compile time to certify that
> the operation, whenever invoked, will actually fulfill postconds after being
> executed.
>
> For those talking instead about Program Verification, then "precondition"
> means what it means in Hoare logic: a formal analysis has been performed on
> the statements that make up the operation, and the conclusion has been
> reached (at compile time) that whenever the operation is invoked with valid
> preconds, and the operation completes, it will be the case that the
> postconds will hold.
>
> I think the OCL standard just lets you pick an interpretation.
>
> Miguel
>
>
>
|
|
|
Goto Forum:
Current Time: Thu May 08 03:29:50 EDT 2025
Powered by FUDForum. Page generated in 0.05586 seconds |
Home