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

Ві́денський ме́тод розро́бки (англ. Vienna Development Method, VDM) — набір технологій для моделювання комп'ютерних систем, аналізу створених моделей і переходу до деталізованого проектування та програмування. Один з найстаріших формальних методів, вплинув на розвиток багатьох інших, як Z, RAISE, та B. За його спиною стоять інструменти промислової якості, та стандарт ISO. Метод з'явився в результаті роботи віденської лабораторії IBM в середині 70-тих. Нотація та допоміжні інструменти з того часу постійно розвивались, і сьогодні метод застосовується до широкого кола задач.

Має розширення VDM++, для об'єктно-орієнтованих систем.

Філософія

Обчислювальні системи можуть бути змодельованими через мову VDM-SL на вищому рівні абстракції ніж той, що може бути досягнутий використанням мов програмування. Це дозволить аналізувати проектування та означення ключових властивостей, враховуючи також дефекти на ранніх стадіях розробки. Моделі, які були проаналізовані, можуть бути переведені в детальний проект системи через процес вдосконалення та фільтрації. Мова має формальну семантику, що дозволяє доводити властивості моделей з високим ступенем впевненості. Також мова має виконувану підмножину, тому моделі можна аналізувати через тестування. Виконуються моделі через графічний інтерфейс, тому можуть бути оціненими експертами, яким не обов'язково знайомитись із самою мовою моделювання.

Можливості VDM

Синтаксис та семантика VDM-SL і VDM++ детально описуються в інструкціях до VDMTools. Стандарт ISO містить формальний опис семантики мови. В решті цієї статті використовується описаний ISO синтаксис для обміну (ASCII). Деякі тексти потребують точнішого математичного запису.

Модель VDM-SL — це опис системи, що дається в термінах функцій, які виконуються над даними. Він складається з описів типів даних і функцій та операцій, що застосовуються до цих типів.

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

VDM-SL включає наступні типи, що моделюють числа та символи:

Базові типи
Тип	Пояснення	Значення
bool	Булевий тип	false, true
nat	Натуральне число (включно з нулем)	0, 1, 2, 3, …
nat1	Натуральне число (без нуля)	1, 2, 3, 4, …
int	Ціле число	…, −3, −2, −1, 0, 1, 2, 3, …
rat	Раціональне число	a/b, де a та b цілі, b не 0
real	Дійсне число	…
char	Символи	A, B, C, …
token	Неструктуровані лексеми	…
<A>	тип quote, що містить значення <A>	…

Типи даних описуються для представлення основних даних системи, що моделюється. Опис кожного типу представляє нове ім'я типу, і дає представлення в термінах базових типів, або типів, що вже були описані. Наприклад тип, що моделює ідентифікатор користувача в системі керування аккаунтами, може бути описаний так:

types
    UserId = nat

Для маніпулювання значеннями які належать типам, описуються оператори. Цілочисельне додавання, віднімання і інше даються вже готовими, так як і булеві оператори такі як рівність та нерівність. Мова не фіксує мінімальне чи максимальне можливе число, чи точність для дійсних чисел. Такі обмеження описуються в міру необхідності для кожної моделі, за допомогою інваріантів типів даних — булевих виразів, які описують вимоги, яких мають притримуватись всі елементи описуваного типу. Наприклад вимога того що ідентифікатор користувача має бути не більшим за 9999 може бути описаний так (де <= означає булевий оператор «менше чи рівне» для натуральних чисел):

UserId = nat
inv uid == uid <= 9999

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

Інші базові типи включають char для символів. В деяких випадках представлення типу не стосується цілей моделі і тільки додає складності. В таких випадках члени типу представляються як безструктурні токени. Значення на типах токенів можуть тільки перевірятись на рівність — і не описано ніяких інших операцій. Де потрібні особливі, іменовані значення вводиться тип quote. Кожен такий тип складається з однієї змінної що однойменна типу. Значення типу quote (також відомі як quote literals) можуть тільки перевірятись на рівність.

Наприклад, в моделюванні світлофора, зручно описати значення, що представляють кольори сигналів, як quote types:

 <Red>, <Amber>, <FlashingAmber>, <Green>

Конструктори типів: Об'єднання, Добуток та композитні типи

Базові типи дуже обмежені. Зате можна створювати більш структуровані типи за допомогою конструкторів.

