在VDM++中打印到控制台？

Question

如何将文本或值打印到控制台以验证我的模型是否正常工作？

我想做这样的事情：

class Main
operations
    public Run: () ==> ()
    Run() ==
        print "Text"
        print mon.Func()
end Main

这似乎是可能的，但我就是想不出该怎么做。

Answer 1

Nick Battle回答了我的问题，但对于VDM的其他初学者来说，他的答案中缺少一个细节，即如何包含库。

在使用IO库之前，您首先必须包含它。我正在使用Overture，要将库包含到您的项目中，您必须右键单击侧边菜单中的项目，然后按New > Add VDM Library。然后，您可以选择要包含在弹出菜单中的库。在这里您选择IO。

在此之后，您应该能够使用IO`println(val)函数打印值。

Answer 2

您需要使用VDM IO库。有几个操作可以完成您想要的操作- println (用于打印固定值)和printf，它具有参数替换。例如，您可以调用IO`println("hello")。

在Overture和VDMJ的最新版本中，您还可以使用VDM注释来打印值，而无需向规范本身的“内容”添加任何内容。注释是作为注释添加的。参见@Printf。