VDM++时钟时间

Question

我用vdm++实现了一个随机数生成器。但是我想把种子设为计算机的时钟时间。有没有人知道是否有与c++函数time(NULL)等价的vdm++函数

谢谢。

Answer 1

没有像time(NULL)这样的内置库来获取系统时间，但是如果您正在使用Overture IDE for VDM，那么在Java语言中创建这样一个函数并将其链接到您的模型是很容易的。

序曲用户指南中有一节介绍了这一点：14.1 Defining Your Own Java Libraries to be used from 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()来获取系统时间。