Consider aligning loops with IBM tool semantics

[MattWindsor91]

IBM Rational's understanding of LoopFragments is as follows:

A loop interaction operator indicates that the interaction fragment runs repeatedly. The number of times the fragment runs is determined by the minint and maxint parameters of the operator. The syntax of the loop operator is loop (minint, maxint) where maxint can also be infinity (*). After the minimum number of iterations is satisfied, a Boolean expression is tested on each pass. When the Boolean expression tests false, the loop ends.

This is different from our setup, where we currently loop the body between minint and maxint times, but (I believe) have the guard simply act as if it empties the loop body whenever it tests false.

It would be worth double-checking the UML specification to see who has the right of it.

[MattWindsor91]

UML 2.5.1, emphasis mine:

The interactionOperator loop designates that the CombinedFragment represents a loop. The loop operand will be
repeated a number of times. The Guard may include a lower and an upper number of iterations of the loop as well as a Boolean expression. The semantics is such that a loop will iterate minimum the ‘minint’ number of times (given by the iteration expression in the guard) and at most the ‘maxint’ number of times. After the minimum number of iterations have executed and the Boolean expression is false the loop will terminate. The loop construct represents a recursive application of the seq operator where the loop operand is sequenced after the result of earlier iterations.

If the loop contains a separate InteractionConstraint with a specification, the loop will only continue if that specification evaluates to true during execution regardless of the minimum number of iterations specified in the loop.

Confusingly, Guard and InteractionConstraint here refer to the same thing -- what we in RoboCert call a Guard. (But, in hindsight, should probably call an InteractionConstraint - this somehow got missed when I was renaming things for UML parity.)

Some things to unpick here:

• The and here suggests that, indeed, the semantics should be that the initial minint overrides the guard.
• This semantics is slightly non-compositional, in that we have to treat InteractionOperand differently if they're in loops (ie, we can't just emit a guard). But if UML does it, we should do it.
• In UML, what we call DiscreteBound is part of InteractionConstraint. I suppose that, if we adopt the semantics where both guard condition and minimum iteration count must be considered jointly, it might make sense for them to be together. But this would involve introducing WFCs and, as we'd need to special-case the rule for LoopFragment to deal with the guard anyway, the only advantage to making this change is UML faithfulness.
• I'm unsure what the second paragraph is trying to say - the OCL at 17.12.12.5 suggests that the loop InteractionConstraint is the exact same as the InteractionConstraint of its operand.
• Incidentally, an InteractionConstraint is arbitrary (except minint and maxint); it can be human or machine readable. RoboCert's notion of ExprGuard, ElseGuard, and EmptyGuard is synthetic.