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

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

Философия [ править ]

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

История [ править ]

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

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

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

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

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

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

Возможности VDM [ править ]

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

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

Основные типы: числовые, символьные, токен и кавычки [ править ]

VDM-SL включает следующие основные типы моделей чисел и символов:

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

типыUserId = nat

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

UserId = natinv uid == uid <= 9999

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

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

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

<Красный>, <Янтарь>, <Мигающий Янтарь>, <Зеленый>

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

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

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

SignalColour = <Red> | <Янтарь> | <Мигающий янтарь> | <Зеленый>

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

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

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

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

Дата :: день: nat1 месяц: nat1 год: нацinv mk_Date (d, m, y) == d <= 31 и m <= 12

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

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

Коллекции [ править ]

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

Наборы [ править ]

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

UGroup = набор UserId

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

Последовательности [ править ]

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

Строка = последовательность символов

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

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

Карты [ править ]

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

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

Определяет тип, Birthdaysкоторому сопоставляются символьные строки Date. Опять же, в отображениях определены операторы для индексации в отображении, объединения отображений, перезаписи, извлечения вложенных отображений.

Структурирование [ править ]

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

Структурирование в VDM-SL [ править ]

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

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

Структурирование в VDM ++ [ править ]

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

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

Функциональность моделирования [ править ]

Функциональное моделирование [ править ]

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

КОРЕНЬ (x: nat) r: реальныйсообщение r * r = x

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

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

КОРЕНЬ (x: nat) r: реальныйсообщение r * r = x и r> = 0

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

SQRTP (x: реальный) r: реальныйpre x> = 0сообщение r * r = x и r> = 0

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

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

SqList: последовательность нат -> последовательность натSqList (s) == if s = [] then [] else [(hd s) ** 2] ^ SqList (tl s)

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

SqListImp (s: последовательность nat) r: последовательность natpost len ​​r = len s и для всех i в наборе inds s & r (i) = s (i) ** 2

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

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

f (p: T_p) r: T_rpre pre-f (p)пост пост-ф (р, р)

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

f: T_p -> T_r

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

для всех 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конец

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

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

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

НАГРУЗКА (i: nat)ext wr someStateRegister: natопубликовать someStateRegister = i

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

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

ДОБАВИТЬ (i: nat)ext wr someStateRegister: natопубликовать someStateRegister = someStateRegister ~ + i

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

Примеры [ править ]

Макс функция [ править ]

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

max (s: набор nat) r: natпредварительная карта s> 0разместить r в наборе s и forall r 'в наборе s & r' <= r

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

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

multp (я, j: нат) г: натпредварительно правдасообщение r = i * j

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

multp (я, j) ​​== если я = 0 тогда 0 иначе, если четно (я) затем 2 * multp (i / 2, j) иначе j + multp (i-1, j)

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

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

Это можно показать правильно:

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

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

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

типы

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

заявить TheQueue of q: очередьконец

операции

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

DEQUEUE () e: Qeltext wr q: очередьpre q <> []сообщение q ~ = [e] ^ q;

IS-EMPTY () r: boolext rd q: очередьсообщение r <=> (len q = 0)

Пример банковской системы [ править ]

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

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

AccData :: владелец: CustNum баланс: Баланс

государственный банк accountMap: сопоставить AccNum с AccData overdraftMap: сопоставить CustNum с овердрафтомinv mk_Bank (accountMap, overdraftMap) == для всех в наборе rng accountMap & a.owner в наборе dom overdraftMap и a.balance> = -overdraftMap (a.owner)

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

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

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

NEWAC (cu: CustNum) r: AccNumext wr accountMap: сопоставить AccNum с AccData rd overdraft Карта карты CustNum to Overdraftpre cu in set dom overdraftMapсообщение r отсутствует в наборе dom accountMap ~ и accountMap = accountMap ~ ++ {r | -> mk_AccData (cu, 0)}

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