Конструктори базових типів
T1 ${\displaystyle |}$ T2 ${\displaystyle |}$ … ${\displaystyle |}$ Tn	Об'єднання типів T1,...,Tn
T1*T2*...*Tn	Декартовий добуток типів T1,...,Tn
T :: f1:T1 ... fn:Tn	Композитний (Структурний) тип

Найпростіший конструктор — об'єднання базових типів. Тип A | B містить всі елементи типу A і всі елементи типу B. В прикладі зі світлофором, тип що моделює колір сигналу може бути записаний так:

SignalColour =  <Red> | <Amber> | <FlashingAmber> | <Green>

Всі зазначені типи в VDM-SL описуються аналогічно тому, як показано вище, за допомогою об'єднання quoute types.

Декартів добуток також описується в 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) == day <=31 and month<=12

моделює простий тип дати. Значення mk_Date(1,4,2001) відповідає 1 квітня 2001. Якщо дана дата d, то вираз d.month є натуральним числом, що представляє місяць. Обмеження на кількість днів в місяці і високосні роки можуть бути включені в інваріант.

Колекції: Множини, Відображення та Послідовності

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

Конструктор типу «множина» (пишеться set of T де T це попередньо описаний тип) створює тип, в який входять всі скінченні множини значень що беруться з типу T. Наприклад, опис типу

 UGroup = set of UserId

описує тип UGroup що складається з усіх скінченних множин зі значень UserId. Над множинами описуються різні оператори, для конструювання їх об'єднання, перетину, визначення строгого та нестрогого включення і т. д.

Основні оператори на множинах (s, s1, s2 — множини)
{a, b, c}	Перечислення множини : множина з елементів a, b і c
${\displaystyle \{}$ x ${\displaystyle |}$ x:T & P(x)${\displaystyle \}}$	Включення множини: множина елементів 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	Потужність (cardinality) множини s

Конструктор скінченної послідовності (пишеться seq of T де T тип визначений раніше) утворює тип, в який входять всі скінченні списки значень взятих з типу T. Наприклад, означення типу

String = seq of char

Описує тип String що утворений з усіх скінченних рядків символів. Задаються оператори для конструювання конкатенацій, вибору елементів та підпослідовностей і т.і. Багато з цих операцій є частковими, тобто можуть використовуватись не у всіх випадках. Наприклад, операція вибору п'ятого елементу послідовності що містить тільки три елементи є невизначеною.

Порядок та повторення елементів в послідовності є важливими, тому [a, b] не дорівнює [b, a], і [a] не дорівнює [a, a].

Основні оператори на послідовностях (s, s1,s2 — послідовності)
[a, b, c]	Перелічення послідовності: послідовність елементів a, b та c
[f(x)${\displaystyle |}$ x:T & P(x)]	Включення послідовності: послідовність виразів f(x) для кожного x з (числового) типу T, для якого винонується P(x) (x значення x беруться в порядку зростання)
hd s	Голова (перший елемент) s
tl s	Хвіст (все що залишилось від s після того як відірвали голову)
len s	Довжина s
elems s	Множина елементів s
s(i)	i^-тий елемент s
s1^s2	послідовність утворена за допомогою конкатенації послідовностей s1 та s2

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

 Birthdays = map String to Date

Задає тип Birthdays який відображає рядки символів в дати. Знову ж таки, описуються оператори для відношень.

Основні оператори на відношеннях
{a ${\displaystyle |}$-> r, b ${\displaystyle |}$-> s}	Перелічення відношеня: a відображається в r, b відображається в s
{x ${\displaystyle |}$-> f(x) ${\displaystyle |}$ x:T & P(x)}	Задання відношення: x відображається в f(x) для всіх x з типу T для яких виконується P(x)
dom m	Множина визначення (домен) m
rng m	Множина значень (range) m
m(x)	m застосоване до x
m1 munion m2	Об'єднання відношень m1 та m2 (m1, m2 мають бути сумісними там де вони накладаються)
m1 ++ m2	m2 накласти на m1.

Структурування

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

Структуризація в VDM-SL

Стандарт ISO для VDM-SL є інформативним додатком, що містить різні принципи структуризації. Існують такі традиційні принципи приховування інформації з модулями:

