Венский метод разработки

Венский метод разработки (VDM) является одним из наиболее давно установленных формальных методов для разработки компьютерных систем. Возникнув в результате работы, выполнявшейся в Венской лаборатории IBM в 1970-х годах, он вырос и включает в себя группу методов и инструментов, основанных на формальном языке спецификации - языке спецификации VDM (VDM-SL). Он имеет расширенную форму, VDM ++, которая поддерживает моделирование объектно-ориентированных и параллельных систем. Поддержка VDM включает коммерческие и академические инструменты для анализа моделей, включая поддержку тестирования и доказательства свойств моделей и генерации программного кода из проверенных моделей VDM. Существует история промышленного использования VDM и его инструментов, и растущее количество исследований в области формализма привело к заметному вкладу в разработку критических систем, компиляторов, параллельных систем и в логике для информатики.

• 1 Философия
• 2 История
• 3 Возможности VDM
  • 3.1 Основные типы: числовые, символьные, токен и кавычки
  • 3.2 Конструкторы типов: объединение, произведение и составные типы
  • 3.3 Коллекции
    • 3.3.1 Наборы
    • 3.3.2 Последовательности
    • 3.3.3 Карты
  • 3.4 Структурирование
    • 3.4.1 Структурирование в VDM-SL
    • 3.4.2 Структурирование в VDM ++
• 4 Функциональность моделирования
  • 4.1 Функциональное моделирование
  • 4.2 Моделирование на основе состояний
• 5 Примеры
  • 5.1 Функция max
  • 5.2 Умножение натуральных чисел
  • 5.3 Очередь абстрактного типа данных
  • 5.4 Пример банковской системы
• 6 Поддержка инструментов
• 7 Производственный опыт
• 8 Уточнение
  • 8.1 Верификация данных
    • 8.1.1 Пример реификации данных
• 9 См. Также
• 10 Дополнительная литература
• 11 Ссылки
• 12 Внешние ссылки

Вычислительные системы могут быть смоделированы в VDM-SL на более высоком уровне абстракции, чем это достижимо с использованием языков программирования, что позволяет анализировать конструкции и определять ключевые особенности, включая дефекты, на ранней стадии разработки системы. Проверенные модели могут быть преобразованы в подробные системные проекты посредством процесса уточнения. Язык имеет формальную семантику, позволяющую доказывать свойства моделей с высокой степенью уверенности. Он также имеет исполняемое подмножество, так что модели могут быть проанализированы путем тестирования и могут выполняться через графические пользовательские интерфейсы, так что модели могут быть оценены экспертами, которые не обязательно знакомы с самим языком моделирования.

Истоки VDM-SL лежат в IBM лаборатории в Вене, где первая версия языка называлась V ienna D определение L язык (VDL). VDL в основном использовался для описания операционной семантики в отличие от VDM - Meta-IV, который обеспечивал денотационную семантику

«К концу 1972 года Венская группа снова обратила свое внимание на проблема систематической разработки компилятора на основе определения языка. Общий подход был назван «Венским методом разработки»... Фактически принятый метаязык («Meta-IV») используется для определения основных частей PL / 1 (как указано в ECMA 74 - интересно, что «формальный» документ стандартов, написанный как абстрактный интерпретатор ») на BEKIČ 74.»

Нет никакой связи между Meta-IV и Meta-II языком Шорре или его преемником Дерево Мета ; это были системы компилятор-компилятор, а не подходящие для формального описания проблем.

Итак, Meta-IV «использовался для определения основных частей» языка программирования PL / I. Другие языки программирования, ретроспективно или частично описанные с использованием Meta-IV и VDM-SL, включают язык программирования BASIC, FORTRAN, язык программирования APL, АЛГОЛ 60, язык программирования Ada и язык программирования Pascal. Meta-IV превратилась в несколько вариантов, обычно описываемых как датская, английская и ирландская школы.

«Английская школа» основана на работе Клиффа Джонса по аспектам VDM, не связанным конкретно с определением языка и дизайном компилятора (Jones 1980, 1990). Он подчеркивает моделирование постоянного состояния за счет использования типов данных, созданных из обширной коллекции базовых типов. Функциональность обычно описывается с помощью операций, которые могут иметь побочные эффекты для состояния и которые в большинстве случаев указываются неявно с использованием предусловия и постусловия. «Датская школа» (Бьёрнер и др., 1982) имела тенденцию подчеркивать конструктивный подход с явной рабочей спецификацией, используемой в большей степени. Работа в датской школе привела к созданию первого проверенного в Европе компилятора Ada.

Стандарт ISO для языка был выпущен в 1996 году (ISO, 1996).

Синтаксис и семантика VDM-SL и VDM ++ подробно описаны в языковых руководствах VDMTools и в имеющихся текстах. Стандарт ISO содержит формальное определение семантики языка. В оставшейся части этой статьи используется синтаксис обмена, определенный ISO (ASCII). Некоторые тексты предпочитают более сжатый математический синтаксис.

Модель VDM-SL - это описание системы, данное в терминах функциональности, выполняемой с данными. Он состоит из серии определений типов данных и функций или операций, выполняемых с ними.

Базовые типы: числовые, символьные, токен и кавычки

VDM-SL включает следующие базовые типы, моделирующие числа и символы:

Типы данных определены для представления основных данных моделируемой системы. Каждое определение типа вводит новое имя типа и дает представление в терминах основных типов или в терминах уже введенных типов. Например, тип, моделирующий идентификаторы пользователей для системы управления входом в систему, может быть определен следующим образом:

типы UserId = nat

Для управления значениями, принадлежащими типам данных, операторы определены в ценности. Таким образом, обеспечивается сложение натуральных чисел, вычитание и т. Д., А также булевы операторы, такие как равенство и неравенство. Язык не устанавливает максимальное или минимальное представимое число или точность действительных чисел. Такие ограничения определяются там, где они требуются в каждой модели, с помощью инвариантов типа данных - логических выражений, обозначающих условия, которые должны соблюдаться всеми элементами определенного типа. Например, требование, чтобы идентификаторы пользователей не превышали 9999, можно было бы выразить следующим образом (где <=- логический оператор "меньше или равно" для натуральных чисел):

UserId = nat inv uid == uid <= 9999

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

Другие базовые типы включают char для символов. В некоторых случаях представление типа не имеет отношения к цели модели и только добавит сложности. В таких случаях члены типа могут быть представлены как бесструктурные токены. Значения типов токенов можно сравнивать только на равенство - для них не определены другие операторы. Если требуются определенные именованные значения, они представлены как типы кавычек. Каждый тип кавычек состоит из одного именованного значения с тем же именем, что и сам тип. Значения типов кавычек (известных как литералы кавычек) можно сравнивать только на равенство.

Например, при моделировании диспетчера светофора может быть удобно определить значения для представления цветов светофора в виде типов цитат:

, , , 

Конструкторы типов: объединение, продукт и составные типы

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

Самый простой конструктор типа формирует объединение двух предопределенных типов. Тип (A | B)содержит все элементы типа A и все элементы типа B. В примере контроллера сигнала трафика тип, моделирующий цвет сигнала трафика, может быть определен следующим образом:

SignalColour = | | | 

Перечислимые типы в VDM-SL определены, как показано выше, как объединения на типы цитат.

Декартовы типы произведения также могут быть определены в VDM-SL. Тип (A1 *… * An)- это тип, состоящий из всех кортежей значений, первый элемент которых относится к типу A1, а второй - к типу A2и так далее. Составной тип или тип записи - это декартово произведение с метками для полей. Тип

T :: f1: A1 f2: A2... fn: An

- это декартово произведение с полями, помеченными f1,…, fn. Элемент типа Tможет быть составлен из его составных частей с помощью конструктора, записанного mk_T. И наоборот, учитывая элемент типа T, имена полей могут использоваться для выбора именованного компонента. Например, тип

Date :: day: nat1 month: nat1 year: nat inv mk_Date (d, m, y) == d <=31 and m<=12

