Венский метод развития

Венский метод разработки ( VDM ) — один из старейших формальных методов разработки компьютерных систем. Возникло на основе работы, проделанной в лаборатории IBM в Вене. в 1970-е годы он расширился и включил в себя группу методов и инструментов, основанных на формальном языке спецификаций — языке спецификаций VDM (VDM-SL). Имеет расширенную форму VDM++. который поддерживает моделирование объектно-ориентированных и параллельных систем. Поддержка VDM включает коммерческие и академические инструменты для анализа моделей, включая поддержку тестирования и проверки свойств моделей, а также создания программного кода на основе проверенных моделей VDM. Существует история промышленного использования VDM и его инструментов, а растущий объем исследований в области формализма привел к заметному вкладу в разработку критических систем, компиляторов , параллельных систем и логики для информатики .

Философия

Вычислительные системы можно моделировать в VDM-SL на более высоком уровне абстракции, чем это возможно с использованием языков программирования, что позволяет анализировать конструкции и выявлять ключевые особенности, включая дефекты, на ранней стадии разработки системы. Модели, прошедшие валидацию, могут быть преобразованы в подробные проекты систем посредством процесса уточнения. Язык имеет формальную семантику, позволяющую доказывать свойства моделей с высоким уровнем достоверности. Он также имеет подмножество исполняемых файлов, поэтому модели можно анализировать путем тестирования и выполнять через графические пользовательские интерфейсы, чтобы модели могли оцениваться экспертами, которые не обязательно знакомы с самим языком моделирования.

История

Истоки VDM-SL лежат в IBM в Вене где первая версия языка называлась Венским определений языком лаборатории , (VDL). VDL по существу использовался для описания операционной семантики в отличие от VDM - Meta-IV, который предоставлял денотационную семантику.

«К концу 1972 года Венская группа вновь обратила внимание на проблему систематической разработки компилятора из определения языка. Принятый общий подход получил название «Венский метод разработки»... Фактически принятый метаязык («Мета-IV») используется для определения основных частей PL/1 (как указано в ECMA 74 – что интересно, «формального документ о стандартах, написанный как абстрактный интерпретатор») в BEKIČ 74.»

нет связи Между Мета-IV , и язык Шорре META II или его преемник Tree Meta ; это были системы компилятор-компилятор, а не подходящие для формального описания проблем.

Таким образом, Meta-IV «использовался для определения основных частей» языка программирования PL/I . Другие языки программирования, ретроспективно описанные или частично описанные с использованием Meta-IV и VDM-SL, включают язык программирования BASIC , FORTRAN , язык программирования APL , ALGOL 60, язык программирования Ada и язык программирования Pascal . Мета-IV развилась в несколько вариантов, обычно называемых датской, английской и ирландской школами.

«Английская школа» возникла на основе работ Клиффа Джонса по аспектам VDM, не связанным конкретно с определением языка и проектированием компилятора (Джонс 1980, 1990). Он подчеркивает необходимость моделирования постоянных состояние посредством использования типов данных, созданных на основе богатой коллекции базовых типов. Функциональность обычно описывается с помощью операций, которые могут иметь побочные эффекты на состояние и которые обычно указываются неявно с использованием предварительного и постусловия. «Датская школа» ( Bjørner et al., 1982) склонна подчеркивать конструктивный подход с четкими операционными спецификациями, используемыми в большей степени. Работа в датской школе привела к созданию первого проверенного в Европе компилятора Ada .

Стандарт ISO для этого языка был выпущен в 1996 году (ISO, 1996).

Возможности VDM

Синтаксис и семантика VDM-SL и VDM++ подробно описаны в руководствах по языку VDMTools и в доступных текстах. Стандарт ISO содержит формальное определение семантики языка. В оставшейся части этой статьи используется синтаксис обмена, определенный ISO (ASCII). Некоторые тексты предпочитают более краткий математический синтаксис .

Модель VDM-SL — это описание системы, данное с точки зрения функциональности, выполняемой с данными. Он состоит из серии определений типов данных и функций или операций, выполняемых над ними.

Основные типы: числовые, символьные, токены и типы кавычек

VDM-SL включает следующие основные типы номеров и символов моделирования:

Основные типы

