Язык 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 языка.