• Іменування модулів: Кожен модуль синтаксично починається ключовим словом module після якого пишуть ім'я модуля. В кінці модуля пишуть ключове слово end після якого також стоїть ім'я модуля.
• Імпорт: Можливо імпортувати описи які експортуються в інші модулі. Це робиться в розділі імпорту який почитається з слова imports і продовжується послідовністю імпортів з різних модулів. Кожен з цих імпортів починається з слова from, потім ім'я модуля, і підписів модуля. Підписами модуля може бути як просто слово all, що вказує на імпорт всіх описів які експортуються з того модуля, або послідовністю конктретно вказаних описів. Підписи імпорту окремі для типів, значень, функцій та операцій і кожен з таких підписів починається з відповідного ключового слова. На додаток, ці підписи імпорту іменують конструкції до яких хочуть отримати доступ. Також може бути присутня додаткова інформація типу, і наостанок є можливість перейменувати кожну конструкцію що імпортується. Також, якщо потрібна можливість доступу до складових типу, при його імпорті потрібно вживати ключове словоstruct
• Експорт:Якщо модуль хоче дати іншим модулям доступ до своїх описів, він має експортувати їх ключовим словом exports після якого пишуть підписи що експортуються з нього. Підписи що експортуються можуть бути як ключовим словом all так і послідовністю конкретних підписів. Такі підписи задаються окремо для типів, значень, функцій і операцій кожна з яких починається з відповідного ключового слова. В випадку коли хтось хоче експортувати внутрішню структуру типу, треба використати ключове слово struct.
• Особливіші можливості: В попередніх версіях VDM-SL tools також була підтримка модулів з параметрами, та реалізації таких модулів. Тим не менш, такі можливості були видалені з VDMTools близько 2000-го бо майже ніколи не використовувались в промислових програмах та не було значної кількості інструментів з такими можливостями.

Структуризація VDM++

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

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

Моделювання функціональності

Функціональне моделювання

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

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

Тут постумова не описує метод для обчислення результату r, але вказує які властивості він має мати. Зауважте, що це описує функцію, яка повертає правильний квадратний корінь; немає вимоги, щоб це був додатний чи від'ємний корінь. Наприклад можна задати функцію що повертає від'ємний корінь з 4 але додатній з усіх інших вводів. Також варто зауважити, що функції в VDM-SL мають бути детерміновані тобто функція завжди має повертати одні і ті самі результати на одних і тих самих даних.

Строгіша специфікація функції досягається посиленням постумови. Наприклад наступний опис змушує функцію повертати «правильний» корінь.

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

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

 SQRTP(x:real)r:real
 pre x >=0
 post r*r = n 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)

і явну функцію:

 f:T_p -> T_r

ми кажемо, що вона задовольняє специфікацію тоді і тільки тоді:

forall p in set T_p & pre-f(p) => f(p):T_r and post-f(p, f(p))

Тому, «f є корректною реалізацією» має інтерпретуватись як «f задовольняє специфікацію».

Моделювання станів

В VDM-SL, функції не мають побічних ефектів таких як зміни стану постійної глобальної змінної. Це корисна здатність багатьох мов програмування, тому подібна концепція існує; тільки замість функцій для зміни змінних стану (глобальних) використовуються операції.

Наприклад, якщо ми маємо стан, що складається з одної змінної someStateRegister : nat, ми можемо описати це в VDM-SL як:

state Register of 
    someStateRegister : nat 
end

А в VDM++ це описують трохи інакше:

instance variables
    someStateRegister : nat

Операція для завантаження значення в цю змінну має бути описана як:

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

Пункт зовнішнє (ext) описує до яких частин стану операція має доступ; rd вказує доступ тільки для читання а wr доступ для читання та запису.

Іноді важливо послатись на значення змінної до її модифікації; наприклад операція що додає значення до змінної може бути описана так:

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

Де символ ~ біля змінної стану вказує на значення змінної до виконання операції.

Приклади

Функція max

Це приклад неявного опису функції. Функція повертає елемент з множини додатних цілих:

max(s:set of nat)r:nat
pre true
post r in set s and 
    forall r' in set s & r' <= r

Множення натуральних чисел

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

Застосуємо доведення forall p:T_p & pre-f(p) => f(p):T_r and 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)

Тоді доведення приймає вигляд:

 forall i, j : nat & multp(i,j):nat and multp(i, j) = i*j

