Search code examples
umlpreconditionsoclpost-conditions

OCL: How can I write pre and postconditions for the operation max to find the maximum value from a collection?

I am trying to write pre and post conditions to find the maximum value of a collection 'col'. I'm not really sure how to go about it, recursively so I was wondering if someone could help!

pre: true 
post: result = ...
Solution

  • What I would do:

    pre:  not col.isEmpty()
post: col -> includes(result) and col -> forAll(a | a <= result)

    EDIT2: I discussed this question with some OCL experts. They pointed out that it's necessary to have col -> includes(result) in the post condition. Otherwise result may be any value greater than all elements of col, but is not necessarily an element of col.

    EDIT:

    The post condition means: for each element a of col, it is true that a <= result The forAll operation is defined on page 45 of the OCL Specification 2.3.1. Its syntax is 

    collection->forAll( v | boolean-expression-with-v )

    Its semantics is:

    This forAll expression results in a Boolean. The result is true if the boolean-expression is true for all elements of collection. If the boolean-expression-with-v is false for one or more v in collection, then the complete expression evaluates to false. For example, in the context of a company:

    Examples:

     context Company
      inv: self.employee->forAll( age <= 65 )
      inv: self.employee->forAll( p | p.age <= 65 )
      inv: self.employee->forAll( p : Person | p.age <= 65 )