Лекция: 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 языка.