**From:** Bernhard Beckert (*beckert@ira.uka.de*)

**Date:** Sat 08 Nov 2003 - 14:08:25 GMT

**Next message:**Tim Klinger: "equality"**Previous message:**Herman Balsters: "RE: OCL 2.0 finalizatioon"

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.

**Next message:**Tim Klinger: "equality"**Previous message:**Herman Balsters: "RE: OCL 2.0 finalizatioon"