Ві́денський ме́тод розро́бки (, 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 T2 … 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 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 Потужність (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) 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 -> 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 Множина значень (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++ структуризація проводиться з використанням класів та множинного наслідування. Ключовими концептами є: