Набор инструментов VDM++: операция или функция не входят в область действия, используя пример реализации дерева

Question

Я использую определение дерева, которое поставляется с VDM++ Toolbox v9.0.2 и, при попытке использовать функцию addRoot() (с использованием интерпретатора), при первом использовании я всегда получаю ошибку: "Ошибка времени выполнения 266: Операция или функция не входят в объем ". Если я снова запускаю функцию, она работает. Почему у него такое поведение?

Я добавляю код дерева, который поставляется с VDM++ Toolbox. (Пожалуйста, игнорируйте ошибки типа и синтаксиса, так как я исправил их все, и это все равно не будет работать)

- START CODE - Класс дерева

class Tree

types

protected 
tree = <Empty> | node;

public
node :: lt: Tree
        nval : int
        rt : Tree

instance variables
protected
root: tree := <Empty>;



operations

protected
nodes : () ==> set of int
nodes () ==
  cases root:
    <Empty> -> return ({}),
    mk_node(lt,v,rt) -> return(lt.nodes() union {v} union rt.nodes())
  end ;

protected
addRoot : int ==> ()
addRoot (x) ==
  root := mk_node(new Tree(),x,new Tree());

protected
rootval : () ==> int
rootval () == return root.nval
pre root <> <Empty>;

protected
gettree : () ==> tree
gettree () == return root;

protected
leftBranch : () ==> Tree
leftBranch () == return root.lt
pre not isEmpty();

protected
rightBranch : () ==> Tree
rightBranch () == return root.rt
pre not isEmpty();

protected
isEmpty : () ==> bool
isEmpty () == return (root = <Empty>);

end Tree

- КОНЕЦ КОДА -

Answer 1

Я рад, что вам удалось разобраться с этим. Бесполезно (для тестирования), что все операции защищены - хотя я волнуюсь, работает ли это со 2-й попытки!

Я попробовал спецификацию, используя Overture, а не VDMTools, чтобы увидеть, было ли это иначе. Конечно, у него та же проблема с защищенными методами (вы не можете выбрать их для тестирования). Но он также указывает на несколько ошибок проверки типов: для оператора case "узлов" требуется предложение "другие" (например, "другие -> ошибка"), в противном случае операция может вернуть значение void; и предварительные условия, которые вызывают isEmpty(), на самом деле не должны этого делать - вы можете вызывать функции из предварительного условия, но не операции, так как они могут изменить состояние модели. Поэтому я заменил эти вызовы на "root = ". Тогда все в порядке.

Смотрите http://www.overturetool.org/