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

Question 1

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 )

Question 2

post: result= col -> any(a | col->forAll(a2 | a >=a2))

where "any" returns one of the elements that satisfy the condition, i.e. like a select but guarantees that only a single element is returned, randomly selected if several elements in the collection satisfy the condition;

the condition inside the "any" guarantees that the selected element "a" is the maximum value in the collection by comparing it with all the others

Check also this OCL tutorial . In fact, the limitations of OCL to deal with aggregates and other kinds of statistical functions is one of the open issues with this language.

Question 3

OCL defines Collection::max() as

post: result = self->iterate( elem; acc : T = self.first() | acc.max(elem) )

where "the max operation -supported by the elements- must take one parameter of type T and be both associative and commutative".

I understand that it should be post: result = self->iterate( elem; acc : T = self.asSequence()->first() | acc.max(elem) ) because first() is not defined for Collection.

The collection is converted to a sequence. An accumulator (acc) is initialized with the first value of the sequence. The iterate expression updates the accumulator as the max between the current value of acc and the iterator elem. If the collection is empty the result is self.first(), which is invalid.

Question 4

If I understand you correctly than maybe this can help: http://math.hws.edu/eck/cs124/javanotes6/c4/s6.html#subroutines.6.1

Precondition is something that must be meet before your method is executed. This will mostly be some asserts about input data, for example the collection is not null. Post-condition defines what will be true after the method has finished. In your case this can be for example: the method returned element with value maximum value in given collection.