bool	Логический тип данных	ложь, правда
nat	натуральные числа (включая ноль)	0, 1, 2, 3, 4, 5 ...
nat1	натуральные числа (кроме нуля)	1, 2, 3, 4, 5, ...
int	целые числа	..., −3, −2, −1, 0, 1, 2, 3, ...
rat	рациональные числа	а/б , где а и b — целые числа, б нет 0
real	действительные числа	...
char	персонажи	А, Б, В, ...
token	бесструктурные токены	...
<A>	тип котировки, содержащий значение <A>	...

Типы данных определяются для представления основных данных моделируемой системы. Каждое определение типа вводит новое имя типа и дает представление в терминах базовых типов или в терминах уже введенных типов. Например, идентификаторы пользователей, моделирующие тип системы управления входом в систему, могут быть определены следующим образом:

types
UserId = nat

Для управления значениями, принадлежащими типам данных, для значений определяются операторы. Таким образом, обеспечивается сложение, вычитание и т. д. натуральных чисел, а также логические операторы, такие как равенство и неравенство. Язык не фиксирует максимальное или минимальное представимое число или точность действительных чисел. Такие ограничения определяются там, где они необходимы в каждой модели, с помощью инвариантов типа данных — логических выражений, обозначающих условия, которые должны соблюдаться всеми элементами определенного типа. Например, требование, чтобы идентификаторы пользователей были не больше 9999, можно было бы выразить следующим образом (где <= — это логический оператор «меньше или равно» для натуральных чисел):

UserId = nat
inv uid == uid <= 9999

Поскольку инварианты могут быть сколь угодно сложными логическими выражениями, а принадлежность к определенному типу ограничивается только теми значениями, которые удовлетворяют инварианту, правильность типа в VDM-SL не определяется автоматически во всех ситуациях.

Другие базовые типы включают char для символов. В некоторых случаях представление типа не соответствует цели модели и только усложнит ее. В таких случаях члены типа могут быть представлены как бесструктурные токены. Значения типов токенов можно сравнивать только на предмет равенства — для них не определены другие операторы. Если требуются определенные именованные значения, они представляются как типы цитат. Каждый тип котировки состоит из одного именованного значения с тем же именем, что и сам тип. Значения типов кавычек (известных как литералы кавычек) можно сравнивать только на предмет равенства.

Например, при моделировании контроллера светофора может быть удобно определить значения для представления цветов светофора в виде типов котировок:

<Red>, <Amber>, <FlashingAmber>, <Green>

Конструкторы типов: объединение, произведение и составные типы

Сами по себе базовые типы имеют ограниченную ценность. Новые, более структурированные типы данных создаются с использованием конструкторов типов.

Конструкторы базового типа

T1 | T2 | ... | Tn	Союз типов T1,...,Tn
T1*T2*...*Tn	Декартово произведение типов T1,...,Tn
T :: f1:T1 ... fn:Tn	Композитный (запись) тип

Самый простой конструктор типов образует объединение двух предопределенных типов. Тип (A|B) содержит все элементы типа A и все элементы типа B. В примере контроллера светофора тип, моделирующий цвет светофора, можно определить следующим образом:

SignalColour =  <Red> | <Amber> | <FlashingAmber> | <Green>

Перечисляемые типы в VDM-SL определяются, как показано выше, как объединения типов кавычек.

Декартовы типы продуктов также могут быть определены в VDM-SL. Тип (A1*…*An) — тип, состоящий из всех кортежей значений, первый элемент которых принадлежит типу A1 и второй из типа A2 и так далее. Составной тип или тип записи представляет собой декартово произведение с метками для полей. Тип

T :: f1:A1
     f2:A2
     ...
     fn:An

является декартовым произведением с полями, помеченными f1,…,fn. Элемент типа T может быть составлен из составных частей конструктором, написанным mk_T. И наоборот, если задан элемент типа T, имена полей можно использовать для выбора именованного компонента. Например, тип

Date :: day:nat1
        month:nat1
        year:nat
inv mk_Date(d,m,y) == d <=31 and m<=12

моделирует простой тип даты. Значение mk_Date(1,4,2001) соответствует 1 апреля 2001 г. Учитывая дату d, выражение d.month — натуральное число, обозначающее месяц. При желании в инвариант можно включить ограничения по дням в месяце и високосным годам. Объединив это:

mk_Date(1,4,2001).month = 4

Коллекции

Типы коллекций моделируют группы значений. Наборы — это конечные неупорядоченные коллекции, в которых дублирование значений подавлено. Последовательности — это конечные упорядоченные коллекции (списки), в которых может произойти дублирование, а отображения представляют собой конечные соответствия между двумя наборами значений.

Наборы

Конструктор типа множества (написанный set of T где T является предопределенным типом) конструирует тип, состоящий из всех конечных наборов значений, взятых из типа T. Например, определение типа

UGroup = set of UserId

определяет тип UGroup состоящее из всех конечных множеств UserId ценности. На множествах определяются различные операторы для построения их объединения, пересечений, определения правильных и нестрогих отношений подмножеств и т. д.

Основные операторы на множествах (s, s1, s2 — множества)

{a, b, c}	Перечисление Set: набор элементов a, b и c
{x | x:T & P(x)}	Понимание множества: набор x из типа T такой, что P(x)
{i, ..., j}	Набор целых чисел в диапазоне i к j
e in set s	e является элементом множества s
e not in set s	e не является элементом множества s
s1 union s2	Союз наборов s1 и s2
s1 inter s2	Пересечение множеств s1 и s2
s1 \ s2	Разница сетов s1 и s2
dunion s	Распределенное объединение множества множеств s
s1 psubset s2	s1 является (собственным) подмножеством s2
s1 subset s2	s1 — это (слабое) подмножество s2
card s	Мощность множества s

Последовательности

Конструктор типа конечной последовательности (записанный seq of T где T является предопределенным типом) конструирует тип, состоящий из всех конечных списков значений, взятых из типа T. Например, определение типа

String = seq of char

Определяет тип String состоит из всех конечных строк символов. В последовательностях определены различные операторы для построения конкатенации, выбора элементов и подпоследовательностей и т. д. Многие из этих операторов являются частичными в том смысле, что они не определены для определенных приложений. Например, выбор 5-го элемента последовательности, содержащей только три элемента, не определен.

Порядок и повторение элементов в последовательности имеют значение, поэтому [a, b] не равен [b, a], и [a] не равен [a, a].

Основные операторы над последовательностями (s, s1,s2 — последовательности)

[a, b, c]	Перечисление последовательности: последовательность элементов a, b и c
[f(x) | x:T & P(x)]	Понимание последовательности: последовательность выражений f(x) для каждого x (числового) типа T такой, что P(x) держит ( x значения взяты в числовом порядке)
hd s	Голова (первый элемент) s
tl s	Хвост (оставшаяся последовательность после удаления головы) s
len s	Длина s
elems s	Набор элементов s
s(i)	The iй элемент s
inds s	набор индексов для последовательности s
s1^s2	последовательность, образованная путем объединения последовательностей s1 и s2

Карты

Конечное отображение — это соответствие между двумя множествами, доменом и диапазоном, с элементами индекса домена диапазона. Следовательно, она аналогична конечной функции. Конструктор типа отображения в VDM-SL (написан map T1 to T2 где T1 и T2 являются предопределенными типами) конструирует тип, состоящий из всех конечных отображений из наборов T1 значения для наборов T2 ценности. Например, определение типа

Birthdays = map String to Date

Определяет тип Birthdays который сопоставляет строки символов с Date. Опять же, в отображениях определяются операторы для индексации в отображении, слияния отображений, перезаписи извлечения подотображений.

Основные операторы отображений

{a |-> r, b |-> s}	Перечисление сопоставления: a карты в r, b карты в s
{x |-> f(x) | x:T & P(x)}	Понимание картографии: x карты в f(x) для всех x для типа T такой, что P(x)
dom m	Домен m
rng m	Диапазон m
m(x)	m применяется к x
m1 munion m2	Союз картографов m1 и m2 ( m1, m2 должны быть последовательны там, где они перекрываются)
m1 ++ m2	m1 перезаписано m2

Структурирование

Основное различие между нотациями VDM-SL и VDM++ заключается в способе структурирования. В VDM-SL имеется обычное модульное расширение, тогда как в VDM++ имеется традиционный объектно-ориентированный механизм структурирования с классами и наследованием.

Структурирование в VDM-SL