моделирует простой тип даты. Значение mk_Date (1,4,2001)соответствует 1 апреля 2001 года. Для даты dвыражение d.monthявляется натуральным числом, представляющим месяц. При желании в инвариант можно включить ограничения на количество дней в месяц и високосные годы. Их объединение:

mk_Date (1,4,2001).month = 4

Коллекции

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

Наборы

Конструктор типа набора (записывается набор T, где T- предопределенный тип) создает тип, состоящий из всех конечных наборов значения взяты из типа T. Например, определение типа

UGroup = set of UserId

определяет тип UGroup, состоящий из всех конечных наборов значений UserId. На множествах определены различные операторы для построения их объединения, пересечений, определения собственных и нестрогих отношений подмножеств и т. Д.

Sequences

Конструктор типа конечной последовательности (записывается seq of T, где T- предопределенный тип) создает тип, состоящий из всех конечных списков значений, взятых из типа T. Например, определение типа

String = seq of char

Определяет тип String, состоящий из всех конечных строк символов. В последовательностях определены различные операторы для построения конкатенации, выбора элементов и подпоследовательностей и т. Д. Многие из этих операторов являются частичными в том смысле, что они не определены для определенных приложений. Например, выбор 5-го элемента последовательности, содержащей только три элемента, не определен.

Порядок и повторение элементов в последовательности имеют значение, поэтому [a, b]не равно [b, a]и [a]не равно [a, a].

Maps

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

Дни рождения = сопоставить строку с датой

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

Структурированием

Основное различие между нотациями VDM-SL и VDM ++ - это способ структурирования. В VDM-SL есть обычное модульное расширение, тогда как VDM ++ имеет традиционный объектно-ориентированный механизм структурирования с классами и наследованием.

Структурирование в VDM-SL

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

• Именование модулей : каждый модуль синтаксически начинается с ключевого слова module, за которым следует имя модуля. В конце модуля записывается ключевое слово end, за которым снова следует имя модуля.
• Импорт : можно импортировать определения, которые были экспортированы из других модулей. Это делается в разделе импорта, который начинается с ключевого слова import, за которым следует последовательность импорта из разных модулей. Каждый из этих импортов модулей начинается с ключевого слова из, за которым следует имя модуля и подпись модуля. Сигнатура модуля может быть либо просто ключевым словом all, указывающим на импорт всех определений, экспортированных из этого модуля, либо это может быть последовательность сигнатур импорта. Сигнатуры импорта специфичны для типов, значений, функций и операций, и каждая из них запускается с помощью соответствующего ключевого слова. Кроме того, эти сигнатуры импорта называют конструкции, к которым есть желание получить доступ. Кроме того, может присутствовать дополнительная информация о типе и, наконец, можно переименовать каждую из конструкций при импорте. Для типов необходимо также использовать ключевое слово struct, если кто-то хочет получить доступ к внутренней структуре определенного типа.
• Экспорт : определения из модуля, которые нужно использовать для других модулей. имеют доступ к экспортируемым с использованием ключевого слова exports, за которым следует подпись модуля экспорта. Подпись модуля экспорта может состоять либо просто из ключевого слова all, либо в виде последовательности подписей экспорта. Такие сигнатуры экспорта специфичны для типов, значений, функций и операций, и каждая из них запускается с помощью соответствующего ключевого слова. Если нужно экспортировать внутреннюю структуру типа, необходимо использовать ключевое слово struct.
• Более экзотические функции : в более ранних версиях инструментов VDM-SL также была поддержка параметризованных модули и экземпляры таких модулей. Однако эти функции были исключены из VDMTools примерно в 2000 году, потому что они почти никогда не использовались в промышленных приложениях, и при использовании этих функций было много проблем с инструментами.

Структурирование в VDM ++

В VDM ++ структурирование выполнено с использованием классов и множественного наследования. Ключевые понятия:

• Класс : каждый класс синтаксически начинается с ключевого слова class, за которым следует имя класса. В конце класса записывается ключевое слово end, за которым снова следует имя класса.
• Наследование : в случае, если класс наследует конструкции от других классов, имя класса в заголовке класса могут сопровождаться ключевыми словами является подклассом, за которым следует список имен суперклассов, разделенных запятыми.
• Модификаторы доступа : Скрытие информации в VDM ++ выполняется так же, как и в большинстве объектов ориентированные языки с использованием модификаторов доступа. В VDM ++ определения по умолчанию являются частными, но перед всеми определениями можно использовать одно из ключевых слов модификатора доступа: частный, общедоступныйи защищенный.

Функциональное моделирование

В VDM-SL функции определяются на основе типов данных, определенных в модели. Поддержка абстракции требует, чтобы была возможность характеризовать результат, который должна вычислять функция, без необходимости говорить, как он должен быть вычислен. Основным механизмом для этого является неявное определение функции, в котором вместо формулы, вычисляющей результат, логический предикат над входными и результирующими переменными, называемый постусловием, дает свойства результата. Например, функция SQRTдля вычисления квадратного корня из натурального числа может быть определена следующим образом:

SQRT (x: nat) r: real post r * r = x

Здесь постусловие не определяет метод вычисления результата r, но указывает, какие свойства могут быть приняты для его сохранения. Обратите внимание, что это определяет функцию, которая возвращает правильный квадратный корень; не требуется, чтобы это был положительный или отрицательный корень. Вышеуказанной спецификации может удовлетворять, например, функция, возвращающая отрицательный корень из 4, но положительный корень из всех других допустимых входных данных. Обратите внимание, что функции в VDM-SL должны быть детерминированными, чтобы функция, удовлетворяющая приведенному выше примеру, должна всегда возвращать один и тот же результат для одного и того же входа.

Более ограниченная спецификация функции достигается за счет усиления постусловия. Например, следующее определение ограничивает функцию возвратом положительного корня.

SQRT (x: nat) r: real post r * r = x and r>= 0

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

SQRTP (x: real) r: real pre x>= 0 post r * r = x and r>= 0

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

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

SqList: seq of nat ->seq of nat SqList (s) == if s = then else [(hd s) ** 2] ^ SqList (tl s)

Это рекурсивное определение состоит из сигнатуры функции, дающей типы ввода и результата, и тела функции. Неявное определение той же функции может иметь следующую форму:

SqListImp (s: seq of nat) r: seq of nat post len ​​r = len s and forall i in set inds s r (i) = s (i) ** 2

Явное определение в простом смысле является реализацией неявно указанной функции. Корректность явного определения функции по отношению к неявной спецификации может быть определена следующим образом.

Учитывая неявную спецификацию:

f (p: T_p) r: T_r pre pre-f (p) post post-f (p, r)

и an явная функция:

f: T_p ->T_r

мы говорим, что он удовлетворяет спецификации iff :

для всех p в наборе T_p pre-f (p) =>f ( p): T_r и post-f (p, f (p))

Итак, «f- правильная реализация» следует интерпретировать как «fудовлетворяет спецификация ».

Моделирование на основе состояний

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

Например, если у нас есть состояние, состоящее из одной переменной someStateRegister: nat, мы можем определить это в VDM-SL как:

Регистр состояния someStateRegister: nat end

В VDM ++ это вместо этого будет определено как:

переменные экземпляра someStateRegister: nat

Операция загрузки значения в эту переменную может быть определена как:

LOAD (i: nat) ext wr someStateRegister: nat post someStateRegister = i

Предложение externals (ext) указывает, к каким частям состояния может получить доступ операция; rdуказывает доступ только для чтения, а wrозначает доступ для чтения / записи.

Иногда важно указать значение состояния до его изменения; например, операция добавления значения к переменной может быть указана как:

ADD (i: nat) ext wr someStateRegister: nat post someStateRegister = someStateRegister ~ + i

Где ~символ в переменной состояния в постусловии указывает значение переменной состояния до выполнения операции.

Функция max

