VDM++工具箱:操作或函数不在使用示例树实现的范围内

Question

我使用的是VDM++工具箱v9.0.2附带的树定义，当尝试使用函数addRoot() (使用解释器)时，在第一次使用时，我总是得到错误：“运行时错误266:操作或函数不在作用域中”。如果我再次运行这个函数，它就能工作。为什么它会有这样的行为？

我正在添加VDM++工具箱附带的树代码。(请忽略类型和语法错误，因为我已经将它们全部修复，但仍然不起作用)

--启动代码-- Tree类

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

我很高兴你设法解决了这个问题。(对于测试)所有的操作都是受保护的是没有帮助的--尽管我担心它在第二次尝试时会不会起作用！

我使用Overture而不是VDMTools来尝试这个规范，看看有没有什么不同。当然，受保护的方法也存在同样的问题(您不能选择它们进行测试)。但它也指出了几个类型检查错误："nodes“cases语句需要一个"others”子句(如"others -> error")，否则操作可能返回空值；调用isEmpty()的前置条件实际上不应该这样做-您可以从前置条件调用函数，但不能调用操作，因为它们可能会更改模型的状态。因此，我将这些调用替换为"root =“。那就没问题了。

请参阅http://www.overturetool.org/