Метод 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 включает следующие основные типы моделей чисел и символов:
bool | Логический тип данных | false true |
nat | натуральные числа (включая ноль) | 0, 1, 2, 3, 4, 5 ... |
nat1 | натуральные числа (исключая ноль) | 1, 2, 3, 4, 5, ... |
int | целые числа | ..., −3, −2, −1, 0, 1, 2, 3, ... |
rat | рациональное число | a / b , где а и b - целые числа, b не 0 |
real | вещественные числа | ... |
char | символы | А, Б, В, ... |
token | бесструктурные токены | ... |
| тип котировки, содержащий значение
| ... |
Типы данных определены для представления основных данных моделируемой системы. Каждое определение типа вводит новое имя типа и дает представление в терминах основных типов или в терминах уже введенных типов. Например, тип, моделирующий идентификаторы пользователей для системы управления входом в систему, может быть определен следующим образом:
типыUserId = nat
Для управления значениями, принадлежащими типам данных, для значений определены операторы. Таким образом, обеспечивается сложение натуральных чисел, вычитание и т. Д., А также логические операторы, такие как равенство и неравенство. Язык не устанавливает максимальное или минимальное представимое число или точность действительных чисел. Такие ограничения определяются там, где они требуются в каждой модели, посредством инвариантов типов данных - логических выражений, обозначающих условия, которые должны соблюдаться всеми элементами определенного типа. Например, требование, чтобы идентификаторы пользователей не превышали 9999, можно было бы выразить следующим образом (где <=
- логический оператор "меньше или равно" для натуральных чисел):
UserId = natinv uid == uid <= 9999
Поскольку инварианты могут быть произвольно сложными логическими выражениями, а членство в определенном типе ограничено только теми значениями, которые удовлетворяют инварианту, правильность типа в VDM-SL не может быть автоматически разрешена во всех ситуациях.
Другие базовые типы включают char для символов. В некоторых случаях представление типа не имеет отношения к цели модели и только добавит сложности. В таких случаях члены типа могут быть представлены как бесструктурные токены. Значения типов токенов можно сравнивать только на равенство - для них не определены другие операторы. Если требуются определенные именованные значения, они представлены как типы кавычек. Каждый тип кавычек состоит из одного именованного значения с тем же именем, что и сам тип. Значения типов кавычек (известных как литералы кавычек) можно сравнивать только на равенство.
Например, при моделировании контроллера светофора может быть удобно определить значения для представления цветов светофора в виде типов цитат:
<Красный>, <Янтарь>, <Мигающий Янтарь>, <Зеленый>
Конструкторы типов: объединение, произведение и составные типы
Сами по себе основные типы имеют ограниченную ценность. Новые, более структурированные типы данных создаются с помощью конструкторов типов.
T1 | T2 | ... | Tn | Союз типов T1,...,Tn |
T1*T2*...*Tn | Декартово произведение типов T1,...,Tn |
T :: f1:T1 ... fn:Tn | Составной (запись) тип |
Самый простой конструктор типов образует объединение двух предопределенных типов. Тип (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
, имена полей могут использоваться для выбора именованного компонента. Например, тип
Дата :: день: 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
значений. На множествах определены различные операторы для построения их объединений, пересечений, определения собственных и нестрогих отношений подмножеств и т. Д.
{a, b, c} | Перечисление набора: набор элементов a , b иc |
{x | x:T & P(x)} | Понимание набора: набор x из типа, T такой, чтоP(x) |
{i, ..., j} | Набор целых чисел в диапазоне i доj |
e in set s | e является элементом множества s |
e not in set s | e не является элементом множества s |
s1 union s2 | Союз наборов s1 иs2 |
s1 inter s2 | Пересечение множеств s1 иs2 |
s1 \ s2 | Установите разницу наборов s1 иs2 |
dunion s | Распределенное объединение множества наборов s |
s1 psubset s2 | s1 - (собственное) подмножество s2 |
s1 subset s2 | s1 - (слабое) подмножество s2 |
card s | Мощность множества s |
Последовательности
Конструктор типа с конечной последовательностью (записывается, seq of T
где T
- предопределенный тип) конструирует тип, состоящий из всех конечных списков значений, взятых из типа T
. Например, определение типа
Строка = последовательность символов
Определяет тип, String
состоящий из всех конечных строк символов. В последовательностях определены различные операторы для построения конкатенации, выбора элементов и подпоследовательностей и т. Д. Многие из этих операторов являются частичными в том смысле, что они не определены для определенных приложений. Например, выбор 5-го элемента последовательности, содержащей только три элемента, не определен.
Порядок и повторение элементов в последовательности имеет значение, поэтому [a, b]
не равно [b, a]
и [a]
не равно [a, a]
.
[a, b, c] | Последовательность перечисления: последовательность элементов a , b иc |
[f(x) | x:T & P(x)] | Понимание последовательности: последовательность выражений f(x) для каждого x (числового) типа T , P(x) содержащая ( x значения, взятые в числовом порядке) |
hd s | Голова (первый элемент) s |
tl s | Хвост (оставшаяся последовательность после удаления головы) s |
len s | Длина s |
elems s | Набор элементов s |
s(i) | i - Й элементs |
inds s | набор индексов для последовательности s |
s1^s2 | последовательность, образованная конкатенацией последовательностей s1 иs2 |
Карты
Конечное отображение - это соответствие между двумя наборами, доменом и диапазоном, с элементами индексации домена диапазона. Следовательно, он похож на конечную функцию. Конструктор типа отображения в VDM-SL (написано, map T1 to T2
где T1
и T2
являются предопределенными типами) конструирует тип, состоящий из всех конечных отображений из наборов T1
значений в наборы T2
значений. Например, определение типа
Дни рождения = сопоставить строку с датой
Определяет тип, Birthdays
которому сопоставляются символьные строки Date
. Опять же, в отображениях определены операторы для индексации в отображении, объединения отображений, перезаписи, извлечения вложенных отображений.
{a |-> r, b |-> s} | Отображение перечисления: a сопоставляется r , b сопоставляется сs |
{x |-> f(x) | x:T & P(x)} | Понимание сопоставления: x сопоставляется f(x) для всех x для типа, T такого чтоP(x) |
dom m | Область m |
rng m | Диапазон m |
m(x) | m применительно к x |
m1 munion m2 | Объединение сопоставлений m1 и m2 ( m1 , m2 должно быть согласовано там, где они перекрываются) |
m1 ++ m2 | m1 перезаписан m2 |
Структурирование
Основное различие между нотациями 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
Это можно показать правильно:
- Доказательство того, что рекурсия заканчивается (это, в свою очередь, требует доказательства того, что числа становятся меньше на каждом шаге)
- Математическая индукция
Абстрактный тип данных очереди
Это классический пример, иллюстрирующий использование неявной спецификации операции в модели хорошо известной структуры данных на основе состояний. Очередь моделируется как последовательность, состоящая из элементов определенного типа 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 или новее.
Рекомендации
- ^ Некоторое представление об этой работе, включая технический отчет TR 25.139 « Формальное определение подмножества PL / 1 » от 20 декабря 1974 года, перепечатано в Jones 1984, p.107-155. Особо следует отметить упорядоченный список авторов: Х. Бекич, Д. Бьёрнер, В. Хенхапл, К. Б. Джонс, П. Лукас.
- ^ Двойной плюс заимствован изобъектно-ориентированного языка программирования C ++, основанного на C.
- ^ Бьорнер & Jones 1978, Введение , p.ix
- ^ Вступительное слово Клифф Б. Джонс (редактор) в Bekič 1984, p.vii
- ^ Бьорнер & Jones 1978, Введение , p.xi
- ^ Бьорнер & Jones 1978, с.24.
- ^ См. Статью о настойчивости для ее использования в информатике.
- ^ Клемменсен, Герт Б. (январь 1986 г.). «Ретаргетинг и повторный хостинг системы компиляции DDC Ada: пример из практики - Honeywell DPS 6». ACM SIGAda Ada Letters . 6 (1): 22–28. DOI : 10.1145 / 382256.382794 .
- ↑ Питер Горм Ларсен, «Десять лет исторического развития» Начальная загрузка «VDMTools» , в журнале Universal Computer Science , том 7 (8), 2001 г.
- ^ Системы моделирования: практические инструменты и методы в разработке программного обеспечения
- ^ Проверенные проекты для объектно-ориентированных систем
Внешние ссылки
- Информация о VDM и VDM ++ (архивная копия на archive.org)
- Венский язык определений (VDL)