Описание тега vdm-sl

Описание тега Вопросы с тегом
A language for the design and specification of systems, supporting the Vienna Development Method. The VDM language is supported by the Overture Tool.
1 ответ

Перевод VDM в Изабель

Я пытаюсь перевести модель VDM на Изабель, но почему-то, что я делаю, не работает Следующий пример - функция VDM моей модели Dot_Move_invariant: Dot * Dot -> bool Dot_Move_invariant(d1, d2) == d1 < d2 and let coordinate_1 = Dot_Coord(d1) in le…
12 дек '17 в 20:55
1 ответ

Есть ли уроки для VDM-SL Toolbox

Я пытаюсь работать с VDM-SL Toolbox, но не могу найти учебники. Если у кого-то есть какие-то учебники, пожалуйста, поделитесь. Спасибо
14 окт '16 в 14:41
1 ответ

Неявные функции: карри и тотальность

При указании неявной функции в VDM-SL возможно ли указать карри функцию? В следующих тестах test1 и test2 - явные функции без кеширования и с карри, а test3 - неявная функция без кеширования. Все принимаются Увертюрой. test4 - это попытка неявной фу…
07 фев '16 в 07:15
1 ответ

Особенности функций и типов продукции

В чем разница между типами (seq of nat * seq of nat) -> nat а также seq of nat * seq of nat -> nat Согласно справочному руководству по языку * имеет более высокий приоритет, чем -> поэтому скобки не имеют никакого эффекта; семантически один…
23 июн '17 в 06:53
1 ответ

Обозначение VDM-SL для одного конечного подмножества

Не уверен, что это в рамках SO, но: Используя VDM-SL, я искал "лучший" способ описания одного конечного подмножества ℕ. В своих путешествиях я нашел несколько способов, которыми люди передают это, но мне интересно, какой из них является наиболее при…
18 фев '15 в 16:42
1 ответ

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

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

От неявных к явным определениям функций

Я создавал спецификации, используя неявные определения функций в VDM-SL, и это сработало очень хорошо. Теперь я хочу создать прототип спецификации, используя явные определения функций (на данном этапе никаких операций). Один из способов сделать это …
08 фев '16 в 20:27
2 ответа

VDMSL Рекурсивная функция минимальное значение последовательности

Я думаю, что это должно быть относительно просто, было интересно, если бы кто-нибудь знал, как ответить на это: Определите рекурсивную функцию seq-min: N+ -> N, которая возвращает наименьшее значение в последовательности натуральных чисел. Я думал ч…
02 июн '14 в 21:55
0 ответов

Как бы я посчитал промежуточную сумму в последовательности? - VDM-SL

Я только начинаю с VDM-SL и мне нужно выяснить, как рассчитать общую стоимость последовательности предметов. У меня есть следующие типы: types Item :: id : token cost : nat; Box = seq of Item; И мне нужно выполнить следующую функцию, которая вычисли…
04 июн '19 в 18:47
1 ответ

У меня есть две ошибки в проекте vdm sl: 1) Action = <OPEN_BARRIER>; 2) Время :: час: нац;

Модель умной парковки в vdm-sl типы Id = token; Status = <EMPTY> | <OCCUPIED>; Type = <A> | <B> | <C> | <D> | <E>; Node :: id : Id status : Status indegree : nat outdegree : nat type : Type dist : int inv mk…
14 окт '19 в 13:58
1 ответ

Невозможно вернуть каждый элемент из набора при его прохождении через цикл for all

Я пытаюсь вернуть каждый элемент из набора, содержащего объекты Brewage, запустив его через цикл for all. Но возвращаемое значение теряется, когда я пытаюсь это сделать. Функция цикла: public pure Scan: set of Brewage ==> Brewage Scan(brewage) ==…
29 окт '19 в 01:20
1 ответ

Как мне преобразовать / оперировать набором / последовательностью?

У меня есть набор S = { 1, 2, 3, 4, 5 }. Каков синтаксис для изменения содержимого набора (или, скорее, создания нового набора) путем применения к нему математической операции, например умножения, степени?
05 фев '20 в 17:24
1 ответ

Как я могу применить предикат к набору?

Скажем, у меня есть набор, S = { 1, 2, 3, 4 } (содержание не имеет значения) я могу сказать forall x in set S & x mod 2 = 0но это даст мне логический ответ - все ли в нем числа четны? Что, если я хочу увидеть всех участников набора, для которыхx…
05 фев '20 в 15:40
0 ответов

Любой инструмент для преобразования требований NL в формальный язык спецификации с использованием VDM

У меня вопрос относительно VDM++ а также VDM-slинструмент. Есть ли какой-нибудь инструмент, в котором мы просто пишем пример использования требований, и он преобразуется вVDM на основе формального языка спецификации.
12 фев '20 в 08:42
1 ответ

VDM-SL - функция принимает набор целых чисел и возвращает идентичный набор

Попытка найти функцию, которая принимает целое число и возвращает неотрицательное значение этого целого числа, которое я выяснил Abs : int -> nat Abs(num) == if num < 0 then -num else num; теперь я пытаюсь создать другую функцию, которая прини…
06 ноя '19 в 00:42
2 ответа

Оператор суммирования наборов / последовательностей?

У меня есть набор, S = { 1, 2, 3, 4, 5 }. Если бы я хотел суммировать это в стандартной логике, это просто ∑S (нет MathJax на SO, поэтому я не могу это хорошо отформатировать). Какой эквивалент VDM? Я не вижу ничего в разделе числовых значений / наб…
05 фев '20 в 19:07
0 ответов

{VDM-SL} Предложите решение с фиксированной точкой для функционального

Предложите решение с фиксированной точкой для функционала T1(F, x, y) == if x = 0 then 1 else y * F(x-1,y) Я не отвечал на вопрос, который использовал две переменные, такие как x & Итак, когда дело доходит до решения этой проблемы, я не знаю, ко…
13 мар '21 в 01:48
2 ответа

Ошибка типа VDM++: здесь нельзя использовать компонент состояния totalPrice.

Я написал код, который рассчитывает общую стоимость книги, умноженную на количество книги и цену книги в VDM++. class Book types public Title = seq of char; instance variables private bookTitle: Title; private numberOfPages: nat1; private totalPrice…
05 дек '21 в 16:37
1 ответ

В чем разница между неявным и явным в VDM-SL

Итак, как понятно из названия, в чем разница между неявным и явным? Является ли неявная функция и явная операция? или это неявный предварительный код и явные спецификации самой VDM-SL? я немного запутался
21 янв '22 в 04:13