ModelicaSpecification icon indicating copy to clipboard operation
ModelicaSpecification copied to clipboard

Constraint on arrays used to determine implicit iterators.

Open qlambert-pro opened this issue 1 year ago • 2 comments

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;

qlambert-pro avatar Sep 28 '22 10:09 qlambert-pro

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.

henrikt-ma avatar Sep 28 '22 11:09 henrikt-ma

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).

HansOlsson avatar Sep 28 '22 21:09 HansOlsson