Можна довести коректність цього через:

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

Абстрактний тип — черга

Це класичний приклад що ілюструє використання неявних специфікацій операцій в моделі відомої структури даних, що базується на станах. Черга моделюється як послідовність що складається з елементів типу Qelt. Представлення типу Qelt є неважливим, тому задається як token.

types
    Qelt = token;
    Queue = seq of 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:Queue
 pre q <> [] 
 post q~ = [e]^q;

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

Приклад банківської системи

Як дуже простий приклад моделі VDM-SL візьмемо систему для обслуговування деталей рахунків клієнтів банку. Клієнти моделюються номерами (CustNum), рахунки теж (AccNum). Представлення номерів не має значення, тому теж моделюється неструктурованими лексемами. Баланси і перевищення кредиту теж моделюються числовими типами.

 AccNum = token;
 CustNum = token;
 Balance = int; 
 Overdraft = nat;

 AccData :: owner : CustNum
            balance : Balance

 state Bank of 
   accountMap : map AccNum to AccData
   overdraftMap : map CustNum to Overdraft
 inv mk_Bank(accountMap,overdraftMap) == for all a in set rng accountMap & a.owner in set dom overdraftMap and a.balance >= -overdraftMap(a.owner)

З операціями: NEWC додає новий номер клієнта:

 operations 
 NEWC(od : Overdraft)r : CustNum
 ext wr overdraftMap : map CustNum to Overdraft
 post r not in set dom ~overdraftMap and 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 [Архівовано 24 серпня 2010 у Wayback Machine.] найкращий комерційний інструмент для VDM та VDM++, створений, розповсюджується, розробляється та підтримується CSK Systems [Архівовано 13 січня 2010 у Wayback Machine.], на основі ранніх розробок Danish Company IFAD. Інструкція [Архівовано 28 травня 2009 у Wayback Machine.]) і підручник знаходяться в вільному доступі. Доступні всі ліцензії доступні, безплатні для повної версії інструменту. Повна версія включає автоматичну генерацію коду для мов Java і C++, підтримку динамічних бібліотек та CORBA.
• Overture [Архівовано 31 серпня 2010 у Wayback Machine.] програма з відкритим кодом що розробляється спільнотою. Метою є надати безплатний інструмент для VDM++ на основі платформи Eclipse.
• SpecBox: від Adelard надає перевірку синтаксису, деяку просту перевірку семантики, та файл LaTeX що дозволяє отримати специфікацію в математичному записі. Це безплатний інструмент, проте він більше не підтримується.
• Макроси LaTeX та LaTeX2e, що підтримують запис моделей VDM в математичному синтаксисі стандарту ISO. Розробляються та підтримуються Національною фізичною лаболаторією Об'єднаного Королівства. Документація та макроси доступні онлайн.

Промисловий досвід

VDM широко застовосувався в різних прикладних областях. Найвідомішими з цих застосувань є:

• Компілятори Ada та Chill: Перший в Європі підтверджений компілятор мови Ada був розроблений в DDC-International з використанням VDM. Подібно, семантику Chill та Modula-2 описували з використанням VDM.
• ConForm: Експеримент в British Aerospace з порівняння їх звичайного методу розробки захищеного шлюзу з розробкою з використанням VDM.
• Dust-Expert: Проект Adelard в Об'єднаному Королівстві для програм що визначають достатній рівень безпеки в планах заводів.
• Розробка VDMTools: Більшість компонент набору інструментів VDMTools й самі були розроблені з використанням VDM. Ця розробка була проведена на IFAD [Архівовано 28 липня 2010 у Wayback Machine.] в Данії та CSK [Архівовано 4 лютого 2010 у Wayback Machine.] в Японії.^[1].
• TradeOne: Деякі ключові компоненти офісної системи TradeOne що розроблялась y CSK [Архівовано 4 лютого 2010 у Wayback Machine.] systems для Японської фондової біржі використовували VDM.

Примітки

1. Peter Gorm Larsen, "Ten Years of Historical Development "Bootstrapping" VDMTools" [Архівовано 23 січня 2021 у Wayback Machine.], In Journal of Universal Computer Science, volume 7(8), 2001

Посилання

• VDM Portal [Архівовано 28 серпня 2008 у Wayback Machine.]