ModelicaSpecification
ModelicaSpecification copied to clipboard
Constraint on arrays used to determine implicit iterators.
The specs say:
The size of an array - the iteration range - is evaluated on entry to the for-loop and the array size shall not change during the execution of the for-loop.
I suggests we remove the constraint on the fact that the size should not change during execution. There are three reasons why I think this is a good idea:
- Checking for that is undecidable in the general case
- The fact the size of the array is evaluated on entry to the for-loop catches most of the craziness
- We don't disallow it for explicit range
In other words I think the following model:
model VarArrayRange
function f
input Integer inN;
output Integer outN;
protected
Integer x[:];
Integer s;
algorithm
outN := 1;
x := ones(inN);
for i loop
s := size(x, 1);
x := ones(s - x[i]);
outN := outN * s;
end for;
end f;
Integer n = f(5);
end VarArrayRange;
should behave like
model VarArrayRange
function f
input Integer inN;
output Integer outN;
protected
Integer x[:];
Integer s;
algorithm
outN := 1;
x := ones(inN);
for i in 1:size(x, 1) loop
s := size(x, 1);
x := ones(s - x[i]);
outN := outN * s;
end for;
end f;
Integer n = f(5);
end VarArrayRange;
I'd prefer not allowing any assignment to the array as a whole inside the loop, as an easier requirement to formulate than that it should be possible to statically prove that any assignment maintains the size.
The reason I'd prefer this over removing the constraint is that I'd like the use of implicit range to be a safe and natural way to avoid indexing out of range.
I'd prefer not allowing any assignment to the array as a whole inside the loop, as an easier requirement to formulate than that it should be possible to statically prove that any assignment maintains the size.
I would also prefer this.
The reason I'd prefer this over removing the constraint is that I'd like the use of implicit range to be a safe and natural way to avoid indexing out of range.
Yes, and obviously assigning to specific elements is safe - like:
for i loop
x[i]=i;
end for;
Note that this suggestion also indicates how to check the current semantics; extract the size of the array at the start and assert that it is the same after each assignment to the entire array (if there are any).