• Гідрологія і Гідрометрія
• Господарське право
• Економіка будівництва
• Економіка природокористування
• Економічна теорія
• Земельне право
• Історія України
• Кримінально виконавче право
• Медична радіологія
• Методи аналізу
• Міжнародне приватне право
• Міжнародний маркетинг
• Основи екології
• Предмет Політологія
• Соціальне страхування
• Технічні засоби організації дорожнього руху
• Товарознавство продовольчих товарів

Мова формальної специфікацій – VDM

Мова специфікації VDM (Vienna Development Method) була розроблена у віденській лабораторії компанії IBM і призначалася для опису мов типу ПЛ/1, трансляторів і систем із складними структурами даних. У мові специфікується правильна програма і набір тверджень для її доведення.

Мова містить типи даних:

Х – натуральні числа з нулем;

N – натуральні числа без нуля;

Int – цілі числа;

Bool – булеві;

Qout – рядки символів;

Token – знаки і спеціальні позначення операцій.

Функція специфікує властивості структур даних і операцій над ними – апплікативно (функціонально) або імперативно (алгоритмічно). Наприклад, опис функції min у мові VDM двома способами:

min N1 N2 ® N3,

min (N1 N2) = if N1< N2 then N3.

Об'єкти мови VDM: множини, дерева, послідовності, відображення, сконструйовані складні структури.

Множина: X–set і операції Î,Í,È, Ç і ін. Правило, х Î А буде коректним тільки тоді, коли А є підмножиною множини, якій належить х. Дистрибутивне об'єднання підмножин покажемо на прикладі:

union {(1, 2), (0, 2), (3, 1) } = (0, 1, 2, 3).

Списки (послідовності): Х – операція, len – довжина списку, inds – номери елементу в списку. Наприклад, inds lst =(i ÎX [f £ i £ len]).

Узяття першого (голови) елементу списку –hd і залишку (хвоста) після видалення першого елементу із списку – tl. Наприклад, hd (а, b, с, d) = (a), tl (а, b, с, d) = (b, ,с, d).

Дерево: mk об'єднує послідовності, множини і відображення. Елементи дерев можуть конструюватися. Наприклад, час 10.30 – конструкція let mk, час (h, m) = t , tin визначає значення h = 10, а m = 30.

Відображення: map – таблиця з ключів і значень. Операція dom будує множину ключів, rng – множину його значень.

Специфікація програми у VDM – це опис інваріантних властивостей, наприклад, inv функція, аргументи і опис її операцій. Перевірки специфікації – це і перед – і постумови, твердження, які специфікуються засобами VDM, і мають таку семантику їх тлумачення у VDM.

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

Нижче наведено покрокову деталізацію специфікації програм мовою VDM:

1. Визначення термінів, якими буде специфікуватися програма.

2. Опис понять і об'єктів, для позначення яких використовується денотат, що ідентифікується за допомогою деякого імені (або фрази).

3. Опис інваріантних властивостей програми.

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

5. Розроблення формальних умов виконання інваріанту програми та специфікація перед –, постумов та тверджень щодо виконання інваріанту програми.

6. Статичний огляд інваріанту програми стосовно специфікованого формалізму доказу цього інваріанту.

7. Використання діючих CASE-засобів, що забезпечують виконання процесу верифікації програм.

Приклад програми. Реєстрація компонента (ком) в репозитарії (repoz). Опис даних на мові „Паскаль” з використанням конструкцій мови VDM при роботі зі списком компонентів (list_ptr).

post-Add_rd (r): Rn ® bool

r Ï elems l1.rds

li’.rds =li.rds <mk-R.card(r, <>)>& li’.ctlg = li.ctlgli’ril = li.ril

=type

list = record

next: pointer

value: poiter

end;

list_ptr = list;

R_card = record

r.name: string;

ком: list_ptr

end;

repoz = record

rdrs: list_ptr;

ctlg: list_ptr;

ril: list_ptr

end;

var

L: repoz;

procedure Add_rd(r=string);

var

rcrd:R_card;

LL : list_ptr;

begin

if find _rds, r) then

begin

writeln (‘компонент зарієстрований’)

end;

new (Rcrd);

Rcrd.r­_name := r;

Rcd.ком:=nil;

new (LL);

LL.next:=L.rds;

LL.value:=ltcrd;

L.rds:=LI.

end;

Читайте також:

1. Мова формальної специфікації – RAISE
2. Наслідки неформальної передачі інформації
3. Паспорт неформальної підліткової групи
4. Поняття організації. Сутність і основні риси формальної організації
5. Поняття та означення формальної системи знань

Переглядів: 914