Описание базовых конструкций языка VDM

Язык VDM появился в венской лаборатории как метод для описания языка ПЛ/1, разработки трансляторов и систем со сложными структурами данных[1]. Главная цель этого языка — спецификация программ и данных. Язык VDM предоставляет математическую символику для описания спецификации. В нем содержатся следующие 'ГД:

X — натуральные числа с нулем;

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

Int — целые числа;

Bool — булев тип;

Qout — строки символов;

Token — знаки и специальные обозначения операций.

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

Алгоритмически описание значения этой функции имеет вид:

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

Множество может быть конечным и обозначаться X-set. При работе с множеством используются операции е, с, u, п и др. Язык включает в себя правила проверки правильности задания этих операций. Пример: х е А будет корректным только тогда, когда А является подмножеством из множества, которому принадлежит х.

Дистрибутивное объединение подмножеств имеет вид

Списки (последовательности) — это цепочки элементов одинакового типа из множества X. Операция 1еп задает длину списка, a inds — номер элемента списка.

Например, inds 1st =(i еХ f len|).

К операциям относятся: взятие первого (головы) элемента списка — hd и остатка (хвоста) после удаления первого элемента из списка — tl.

Например, hd (а, 6, с, d) = (a), tl (а> b, с, d) = (6, с, d).

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

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

Например, пусть t — переменная типа Время, значением которой является 10:30, тогда конструкция имеет вид

Отображение — это конструкция шар, позволяющая создавать абстрактную таблицу из двух столбцов: ключей и значений. Все объекты таблицы принадлежат одному ТД — множеству. Операция dom строит множество ключей, a rng — множество всех его значений. Кроме того, есть такие операции: исключить строку, слить две таблицы и др.

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

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

Постусловие — это предикат, который является истинным после выполнения предусловия, завершения текущей операции и выполнения инвариантных свойств программы.

Метод VDM ориентирован на пошаговую детализацию спецификации программ. На первом уровне строится грубая спецификация — модель программы в языке VDM, которая постепенно уточняется, пока не получится окончательный текст в ЯП. Разработка спецификации проводится по следующей схеме:

  • 1) выбор терминов для спецификации программы;
  • 2) описание понятий и объектов с использованием денотат, идентифицируемых с помощью некоторого имени;
  • 3) описание инвариантных свойств программы;
  • 4) определение операций (например, ввести объект, удалить и др.), которые изменяют состояние программы и сохраняют инвариантные свойства.

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

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

Для демонстрации возможностей VDM языка рассмотрим задачу «Поиск», которая занимается поиском имени компонента С в каталоге (catalR) репозитария компонентов. Затем эго имя сравнивается с заданным именем в запросе пользователя. В случае совпадения имен проверяются параметры, из каталога извлекается код компонента для передачи пользователю.

Спецификация переменных программы «Поиск»

где developer — разработчик компонента С; facet — переменная, в которую посылается код компонента, выбранного из каталога catalR репозитория repoz при совпадении имен в каталоге и запросе; role — переменная, в которой хранится текущий элемент из репозитария, найденный по фасету компонента с номером N для user; autors : Milk — имя разработчика компонента; free : Bool — переменная, которая используется для задания признака: компонент нс найден или к нему никто не обращался.

Описание инвариантных свойств программы

Проверяется список имен в каталоге, который содержит N элементов, представляющих собой элементы типа set, совпадающие с именем в запросе, после чего результат сохраняется в role.

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

Таким образом, можно сделать вывод о том, что методы систематического и теоретического программирования постоянно развиваются и пополняются новыми возможностям.

  • [1] См. об этом: Biomer D„Jones С. В. The Vienna Development Methods (VDM): The MetaLanguage. Vol. 61 of Lecture Notes in Computer Science. Heiderberg : Springer Verlag, 1978.
 
Посмотреть оригинал
< Пред   СОДЕРЖАНИЕ   ОРИГИНАЛ     След >