ACINF (cu: CustNum) r: карта AccNum для балансаext rd accountMap: сопоставить AccNum с AccDatapost r = {an | -> accountMap (an) .balance | 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. ^[8] Аналогичным образом семантика CHILL и Modula-2 была описана в их стандартах с использованием VDM.
• ConForm: эксперимент British Aerospace, сравнивающий стандартную разработку доверенного шлюза с разработкой с использованием VDM.
• Dust-Expert: проект, осуществляемый Adelard в Великобритании для приложения, связанного с безопасностью, определяющего, что безопасность соответствует требованиям при компоновке промышленных предприятий.
• Разработка VDMTools: большинство компонентов набора инструментов VDMTools сами разрабатываются с использованием VDM. Эта разработка была сделана в IFAD в Дании и CSK в Японии . ^[9]
• TradeOne: Некоторые ключевые компоненты системы бэк-офиса TradeOne, разработанные CSK systems для японской фондовой биржи, были разработаны с использованием VDM. Существуют сравнительные измерения производительности разработчиков и плотности дефектов компонентов, разработанных VDM, по сравнению с традиционно разработанным кодом.
• FeliCa Networks сообщила о разработке операционной системы для интегральной схемы для приложений сотовой связи .

Уточнение [ править ]

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

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

Реификация данных [ править ]

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

для всех a: ABS_REP & существует 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 проверяет, есть ли указанный рабочий на фабрике или нет

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

типы

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

государственная АРМК пресс: Рабочиеконец

операции

В ЭТОМ()ext wr pres: Рабочиеpost pres = {};

ENTER (p: человек)ext wr pres: Рабочиеpre p не в наборе preпост пресс = пресс ~ союз {р};

ВЫХОД (p: Человек)ext wr pres: Рабочиеpre p in set presсообщение прес = прес ~ \ {р};

ЕСТЬ-ПРИСУТСТВУЕТ (p: Person) r: boolвнешняя печать: Рабочиеразместить r <=> p в наборе пресс ~

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

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

См. Также [ править ]

• Формальные методы
• Формальная спецификация
• Код пиджина
• Логика предикатов
• Исчисление высказываний
• Язык спецификации Z , основная альтернатива VDM-SL (сравнить)
• COMPASS Modeling Language (CML), комбинация VDM-SL с CSP , основанная на унифицирующих теориях программирования , разработанная для моделирования систем систем (SoS)

Дальнейшее чтение [ править ]

• Бьёрнер, Дайнс; Клифф Б. Джонс (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.
• Фитцджеральд, Дж. С. и Ларсен, П. Г., Системы моделирования: практические инструменты и методы в разработке программного обеспечения . Издательство Кембриджского университета , 1998 ISBN 0-521-62348-0 (японское издание, паб. Iwanami Shoten 2003 ISBN 4-00-005609-3 ). ^[10]  
• Фитцджеральд Дж. С. , Ларсен П. Г., Мукерджи П., Плат Н. и Верхоф М. Утвержденные проекты для объектно-ориентированных систем . Springer Verlag 2005. ISBN 1-85233-881-4 . Веб-сайт поддержки [1] включает примеры и бесплатную поддержку инструментов. ^[11] 
• Джонс, CB , Систематическая разработка программного обеспечения с использованием VDM , Prentice Hall 1990. ISBN 0-13-880733-7 . Также доступно онлайн и бесплатно: http://www.csr.ncl.ac.uk/vdm/ssdvdm.pdf.zip 
• Бьёрнер, Д. и Джонс, CB , Разработка формальных спецификаций и программного обеспечения, Prentice Hall International, 1982. ISBN 0-13-880733-7 
• Дж. Доус, Справочное руководство VDM-SL , Pitman 1991. ISBN 0-273-03151-1 
• Международная организация по стандартизации , информационные технологии - Языки программирования, их среды и интерфейсы системного программного обеспечения - Венский метод разработки - Язык спецификации - Часть 1: Базовый язык Международный стандарт ISO / IEC 13817-1, декабрь 1996.
• Джонс, CB , Разработка программного обеспечения: строгий подход , Prentice Hall International, 1980. ISBN 0-13-821884-6 
• Джонс, CB и Шоу, RC (ред.), Примеры систематической разработки программного обеспечения , Prentice Hall International, 1990. ISBN 0-13-880733-7 
• Бикарреги, Дж. К., Фицджеральд, Дж. С. , Линдси, Пенсильвания, Мур, Р. и Ричи, Б., Доказательство в VDM: Руководство для практикующего . Формальные подходы Springer Verlag к вычислениям и информационным технологиям (FACIT), 1994. ISBN 3-540-19813-X . 

Эта статья основана на материалах, взятых из Free On-line Dictionary of Computing до 1 ноября 2008 г. и включенных в соответствии с условиями «перелицензирования» GFDL версии 1.3 или новее.

Ссылки [ править ]

Внешние ссылки [ править ]

• Информация о VDM и VDM ++ (архивная копия на archive.org)
• Венский язык определений (VDL)