В стандарте ISO для VDM-SL есть информативное приложение, содержащее различные принципы структурирования. Все они следуют традиционным принципам сокрытия информации с помощью модулей, и их можно объяснить следующим образом:

• Именование модуля : каждый модуль синтаксически начинается с ключевого слова module за которым следует имя модуля. В конце модуля ключевое слово end пишется, за которым снова следует имя модуля.
• Импорт : можно импортировать определения, экспортированные из других модулей. Это делается в разделе импорта , который начинается с ключевого слова imports а затем следует последовательность импортов из разных модулей. Импорт каждого из этих модулей начинается с ключевого слова from за которым следует имя модуля и подпись модуля. может Подпись модуля быть просто ключевым словом all указывающий на импорт всех определений, экспортированных из этого модуля, или это может быть последовательность сигнатур импорта. Сигнатуры импорта специфичны для типов, значений, функций и операций, и каждая из них начинается с соответствующего ключевого слова. Кроме того, эти подписи импорта называют конструкции, к которым требуется получить доступ. Кроме того, может присутствовать необязательная информация о типе и, наконец, можно переименовать каждую из конструкций при импорте. Для типов также необходимо использовать ключевое слово struct если кто-то хочет получить доступ к внутренней структуре определенного типа.
• Экспорт : определения из модуля, к которым другие модули должны иметь доступ, экспортируются с использованием ключевого слова exports за которым следует подпись модуля экспорта. Подпись модуля экспорта может просто состоять из ключевого слова all или как последовательность экспортных подписей. Такие сигнатуры экспорта специфичны для типов, значений, функций и операций, и каждая из них начинается с соответствующего ключевого слова. Если вы хотите экспортировать внутреннюю структуру типа, используйте ключевое слово struct необходимо использовать.
• Более экзотические возможности : В более ранних версиях инструментов VDM-SL также была поддержка параметризованных модулей и экземпляров таких модулей. Однако примерно в 2000 году эти функции были исключены из VDMTools, поскольку они почти никогда не использовались в промышленных приложениях, и с этими функциями возникало значительное количество проблем с инструментом.

Структурирование в VDM++

В VDM++ структурирование осуществляется с помощью классов и множественного наследования. Ключевые понятия:

• Класс : каждый класс синтаксически начинается с ключевого слова class за которым следует имя класса. В конце класса ключевое слово end пишется, за которым снова следует имя класса.
• Наследование : если класс наследует конструкции от других классов, за именем класса в заголовке класса могут следовать ключевые слова. is subclass of за которым следует список имен суперклассов, разделенных запятыми.
• Модификаторы доступа . Скрытие информации в VDM++ осуществляется так же, как и в большинстве объектно-ориентированных языков, с использованием модификаторов доступа. В VDM++ определения по умолчанию являются частными, но перед всеми определениями можно использовать одно из ключевых слов модификатора доступа: private, public и protected.

Функциональность моделирования

Функциональное моделирование

В VDM-SL функции определяются по типам данных, определенным в модели. Поддержка абстракции требует, чтобы была возможность охарактеризовать результат, который должна вычислить функция, без необходимости указывать, как он должен быть вычислен. Основным механизмом для этого является неявное определение функции , в котором вместо формулы, вычисляющей результат, логический предикат над входными и результирующими переменными, называемый постусловием , задает свойства результата. Например, функция SQRT для вычисления квадратного корня из натурального числа можно определить следующим образом:

SQRT(x:nat)r:real
post r*r = x

Здесь постусловие не определяет метод вычисления результата r но указывает, какие свойства можно предполагать присущими ему. Обратите внимание, что здесь определяется функция, которая возвращает действительный квадратный корень; нет требования, чтобы это был положительный или отрицательный корень. Приведенной выше спецификации будет удовлетворять, например, функция, которая возвращает отрицательный корень из 4, но положительный корень всех остальных допустимых входных данных. Обратите внимание, что функции в VDM-SL должны быть детерминированными , чтобы функция, удовлетворяющая приведенному выше примеру спецификации, всегда возвращала один и тот же результат для одного и того же ввода.

Более ограниченная спецификация функции достигается за счет усиления постусловия. Например, следующее определение ограничивает функцию возвратом положительного корня.

SQRT(x:nat)r:real
post r*r = x and r>=0

