4. Теорія програмування та обчислень

7. Методи формальної семантики

В реальних МП, в кращому випадку лише синтаксис задається строго формально, а семантика задається лише інтуїтивно, Тому з кожною мовою реального програмування спражена важлива проблема – формалізація її семантики. Задання семантики в кожному випадку спряжене з подоланням серйозних труднощів. Як бачили, навіть для такої “ювелірної” мови як λ-нотація було спряжене з подоланням принципової проблематики. Дійсно, так операція Ap,задана на впорядкованій парі (a,f), де a та f мають різний тип, семантика зпряжена з розв’язком проблеми самопримінення – примінення функції f до самої себе. В реальних МП ця проблема суттєво ускладнюється. Навіть в λ-численні ця проблема стояла відкритою більше 50-ти років. Теорія Скотта створила фундамент для розв’язку проблеми формалізації λ-нотації. В основі цієї формалізації лежить інтегрована структура програмування. Дійсно, задати формально семантику λ-нотації = задати семантику терму Ap(a,f) та терму x.t(x). Що стосується терму Ap(a,f), то він інтерпритується в семантичних структурах. Конкретніше, він інтерпритується як функція (а це поняття семантичне), що задана на парі (a,f), один з компонентів якої є знову функція (семантичне поняття) та об’єкт a (яке знову ж є теоретико-множинним елементом, а не символом – а це семантика). Звідси випливає, що інтерпритація a задається в термінах лише семантичних понять.

Розглянемо тепер другий терм - x.t(x).. Перш за все, відзначимо, що використовуючи співвідношення Шенфінкеля, що зіставляє кожній функції f(x,y) нову функцію (y)=f_x(y), що параметризована x-ом, ми зводимо інтерпритацію подібних термів до інтерпритації унарних функцій. Але ж, як бачимо, на відміну від семантики Ap(a,f), ми приречені поряд з суто семантичними поняттями використовувати синтаксичні поняття (типові вирази t(x) з вільно змінною x). В зв’язку з цим семантика вказаних виразів (тобто функція, що йому відповідає) задається шляхом стандартної інтерпритації терму t(x) на елементах з області значень змінної x, яка пробігає її. Таким чином, на відміну від аплікації, λ-абстракція інтерпретується шляхом від синтаксису до семантики. Таким чином, формалізація семантики λ-нотації є дійсно змішаною.

4. Теорія програмування та обчислень

8. Формальні методи програмування

Формальні методі (англ. Formal methods) — в комп'ютерних науках, основані на математиці методи написання специфікацій, розробки та верифікації (перевірки) програмного забезпечення (ПЗ) та комп'ютерного обладнання. Цей підхід особливо важливий для вбудованих систем, для яких важливими є надійність або безпека, для захисту від появи помилок в процесі розробки. Застосування формальних методів особливо ефективно на ранніх етапах написання вимог та специфікацій, але, також, можуть використовуватись для повністю формальної розробки реалізації (наприклад, програми). Існують стандарти на критерії безпечності та захищенності программ. Частіше за все для реалізації валідації ПЗ використовуються теорія скінчених автоматів.

Формальні методи можуть бути застосовані на декількох рівнях:

Рівень 0

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

Рівень 1

Формальний підхід до розробки програмного забезпечення та перевірки може використовуватись для формальнішої реалізації програми. Наприклад, може виконуватись доведення властивостей або уточнення (англ. refinement) із формальної специфікації в програмі. Такий підхід найоптимальніший у вбудованих системах, які повинні мати високий рівень безпеки або надійності.

Рівень 2

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

Відомі формальні методи: Event-B, Z-notation, ASM, RAISE, SLAM, Мережі Петрі та ін.