Язык VDM (Vienna Development Method) разработан в венской лаборатории компании IBM для описания языков типа ПЛ/1, трансляторов и систем со сложными структурами данных [6.7, 6.8]. Главная его цель - специфицировать правильно программу и описать набор утверждений для ее доказательства, принося в жертву скорость разработки и эффективность, даже если полученная программа громоздка и не всегда удобна в использовании, но является правильной.
Этот язык имеет математическую символику, которая легко воспринимается математически подготовленными студентами последних курсов университетов за 5-6 лекций. В языке содержатся следующие типы данных:
·

- натуральные числа с нулем;
·

- натуральные числа без нуля;
·

- целые числа;
·

- булевы;
·

- строки символов;
·

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

в VDMимеет вид:

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

. При работе с множеством используются операции

,

,

,

и др. Язык имеет правила проверки правильности задания этих операций. Пример,

будет корректным только тогда, когда

является подмножеством множества, которому принадлежит

. Пример дистрибутивного объединения дан ниже:

Списки ( последовательности ) - это цепочки элементов одинакового типа из множества

. Операция

задает длину списка, а

- номера элементов списка.
Например,

.
К списковым операциям относится взятие первого (головы) элемента списка -

и остатка (хвоста) после удаления первого элемента из списка -

.
Например,

,

.
Могут использоваться также операция конкатенации (соединение двух списков) и операция дистрибутивной конкатенации.
Дерево- это конструкция

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

- переменная типа Время, значение которой - 10 ч. 30 мин, тогда конструкция

определяет значение

, а

.
Отображение- это конструкция

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

позволяет строить множество ключей, а

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

функция, содержащая описание типов аргументов, результата и операций самой функции. Для проверки правильности спецификации программы средствами языка VDM задаются пред- и постусловия, аксиомы и утверждения.
Предусловие - это предикат с операцией, к которой обращается программа после получения начального состояния для определения правильности выполнения или фиксации ошибочной ситуации.
Утверждение задает описание операций проверки правильности программы в разных ее точках. Операторы программы изменяют состояние переменных в заданной точке, а операции утверждений анализируют ее (например, после операции работы с БД) в целях определения правильности выполнения этой операции. При возникновении непредвиденной ситуации, аксиомы и утверждения должны предусматривать соответствующие действия.
Постусловие - это предикат, который - истинный после выполнения предусловия, завершения текущих операции в заданных точках при выполнении инвариантных свойств программ.
Метод VDM предусматривает пошаговую детализацию спецификации программ. На первом уровне строится грубая спецификация - модель в языке VDM, которая постепенно уточняется, пока не получится окончательный текст описания программы.
Разработка спецификации проводится по следующей схеме:
1. Определение терминов, которыми будет специфицироваться программа.
2. Описание понятий и объектов, для обозначения которых используется денотат, идентифицируемый с помощью некоторого имени (или фразы).
3. Описание инвариантных свойств программы.
4. Определение операций над структурами программы (например, ввести объект, удалить и др.), изменяющие ее состояние и сохранение инвариантных свойств.
При переходе от одного шага детализации к другому модель программы детализируется и постепенно становится ближе к конечному описанию. Функции - это операции, которые уточняются при детализации структуры программы на каждом шаге спецификации и описания поведения модели.
При реальном выполнении спецификация исполняется итерационно. На первом уровне проверяется только свойства модели программы при заданных ограничениях независимо от среды. Затем используется уточненная и расширенная спецификация с набором формальных утверждений. И так до тех пор, пока окончательно не будет завершен процесс пошагового доказательства спецификации.
Для демонстрации возможностей VDM языка рассмотрим задачу поиска ("Поиск") в каталоге (

) репозитария компонентов имени компонента

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

где

- cведения о разработчике компонента

;

- переменная, в которую посылается код компонента, выбранного из каталога

репозитария

при совпадении имен в каталоге и запросе;

- переменная, в которой хранится текущий элемент из репозитария, найденный по фасете компонента с номером

для

;

- имя разработчика компонента;

- переменная, которая используется для задания признака - компонент не найден или к нему никто не обращался.
Описание инвариантных свойств программы

Операторы программы проверяют список имен компонентов в каталоге, который содержит

элементов типа

. Если они совпадают с именем в запросе, результат сохраняется в

.
Доказательство инвариантных свойств программ должно проводиться автоматизированным способом с помощью специально созданных инструментальных средств поддержки VDM языка.