Все спецификации функций могут быть ограничены предварительными условиями , которые являются логическими предикатами только для входных переменных и описывают ограничения, которые предположительно удовлетворяются при выполнении функции. Например, функция вычисления квадратного корня, которая работает только с положительными действительными числами, может быть указана следующим образом:

SQRTP(x:real)r:real
pre x >=0
post r*r = x and r>=0

Предусловие и постусловие вместе образуют контракт , которому должна соответствовать любая программа, претендующая на реализацию функции. Предварительное условие записывает допущения, при которых функция гарантирует возврат результата, удовлетворяющего постусловию. Если функция вызывается на входных данных, которые не удовлетворяют ее предварительному условию, результат не определен (более того, завершение даже не гарантируется).

VDM-SL также поддерживает определение исполняемых функций наподобие функционального языка программирования. В явном определении функции результат определяется посредством выражения над входными данными. Например, функция, которая создает список квадратов списка чисел, может быть определена следующим образом:

SqList: seq of nat -> seq of nat
SqList(s) == if s = [] then [] else [(hd s)**2] ^ SqList(tl s)

Это рекурсивное определение состоит из сигнатуры функции, указывающей типы ввода и результата, а также тела функции. Неявное определение той же функции может иметь следующий вид:

SqListImp(s:seq of nat)r:seq of nat
post len r = len s and
     forall i in set inds s & r(i) = s(i)**2

Явное определение в простом смысле является реализацией неявно заданной функции. Корректность явного определения функции по отношению к неявной спецификации можно определить следующим образом.

Учитывая неявную спецификацию:

f(p:T_p)r:T_r
pre pre-f(p)
post post-f(p, r)

и явная функция:

f:T_p -> T_r

мы говорим, что он удовлетворяет спецификации тогда и только тогда :

forall p in set T_p & pre-f(p) => f(p):T_r and post-f(p, f(p))

Так, " f является правильной реализацией» следует интерпретировать как « f соответствует спецификации».

Моделирование на основе состояний

В VDM-SL функции не имеют побочных эффектов, таких как изменение состояния постоянной глобальной переменной. Это полезная возможность во многих языках программирования, поэтому существует подобная концепция; вместо функций операции используются для изменения переменных состояния (также известных как глобальные переменные ).

Например, если у нас есть состояние, состоящее из одной переменной someStateRegister : nat, мы могли бы определить это в VDM-SL как:

 state Register of
   someStateRegister : nat
 end

Вместо этого в VDM++ это будет определяться как:

 instance variables
   someStateRegister : nat

Операцию загрузки значения в эту переменную можно указать так:

 LOAD(i:nat)
 ext wr someStateRegister:nat
 post someStateRegister = i

Пункт о внешних параметрах ( ext) указывает, к каким частям состояния может получить доступ операция; rd указывая доступ только для чтения и wr доступ для чтения/записи.

Иногда важно обратиться к значению состояния до его изменения; например, операция по добавлению значения к переменной может быть указана как:

 ADD(i:nat)
 ext wr someStateRegister : nat
 post someStateRegister = someStateRegister~ + i

Где ~ Символ переменной состояния в постусловии указывает значение переменной состояния до выполнения операции.

Примеры

Дополнительная информация: Meta-IV (язык спецификации).

максимума ​ Функция

Это пример неявного определения функции. Функция возвращает наибольший элемент из набора положительных целых чисел:

 max(s:set of nat)r:nat
 pre card s > 0
 post r in set s and
      forall r' in set s & r' <= r

Постусловие характеризует результат, а не определяет алгоритм его получения. Предварительное условие необходимо, поскольку ни одна функция не может вернуть r в наборе s, если набор пуст.

Умножение натуральных чисел

 multp(i,j:nat)r:nat
 pre true
 post r = i*j

Применение обязательства доказывания forall p:T_p & pre-f(p) => f(p):T_r and post-f(p, f(p)) к явному определению multp:

 multp(i,j) ==
  if i=0
  then 0
  else if is-even(i)
       then 2*multp(i/2,j)
       else j+multp(i-1,j)

Тогда обязанность доказывания становится:

 forall i, j : nat & multp(i,j):nat and multp(i, j) = i*j

Это можно доказать правильно:

1. Доказательство завершения рекурсии (для этого, в свою очередь, необходимо доказать, что числа становятся меньше на каждом шаге)
2. Математическая индукция

