VDM-спецификация программ

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