Ви є тут

Композиційні методи специфікації та верифікації програмних систем

Автор: 
Панченко Тарас Володимирович
Тип роботи: 
Дис. канд. наук
Рік: 
2006
Артикул:
0406U002017
129 грн
Додати в кошик

Вміст

РОЗДІЛ 2
Композиційно-номінативні методи специфікації
2.1. Композиційно-номінативний підхід до моделювання програмних систем
Композиційне програмування (КП) як теоретичне підґрунтя і основа програмології
– науки про програми – було започатковане В. Н. Редьком [21,22] в 1960-х роках
як розвиток структурологічного підходу Г. Фреге [79], який був перенесений на
програмування А. А. Ляпуновим [80–82] та розвинений Ю. І. Яновим [83,84],
А. П. Єршовим [85–90], Л. О. Калужніним [91,92], В. М. Глушковим [93,94] та
іншими.
В основі КП покладено декілька базових принципів, які досить детально
обґрунтовуються в роботах [21,24,47] та ряді інших. Ці фундаментальні принципи
визначають напрямок досліджень композиційних методів, які є основою КП, та
накреслюють мету КП. Головні принципи носять філософсько-методологічне
навантаження і стверджують, що:
програмування – не стала величина, а така, що розвивається, отже і досліджувати
це поняття необхідно у його розвитку (принцип розвитку), (як наслідок, всі
об’єкти мають бути досліджені методом від абстрактного до конкретного), більш
того, уточнення поняття програми відбувається у відповідності до загальних
законів гносеології (принцип гносеологічності),
прагматичний, семантичний та синтаксичний аспекти програмування підпорядковані
один одному (принцип підпорядкування) і можуть бути відокремлені при
дослідженні (принцип відокремлення), а саме: прагматика від семантики, а
семантика від синтаксису, що дозволяє зосереджувати увагу лише на головних
аспектах при розгляді на відповідних рівнях (абстракції),
на найвищому рівні абстракції програми можна розглядати як функції, що вхідним
даним ставлять у відповідність деякі вихідні дані, але точніше – програми суть
застосування композицій (засобів побудови) до функцій (принципи
функціональності та композиційності).
Останній принцип конкретизує програми як результат застосування деяких засобів
побудови до базових функцій, а отже вказує на структурність програм як
результату, а також на важливість розгляду процесу побудови програм –
програмобудування (або програмування).
Ще один важливий принцип – інтенсіональності (інтенсіонал від лат. intension –
смисл, зміст), який підкреслює важливу відмінність програмування від класичної
математики. В програмуванні усвідомлення важливості інтенсіональних аспектів
сформувалось відносно недавно [1]. В. Н. Редько сформулював принцип
інтенсіональності: програмування – інтенсіональне [47,24] за своєю природою.
Останнє підсилює принцип відокремлення і означає, що семантика не визначається
синтаксисом, а також, що об’єкти, структури та поняття, що використовуються в
програмуванні мають передусім смислове (смисл, інтенсіонал) навантаження, а не
формальне (форма, екстенсіонал). Простий приклад: у функції може існувати
деякий “час життя”, після якого вона змінює свою поведінку (наприклад, перестає
перетворювати вхідні дані на вихідні). До речі, це дуже характерний приклад для
практичного програмування (наприклад, питання доступності в мережі Інтернет
деяких відомих ресурсів), але з математичної точки зору (екстенсіонально) така
ситуація є незрозумілою (функція або є, або її немає...).
Далі на основі цих принципів відбувається розвиток теорії програмування  –
програмології. Головною категорією програмології, яка забезпечує її
концептуальну єдність, є поняття програми. Тому побудова фундаменту
програмології зводиться передусім до експлікації за Карнапом [95] цього
фундаментального поняття [24] та розробки методів специфікації програмних
систем. Експлікація за Карнапом (від лат. explicatio – уточнення, розгортання,
роз’яснення) являє собою математично строгу експлікату, яка отримується шляхом
адекватного розгортання вихідного інтуїтивного поняття як експліканда,
починаючи з його роз’яснення і закінчуючи уточненням [24].
На шляху експлікації програмування програмні системи розглядають, як правило,
на трьох рівнях абстракції [49] по даним:
абстрактний, коли про дані нічого не відомо і вони є нерозрізнюваними “чорними
скриньками”,
булевий, коли дані є конкретними “білими скриньками”, і приймають значення з
допустимої множинами (розрізняють, як правило, передбулевий (тільки одне
значення), булевий (два значення) та постбулевий (більше) підрівні),
іменний (або номінативний), коли дані розглядаються як структуровані об’єкти,
що мають певну будову.
Перший рівень є досить абстрактним, він не представляє великого інтересу з
точки зору практичного програмування, але необхідний для послідовності та
повноти розгляду програмних систем.
Другий рівень можна асоціювати з булевою алгеброю та теорією множин. Аналогії
очевидні та вказують на реальний зв’язок класичної дискретної математики з КП.
Третій рівень є подальшим розвитком і синтезом перших двох. Він найбільш
адекватно (але все ще досить загально) специфікує структури даних реального
програмування. На цьому рівні постулюється принцип іменування (або
номінативності), який фіксує структуру даних. А саме, вводиться множина (домен)
імен [2 тут і надалі будемо використовувати стандартні позначення для
композиційних методів та композиційно-номінативних мов, при необхідності
надаючи посилання на джерела] V і множина (домен) значень W. Тоді множина
(домен) даних D визначається як D = W И (V ® D). Визначення є рекурсивним і
означає, що кожне дане має таку структуру – воно містить значення з множини
базових значень W, або є множиною пар: ім’я (з V) – значення (з D). В
залежності від того, чи є відображення V ® D однозначним чи ні, розрізняють
іменні (однозначні) та номінативні (багатозначні – одне ім’я може мати кілька
знач