Абстрактный тип данных очереди

Это классический пример, иллюстрирующий использование неявной спецификации операции в модели на основе состояний известной структуры данных. Очередь моделируется как последовательность, состоящая из элементов типа Qelt. Представление Qelt не имеет значения и поэтому определяется как тип токена.

 types

 Qelt = token;
 Queue = seq of Qelt;

 state TheQueue of
   q : Queue
 end

 operations

 ENQUEUE(e:Qelt)
 ext wr q:Queue
 post q = q~ ^ [e];

 DEQUEUE()e:Qelt
 ext wr q:Queue
 pre q <> []
 post q~ = [e]^q;

 IS-EMPTY()r:bool
 ext rd q:Queue
 post r <=> (len q = 0)

Пример банковской системы

В качестве очень простого примера модели VDM-SL рассмотрим систему ведения сведений о банковских счетах клиентов. Клиенты моделируются по номерам клиентов ( CustNum ), счета моделируются по номерам счетов ( AccNum ). Представления номеров клиентов считаются несущественными и поэтому моделируются типом токена. Остатки и овердрафты моделируются числовыми типами.

 AccNum = token;
 CustNum = token;
 Balance = int;
 Overdraft = nat;

 AccData :: owner : CustNum
            balance : Balance

 state Bank of
   accountMap : map AccNum to AccData
   overdraftMap : map CustNum to Overdraft
 inv mk_Bank(accountMap,overdraftMap) == for all a in set rng accountMap & a.owner in set dom overdraftMap and
                                         a.balance >= -overdraftMap(a.owner)

С операциями: NEWC присваивает новый номер клиента:

 operations
 NEWC(od : Overdraft)r : CustNum
 ext wr overdraftMap : map CustNum to Overdraft
 post r not in set dom ~overdraftMap and overdraftMap = ~overdraftMap ++ { r |-> od};

NEWAC присваивает новый номер счета и обнуляет баланс:

 NEWAC(cu : CustNum)r : AccNum
 ext wr accountMap : map AccNum to AccData
     rd overdraftMap map CustNum to Overdraft
 pre cu in set dom overdraftMap
 post r not in set dom accountMap~ and accountMap = accountMap~ ++ {r|-> mk_AccData(cu,0)}

ACINF возвращает все балансы всех счетов клиента в виде карты номеров счетов для баланса:

 ACINF(cu : CustNum)r : map AccNum to Balance
 ext rd accountMap : map AccNum to AccData
 post r = {an |-> accountMap(an).balance | an in set dom accountMap & accountMap(an).owner = cu}

Поддержка инструментов

Ряд различных инструментов поддерживают VDM:

• VDMTools был ведущим коммерческим инструментом для VDM и VDM++, который принадлежал, продавался, обслуживался и разрабатывался CSK Systems на основе более ранних версий, разработанных датской компанией IFAD. руководства руководства и практические . Доступны Все лицензии доступны бесплатно для полной версии инструмента. Полная версия включает автоматическую генерацию кода для Java и C++, библиотеку динамической компоновки и поддержку CORBA.
• Overture — это инициатива сообщества с открытым исходным кодом, направленная на предоставление свободно доступной поддержки инструментов для всех диалектов VDM (VDM-SL, VDM++ и VDM-RT) первоначально поверх платформы Eclipse, а затем поверх платформы Visual Studio Code. Его цель — разработать основу для совместимых инструментов, которые будут полезны для промышленного применения, исследований и образования.
• vdm-mode — это набор пакетов Emacs для написания спецификаций VDM с использованием VDM-SL, VDM++ и VDM-RT. Он поддерживает подсветку и редактирование синтаксиса, оперативную проверку синтаксиса, завершение шаблонов и поддержку интерпретатора.
• SpecBox : от Adelard обеспечивает проверку синтаксиса, некоторую простую семантическую проверку и создание файла LaTeX, позволяющего печатать спецификации в математической нотации. Этот инструмент доступен бесплатно, но в дальнейшем не поддерживается.
• Макросы LaTeX и LaTeX2e доступны для поддержки представления моделей VDM в математическом синтаксисе стандартного языка ISO. Они были разработаны и поддерживаются Национальной физической лабораторией Великобритании. Документация и макросы доступны в Интернете.

