0

I'm using the Tree definition, that comes with The VDM++ Toolbox v9.0.2 and, when trying to use the function addRoot() (using the interpreter), on the first usage, I always get the error: "Run-Time Error 266: Operation or function is not in scope". If I run the function again, it works. Why does it have this behaviour?

I'm adding the Tree code that comes with VDM++ Toolbox. (Please ignore type and syntax errors, since I've fixed them all and it still won't work)

-- START CODE -- The Tree Class

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

-- END CODE --

4

1 回答 1

1

我很高兴你设法解决了这个问题。操作都受到保护是无益的（对于测试） - 尽管我担心它是否在第二次尝试中起作用！

我使用 Overture 而不是 VDMTools 尝试了规范，看看是否有任何不同。当然，受保护的方法也有同样的问题（你不能选择它们来测试）。但它也指出了几个类型检查错误：“nodes”case 语句需要一个“others”子句（如“others -> error”），否则操作可能返回 void 值；并且调用 isEmpty() 的前提条件确实不应该这样做 - 您可以从前提条件调用函数，但不能调用操作，因为它们可能会改变模型的状态。所以我用“root = <Empty>”替换了这些调用。然后就好了。

见http://www.overturetool.org/

于 2013-11-13T14:12:24.197 回答