Can an OCL Post condition be inside an if then statement?

Question

I'm new to OCL and I have some doubts about how the pre and postconditions work.

Can a post condition be placed inside an if then statement?

For example, the following piece of code is valid or I'm just mixing concepts?

Context [some context here]
if ( 
... some conditions...
) then ( 
result = 1
post: self.isComplete() -- for example
)
endif

Thank you very much for your help

Answer 1

I would rewrite it as:

Context MyContext :: Integer
    post :
        if <some condition>
        then
            result = 1
        endif

If you need more condition you can do this with:

Context MyContext :: Integer
    post :
        if <some condition>
        then
            -- Another condition
            if self.isComplete()
            then
                result = 1
            else
               result = 0
            endif
        else
            result = 0
        endif

Answer 2

You could use implies operator like below:

context k 
inv
(k.count=0)implies(k.status='nothing')

Answer 3

Simple answer. No. The Complete OCL post: declaration is an independent complement to an Operation.

A post-condition may fail if the actual model data is not compatible with the OCL programmer's expectations. So if you want a failure, then you get into the difficult area of how OCL fails reliably and usefully. See [1]. Alternatively if you just want a more complex control flow, rewrite as indicated in the earlier answer.

Since your internal post-condition could be reified as an external post-condition on a helper operation, there is clearly an opportunity for an OCL syntax enhancement to allow something along the lines of what you suggested.

Pre and post-conditions are poorly supported by current tooling. USE has an option to execute them, Eclipse OCL doesn't; they are only parsed for syntax validity. Executing post-conditions at run-time can be very expensive and difficult since the most pathological usage of @pre may require a copy of the whole system state.

The expensive run-time execution may be acceptable for a few test runs, but do you want to inflict it on your end users and what are those users to do if the post-condition fails?

Work described in [1] uses symbolic analysis to migrate the evaluation to compile-time ensuring that the conditions are respected and would not fail at run-time if the extra time was used.

However no symbolic analysis can accommodate all possible control flow so an oclAssert(expr, invariant) wrapper is needed to help the symbolic analysis by asserting that the local invariant is true for the returned expr. A similar wrapper could support your usage except that you want to provoke a run-time failure rather than promise that a hazard is not possible.

[1] http://www.eclipse.org/modeling/mdt/ocl/docs/publications/OCL2021Validity/OCLValidity.pdf