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

Матеріал з Вікіпедії — вільної енциклопедії.
Перейти до: навігація, пошук

Ві́денський ме́тод розро́бки (англ. 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 | 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 Distributed union of set of sets s WTFIT?
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 беруться в порядку зростання ORLY?)
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++ структуризація проводиться з використанням класів та множинного наслідування. Ключовими концептами є:

  • Клас: Кожен клас синтаксично починається з ключового слова 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 найкращий комерційний інструмент для VDM та VDM++, створений, розповсюджується, розробляється та підтримується [ttp://www.csk.com CSK Systems], на основі раннніх розробок Danish Company IFAD. Інструкція) і підручник знаходяться в вільному доступі. Доступні всі ліцензії доступні, безплатні для повної версії інструменту. Повна версія включає автоматичну генерацію коду для мов Java і C++, підтримку динамічних бібліотек та CORBA.
  • Overture програма з відкритим кодом що розробляється спільнотою. Метою є надати безплатний інструмент для 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 в Данії та CSK в Японії.[1].
  • TradeOne: Деякі ключові компоненти офісної системи TradeOne що розроблялась y CSK systems для Японської фондової біржі використовували VDM.

Примітки[ред.ред. код]

  1. Peter Gorm Larsen, "Ten Years of Historical Development "Bootstrapping" VDMTools", In Journal of Universal Computer Science, volume 7(8), 2001

Посилання[ред.ред. код]