Промышленный опыт

VDM широко применяется в различных областях применения. Наиболее известные из этих приложений:

• Ada и CHILL Компиляторы : первый одобренный в Европе компилятор Ada был разработан Dansk Datamatik Center с использованием VDM. Аналогичным образом семантика CHILL и Modula-2 была описана в их стандартах с использованием VDM.
• ConForm: эксперимент компании British Aerospace, сравнивающий традиционную разработку доверенного шлюза с разработкой с использованием VDM.
• Dust-Expert: проект, реализованный компанией Adelard в Великобритании для применения, связанного с безопасностью и определяющего соответствие безопасности при планировке промышленных предприятий.
• Разработка VDMTools: Большинство компонентов набора инструментов VDMTools сами разрабатываются с использованием VDM. Эта разработка была реализована в IFAD в Дании и CSK в Японии .
• TradeOne: Некоторые ключевые компоненты бэк-офисной системы TradeOne, разработанной CSK Systems для японской фондовой биржи, были разработаны с использованием VDM. Существуют сравнительные измерения производительности разработчиков и плотности дефектов компонентов, разработанных с помощью VDM, по сравнению с кодом, разработанным традиционным способом.
• FeliCa Networks сообщила о разработке операционной системы для интегральной схемы для приложений сотовой связи .

Уточнение

Использование VDM начинается с очень абстрактной модели и доводит ее до реализации. Каждый шаг включает в себя материализацию данных , а затем декомпозицию операций .

Реификация данных превращает абстрактные типы данных в более конкретные структуры данных , в то время как декомпозиция операций превращает (абстрактные) неявные спецификации операций и функций в алгоритмы , которые могут быть непосредственно реализованы на выбранном компьютерном языке.

${\begin{array}{|rcl|}{\textbf {Specification}}&&{\textbf {Implementation}}\\\hline {\text{Abstract data type}}&\xrightarrow {\text{Data reification}} &{\text{Data structure}}\\{\text{Operations}}&{\xrightarrow[{\text{Operation decomposition}}]{}}&{\text{Algorithms}}\end{array}}$

Реификация данных

Реификация данных (поэтапное уточнение) предполагает поиск более конкретного представления абстрактных типов данных, используемых в спецификации. Прежде чем будет достигнута реализация, может пройти несколько шагов. Каждый шаг реификации для абстрактного представления данных ABS_REP предполагает предложение нового представительства NEW_REP. Чтобы показать, что новое представление является точным, функция извлечения , которая связывает определяется NEW_REP к ABS_REP, то есть retr : NEW_REP -> ABS_REP. Корректность реификации данных зависит от доказательства адекватности , т.е.

 forall a:ABS_REP & exists r:NEW_REP & a = retr(r)

Поскольку представление данных изменилось, необходимо обновить операции и функции, чтобы они работали над NEW_REP. Должно быть показано, что новые операции и функции сохраняют любые инварианты типов данных в новом представлении. Чтобы доказать, что новые операции и функции моделируют те, которые содержатся в исходной спецификации, необходимо выполнить два обязательства по доказательству:

• Правило домена:

 forall r: NEW_REP & pre-OPA(retr(r)) => pre-OPR(r)

• Правило моделирования:

 forall ~r,r:NEW_REP & pre-OPA(retr(~r)) and post-OPR(~r,r) => post-OPA(retr(~r,), retr(r))

Пример реификации данных

В системе безопасности бизнеса работникам выдаются удостоверения личности; они подаются в устройства считывания карт при входе на завод и выходе с него. Необходимые операции:

• INIT() инициализирует систему, предполагает, что фабрика пуста
• ENTER(p : Person) фиксирует, что на фабрику входит рабочий; данные работника считываются с удостоверения личности)
• EXIT(p : Person) записывает, что рабочий выходит с завода
• IS-PRESENT(p : Person) r : bool проверяет, находится ли указанный рабочий на фабрике или нет

Формально это будет:

 types

 Person = token;
 Workers = set of Person;

 state AWCCS of
   pres: Workers
 end

 operations

 INIT()
 ext wr pres: Workers
 post pres = {};

 ENTER(p : Person)
 ext wr pres : Workers
 pre p not in set pres
 post pres = pres~ union {p};

 EXIT(p : Person)
 ext wr pres : Workers
 pre p in set pres
 post pres = pres~\{p};

 IS-PRESENT(p : Person) r : bool
 ext rd pres : Workers
 post r <=> p in set pres~

