OCL 2.0 FTF



Date view Thread view Subject view Author view Attachment view

From: Bernhard Beckert (beckert@ira.uka.de)
Date: Sat 08 Nov 2003 - 14:08:25 GMT


Dear all,

enclosed I am sending two further issues for the OCL 2.0 finalization:
a) Remove the restriction on recursion in post-conditions
b) Clarify whether let expressions can be recursive

Best regards
Bernhard




-- 

+------------------------------------------------------------+
|  Bernhard Beckert, WWW: http://i12www.ira.uka.de/~beckert/ |
+------------------------------------------------------------+


Remove the restriction on recursion in post-conditions

Author: Bernhard Beckert (beckert@uni-koblenz.de)

Description: 
The restriction in the description of post-conditions (Section 2.5.2) that 
recursion must not be infinite (i.e. must terminate) should be removed.


Rationale:

The problem of deciding whether a given recursive definition
terminates is in general undecidable. Thus, if the restriction that
recursion must terminate remains, then syntactical correctness of
post-conditions (with recursion) is undecidable.

That is a very bad situation. Syntactical correctness should always be
decidable.

There are basically two solutions to this problem

A) Remove the restriction and allow termination.

B) Further restrict the allowed syntactical forms of recursion to
   cases for which termination is decidable.

I suggest to adopt option A for the following reasons:

1) Option B has the disadvantage that "artificial" syntactical
   restrictions have to be added that may rule out useful (and
   terminating) definitions.

2) Termination is not vital. If a recursive post-condition 

     result = expression

   does not terminate, then the post-condition still has a
   well-defined semantics, which is the most important property of a
   definition. The fact that the value of the expression and, thus,
   the value of result may not be computable is of disadvantage, but
   whether that renders the constraint useless depends on the
   application (testing, verification, ...). Note also, that even for
   a non-terminating definition it can in many cases be checked
   whether the post-condition holds in a particular state.

   Examples: The following two recursive post-conditions of an
   operation m() do not terminate, but it is still easy to check that
   the first one is true and the second is not:

     result = m()

     result = m() + 1


Clarify whether let expressions can be recursive

Author: Bernhard Beckert (beckert@uni-koblenz.de)

Description: 
The decription of let expressions does not explicitly state whether
they can be recursive. This should be clarified.


Rationale:

There is some confusing regarding the question of whether let
expressions can be recursive, i.e., whether the defined variable may
occur in the defining expression.  The description of let expressions
in Section 3.3.6 (p. 3-17) should clearly and explicitly answer this
question. Moreover, if recursion is allowed, then the semantics of a
non-terminating recursion has to be clarified as well.

Possible ways to answer this question are:

A) Recursion is forbidden.

B) Recursion is allowed. But certain syntactically restricted are
   imposed on recursive definitions that ensure termination.

C) Recursion is allowed. In addition, the semantics is defined to be
   the "undefined value" if the recursion does not terminate.

D) Recursion is allowed. In addition, the semantics of non-terminating
   recursive definitions is defined to be the smallest fix-point of
   the definition if it exists and is unique, and the "undefined
   value" otherwise.


I suggest to use option D, because it gives the desired results for
most practical examples. In particular it allows to define transitive
closure for arbitrary relations.

Date view Thread view Subject view Author view Attachment view