Это пример неявного определения функции. Функция возвращает самый большой элемент из набора положительных целых чисел:

max (s: набор nat) r: nat pre card s>0 post r в наборе s и forall r 'в наборе s r' <= r

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

Умножение натуральных чисел

multp (i, j: nat) r: nat pre true post r = i * j

Применение обязательства доказательства для всех p: T_p pre-f (p) =>f (p): T_r и post-f (p, f (p))до явного определения multp:

multp (i, j) = = if i = 0 then 0 else if is-even (i) then 2 * multp (i / 2, j) else j + multp (i-1, j)

Тогда обязательство по доказательству становится следующим:

для всех i, j: nat multp (i, j): nat и multp (i, j) = i * j

Правильность этого можно показать следующим образом:

1. Доказав, что рекурсия заканчивается (это, в свою очередь, требует доказательства того, что числа становятся меньше на каждом шаге)
2. Математическая индукция

Абстрактный тип данных очереди

Это классический пример, иллюстрирующий использование неявной спецификации операции в состоянии основанная на модели известной структуры данных. Очередь моделируется как последовательность, состоящая из элементов типа Qelt. Представление Qeltнесущественно и поэтому определяется как тип токена.

типы

Qelt = токен; Очередь = последовательность Qelt;

state TheQueue of q: Queue end

operations

ENQUEUE (e: Qelt) ext wr q: Queue post q = q ~ ^ [e];

DEQUEUE () e: Qelt ext wr q: Очередь до q <>post q ~ = [e] ^ q;

IS-EMPTY () r: bool ext rd q: Queue post r <=>(len q = 0)

Пример банковской системы

В качестве очень простого примера модели VDM-SL, рассмотрите систему для ведения реквизитов банковского счета клиента. Клиенты моделируются номерами клиентов (CustNum), счета моделируются номерами счетов (AccNum). Представления номеров клиентов считаются несущественными и поэтому моделируются типом токена. Балансы и овердрафты моделируются числовыми типами.

AccNum = токен; CustNum = токен; Баланс = int; Овердрафт = нац;

AccData :: owner: CustNum balance: Balance

state Bank of accountMap: сопоставить AccNum с AccData overdraftMap: сопоставить CustNum с Overdraft inv mk_Bank (accountMap, overdraftMap) == для всех в наборе rng accountMap a.owner в set dom overdraftMap и a.balance>= -overdraftMap (a.owner)

С операциями: NEWC назначает новый номер клиента:

операций NEWC (od: Overdraft) r: CustNum ext wr overdraftMap: сопоставить CustNum с Overdraft post r не в наборе dom ~ overdraftMap и overdraftMap = ~ overdraftMap ++ {r | ->od};

NEWAC назначает новый номер счета и устанавливает баланс на ноль:

NEWAC (cu: CustNum) r: AccNum ext wr accountMap: map AccNum to AccData rd overdraftMap map CustNum to Overdraft pre cu in set dom overdraftMap post r not in set dom accountMap ~ and accountMap = accountMap ~ ++ {r | ->mk_AccData (cu, 0)}

ACINF возвращает все балансы всех счетов клиента, как карта номера счета для баланса:

ACINF (cu: CustNum) r: map AccNum to Balance ext rd accountMap: map AccNum to AccData post r = {an | ->accountMap (an).balance | an in set dom accountMap accountMap (an).owner = cu}

Ряд различных инструментов поддерживает VDM:

