Описание тега vdm++

Описание тега Вопросы с тегом
Язык для проектирования и спецификации систем, основанный на Венском методе разработки. VDM++ поддерживает объектно-ориентированные и параллельные спецификации. Язык VDM поддерживается программой Overture Tool.
2 ответа

Как установить Overture на Windows

Я запускаю Widows 7 Professional в 64-битной системе с Java SE 10. Я скачал Overture-2.6.2-win32.win32x86-64.zip и разархивировал его под c: и нажал на приложение Overture. Это началось и попросило путь к рабочей области. Я взял по умолчанию, но это…
15 окт '18 в 21:50
1 ответ

Температурные логические выражения

Я работаю над некоторыми логическими выражениями. Я хочу объединить 2 выражения в одно, но не совсем точно, как. Я использую VDM Overture Tool. Я смотрю на набор из 5 температур. Некоторым за 400, некоторым под и т.д. Мое первое выражение верно, ког…
18 фев '13 в 15:47
1 ответ

Инструмент увертюры в Debian каждый раз дает сбой

Я установил Debian 7 на свой компьютер. Я установил Overture Tool, скачав и распаковав ZIP-файл. Каждый раз, когда я пытаюсь запустить Overture, я получаю следующее сообщение об ошибке: # A fatal error has been detected by the Java Runtime Environme…
02 сен '15 в 11:18
1 ответ

Как округлить вещественное число?

Скажем, я хотел округлить действительное число до натурального числа, как я могу сделать это в VDM++? Библиотека MATH, похоже, не имеет какой-либо функции, которая делает это. Спасибо Рикардо
28 дек '16 в 11:58
2 ответа

Modelio и Overture, это работает отдельно?

Итак... Я пытаюсь работать как с Modelio, так и с Overture, но обе программы действительно новые для меня. Я хочу сначала сделать модель в Modelio, а затем экспортировать ее в Overture. Но должно ли это работать так, или я должен сделать это отдельн…
04 янв '17 в 10:11
2 ответа

Формальные методы - Карта цен, относящая автомобили к цене с двумя наборами BL и Fiat

У меня есть вопрос из главы 5 "Практические формальные методы с VDM" Дерека Эндрюса и Даррела INCE, на который я не был уверен, как ответить, так что вот, спасибо за любую помощь! Если цена на карте соотносит автомобили с их ценой, в набор BL входят…
29 май '14 в 17:43
1 ответ

Набор инструментов VDM++: операция или функция не входят в область действия, используя пример реализации дерева

Я использую определение дерева, которое поставляется с VDM++ Toolbox v9.0.2 и, при попытке использовать функцию addRoot() (с использованием интерпретатора), при первом использовании я всегда получаю ошибку: "Ошибка времени выполнения 266: Операция и…
13 ноя '13 в 12:52
1 ответ

Ошибка в конструкторе VDM++

Я получаю глупую ошибку в VDM++ ToolBox Academic. Когда я пытаюсь запустить операцию, это дает мне эту ошибку: Run-Time Error 280: No constructor with this parameter list is in scope value: "Game" Мой конструктор: public Game: Date * Team * Team ==&…
03 дек '12 в 14:59
2 ответа

Исполнение при наличии привязок типов

Рассмотрим два определения функций test1 (x:nat) res:set of nat == { m | m:nat & m in set {0,...,x} }; test2 (x:nat) res:set of nat == { m | m in set {0,...,x} & true }; Запуск test2(1000) в Overture дает набор натуральных чисел до 1000. Зап…
14 фев '16 в 03:30
1 ответ

Увертюра и математический синтаксис

Можно ли использовать математический синтаксис VDM с Overture или он ограничен синтаксисом ASCII. В качестве альтернативы, при генерации LaTeX, может ли математический синтаксис использоваться для вывода? Я едва использовал LaTeX. Я попытался взять …
08 фев '16 в 08:18
4 ответа

Глубина рекурсивного стека вызовов

У меня есть рекурсивная функция, которая работает для ввода, где глубина стека вызовов до 1000, но не работает для больших входов. Я преобразовал функцию в хвостовую рекурсию, и это позволило ей достичь 1350. Каковы пределы и есть ли способ увеличит…
14 фев '16 в 01:02
1 ответ

Переменная экземпляра не инициализирована. Это почему?

Я получил эту проблему с моими переменными экземпляра. Они не будут инициализированы, и я не уверен, что именно означает. Это то же самое для каждого класса, который у меня есть. Я разместил один из кодов ниже: class Good types public evalGood :: go…
06 янв '17 в 08:54
1 ответ

Что означают противоположные угловые скобки <>?

Пример 1 forall x,y in set {1,…,5} &amp; X &lt;&gt; y =&gt; not m.temps(x) = m.temps(y) Пример 2 exists i,j in set inds m.temps &amp; i &lt;&gt; j and m.temps(i) &gt; 400 and m.temps(j) &gt; 400 Что означает <> в этих предложениях?
30 окт '14 в 13:08
2 ответа

Установить понимание в VDM++

Я определил 2 типа: public string = seq1 of char; public config = map string to bool; Я также определил набор тестов: dcl subFeatures : set of string := {"test1", "test2", "test3"}, И я пытаюсь создать набор допустимых конфигов: { elem | elem : conf…
05 фев '17 в 23:02
1 ответ

Увертюра /Stackru/VDM проекты повреждены / исчезли

Я провел последние 2 недели, работая над учебной работой в колледже, и я почти закончил ее на 90%. Я решил открыть Overture сейчас и похоже, что все мои проекты повреждены: (((((( http://gyazo.com/8e25549bbca700a22399e736a88a1996 Если у кого-то есть…
29 мар '15 в 18:10
1 ответ

Импортировать модуль из другого проекта в Overture

Когда я импортирую один модуль из другого в Overture, все довольно просто. Однако я не могу понять, как импортировать модуль из другого проекта. Что я делаю, это: создать проект P1 создать модуль A в P1 создать проект P2 укажите P1 в качестве ссылки…
09 фев '16 в 08:34
0 ответов

modelio не импортирует экспортированный файл увертюры uml

Я хочу научиться использовать Modelio и Overture вместе, чтобы научиться моделировать программы с UML и VDM. Вся процедура создания модели UML, ее экспорта в XMI (расширение uml) и импорта в Overture выполнена успешно. Однако, когда я пытаюсь экспор…
11 фев '16 в 21:18
1 ответ

Генерация случайного числа в vdm++

Кто-нибудь знает, как генерировать случайное число в vdm++? Библиотека математики не работает для меня.
28 ноя '12 в 15:50
1 ответ

Рекурсивная функция в VDM

Как бы я определить рекурсивную функцию, чтобы найти наибольшую степень двух меньше, чем входное число в VDM? Функция выглядит следующим образом: наибольшее: N -> N Все, что у меня есть, это: самый большой (n) = если n=1, то 0 иначе, если n=2, то 1 …
27 май '17 в 21:06
1 ответ

Часы VDM++

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