Поскольку в большинстве языков программирования есть концепция, сравнимая с набором (часто в форме массива), первым шагом спецификации является представление данных в виде последовательности. Эти последовательности не должны допускать повторения, поскольку мы не хотим, чтобы один и тот же рабочий процесс появлялся дважды, поэтому мы должны добавить инвариант к новому типу данных. В данном случае порядок не важен, поэтому [a,b] то же самое, что [b,a].

Венский метод разработки полезен для систем, основанных на моделях. Это нецелесообразно, если система основана на времени. В таких случаях исчисление коммуникационных систем более полезно (CCS).

См. также

• Формальные методы
• Формальная спецификация
• Пиджин-код
• Логика предикатов
• Пропозициональное исчисление
• Язык спецификации Z , основная альтернатива VDM-SL (сравнить)

Дальнейшее чтение

• Бьёрнер, Дайнс; Клифф Б. Джонс (1978). Венский метод разработки: метаязык, конспекты лекций по информатике 61 . Берлин, Гейдельберг, Нью-Йорк: Springer. ISBN  978-0-387-08766-5 .
• О'Риган, Джерард (2006). Математические подходы к качеству программного обеспечения . Лондон: Спрингер. ISBN  978-1-84628-242-3 .
• Клифф Б. Джонс, изд. (1984). Языки программирования и их определение — Х. Бекич (1936-1982) . Конспекты лекций по информатике . Том. 177. Берлин, Гейдельберг, Нью-Йорк, Токио: Springer-Verlag. дои : 10.1007/BFb0048933 . ISBN  978-3-540-13378-0 . S2CID   7488558 .
• Фицджеральд Дж. С. и Ларсен П. Г. Системы моделирования: практические инструменты и методы разработки программного обеспечения . Издательство Кембриджского университета , 1998 г. ISBN   0-521-62348-0 (паб японского издания. Iwanami Shoten, 2003 г.) ISBN   4-00-005609-3 ).
• Фицджеральд Дж. С. , Ларсен П. Г., Мукерджи П., Плат Н. и Верхуф М. Валидированные конструкции объектно-ориентированных систем . Спрингер Верлаг 2005. ISBN   1-85233-881-4 . Веб-сайт поддержки [1] включает примеры и бесплатную поддержку инструментов.
• Джонс, CB , Систематическая разработка программного обеспечения с использованием VDM , Prentice Hall , 1990. ISBN   0-13-880733-7 . Также доступно онлайн бесплатно: http://www.csr.ncl.ac.uk/vdm/ssdvdm.pdf.zip
• Бьорнер, Д. и Джонс, CB , Формальная спецификация и разработка программного обеспечения Prentice Hall International, 1982. ISBN   0-13-880733-7
• Дж. Доус, Справочное руководство VDM-SL , Pitman , 1991. ISBN   0-273-03151-1
• Международная организация по стандартизации , Информационные технологии. Языки программирования, их среды и интерфейсы системного программного обеспечения. Венский метод разработки. Язык спецификаций. Часть 1. Базовый язык. Международный стандарт ISO/IEC 13817-1, декабрь 1996 г.
• Джонс, CB , Разработка программного обеспечения: строгий подход , Prentice Hall International, 1980. ISBN   0-13-821884-6
• Джонс, CB и Шоу, RC (ред.), Тематические исследования в области систематической разработки программного обеспечения , Prentice Hall International, 1990. ISBN   0-13-880733-7
• Бикарреги Дж. К., Фицджеральд Дж. С. , Линдсей П. А., Мур Р. и Ричи Б. Доказательство в VDM: Руководство для практикующего . Формальные подходы Springer Verlag к вычислительным и информационным технологиям (FACIT), 1994. ISBN   3-540-19813-X .

Внешние ссылки

• Информация о VDM и VDM++ (копия в архиве на archive.org)
• Венский язык определений (VDL)
• Язык моделирования COMPASS. Архивировано 19 февраля 2020 г. на Wayback Machine (CML), комбинации VDM-SL с CSP , основанной на унифицированных теориях программирования , разработанной для моделирования систем систем (SoS).