Previous: | 4.2 More than Complete | |
Up: | 4. Completeness | |
Next: | 5. Conclusions |
This section addresses the Turing completeness of OCL. It is relatively easy to show that the language is not complete, moreover, that the functions expressible in OCL are all primitive recursive. In order to prove so, we show that LOOP-programs can and WHILE-programs cannot be written in OCL (see [Sch95]).
The syntax of LOOP-programs is as follows:
P ::= X - X + C | X - X - C | LOOP X DO P END | P ; P X ::= x_{0} | x_{1} | x_{2} | ... (variables) C ::=0|1|2| ... (constants)
The semantics of LOOP-programs is straightforward. Given a LOOP-program that computes a k-ary function f, it is assumed that the input values are initially stored in the variables , that any other variable has initial value 0, and that the result is stored in the variable x_{0} after execution of the program. The value assignment x_{i} <- x_{j} + c is interpreted as usual, that is, the new value of the variable x_{i} is the value of x_{j} plus c. The value assignment x_{i} <- x_{j} - c is the non-negative subtraction, that is, if c > x_{j} then the new value of x_{i} is 0 otherwise the value of x_{j} minus c. A LOOP-program of the form P_{1} ; P_{2} is interpreted as the execution of P_{1} and afterwards the execution of P_{2}. Finally a LOOP-program of the form LOOP x_{i} DO P END is interpreted as follows: the program P is executed ntimes, where n is the value of the variable x_{i} at the beginning (i.e. the change of the value of x_{i} within P does not affect the number of repetitions).
LOOP-programs are WHILE-programs, and additionally if P is a WHILE-program then
is a WHILE-program. The semantics of the new construct is the following: the program P is repeatedly executed as long as the value of x_{i} is different from 0.
Every LOOP-program can be computed by an OCL expression. Indeed, given a LOOP-program P computing a k-ary function and using auxiliary variables , we write an OCL expression that manipulates an array vals_{1} of r+1values (representing the values of the variables ) and returns the first value of this array after executing the translation of P:
The return value of the above expression is the first value of the sequence vals_{1} after iterating one time the execution of . Initially vals_{1} stores the value n_{i} for the variable x_{i} ( ) and 0 otherwise. The return value of is stored in vals_{1}. The function with is a function that manipulates the sequence vals_{n} and is defined by induction on the structure of P as follows:
trans(x_{i} - x_{i} + c, n) = vals_{n}->iterate( val : Integer ; newvals : Sequence(Integer) = Sequence{} | if newvals->size = i then newvals->append(val+c) else newvals->append(val) endif )
trans(x_{i} - x_{j} + c, n) = vals_{n}->iterate( val : Integer ; newvals : Sequence(Integer) = Sequence{} | if newvals->size = i then newvals->append(newvals->at(j+1)+c) else newvals->append(val) endif )
trans(x_{i} - x_{j} + c, n) = vals_{n}->iterate( val : Integer ; newvals : Sequence(Integer) = Sequence{} | if newvals->size = j then (newvals->subSequence(1, i)) -- (1) ->append(val+c) ->union(newvals->subSequence(i+2, j)) -- (2) ->append(val) else newvals->append(val) endif )
trans(x_{i} - x_{i} - c, n) = vals_{_n}->iterate( val : Integer ; newvals : Sequence(Integer) = Sequence{} | if newvals->size = i then newvals->append(if valc then 0 else val-c) else newvals->append(val) endif )
trans(x_{i} - x_{j} - c, n)= vals_{n}->iterate( val : Integer ; newvals : Sequence(Integer) = Sequence{} | if newvals->size = i then newvals->append(if newvals->at(j+1)c then 0 else newvals->at(j+1)-c endif) else newvals->append(val) endif )
trans(x_{i}- x_{j}- c, n)= vals_{n}->iterate( val : Integer ; newvals : Sequence(Integer) = Sequence{} | if newvals->size = j then (newvals->subSequence(1,i)) -- (1) ->append(if valc then 0 else val-c) ->union(newvals->subSequence(i+2,j)) -- (2) ->append(val) else newvals->append(val) endif )
trans(LOOP x_{i} DO P END, n) = Sequence{1..vals_{n}->at(i+1)}->iterate( i : Integer ; -- iterator, will be ignored vals_{n+1} : Sequence(Integer) = vals_{n} | trans(P,n+1) )
trans(P_{1} ; P_{2}, n)= Sequence{1..2}->iterate( step : Integer ; vals_{n+1} : Sequence(Integer) = vals_{n} | if step = 1 then trans(P_{1},n+1) else trans(P_{2},n+1) endif )
So for instance the function f(n,m)=n+m, computed by the program
X0 <- X1 + X2which can be encoded as the following LOOP-program P
X0 <- X1 + 0 ; -- P1 LOOP X2 DO -- P2 X0 <- X0 + 1 -- P21 ENDis translated to the OCL expression obtained by successively calculating as follows:
Sequence{1..1}->iterate( i : Integer ; vals1 : Sequence(Integer) = {0,n,m} | trans(P,1) )->first
Sequence{1..1}->iterate( i : Integer ; vals1 : Sequence(Integer) = {0,n,m} | Sequence{1..2}->iterate( step : Integer ; vals2 : Sequence(Integer) = vals1 | if step = 1 then trans(P1,2) else trans(P2,2) endif ) )->first
Sequence{1..1}->iterate( i : Integer ; vals1 : Sequence(Integer) = {0,n,m} | Sequence{1..2}->iterate( step : Integer ; vals2 : Sequence(Integer) = vals1 | if step = 1 then vals2->iterate( val : Integer ; newvals : Sequence(Integer) = Sequence{} | if newvals->size = 1 then (newvals->subSequence(1,0)) ->append(val+0) ->union(newvals->subSequence(0+2,1)) ->append(val) else newvals->append(val) endif ) else Sequence{1..vals2->at(2+1)}->iterate( i : Integer ; vals3 : Sequence(Integer) = vals2 | trans(P21,3) ) endif ) )->first
Sequence{1..1}->iterate( i : Integer ; vals1 : Sequence(Integer) = {0,n,m} | Sequence{1..2}->iterate( step : Integer ; vals2 : Sequence(Integer) = vals1 | if step = 1 then vals2->iterate( val : Integer ; newvals : Sequence(Integer) = Sequence{} | if newvals->size = 1 then (newvals->subSequence(1,0)) ->append(val+0) ->union(newvals->subSequence(0+2,1)) ->append(val) else newvals->append(val) endif ) else Sequence{1..vals2->at(2+1)}->iterate( i : Integer ; vals3 : Sequence(Integer) = vals2 | vals3->iterate( val : Integer ; newvals : Sequence(Integer) = Sequence{} | if newvals->size = 0 then newvals->append(val+1) else newvals->append(val) endif ) ) endif ) )->first
We now prove that the OCL expression defined in terms of a LOOP-program computes the same function.
By IH, for any natural numbers , for any natural number , if the variable x_{i} changes its value from m_{i} to m'_{i} ( i=1,...,r) after the execution of P', then vals_{n} changes its value from {m_{0},...,m_{r} } {m'_{0},...,m'_{r} } , in particular for n=k+1.
Therefore, if vals_{k} = {l_{0},...,l_{r}} then vals_{k}->at(j+1)= l_{j}, vals_{k+1} is initialized by with the value of vals_{k}, and if after l_{j} successive executions of P' the variable x_{i} changes its value from l_{i} to l'_{i}, then after l_{j} successive executions of vals_{k+1} changes its value from {l_{0},...,l_{r} } {l'_{0},...,l'_{r} }
Given that the last value of vals_{k+1} is the return value of , the thesis holds.
This case is also trivial by IH.
Hence, every LOOP-computable function is also computable using an OCL expression.
Consider now the WHILE construct of WHILE-programs. The iterating construct iterate runs through a collection (randomly ordered if not a sequence) from its beginning to its end. Thus, an iterate terminates if, and only if, the collection is finite. Notice that, on the one hand and according to [RAT97, p. 13], there are three ways of getting a collection:
Set{1,2,5,3}
, or
In any way, an iterate either performs a previously determined number of iterations or does not terminate, since there is no possibility of interrupting an iterate (like e.g. the break command of C). In other words, the WHILE construct cannot be encoded in OCL, and thus semidecidable problems in general cannot be solved in OCL.
Therefore, given that the class of primitive recursive functions coincides with the class of LOOP-computable functions and that the class of -recursive functions coincides with the class of WHILE-computable functions (see [Sch95]), OCL allows only for the definition of primitive recursive functions (or totally undefined functions if Integer.allInstances is a valid OCL expression).