МАРК РЕГНЕРУС ДОСЛІДЖЕННЯ: Наскільки відрізняються діти, які виросли в одностатевих союзах
РЕЗОЛЮЦІЯ: Громадського обговорення навчальної програми статевого виховання ЧОМУ ФОНД ОЛЕНИ ПІНЧУК І МОЗ УКРАЇНИ ПРОПАГУЮТЬ "СЕКСУАЛЬНІ УРОКИ" ЕКЗИСТЕНЦІЙНО-ПСИХОЛОГІЧНІ ОСНОВИ ПОРУШЕННЯ СТАТЕВОЇ ІДЕНТИЧНОСТІ ПІДЛІТКІВ Батьківський, громадянський рух в Україні закликає МОН зупинити тотальну сексуалізацію дітей і підлітків Відкрите звернення Міністру освіти й науки України - Гриневич Лілії Михайлівні Представництво українського жіноцтва в ООН: низький рівень культури спілкування в соціальних мережах Гендерна антидискримінаційна експертиза може зробити нас моральними рабами ЛІВИЙ МАРКСИЗМ У НОВИХ ПІДРУЧНИКАХ ДЛЯ ШКОЛЯРІВ ВІДКРИТА ЗАЯВА на підтримку позиції Ганни Турчинової та права кожної людини на свободу думки, світогляду та вираження поглядів Контакти
Тлумачний словник |
|
|||||||
Мови специфікації програм –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) дозволяють описувати різні способи можливого застосування системи. Програмування в обмеженнях використовують перед - і постумови для опису даних, операцій, інваріантів даних програм, що доводяться. Читайте також:
|
||||||||
|