VDM ++時鐘時間

Question

我在vdm ++中實現了一個隨機數發生器。但我想讓種子成爲計算機的時鐘。有誰知道是否有一個等效的vdm ++函數C++函數time(NULL)？

謝謝。

Answer 1

不存在任何內置庫來獲取像time(NULL)這樣的系統時間，但是如果您使用Overture IDE進行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 

然後把瓶子和VDM文件的項目裏面是這樣的： 項目根/ lib/ systemtime.jar systemtime.vdmpp

現在您可以使用VDM操作SystemTime`time（）獲取系統時間。