• VDMTools - ведущие коммерческие инструменты для VDM и VDM ++ принадлежат, продаются, обслуживаются и разрабатываются CSK Systems на основе более ранних версий, разработанных датской компанией IFAD. Доступны руководства и практические учебные пособия. Все лицензии доступны бесплатно для полной версии инструмента. Полная версия включает автоматическое создание кода для Java и C ++, библиотеку динамической компоновки и поддержку CORBA.
• Overture - это инициатива сообщества с открытым исходным кодом, направленная на обеспечение свободно доступной инструментальной поддержки VDM ++ поверх платформы Eclipse. Его цель - разработать структуру для совместимых инструментов, которые будут полезны для промышленного применения, исследований и образования.
• vdm-mode - это набор пакетов Emacs для написания спецификаций VDM с использованием VDM-SL, VDM ++ и VDM- RT. Он поддерживает выделение и редактирование синтаксиса, проверку синтаксиса на лету, завершение шаблонов и поддержку интерпретатора.
• SpecBox : от Adelard обеспечивает проверку синтаксиса, некоторую простую семантическую проверку и создание файла LaTeX, позволяющего спецификации быть напечатаны в математической нотации. Этот инструмент находится в свободном доступе, но в дальнейшем не поддерживается. Доступны макросы
• LaTeX и LaTeX2e для поддержки представления моделей VDM в математическом синтаксисе стандартного языка ISO. Они были разработаны и поддерживаются Национальной физической лабораторией Великобритании. Документация и макросы доступны в Интернете.

VDM широко применяется в различных областях приложений. Наиболее известными из этих приложений являются:

• компиляторы Ada и CHILL : первый проверенный в Европе компилятор Ada был разработан Dansk Datamatik Center используя VDM. Аналогичным образом семантика CHILL и Modula-2 была описана в их стандартах с использованием VDM.
• ConForm: эксперимент в British Aerospace, сравнивающий обычную разработку доверенного шлюза с разработкой с использованием VDM.
• Dust-Expert: Проект, выполняемый Adelard в Великобритании для приложения, связанного с безопасностью, определяющий, что безопасность является соответствующей при компоновке промышленных предприятий.
• разработка VDMTools: большинство компонентов набора инструментов VDMTools сами разрабатываются с использованием VDM. Эта разработка была произведена в IFAD в Дании и CSK в Японии.
• TradeOne: разработаны некоторые ключевые компоненты системы бэк-офиса TradeOne by CSK системы для японской фондовой биржи были разработаны с использованием VDM. Существуют сравнительные измерения производительности разработчиков и плотности дефектов компонентов, разработанных VDM, по сравнению с традиционно разработанным кодом.
• FeliCa Networks сообщила о разработке операционной системы для интегральной схемы. для приложений сотового телефона.

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

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

Реификация данных

Рефикация данных (пошаговое уточнение) включает поиск более конкретного представления абстрактных типов данных, используемых в спецификации. До реализации может быть несколько шагов. Каждый шаг реификации для абстрактного представления данных ABS_REPвключает предложение нового представления NEW_REP. Чтобы показать, что новое представление является точным, определена функция извлечения, которая связывает NEW_REPс ABS_REP, то есть retr: NEW_REP ->ABS_REP. Правильность реификации данных зависит от подтверждения адекватности, т. Е.

forall a: ABS_REP exists r: NEW_REP a = retr (r)

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

• Правило домена:

для всех r: NEW_REP pre-OPA (retr (r)) =>pre-OPR (r)

• Правило моделирования:

forall ~ r, r: NEW_REP pre-OPA (retr (~ r)) и post-OPR (~ r, r) =>post-OPA (retr (~ r,), retr (r))

Пример повторной модификации данных

В системе безопасности предприятия работникам выдаются удостоверения личности; они загружаются в считыватели карт при входе и выходе с завода. Необходимые операции:

• INIT ()инициализирует систему, предполагает, что фабрика пуста.
• ENTER (p: Person)записывает, что работник входит на фабрику; данные рабочих считываются из идентификационной карты)
• EXIT (p: Person)записывает, что рабочий покидает фабрику
• IS-PRESENT (p: Person) r: boolпроверяет, чтобы посмотреть, есть ли указанный работник на фабрике или нет

Формально это будет:

типы

Person = token; Рабочие = набор Человека;

состояние AWCCS пресса: Завершение работниками

операций

INIT () ext wr pres: Workers post pres = {};

ENTER (p: Person) ext wr pres: Рабочие pre p not in set pres post pres = pres ~ union {p};

EXIT (p: Person) ext wr pres: Рабочие подготовлены в наборе pre post pres = pres ~ \ {p};

