Студопедия
Новини освіти і науки:
МАРК РЕГНЕРУС ДОСЛІДЖЕННЯ: Наскільки відрізняються діти, які виросли в одностатевих союзах


РЕЗОЛЮЦІЯ: Громадського обговорення навчальної програми статевого виховання


ЧОМУ ФОНД ОЛЕНИ ПІНЧУК І МОЗ УКРАЇНИ ПРОПАГУЮТЬ "СЕКСУАЛЬНІ УРОКИ"


ЕКЗИСТЕНЦІЙНО-ПСИХОЛОГІЧНІ ОСНОВИ ПОРУШЕННЯ СТАТЕВОЇ ІДЕНТИЧНОСТІ ПІДЛІТКІВ


Батьківський, громадянський рух в Україні закликає МОН зупинити тотальну сексуалізацію дітей і підлітків


Відкрите звернення Міністру освіти й науки України - Гриневич Лілії Михайлівні


Представництво українського жіноцтва в ООН: низький рівень культури спілкування в соціальних мережах


Гендерна антидискримінаційна експертиза може зробити нас моральними рабами


ЛІВИЙ МАРКСИЗМ У НОВИХ ПІДРУЧНИКАХ ДЛЯ ШКОЛЯРІВ


ВІДКРИТА ЗАЯВА на підтримку позиції Ганни Турчинової та права кожної людини на свободу думки, світогляду та вираження поглядів



Мови специфікації програм –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) дозволяють описувати різні способи можливого застосування системи.

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


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

  1. Basic Concept of Security and Defense
  2. Cisco Packet Tracer - Знайомство з програмою. Інтерфейс
  3. Concepts and Principles
  4. Different phonological schools and their concept of phoneme
  5. I. Введення в розробку програмного забезпечення
  6. II. Вимоги до складання паспорта бюджетної програми
  7. II. Із програм для 11 класу
  8. II. ПРОГРАМА КУРСУ
  9. II.1 Програмне забезпечення
  10. III. Етапи розробки програмного забезпечення
  11. III. Навчально-програмний етап.
  12. III. Програма




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

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

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

  

© studopedia.com.ua При використанні або копіюванні матеріалів пряме посилання на сайт обов'язкове.


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