Часы VDM++

Question

Я реализовал генератор случайных чисел в vdm++. Но я хотел, чтобы семя было часами с компьютера. Кто-нибудь знает, существует ли эквивалентная функция vdm ++ функции C++ time(NULL)?

Спасибо.

Answer 1

Не существует встроенной библиотеки для системного времени, например time(NULL) но легко создать такую ​​функцию в Java и связать ее с вашей моделью, если вы используете Overture IDE для VDM.

В руководстве пользователя Overture есть раздел об этом: 14.1 Определение собственных библиотек Java, которые будут использоваться из Overture.

Вы должны создать файл jar с классом java, который даст вам системное время, например:

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() для получения системного времени.