IS-PRESENT (p: Person) r: bool ext rd pres: Рабочие отправляют r <=>p в set pres ~

Поскольку большинство языков программирования имеют концепцию, сравнимую с набором ( часто в форме массива), первым шагом в спецификации является представление данных в виде последовательности. Эти последовательности не должны допускать повторения, поскольку мы не хотим, чтобы один и тот же рабочий процесс появлялся дважды, поэтому мы должны добавить инвариант к новому типу данных. В этом случае порядок не важен, поэтому [a, b]то же самое, что и [b, a].

Венский метод разработки полезен для систем на основе моделей. Это не подходит, если система основана на времени. В таких случаях исчисление систем связи (CCS) более полезно.

• Формальные методы
• Формальная спецификация
• Код Pidgin
• Логика предикатов
• Исчисление высказываний
• язык спецификации Z, основная альтернатива VDM-SL (сравнить)
• язык моделирования COMPASS (CML), комбинация VDM-SL с CSP, основанная на Unifying Theories of Programming, разработанная для моделирования Системы систем (SoS)

• Bjørner, Dines; Клифф Б. Джонс (1978). Венский метод разработки: метаязык, конспект лекций по информатике 61. Берлин, Гейдельберг, Нью-Йорк: Springer. ISBN 978-0-387-08766-5.
• О'Реган, Джерард (2006). Математические подходы к качеству программного обеспечения. Лондон: Спрингер. ISBN 978-1-84628-242-3.
• Клифф Б. Джонс, изд. (1984). Языки программирования и их определение - Х. Бекич (1936-1982). Конспект лекций по информатике. 177 . Берлин, Гейдельберг, Нью-Йорк, Токио: Springer-Verlag. doi : 10.1007 / BFb0048933. ISBN 978-3-540-13378-0.
• Фитцджеральд, Дж. С. и Ларсен, П. Г., Системы моделирования: практические инструменты и методы в разработке программного обеспечения. Cambridge University Press, 1998 ISBN 0-521-62348-0 (Japanese Edition pub. Iwanami Shoten 2003 ISBN 4-00-005609-3 ).
• Fitzgerald, JS, Larsen, PG, Mukherjee, P., Plat, N. и Verhoef, M., Проверенные образцы для Объектно-ориентированные системы. Springer Verlag 2005. ISBN 1-85233-881-4. Поддерживающий веб-сайт [1] включает примеры и бесплатную поддержку инструментов.
• Jones, CB, Systematic Software Development using VDM, Prentice Hall 1990. ISBN 0-13 -880733-7. Также имеется on-line and free of charge: http://www.csr.ncl.ac.uk/vdm/ssdvdm.pdf.zip
• Bjørner, D. and Jones, C.B., Formal Specification and Software Development Prentice Hall International, 1982. ISBN 0-13-880733-7
• J. Dawes, The VDM-SL Reference Guide, Pitman 1991. ISBN 0-273-03151-1
• International Organization for Standardization, Information technology – Programming languages, their environments and system software interfaces – Vienna Development Method – Specification Language – Part 1: Base language International Standard ISO/IEC 13817-1, December 1996.
• Jones, C.B., Software Development: A Rigorous Approach, Prentice Hall International, 1980. ISBN 0-13-821884-6
• Jones, C.B. and Shaw, R.C. (eds.), Case Studies in Systematic Software Development, Prentice Hall International, 1990. ISBN 0-13-880733-7
• Bicarregui, J.C., Fitzgerald, J.S., Lindsay, P.A., Moore, R. and Ritchie, B., Proof in VDM: a Practitioner's Guide. Springer Verlag Formal Approaches to Computing and Information Technology (FACIT), 1994. ISBN 3-540-19813-X.

This article is based on material taken from the Free On-line Dictionary of Computing prior to 1 November 2008 and incorporated under the "relicensing" terms of the GFDL, version 1.3 or later.

• Information on VDM and VDM++ (archived copy at archive.org)
• Vienna Definition Language (VDL)