Мови специфікації програм –VDM, RAISE, Concept

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

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

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

Існують різні підходи до класифікації мов специфікації. Це такі.

Універсальні мови специфікації – VDM, Z, RAISE, Spec# мають загально математичну основу з такими засобами:

1) логіки першого порядку, включаючи квантори;

2) арифметичні операції;

3) множини і операції над множинами;

4) описи послідовностей (кортежів, списків) і операції над ними;

5) описи функцій і операцій над ними;

6) описи древо видних структур;

7) засоби побудови моделей областей;

8) процедурні засоби мов програмування (оператори присвоювання, циклу, вибору, виходу);

9) операції композиції, аргументами і результатами яких можуть бути функції, вирази, оператори;

10) механізм конструювання нових структур даних.

Мови специфікації предметних областей (доменів) у програмуванні:

1) специфікації доменів;

2) описи взаємодій і паралельного виконання;

3) специфікації мов програмування і трансляторів;

4) специфікації баз даних і знань;

5) специфікації пакетів прикладних програм тощо.

Мови специфікації специфіки доменів DSL (Domain Specific Language) призначені для формалізованого опису задач в термінах предметної області, що підлягає моделюванню. Ці мови можна підрозділити на зовнішні і внутрішні. Зовнішні мови (типу UML, OWL, XML і ін.) по рівню вищі за мови програмування і зводяться до мови DSL спеціальними генераторами або текстовими редакторами, що трансформують абстрактні поняття та задачі ПрО до понять мови DSL. Внутрішні мови – мови програмування різних задач та їх препроцесори обмежені синтаксисом і семантикою основної базової мови програмування.

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

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

Формальні мови специфікації мов програмування спочатку застосовувалися при розробленні трансляторів. Так, зазвичай, синтаксис мови програмування описувався у КС–граматиках у формі Бекуса–Наура. Такого типа мови є метамовами. Для специфікації семантики мов програмування використовуються формалізми рівностей. Техніка опису мов програмування базується на атрибутних граматиках і абстрактних типах даних з використанням денотаційних, алгебраїчних і атрибутних підходів. У якості мов специфікації трансляторів, а також систем реального часу, де правильність і точність виконання програм є головними, використовуються мови Z, VDM, RAISE.

Мови специфікації з орієнтацією на засоби програмування базуються на рівностях і підстановках з операційною семантикою (Лісп, Рефал); логічні мови; мови операцій (АPL) над послідовностями і матрицями; табличні мови; мережі, графи та ін. Мова логіки предикатів використовується для запису перед – і постумов, інваріантів і процесу верифікації (наприклад, Пролог).

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

У денотаційному підході до семантики надається перевага статичному опису об'єктів у термінах математичних властивостей, а у аксіоматичному – специфікації властивості об'єктів у рамках деякої логічної системи, що містить правила виведення формул та/або інтерпретацій.

Окрім наведеної класифікації мов специфікацій існують інші. Наприклад, можлива класифікація специфікацій за способом виконання:

– виконувана (executable),

– алгебраїчна (algebraic),

– сценарна (use case or scenarios),

– в обмеженнях (constraints).

Виконувані специфікації припускають розроблення прототипів систем для досягнення встановленої мети (VDM, SDL, RSL).

Алгебраїчні специфікації та мови SDL, RSL містять механізми опису аксіом і тверджень, які призначені для проведення доказу специфікованих програм.

Сценарні специфікації (UML) дозволяють описувати різні способи можливого застосування системи.

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

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

<== попередня сторінка	\|	наступна сторінка ==>
Підходи і методи доказу програм	\|	Мова формальної специфікацій – VDM

Не знайшли потрібну інформацію? Скористайтесь пошуком google:

Генерація сторінки за: 0.005 сек.