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

Question

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

我想做这样的事情：

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

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

Answer 1

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

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

Answer 2

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

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

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

Printing to console in VDM++?