Чистый вызов операции может быть непрозрачным с точки зрения ссылок?

Я получаю это предупреждение, когда пытаюсь использовать чистую операцию для двух первых элементов последовательности.

Код выглядит примерно так:

class A
functions
  public func: Seq -> bool
  func(sq) == (
    (hd sq).pureOperation() inter (hd (tl sq)).pureOperation() <> {}
  );
end A

В результате появляется предупреждение: Чистый вызов операции может быть непрозрачным с точки зрения ссылок, а Overture помещает волнистые желтые линии под hd функциями.

Что вызывает это предупреждение и что я могу с этим сделать?


vdm++
person SørenHN    schedule 02.12.2019    source источник
comment
Это также можно сделать так: sq(1).pureOperation() inter sq(2).pureOperation() <> {} но все равно выдает такое же предупреждение.   -  person SørenHN    schedule 02.12.2019

Ответы (1)


arrow_upward
1
arrow_downward

Это предупреждение явилось результатом серьезных дебатов, когда в определение языка были добавлены чистые операции. Проблема в том, что, в конце концов, даже если операция помечена как чистая (и подчиняется всем последующим правилам), мы не можем быть уверены, что вызов операции с одними и теми же аргументами всегда будет давать одно и то же значение. Это необходимо для ссылочной прозрачности в функциях, поэтому мы выдаем предупреждение.

Предупреждение появляется только тогда, когда из функций вызываются чистые операции, но нет никакого способа избежать предупреждения, если вам нужно это сделать.

Например, рассмотрим следующее: операция pure_i является «чистой», так как она просто возвращает значение состояния, но это состояние может быть изменено операцией not_transparent, поэтому функция f(x) будет возвращать разные значения для одного и того же аргумента. :

class A
instance variables
    static public i : nat := 0

operations
    static public pure pure_i : () ==> nat
    pure_i() == return i;

functions
    f : nat -> nat
    f(x) == pure_i() + x;

operations
    static public not_transparent : () ==> ()
    not_transparent() == (
        i := 1;
    );
end A
person Nick Battle    schedule 03.12.2019
comment
Еще один момент: предупреждение не выдается, если функция, вызывающая чистую операцию, является чем-то неявным, например выражением предусловия или постусловия. - person Nick Battle; 03.12.2019
comment
Будет ли лучшим решением вместо этого сделать чистую операцию? - person SørenHN; 03.12.2019
comment
Это позволит избежать предупреждения, но мне нужно понять остальную часть вашей модели, чтобы действительно прокомментировать. Это зависит от того, откуда берется последовательность объектов. Если последовательность является частью состояния другого объекта, может иметь смысл иметь операцию над этим объектом, которая обрабатывает первые два элемента (с предварительным условием, что есть по крайней мере два элемента!) - person Nick Battle; 03.12.2019