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

Question

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

我想做这样的事情：

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

这似乎是可能的，但我只是不知道该怎么做。

score 1 · Accepted Answer

您需要使用 VDM IO 库。有几个操作可以满足您的需求 - println（用于打印固定值）和具有参数替换的 printf。例如，你会调用 IO`println("hello")。

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

score 0 · Accepted Answer

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

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

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

2 回答 2