clock - VDM++ 时钟时间

Question

我在 vdm++ 中实现了一个随机数生成器。但我想种子是来自计算机的时钟时间。有谁知道是否有与 c++ 函数等效的 vdm++ 函数time(NULL)？

谢谢你。

Answer 1

不存在任何内置库来获取系统时间，time(NULL)但如果您使用 Overture IDE for VDM，很容易在 Java 中创建这样的函数并将其链接到您的模型。

Overture 用户指南有一个关于此的部分：14.1 定义您自己的 Java 库以从 Overture 中使用。

您必须使用 java 类创建一个 jar 文件，该类为您提供系统时间，如下所示：

public class SystemTime
{
    public static Value time()
    {
        return new RealValue(System.currentTimeMillis());
    }
}

及其 VDM 对应物：

class SystemTime

operations
public static time : () ==> real
time() == is not yet specified;

end SystemTime

然后将 jar 和 vdm 文件放入项目中，如下所示： Project root/lib/systemtime.jar systemtime.vdmpp

现在您可以使用 VDM 操作 SystemTime`time() 来获取系统时间。