Метод доведення властивостей програм в композиційно-номінативних мовах IPCL
Викладено композиційний метод верифікації систем спеціального класу – моделі багатоекземплярного
 виконання програм у серверному середовищі з паралелізмом у режимі почергового виконання з пере
 ключенням і взаємодією через спільну пам’ять. У роботі специфіковано задачу, побудовано ві...
Збережено в:
| Дата: | 2008 |
|---|---|
| Автор: | |
| Формат: | Стаття |
| Мова: | Українська |
| Опубліковано: |
Інститут програмних систем НАН України
2008
|
| Теми: | |
| Онлайн доступ: | https://nasplib.isofts.kiev.ua/handle/123456789/329 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Цитувати: | Метод доведення властивостей програм в композиційно-номінативних мовах IPCL / Т.В. Панченко // Пробл. програмув. — 2008. — N 1. — С. 3-16. — Бібліогр.: 33 назв. — укр. |
Репозитарії
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1860217677791887360 |
|---|---|
| author | Панченко, Т.В. |
| author_facet | Панченко, Т.В. |
| citation_txt | Метод доведення властивостей програм в композиційно-номінативних мовах IPCL / Т.В. Панченко // Пробл. програмув. — 2008. — N 1. — С. 3-16. — Бібліогр.: 33 назв. — укр. |
| collection | DSpace DC |
| description | Викладено композиційний метод верифікації систем спеціального класу – моделі багатоекземплярного
виконання програм у серверному середовищі з паралелізмом у режимі почергового виконання з пере
ключенням і взаємодією через спільну пам’ять. У роботі специфіковано задачу, побудовано відповідні
моделі, сформульовано два варіанти часткової коректності програм на введених композиційних мовах та запропоновано методологію верифікації, що включає метод з лінійною складністю замість
експоненційної.
The compositional method for verification of special class systems, namely multi-instance program execution model in server environment with shared memory interleaving concurrency, is presented. The task is specified and appropriate models are developed here. Two types of partial correctness properties of programs in introduced compositional languages are formulated. Methodology of verification including method with linear complexity instead of exponential one is developed here.
|
| first_indexed | 2025-12-07T18:16:43Z |
| format | Article |
| fulltext |
Теоретичні та методологічні основи програмування
© Т.В. Панченко, 2008
ISSN 1727-4907. Проблеми програмування. 2008. № 1 3
УДК 681.3
Т.В. Панченко
МЕТОД ДОВЕДЕННЯ ВЛАСТИВОСТЕЙ ПРОГРАМ
В КОМПОЗИЦІЙНО-НОМІНАТИВНИХ МОВАХ IPCL
Викладено композиційний метод верифікації систем спеціального класу – моделі багатоекземплярного
виконання програм у серверному середовищі з паралелізмом у режимі почергового виконання з пере-
ключенням і взаємодією через спільну пам’ять. У роботі специфіковано задачу, побудовано відповідні
моделі, сформульовано два варіанти часткової коректності програм на введених композиційних мовах
та запропоновано методологію верифікації, що включає метод з лінійною складністю замість
експоненційної.
Формулювання задачі. Модель –
стандартне серверне середовище.
Узагальнення
Щодня ми працюємо з системами, які
використовують взаємодію через спільну
пам’ять (shared memory concurrency, або
паралелізм з почерговим виконанням, на
противагу розподіленим системам з пере-
дачею повідомлень – distributed systems
with message passing) [1, 2]. Це операційні
системи, системи управління базами да-
них, системи з централізованим сховищем
даних, служби операційних систем, сер-
вери в клієнт-серверних середовищах
тощо. Дійсно, маємо широкий клас сере-
довищ та прикладних систем, які викорис-
товують механізм взаємодії через спільну
пам’ять. Зрозуміло, що на таких серверних
платформах побудовано безліч критичних
(мається на увазі – до збоїв у роботі) сис-
тем – банківські, медичні, аерокосмічні
тощо. Отже, актуальним є питання
розробки формального методу для дове-
дення коректності систем, що працюють в
перерахованих середовищах.
Існує ряд підходів до вирішення такої
задачі [1]. Одними з перших спроб дове-
дення коректності паралельних програм є
роботи Ешкрофта [3] та Хоара [4]. Овіцкі
та Грісом в [5] зроблено спробу по-
будувати систему висновків щодо парале-
льних програм шляхом узагальнення ме-
тоду Хоара. Ця спроба набула подальшого
розвитку, зокрема Джонс [6, 7] перетворив
метод у композиційний [8]. Харел і Пнуелі
акцентували увагу на зміщенні акценту від
функціональних систем до реактивних [9],
коли мова йде про паралельне виконання.
Так, Пнуелі розвинув підхід Ешкрофта
введенням темпоральної логіки для су-
джень про паралельні програми [10]. Лем-
порт узагальнив твердження про стани до
акцій (actions) – тверджень про пари
станів, або переходи (transitions) [11]. По-
дальший розвиток цього підходу – мова
Unity [12] Ченді та Місри. Щодо загальної
картини, одні методи (наприклад,
TLA [13, 14]) програють композиційним
методам [15 – 18] за рядом параметрів
(розрив між специфікацією та реальною
програмою, підтримка механізму
абстракції тощо [1]), а інші (метод Овіцкі–
Гріса [5] та його варіанти, що є розвитком
аксіоматичного методу Хоара [19, 4]) є
надто складними для застосування в
реальних системах. Останні також
ускладнюють доведення – збільшують
кількість кроків у випадку “чистого”
методу Овіцкі–Гріса (квадратична
складність) або ускладнюють побудову
проміжних тверджень (в методах типу
rely-guarantee) [1]. Аксіоматичні методи
вважаються взагалі більш складними у
застосуванні на практиці щодо паралель-
них систем. Отже, перевага надається ме-
тодам, що базуються на моделюванні та
використовують принцип інваріанта (не-
змінної або постійної властивості) у своїй
основі.
Проаналізуємо серверну архітектуру,
наприклад, роботу Web-сервера чи SQL-
сервера. Так, на будь-якому сервері, як
правило, запущені служби, що чекають
Теоретичні та методологічні основи програмування
4
вхідних сигналів і реагують на них шляхом
запуску відповідного процесу або вико-
нанням певних дій. Нехай A, B, …, C – від-
повідні реакції на різні види вхідних сиг-
налів (запитів). (Власне, це і є задача сер-
вера – опрацьовувати запити і давати на
них відповіді). Оскільки служби “слуха-
ють” вхідний канал (або вхідні канали) по-
стійно (тобто – чекають вхідних сигналів) і
при надходженні запиту одразу запуска-
ють відповідний процес-обробник, може
виникнути (і реально – часто виникає)
ситуація, коли один і той же процес має
кілька екземплярів (інстанцій – many in-
stances – тобто виявляється запущеним де-
кілька разів An, Bm, … Ck). Причому,
оскільки служби працюють в певному опе-
раційному середовищі сервера, яке в пере-
важній більшості випадків (Windows NT,
Windows 2000, Windows 2003 Server,
FreeBSD, Linux та ін.) підтримує конкуре-
нтний (“витискаючий”) паралелізм – фак-
тично, паралелізм з почерговим виконан-
ням – має місце ситуація An || Bm || … || Ck.
Іншими словами, зазвичай ми запускаємо
послідовні (на противагу паралельним)
програми в багатозадачному серверному
середовищі з паралелізмом з почерговим
виконанням в режимі переривання.
Зауваження щодо позначень:
1) будемо позначати композицію
паралельного виконання в режимі чер-
гування, як засіб побудови програми, f || g,
хоча ця композиція має розумітись як
паралельне виконання в режимі
чергування (interleaving) у формі P ||| Q в
сенсі [4]. Однак обрана нотація ближча до
позначень у KIV [20, 21] – методиці та
однойменному наборі утиліт для дове-
дення властивостей програм, які перева-
жно ґрунтуються на перевірці моделі;
2) P || P || … || P (n раз), тобто пара-
лельне виконання в режимі чергування та
переключення n програм P, будемо позна-
чати Pn.
Процеси A, B, …, C – це програми,
написані в деякій реальній мові програму-
вання. Практика показує, що самі процеси
дуже рідко вимагають паралелізму в рам-
ках них самих (тобто для їх написання і
реалізації), а отже, програми A, B, …, C, як
правило, – послідовні. На користь цього
свідчить наступне. Техніка програмування,
в якій допускається розпаралелювання од-
ного процесу на декілька (під час його ви-
конання), називається багатопотоковістю
(multithreading) [4]. Взагалі, багатопотоко-
вість – складна та схильна до помилок
техніка, яка не рекомендується до
використання, окрім, найменших (най-
простіших) програм [4]. Як підсумок, Тоні
Хоар в своїй праці [4] пише, що паралелізм
може бути дозволений лише на найбільш
зовнішньому (найбільш глобальному,
найвищому) рівні роботи (завдання,
програми), а його використання на нижчих
(вкладених) рівнях слід уникати [4].
До речі, якщо подивитись на сучасну
ситуацію з hardware, а саме з процесорами
(CPU), то на сьогодні нарощування обчис-
лювальної потужності здійснюється шля-
хом нарощування кількості ядер проце-
сору, а не потужності самого ядра (див.
повідомлення відомих виробників – Intel,
AMD). Відомо, що щільність розміщення
елементів на базі (транзисторів, тригерів
на кремнієвому кристалі) вже сягнула тієї
межі, яка освоєна практично на сучасному
рівні розвитку фізики та технології.
Моделлю цієї процесорної взаємодії,
виступає паралелізм зі спільною пам’яттю,
адже всі ядра (як і всі процесори в
мультипроцесорних комплексах) мають
доступ до єдиного спільного пристрою
пам’яті, який вони ділять між собою.
Уточнення задачі. Мова IPCL.
Синтаксис
Розглянемо клас композиційних мов
IPCL (Interleaving Parallel Composition
Languages) з паралелізмом в режимі
чергування [22]. Синтаксис таких мов
задається таким виглядом:
P ::= ex =: | P1;P2 | if b then P1 else P2 |
while b do P | P1 || P2,
де оператор присвоювання є вектор-
ним та атомарним, композиції послідов-
ного виконання, розгалуження та циклу-
вання розуміються стандартним чином
[15–18] (причому в операторах розгалу-
ження та циклування умова обчислюється
атомарно, але виконання може бути пере-
рване після обчислення умови і до вико-
Теоретичні та методологічні основи програмування
5
нання першої дії з відповідного програм-
ного блоку [8]), а паралельна композиція
розуміється як недетерміноване попере-
мінне виконання (interleaving) послідовних
атомарних дій підпроцесів, які є аргумен-
тами композиції (наприклад, в стан-
дартному розумінні [8]). Також будемо
опускати зайві дужки в нотації, зокрема:
P1 || (P2 || (… || Pn)… ) будемо записувати
як P1 || P2 || … || Pn.
В роботі [8] вводиться ще одна
композиція – await b then P end, яка
слугує для синхронізації та взаємного
виключення (якщо умова b істинна, то P
виконується одразу і без переривань, якщо
ні – то P так само виконується, як тільки b
набуде значення істини), але вона відсутня
в IPCL. Це пояснюється тим, що по-перше,
така композиція відсутня в деяких мовах,
які працюють в паралельному середовищі
(наприклад, SQL), по-друге, її можна за
необхідності промоделювати через інші
базові композиції (шляхом введення
додаткових змінних).
Композиційна семантика мов класу
IPCL. Паралелізм в композиційному
програмуванні
Мови класу IPCL ґрунтуються на
композиційно-номінативних системах
< NDS, F, {1, 2}, C, arity >. Тут NDS – сис-
тема іменних або номінативних даних (на-
далі – просто дані), F – набір функцій для
перетворення даних, C – композиції над
функціями з F. F = Oper∪Pred, де
Oper = D × D → D×D, а
Pred = D × D → {True, False}, де перше
входження D в декартів добуток –
“глобальні дані”, а друге – “локальні” для
поточного процесу; функції, що
повертають значення з множини
{True, False} (предикати), не змінюють
поточний стан даних D × D – вони
використовуються як умова в операторах
розгалуження та циклування; D = ND(V,W)
у звичайному сенсі. Композиціями є:
- послідовне виконання, позначається
“;” – аналог звичайної композиції
множення або аплікування, послідовної
функціональної композиції (sequential
functional composition) з абстрактним трак-
туванням “o ” [15];
- розгалуження, позначається “if” –
аналог композиції “◊” [15];
- циклування, позначається “while” –
аналог композиції “∗” [15];
- присвоювання, позначається “:=” –
аналог сукупності (певної комбінації)
композицій іменування та розімену-
вання [15] і деяких обчислень;
- паралельне виконання в режимі
чергування (переривання, interleaving,
shared time), позначається “||”.
Зауважимо, що базовою в IPCL є
композиція послідовного виконання (se-
quential composition [15]) “o ”, яку для
зручності позначаємо “;”, при застосуванні
якої її аргументи вважаються такими, що
беруть на вхід дане і повертають повне
дане (а не лише зміни у ньому). Ця компо-
зиція використовується при абстрактному
трактуванні послідовного виконання. Мо-
жна було використовувати композицію по-
ступового виконання (succession composi-
tion “;” в [15]), яка з’являється при
номінативному трактуванні послідовного
виконання – в цьому випадку аргументи
композиції вказують лише на зміни, що
відбулися у вхідному даному. Але абстра-
ктна більш адекватна подальшого мо-
делювання, відображає по суті пере-
творення стану пам’яті (даних), а не лише
його частини, яке потім необхідно накла-
сти (∇) на поточний стан пам’яті (даних),
щоб отримати цілковиту картину після пе-
ретворення.
Визначимо композиційну семантику
мов IPCL. Семантика трьох перших ком-
позицій є стандартною, семантика компо-
зиції паралельного виконання в режимі
чергування визначається через семантику
її аргументів та синтаксичний контекст1
традиційним чином, враховуючи її алгеб-
раїчні та семантичні властивості. Індек-
сом-параметром функції семантики висту-
пає синтаксичний контекст – фрагмент
програми або сама програма. Отже
семантика “;”:
sem A ; B (d) = d ∇’ sem A (d) ∇’ sem B (d ∇’
sem A (d)),
1 пріоритет композиції || найменший, це треба враховувати при
читанні виразів та розстановці дужок
Теоретичні та методологічні основи програмування
6
де ∇’ – покомпонентне накладання
декартового добутку звичайних іменних
(номінативних) даних:
d1 ∇’ d2 = (Pr1(d1) ∇ Pr1(d2),
Pr2(d1) ∇ Pr2(d2)).
Pri(d) – проекція декартового добутку
d за i-ю компонентою, d1, d2 ∈ D × D,
(така невелика видозміна викликана
тим, що дане розглядається як двокомпо-
нентне – таке, що містить “глобальну” і
“локальну” частини), тут ∇ – звичайна
операція накладання даних (двох іменних
або номінативних множин) згідно з
[15–18],
семантика “:=”:sem x := e (d) = d ∇’ f (d),
де f ∈ Oper – (семантична) функція,
яка відповідає синтаксичному оператору
x := e, причому саме присвоєння (результат
f) дає двокомпонентний результат, адже
обчислюються глобальні та локальні дані,
а накладання відбувається на відповідні
компоненти даного d: глобальні змінні – на
першу компоненту; локальні – на другу; x
та e – вектори імен та значень (виразів)
відповідно,
де A, B, C, P, P’, Q, R ∈ Terms – про-
грами в мові IPCL (терми в алгебрі
IPCLA [22]), b – синтаксичне позначення
відповідної умови предиката pred з Pred,
тобто b (d) = sem b (d) = pred (d), а d ∈ D×D.
В усіх наведених визначеннях, якщо
значення b (d) – невизначене, то і значення
лівої частини відповідної рівності буде та-
кож невизначеним. Так само, якщо в будь-
якому з визначень значення правої частини
рівності не визначено, то і значення лівої
частини – невизначено.
Зауважимо, що семантика задається в
синтактико-семантичному підході, адже
вона визначається не тільки через безпосе-
редні компоненти (складові) конструкції, а
суттєво враховує структуру (тобто їх взає-
мне розташування, особливо щодо компо-
зиції паралелізму), що взагалі кажучи, ха-
рактерно для систем з паралелізмом. Глінн
Вінскел зазначає у своїй роботі [23], що
неможливо змоделювати паралельне вико-
нання програми, обмежившись зв’язками
між конфігураціями команд та заключ-
ними станами – тоді необхідно вико-
семантика “if”:
sem if b then P else Q (d) = sem P (d), якщо b (d) = True,
sem if b then P else Q (d) = sem Q (d), якщо b (d) = False,
семантика “while”:
sem while b do P (d) = sem P ; while b do P (d), якщо b (d) = True,
sem while b do P (d) = d, якщо b (d) = False,
далі – семантика “||”:
|| – асоціативна і комутативна:
sem ( A || B ) || C (d) = sem A || ( B || C ) (d)
sem A || B (d) = sem B || A (d)
на синтаксичному рівні це означає відповідно:
( ( A || B ) || C ) (d) = ( A || ( B || C ) ) (d)
( A || B ) (d) = ( B || A ) (d)
|| відносно “if”:
sem if b then P else Q || R (d) = sem P || R (d), якщо b (d) = True,
sem if b then P else Q || R (d) = sem Q || R (d), якщо b (d) = False,
sem if b then P else Q ; P’ || R (d) = sem P ; P’ || R (d), якщо b (d) = True,
sem if b then P else Q ; P’ || R (d) = sem Q ; P’ || R (d), якщо b (d) = False,
|| відносно “while”:
sem while b do P || R (d) = sem P ; while b do P || R (d), якщо b (d) = True,
sem while b do P || R (d) = sem R (d), якщо b (d) = False,
sem while b do P ; P’ || R (d) = sem P ; while b do P ; P’ || R (d), якщо b (d) = True,
sem while b do P ; P’ || R (d) = sem P’ || R (d), якщо b (d) = False,
|| відносно “;”:
sem ( A ; B ) || P (d) = sem A ; ( B || P ) (d),
sem A || P (d) = sem A ; P (d),
Теоретичні та методологічні основи програмування
7
ристовувати зв’язки між окремими атома-
рними (неподільними) кроками при вико-
нанні і такою дією дозволяти одній ко-
манді впливати на стан іншої команди, з
якою вона виконується в паралель. Взагалі,
семантика систем з паралельним виконан-
ням у режимі чергування, як правило, ви-
значається саме в синтактико-семантичних
традиціях, адже цей підхід є більш приро-
днім для розуміння подібних систем.
Функції з F є атомарними транзакці-
ями, неподільними в сенсі паралелізму, їх
виконання не може бути перервано. Отже,
зокрема умови у відповідних композиціях
теж атомарні.
Конкретна мова класу IPCL утворю-
ється шляхом фіксації F.
Легко показати, що семантика опи-
сана повно – тобто, що вона допускає всі
можливі трактування на моделях. Для
цього достатньо довести, що семантика
спорідненої мови (без оператора await)
з [8] виражається в термінах семантики
IPCL – для доведення необхідно викорис-
тати індукцію за структурою програми. До
речі, в [8] показано, що семантика наведе-
ної мови композиційна, звідси семантика
IPCL теж композиційна (це можна
довести, виразивши семантичну функцію
sem у термінах семантики мови з [8]). Ці
два взаємні вираження семантик
показують, що завдання семантики IPCL
коректні та повні (щодо загальновживаної
семантики аналогічної мови з [8]) –
семантичні та прагматичні.
Уточнення – звуження класу
З усіх можливих програм розглядати-
мемо клас багатоекземплярного виконання
послідовних програм у серверному
середовищі (у режимі почергового
переключення між ними): SeqILProgs =
= { Prog | Prog = An || Bm || … || Ck;
A, B, …, C ∈ SeqTerms; n, m, …, k ∈ Z+ }.
Z+ – додатні цілі числа, SeqTerms – про-
грами в мові IPCL (терми в алгебрі
IPCLA [22]), побудовані за допомогою
композицій {:=, ;, if, while}, без застосу-
вання композиції ||.
Даний клас програм, хоча і є звужен-
ням класу всіх програм (термів) у мові
IPCL (в алгебрі IPCLA), насправді, досить
широкий з практичної точки зору.
Детальне обґрунтування цього факту вище
наведено. До речі, в [5] та [24] роз-
глядається саме таке звуження мови (класу
програм), точніше – навіть звуження цього
звуження, адже там степені мають бути
фіксованими (деталі буде проаналізовано
після викладення методу).
Сформулюємо види властивостей
щодо коректності програмного за без-
печення у мовах IPCL.
Два види властивостей програм
Зафіксуємо задачу. Перевірити
(довести) виконуваність властивості для
програми Prog ∈ SeqILProgs. Розглянемо
два варіанти цієї задачі.
1) (властивість 1 типу), яку треба
довести, записуємо у вигляді
{PreCond} Prog {PostCond}2 з властивості
передумови PreCond після виконання про-
грами Prog випливатиме післяумова
PostCond;
2) (властивість 2 типу), яку треба
довести – інваріантна, тобто вона має
виконуватись протягом всього часу роботи
програми Prog. (Цей тип властивості буде
уточнено далі).
Важливо зазначити, що будь-яку
властивість можна записати у вигляді пре-
диката її істинності. Отже, виконуваність
властивості еквівалентна істинності відпо-
відного їй предиката. Обидва варіанти вла-
стивостей є варіаціями поняття властивості
“безпеки” (safety property). В даній роботі
зупинимось на розгляді лише цих типів
властивостей.
Отже, перший варіант відображає
традиційні погляди (зокрема, Хоара) на
часткову коректність (послідовних !)
програм. Другий варіант “лежить в руслі”
переходу до інваріанту замість перед- та
постумов і відображає погляди Ешкрофта-
Лемпорта на коректність (паралельних !)
програм. (В роботі [1] детально описано
еволюцію поглядів щодо коректності па-
ралельних програм).
Уточнимо ці варіанти. Перший варі-
ант – це узагальнена часткова коректність
програми. Тобто припускаємо, що вхідні
2 в сенсі трійок Тоні Хоара (C.A.R. Hoare), тобто: передумова –
дія – постумова
Теоретичні та методологічні основи програмування
8
дані (точніше – початковий стан програми)
задовольняє деякій умові PreCond, і
необхідно довести, що після виконання
програми буде виконуватись умова
PostCond, тобто вихідні дані (точніше –
заключний стан при виконанні програми)
задовольняють цій умові. Другий варіант –
більш сильна вимога до програми. Дове-
дення такої властивості буде гарантувати,
що деяка умова виконується після вико-
нання кожної дії програми – обчислення
значення базової функції з F та/або пере-
дачі керування на будь-якому кроці згідно
композиційної структури програми – (а,
значить, і після завершення виконання, зо-
крема) за умови, що вона мала місце на
початку її роботи.
Методика розв’язання задачі (доведення
властивостей)
Ураховуючи комутативність та асоці-
ативність композиції ||, а також її семан-
тику відносно інших композицій, процес
обчислень програми P ∈ SeqILProgs можна
уявити як послідовне виконання, причому
на кожному кроці виконується одна чер-
гова команда однієї з підпрограм, причому
підпрограма обирається випадково з тих,
які ще недовиконані. Можна також пред-
ставити процес обчислень з синтаксичної
точки зору як переписування терму про-
грами з метою усунення композиції || з її
нотації. Оскільки процедура перепису-
вання (перетворення) терму, враховуючи
вищенаведену семантику композиції ||, є
недетермінованою, на кожному кроці ро-
биться вибір правила переписування як
однієї з альтернатив. У цьому випадку мо-
жна говорити, що цим самим обирається
один з можливих шляхів виконання про-
грами P. Саме виконання елементарних
(атомарних) дій – функції з F – це, власне,
перетворення даних. Кожна підпрограма
може взаємодіяти зі спільними глобаль-
ними та своїми локальними даними.
Побудова моделі. Транзиційна система
Побудуємо модель виконання дові-
льної програми P ∈ SeqILProgs у відповід-
ності з вищенаведеними міркуваннями та
згідно семантики мов IPCL.
Отже, розглянемо програму
P = An || Bm || … || Ck ∈ SeqILProgs. Нехай
numprocs=n+m+…+k. Зробимо помітки для
кожного входження функцій з F в терми
програм A, B, …, C. Також для кожної про-
грами A, B, …, C введемо помітку завер-
шення роботи програми – помітку, що зна-
ходиться після тексту програми, не помі-
чає жодну функцію із програми, але фіксує
стан одразу після завершення виконання
програми – аналог E з [8]. Маємо для кож-
ної програми A, B, …, C множину поміток
Amarks, Bmarks, …, Cmarks відповідно. Зрозу-
міло, що глобальне сховище (простір спі-
льних змінних) має чітко відрізнятися та
прозоро відокремлюватися від локального
сховища (простору локальних змінних) [4].
Тоді S ∈ Amarks
n×Bmarks
m×…×Cmarks
k×D×
×Dnumprocs будемо називати станом
системи, що виконує програму P, або
станом програми P (або просто станом,
якщо з контексту зрозуміло, про який стан
іде мова), де перше входження D в
декартів добуток – “глобальні дані”, а
друге – “локальні” для всіх окремих
послідовних підпрограм (An, Bm, …, Ck) з P,
записані в тій же послідовності, що і самі
підпрограми в термі програми P. Перша
частина декартового добутку (до даних) –
це позиції виконання кожної підпрограми
з P (мітки функцій, які будуть обчислені –
або дій, які будуть виконані –
відповідними підпрограмами, коли дійде
черга до їх виконання – тобто відбудеться
“переключення на них”, на найближчому
кроці). Весь наведений декартів добуток
будемо називати множиною станів і по-
значати States. Отже, стан S∈States
містить в собі інформацію як про стан да-
них (глобальних і локальних), так і про
стан керування, тому цей сукупний стан
ще іноді називають конфігурацією.
Будемо виділяти множину початко-
вих станів StartStates ⊆ States. Зокрема, в
усіх елементів цієї множини перші
(numprocs) компоненти декартового добу-
тку, які відображають мітки, (всі окрім да-
Теоретичні та методологічні основи програмування
9
них) мають значення початкових (перших,
які зустрічаються в записі терму) міток
відповідних процесів. Можна також виді-
лити множину заключних станів, в один з
яких програма P потрапляє після завер-
шення виконання – StopStates ⊆ States. Для
всіх елементів s цієї множини характерно,
що ті ж самі перші (numprocs) їх компоне-
нти будуть мати значення заключних
(останніх в записі терму) міток відповід-
них процесів, а також їх досяжність.
Останнє означає, що для кожного стану
s∈StopStates існує набір станів s1, s2, …,
…, sl∈States такий, що
s1∈StartStates & sl=s & (∀i∈{1, 2, …,
…, l – 1} • (si, si+1)∈Step),
де Step – функція кроку виконання
програми P (про функцію Step, про
розстановку міток див. далі).
Кількість підпрограм програми P, що
знаходяться на деякій позиції mark в стані
S будемо позначати PS[mark]. Такі величини,
що є цілими невід’ємними числами – ко-
рисні для формулювання перед- та по-
стумов, а також інваріантів, при доведенні
властивостей. Наприклад, для довільної
програми A ∈ SeqTerms і стану S ∈ States
завжди виконується nA
marksAmark
markS
n =∑
∈
][ .
З цього зауваження зрозуміло, що ми
дозволяємо явно використовувати стан
керування в формулюванні предикатів
PreCond, PostCond та Inv.
Функцію Step: States → States будемо
називати функцією кроку виконання
програми P, якщо вона визначає всі мож-
ливі перетворення станів, тобто переходи
від одного до іншого стану – за один крок
під час виконання програми P і тільки їх.
Тобто, якщо поточний стан програми P є S,
то за один крок виконання програми P
потрапляємо в стан S’ ∈ Step(S). Під кро-
ком виконання програми P (в певний мо-
мент) розуміємо обчислення однієї з функ-
цій із F, які доступні до обчислення згідно
композиційної семантики програми (в цей
момент).
З виконанням кожного кроку про-
грами P, тобто обчисленням деякої функ-
ції, окрім можливої зміни даних, пов’язана
зміна значення однієї з перших компонент
стану – а саме компоненти, що вказувала
на мітку обчисленої функції. Її значення
стає рівним мітці, куди програма потрап-
ляє після обчислення функції з поточного
кроку. Значення нової мітки визначається
за семантикою композиційного контексту
даної функції.
Функція Step, очевидно, багатозначна
(недетермінована) часткова функція. (З
точки зору теорії множин її скоріше слід
було б назвати відношенням, тобто
Step ⊆ States×States.)
Так, маємо справу з транзиційною
системою (State Transition System), що
складається з множини всіх станів States та
функції переходів Step. Точніше –
ініціалізована нескінченна (за кількістю
станів) нерозмічена транзиційна система,
initialized infinite unlabelled transition
system, в сенсі, наприклад, ASM [25].
Також додатково ми виділяємо множину
початкових станів StartStates та множину
заключних станів StopStates, які є підмно-
жинами States. Зрозуміло, що для кожної
програми з SeqILProgs можна побудувати
відповідну транзиційну систему. Отже, бу-
демо розглядати такі транзиційні системи
в якості моделей програм.
Тепер, визначивши модель про-
грами – як транзиційну систему – та пове-
ртаючись до визначення PreCond, Post-
Cond та Inv, слід уточнити, що ці умови є
предикатами над станом, тобто
PreCond, PostCond, Inv : States → Boo
l, де Bool = {True, False}.
Розстановка міток та визначення
функції Step
Наведемо рекурсивний (за структу-
рою терму коректно побудованої про-
грами) алгоритм визначення функції зміни
(точніше – розстановки) міток і одночас-
ного визначення функції Step.
Теоретичні та методологічні основи програмування
10
де f – семантика відповідної операції
x := e.
Кожній функції, поміченій міткою
(присвоювання або умова), відповідає її
семантика з множини F згідно з вище-
визначеною функцією семантики sem.
Основний виклик функції розста-
вити_мітки() треба виконати для кожного з
варіантів підпроцесів P, тобто для
A, B, …, C (по одному екземпляру для ко-
жного варіанта підпроцесів) у нашому по-
передньому визначенні – даючи кожного
разу вхідними параметрами різні (всі по-
парно відмінні) початкові й кінцеві мітки,
а термом – відповідний терм A, B, …, C.
Тут функції створити_пере-
хід_з_умовою (мітка1, умова, мітка2) та
створити_перехід_з_перетворенням
(мітка1, функція, мітка2) означають
уточнення функції Step (поповнення
декартового добутку Step парами (State,
State’)), а саме – розглянемо, наприклад
обробку терму A.
Так, створити_перехід_з_умовою (мі-
тка1, умова, мітка2) додасть до Step
наступну множину пар:
{ (S1, S2) | S1=(a1, a2, …, an, b, …, c, d,
d1, …, dnumprocs) & S2=(a1’, a2’, …, an’, b, …,
c, d, d1, …, dnumprocs) & ∀i∈Nn • ( ai∈Amarks &
ai’∈Amarks ) & b∈Bmarks
m & … & c∈Cmarks
k &
d∈D & ∀i∈Nnumprocs • di∈D & ∃i∈Nn •
∀j∈Nn \ {i} • ( ai=мітка1 & ai’=мітка2 &
aj’=aj ) & умова(S1) },
де Nn={1, 2, …, n}, а ство-
рити_перехід_з_перетворенням(мітка1,
функція, мітка2) –
функція Розставити_мітки ( початкова_мітка, кінцева_мітка, терм )
{
якщо ( терм = терм1 ; терм2 )
то
{
створити нова_мітка;
розставити_мітки ( початкова_мітка, нова_мітка, терм1 );
розставити_мітки ( нова_мітка, кінцева_мітка, терм2 )
}
інакше
якщо ( терм = if ( терм1 ) then терм2 else терм3) )
то
{
створити нова_мітка1, нова_мітка2;
створити_перехід_з_умовою ( початкова_мітка, терм1(d)=True, нова_мітка1 );
розставити_мітки ( нова_мітка1, кінцева_мітка, терм2 );
створити_перехід_з_умовою ( початкова_мітка, терм1(d)=False, нова_мітка2 );
розставити_мітки ( нова_мітка2, кінцева_мітка, терм3 )
}
інакше
якщо ( терм = while ( терм1 ) do терм2 )
то
{
створити нова_мітка;
створити_перехід_з_умовою ( початкова_мітка, терм1(d)=True, нова_мітка );
створити_перехід_з_умовою ( початкова_мітка, терм1(d)=False, кінцева_мітка );
розставити_мітки ( нова_мітка, початкова_мітка, терм2 )
}
інакше
якщо ( терм = x := e )
то
створити_перехід_з_перетворенням( початкова_мітка, f, кінцева_мітка )
}
Теоретичні та методологічні основи програмування
11
{ (S1, S2) | S1=(a1, a2, …, an, b, …, c, d,
d1, …, dnumprocs) & S2=(a1’, a2’, …, an’, b, …,
c, d’, d1’, …, dn’, dn+1, …, dnumprocs) & ∀i∈Nn
• ( ai∈Amarks & ai’∈Amarks ) & b∈Bmarks
m & …
& c∈Cmarks
k & d∈D & d’∈D & ∀i∈Nnumprocs •
di∈D & ∀i∈Nn • di’∈D & ∃i∈Nn • ∀j∈Nn \
{i} • ( ai=мітка1 & ai’=мітка2 & aj’=aj &
dj’=dj & (d’, di’)=функція(d, di) ) }.
Аналогічно легко можна виписати ці
дві функції, що довизначають Step, для ін-
ших підпроцесів P : B, …, C. Очевидно, що
для різних підпроцесів вони будуть зміню-
вати деяку частину декартового добутку
стану (а саме – не більше трьох компо-
нент), залишаючи інші незмінними. Так
можна промоделювати виконання всієї
програми P як почергове виконання деякої
з поточних операцій (обчислення значень
функцій), зокрема, перевірку умови і
перехід у відповідності з результатом до
блоку “then” або до блоку “else” і
відповідну зміну стану3.
Спрощена модель (відсутність
локальних даних)
Слід зауважити, що у випадку відсу-
тності локальних даних у програм A, B, …,
C (підпрограм P), доцільно розглядати по-
няття спрощеного стану [26] – агрегова-
ного стану такого вигляду: NPmq×D, де
Pmq = ||Amarks||+||Bmarks||+…+||Cmarks||.
4 Перші
||Amarks|| компонент такого стану містять
кількість програм, що перебувають у
відповідних мітках програми A в цьому
стані, причому сума цих компонент в кож-
ному стані для програми P дорівнює n –
кількості інстанцій (екземплярів) про-
грами A в P – в термінах програми P. На-
ступні ||Bmarks|| компонент – містять кіль-
кість програм, що перебувають у відповід-
них мітках програми B у цьому стані, при-
чому сума цих компонент у кожному стані
для програми P дорівнює m (кількості ін-
станцій програми B в P) у термінах про-
3 Запропонований апарат моделювання, зокрема, дозволяє
виразити “миттєвий” if – якщо вважати, що на одному кроці
обчислень відбувається обрахунок значення умови композиції if
та одразу передача управління відповідному блоку (“then” або
“else”) і виконання першого оператора цього блоку, як,
наприклад, відбувається в KIV Tools [175,176] – тобто, по суті, є
більш потужним, ніж запропонована семантика IPCL. Також цей
апарат дозволяє промоделювати оператор await в явному
вигляді (без проміжного моделювання в мові IPCL).
4 ||A||=card(A) – потужність множини A
грами P і т.д. Остання компонента D міс-
тить глобальні спільні дані для всіх під-
програм P.
Спрощений стан оперує з кількос-
тями програм, що знаходяться на кожній
мітці виконання замість ідентифікації по-
зиції (мітки) кожної інстанції кожної
окремої підпрограми (A, B, …, C). Наспра-
вді, підпрограми є нерозрізнюваними з то-
чністю до поточної мітки виконання, якщо
вони не змінюють (фактично, не мають)
локальних даних, а лише оперують зі спі-
льними глобальними даними.
Отримати спрощений стан за станом
можна наступним чином. Оскільки мно-
жини Amarks, Bmarks, …, Cmarks – скінченні, то
нехай Amarks={A1, …, Aa}, …, Cmarks=
= {C1, …, Cc}. Pri(S) – i-а компонента
кортежу S. Візьмемо деякий стан S. Тоді
відповідний йому спрощений стан SS має
вигляд (a1, …, aa, …, c1, …, cc, d), де
aj=||{ i | Pri(S)=Aj , i∈NPmq }||= ][ jASP , ∀j∈Na,
…, cj=||{ i | Pri(S)=Cj , i∈NPmq }||= ][ jCSP ,
∀j∈Nc, d=Prnumprocs+1(S).
Відповідним чином вводяться мно-
жина спрощених станів SStates, спрощені
початкові стани SStartStates (всі вони ма-
ють структуру (n, 0, …, 0, …, k, 0, …, 0,
d)), спрощені заключні стани SStopStates
(їх структура – (0, …, 0, n, …, 0, …, 0, k, d))
та функція кроку виконання програми P
над спрощеними станами – SStep: SStates→
→ SStates. Ця функція зменшує на
одиницю значення деякої компоненти
вектора SStates (наприклад, першу) і
водночас збільшує значення деякої іншої
(наприклад, другої), тобто відбувається
передача керування від однієї мітки (в да-
ному випадку – A1) до іншої мітки (в да-
ному випадку – A2) для однієї з програм (в
даному випадку – A), а також змінює зна-
чення останньої компоненти (глобальних
даних), якщо чергова функція належить
підкласу Oper класу F. Всі ці об’єкти легко
отримати шляхом переведення станів у
спрощені стани або безпосередньо.
Зокрема, створити_перехід_з_умо-
вою(мітка1, умова, мітка2) додасть до
SStep наступну множину пар:
{ (SS1, SS2) | SS1=(a1, a2, …, aa, …, c1,
…, cc, d) & SS2=(a1’, a2’, …, aa’, …, c1, …,
Теоретичні та методологічні основи програмування
12
cc, d) & ∀i∈Na • ( ai∈N & ai’∈N ) & … &
∀i∈Nc • ci∈N & d∈D & ∃i∈Na • ∃j∈Na •
∀k∈Na \ {i, j} • ( Ai=мітка1 & Aj=мітка2 &
ai>0 & ai–1=ai’ & aj+1=aj’ & ak=ak’ ) &
умова(SS1) },
де Nn={1, 2, …, n}, а ство-
рити_перехід_з_перетворенням(мітка1,
функція, мітка2) –
{ (SS1, SS2) | SS1=(a1, a2, …, aa, …, c1,
…, cc, d) & SS2=(a1’, a2’, …, aa’, …, c1, …,
cc, d’) & ∀i∈Na • ( ai∈N & ai’∈N ) & … &
∀i∈Nc • ci∈N & d∈D & d’∈D & ∃i∈Na •
∃j∈Na • ∀k∈Na \ {i, j} • ( Ai=мітка1 &
Aj=мітка2 & ai>0 & ai–1=ai’ & aj+1=aj’ &
ak=ak’ ) & (d’, [])=функція(d, []) },
де [] – порожнє іменне дане.
Також аналогічно до описаної далі
техніки доводяться властивості двох типів,
які досліджуються [26]. Будемо розглядати
спрощені стани, де це доцільно [26].
Метод доведення властивостей
Отже, нехай нам потрібно довести
властивість 1 типу з передумовою-преди-
катом PreCond та постумовою-предикатом
PostCond, або властивість 2 типу з інваріа-
нтом-предикатом Inv, щодо деякої про-
грами P. Всі три предикати є предикатами
від аргументу-стану (або спрощеного
стану).
Покажемо спочатку, що ці два типи
властивостей рівнопотужні в тому сенсі,
що коли виконується умова 1 типу для де-
яких PreCond та PostCond, то завжди мо-
жна підібрати такий Inv (що залежатиме
від PreCond та PostCond), для якого буде
виконуватись умова 2 типу. Будемо вико-
ристовувати поняття рефлексивно-транзи-
тивного замикання відношення Step (або
SStep) і позначати його Step* (або SStep*).
Якщо відношення Step моделює виконання
одного кроку програми P, то Step* моде-
лює виконання довільної кількості кроків
програми P (зокрема, і виконання всієї
програми). Введемо предикат InvCond
(предикат вищого порядку – над іншими
предикатами-аргументами), який нам зна-
добиться далі:
InvCond(Inv, PreCond, PostCond) = ∀S
∈StartStates • ( PreCond(S) → Inv(S) ) &
∀S∈StopStates • ( Inv(S) → PostCond(S) ) &
∀(S, S’)∈Step • ( Inv(S) → Inv(S’) ).
Цей предикат істинний, якщо на всіх
початкових станах S∈StartStates з
PreCond(S) логічно випливає Inv(S), на всіх
заключних станах S∈StopStates з Inv(S) ло-
гічно випливає PostCond(S) та для кожної
пари станів (S, S’)∈Step (кроку програми)
маємо Inv(S) → Inv(S’) (збереження істин-
ності інваріанта).
Нагадаємо, що програма P при моде-
люванні перетворюється в транзиційну си-
стему, яка складається з множини станів
States, функції переходу Step, початкових
станів StartStates та кінцевих станів
StopStates, тобто програма однозначно ви-
значає всі перелічені компоненти моде-
люючої транзиційної системи.
Рівнопотужність двох типів
властивостей
Твердження. Властивість 1 типу ви-
конується для деяких PreCond(S),
PostCond(S) та програми P тоді і тільки
тоді, коли виконується властивість 2 типу
для цієї програми P і деякого інваріанта
Inv(S).
Сформулюємо це твердження ін-
шими словами.
Теорема 1. Нехай програма P (функ-
ція переходу Step*) переводить початковий
стан S (S∈StartStates) в кінцевий стан S’
(S’∈StopStates). Тоді для будь-якої пари
таких станів S та S’ з PreCond(S) випливає
PostCond(S’) тоді і тільки тоді, коли існує
інваріант Inv(s) (s∈States), такий, що є логі-
чним наслідком PreCond(s) для кожного
початкового стану ( ∀s∈StartStates •
• ( PreCond(s) → Inv(s) ) ), з нього випли-
ває PostCond(s) в кожному заключному
стані ( ∀s∈StopStates • ( Inv(s) →
→ PostCond(s) ) ) і він зберігає істинність
для кожного переходу з Step (∀(s, s’)∈
∈Step • ( Inv(s) → Inv(s’) ) ).
Формально це твердження можна за-
писати таким виглядом:
∀Step, States, StartStates, StopStates •
∀PreCond • ∀PostCond • (∀S∈StartStates •
Теоретичні та методологічні основи програмування
13
∀S’∈StopStates • ( PreCond(S) & (S, S’)∈
∈ Step* → PostCond(S’) ) ⇔ ∃Inv •
• InvCond(Inv, PreCond, PostCond) ),
де всі позначення (Step, States,
StartStates, StopStates, PreCond, PostCond,
Inv) використовуються та розуміються у
вищевведеному смислі.
Доведення наведено в [1].
Тепер повернемось до методики до-
ведення властивостей.
Формулювання методу. Роль інваріанта
Схема доведення властивостей така:
1) за програмою у мові IPCL (згі-
дно наведеного алгоритму) будуємо функ-
цію Step та розставляємо мітки;
2) фіксуємо множини початкових
та кінцевих станів (згідно наведених ви-
значень) – StartStates та StopStates;
3) формулюємо перед- та посту-
мови та знаходимо за ними відповідний
інваріант, або ж одразу формулюємо влас-
тивість типу інваріанта;
4) маючи Inv(S), S∈States, робимо
доведення-перевірку за наступними пра-
вилами.
Щоб довести властивість 2 типу, не-
обхідно показати, що кожне перетворення,
допустиме згідно функції Step в деякий по-
точний момент (“просування” виконання
програми шляхом обчислення однієї чер-
гової функції), зберігає істинність інваріа-
нта Inv(S). Тобто необхідно довести
наступне:
∀S∈States • ∀S’∈States ( (Inv(S) & (S,
S’)∈Step) → Inv(S’) ).
Тоді, якщо ∀S∈StartStates • Inv(S),
що також слід перевірити, то за індукцією
Inv(S) має місце для всіх станів S, які є
досяжними для програми P (згідно функції
Step), зокрема, і ∀S∈StopStates • Inv(S).
Властивість 2 типу, так, буде доведено.
Для доведення властивості 1 типу
слід, згідно зі сформульованим і до-
веденим твердженням, знайти інваріант
(предикат) Inv(S), такий, що задовольняє
умові InvCond(Inv, PreCond, PostCond) для
заданих PreCond та PostCond. Фактично,
якщо такий інваріант буде знайдено, то
доведення можна вважати завершеним.
Так само ми доведемо істинність преди-
ката-інваріанта на кожному кроці вико-
нання програми, якщо до цього кроку мо-
жна дійти, стартувавши виконання з де-
якого початкового стану, для якого вико-
нувалась умова PreCond(S), а оскільки з
істинності Inv(S) випливає істинність
PostCond(S) на заключних станах
(∀S∈StopStates • ( Inv(S) → PostCond(S) )),
то доведемо те, що було необхідно
(властивість 1 типу).
Висновки щодо методу. Порівняння з
іншими методами. Постаналіз
З усіх кроків креативним є лише тре-
тій, тобто знаходження (або формулю-
вання) відповідного інваріанта. Один з
можливих інваріантів сформульований при
доведенні твердження в явному ви-
гляді [1], але він надто складний для прак-
тичних доведень і має лише теоретичний
зміст, адже він є, фактично, функціоналом
вищого порядку. На практиці необхідно
знаходити інваріант, який якомога точніше
відображав би поведінку програми (для
цього розроблений ряд підходів, зокрема,
С.Л. Кривим [27] та ін., але в загальному
випадку проблема залишається частково
розв’язною). Інші кроки методу є
механічними, тому можуть бути автома-
тизовані.
Зауважимо, що доведення за наведе-
ним методом можна проводити для
зазначеного вигляду (класу) програм
(P ∈ SeqILProgs), де кількості паралельно
виконуваних (під)програм є довільними
натуральними (з 0) числами, фіксованими
є тільки їх типи (A, B, …, C), причому
складність таких доведень буде лінійною
(за кількістю кроків) щодо кількості
операторів у (під)програмах (див. при-
клади, додаток Б), на відміну від багатьох
інших методів. У такому випадку отрима-
ємо свого роду символічні доведення над
загальною формою програми, тобто реа-
льно викладений метод може оперувати
“узагальненим виглядом програми”. Він не
може бути зведений до простої перевірки
моделей (model checking), адже по-перше,
всі стани не можна перелічити, бо не є фі-
ксованою кількість (ступінь) кожної з па-
ралельних підпрограм. По-друге, в кож-
ному конкретному випадку, при великих
Теоретичні та методологічні основи програмування
14
кількостях паралельних підпрограм, кіль-
кість станів буде також значною. Даний
метод не є варіантом символьної перевірки
моделей (symbolic model checking), який не
використовує ні евристики, ні інші
покращення, викладені в літературі. Також
зрозуміло, що запропонований метод не є
варіантом доведення теорем (theorem
proving) в чистому вигляді, але останні є
високоінтерактивними (мають високій
ступінь взаємодії з людиною, тобто люд-
ського втручання [28]), адже в даному
методі необхідно лише один раз спочатку
сформулювати інваріант – решта (інші
кроки методу), як вже зазначалось, може
бути виконано автоматично. До того ж,
доведення теорем посилається на логіку і є
математичним підходом, водночас як да-
ний метод спирається на текст програми,
семантику та моделюючу транзиційну сис-
тему, є змішаним підходом. Щодо порів-
няння з методами перевірки моделей, то
запропонований метод позбавлений “про-
блеми вибуху” кількості станів (але за-
лежність складності доведення є лінійною
за відношенням до кількості операторів у
нотації програми).
В запропонованому методі сконцент-
ровано ряд ідей. Як і в більшості методів,
що базуються на станах, вводиться поняття
стану та використовується операційна се-
мантика для моделювання поведінки про-
грами. Поняття стану тут інкорпорує в
себе як стан пам’яті, так і стан керуючого
пристрою (стан керування – позиції в
контрольних точках програми). Моделю-
вання програми здійснюється, як і в мето-
диці ASM (Abstract State Machines) [25, 29]
Гуревича, за допомогою деякої абстрактної
машини над цими станами (машина – “пе-
ретворювач станів”), фактично – транзи-
ційної системи, аналог яких – дискретні
перетворювачі, можна знайти у роботах
Глушкова. Поняття інваріанта, яке бере
корені в роботах Флойда [30], Хоара [31], а
згодом і Ешкрофта [3], для паралельних
програм, та широко використовується в
TLA (Лемпорт, нагадаємо, наголошує на
виключній важливості інваріанта для до-
ведень та суджень над паралельними про-
грамами), відіграє в методі одну з ключо-
вих ролей. Також метод бере базові ідеї
щодо коректності програми, сформульо-
вані Хоаром у вигляді перед- та постумов.
Доведення в методі виходить в загальному
випадку схожим на доведення в методі
TLA, хоча базується на простішій та ближ-
чій до тексту програми моделі. В методі не
передбачено введення додаткових допомі-
жних змінних (наприклад, в методах
Овіцкі-Гріса), отже, він позбавлений
недоліків, згадуваних у [32, 33] (як
мінімум, складнощів з розумінням ролі та
смислового навантаження таких змінних, а
також з їх придумуванням), зате можна
використовувати явно стан керування
програми. Це дозволяє зв’язувати
передумову та післяумову (взагалі, стани
та судження про них) в єдиний інваріант
для доведення явно, а не за допомогою
“незрозумілих змінних” [33].
Разом з тим запропонований метод
має відмінності від усіх перелічених. По-
перше, він базується на композиційній се-
мантиці, тобто базові функції мають бути
задані в термінах композиційно-номінати-
вної семантики, сама семантика мов IPCL є
композиційною отже, метод має компо-
зиційно-номінативну природу. По-друге,
метод має конкретні відмінності від інших.
А саме, на відміну від TLA, метод суттєво
прив’язаний до тексту програми на мові
IPCL, яка схожа на звичайні мови імпера-
тивного програмування (на яких, власне, і
пишеться переважна більшість реального
програмного забезпечення). Переваги та-
кого підходу обговорювались вище. Метод
пропонує іншу, аніж в ASM, модель вико-
нання, більш схожу на операційну семан-
тику звичайних мов програмування (нага-
даємо, в ASM моделлю є нескінченний
цикл з паралельно виконуваних умовних
операторів). Те ж саме зауваження відно-
ситься і до мови Unity Ченді та Місри [12].
Мова, яка розглядається в роботі Ешкро-
фта, містить конструкцію fork, яка має
іншу семантику, ніж композиція паралель-
ного виконання в режимі чергування, вве-
дена тут. Щодо робіт Хоара, то в них роз-
глядаються лише паралельні середовища з
обміном повідомленнями (розподілені сис-
теми), розвиваються відповідні моделі та
методи. Відмінність від методу Овіцкі-
Гріса (та його композиційного або rely-
Теоретичні та методологічні основи програмування
15
guarantee [6, 7] розширення Джонсом чи
assumption-commitment [12] розширення
Ченді та Місри) полягає в моделі, яка
базується на аксіоматичній семантиці та її
розширенні, водночас коли даний метод є
ближчим до операційної семантики та мо-
делювання (належить до методів, що ба-
зуються на станах). Зрештою, клас
програм, розглядається в рамках
наведеного методу, в явному вигляді не
розглядається в жодному іншому підході, а
в деяких (напевно, в більшості) взагалі не
матиме адекватного представлення.
Висновки
Отже, запропонований метод це
методологія доведення (критичних)
властивостей програм в композиційних
мовах IPCL [22]. Він дійсно нова комбіна-
ція відомих технік та методик щодо до-
ведення коректності програмного забезпе-
чення (особливо, паралельних систем, сер-
верного програмного забезпечення для
клієнт-серверних середовищ), побудова-
ний на фундаменті композиційно-номіна-
тивних методів для спеціального, але до-
сить широкого класу програм. Відмінності
методу від інших підходів детально
проаналізовано вище. Сформульований
метод має на меті побудувати “місток” між
реальними програмами, написаними на
звичайних імперативних мовах програму-
вання, та математичними об’єктами (твер-
дження, формули, властивості, доведення
тощо). Відсутність якого можемо бачити в
більшості відомих методів, які стартують
одразу від математичних формул та систем
(алгебр, транзиційних систем тощо).
Закладена в основу методу модель
дозволяє оперувати програмами, запуще-
ними в паралель довільну кількість разів
(багато одночасно виконуваних екземпля-
рів у режимі паралельного почергового ви-
конання). Явно така модель не використо-
вується в жодному з відомих підходів, всі
підходи вимагають точної кількості про-
грам та операторів, заданої наперед, осо-
бливо це стосується методів перевірки мо-
делей (model checking). Метод базується на
композиційно-номінативних системах, що
дозволяє вільно обирати найбільш підхо-
дящий рівень для моделювання тієї чи ін-
шої задачі та доведення критичних власти-
востей систем. Метод допускає автомати-
зацію більшості етапів доведення власти-
востей. Запропонований метод верифікації
має лінійну складність доведення щодо
кількості операторів програми замість екс-
поненційної, як в більшості методів пере-
вірки моделей, тобто він позбавлений
“проблеми вибуху” кількості станів.
Викладений метод апробовано на
реальних системах. Один з таких при-
кладів – доведення критичних властивос-
тей системи виплати міжнародних грошо-
вих переказів Vigo Remittance Corp., реалі-
зованої для ВАТ “Державний ощадний
банк України”.
1. Панченко Т.В. Композиційні методи специ-
фікації та верифікації програмних систем.
– Автореф. дис. канд. фіз.-мат. наук. – К.,
2006. – 17 с.
2. Wikipedia, Internet-енциклопедія
(www.wikipedia.org)
3. Ashcroft E.A. Proving assertions about paral-
lel programs // J. of Computer and System
Sciences. – 1975. – N 10. – P. 110–135.
4. Hoare C.A.R. Communicating Sequential
Processes. – Prentice Hall International,
1985. – 238 p.
5. Owicki S. and Gries D. An Axiomatic Proof
Technique for Parallel Programs // Acta In-
formatica. – 1976. – Vol. 6, N 4. –
P. 319–340.
6. Jones C.B. Development Methods for Com-
puter Programs Including a Notion of Inter-
ference: DPhil. Thesis. – Oxford University
Computing Laboratory, 1981. – 315 p.
7. Jones C.B. Specification and Design of
(Parallel) Programs // Information Processing
Letters: IFIP Information Processing'83 (In
IFIP 9th World Congress). – 1983. –
P. 321–331.
8. Xu Q., de Roever W.-P., He J. The Rely-Guar-
antee Method for Verifying Shared Variable
Concurrent Programs // Formal Aspects of
Computing. – 1997. – Vol. 9, N 2. –
P. 149–174.
9. Harel D., Pnueli A. On the development of
reactive systems // Apt K.R. (ed.) Logics and
models of concurrent systems, NATO ASI
Series. – Springer-Verlag, 1985. – Vol. F13. –
P. 477–498.
10. Pnueli A. The temporal logic of programs //
Proc. 18th Annual Symposium on the Foun-
dations of Computer Science (Providence). –
Теоретичні та методологічні основи програмування
16
New York: IEEE Computer Society Press,
1977. – P. 46–57.
11. Lamport L. Verification and Specification of
Concurrent Programs // deBakker J., deRo-
ever W., Rozenberg G. (eds.) A Decade of
Concurrency. – Berlin: Springer-Verlag,
1993. – Vol. 803. – P. 347–374.
12. Chandy K.M., Misra J. Parallel Program De-
sign: A Foundation. – Reading, MA: Addison-
Wesley Publishing Company, 1988. – 493 p.
13. Lamport L. The temporal logic of actions //
ACM Transactions on Programming
Languages and Systems. – 1994. – Vol. 16,
N 3. – P. 872 – 923.
14. Manna Z., Pnueli A. The Temporal Logic of
Reactive and Concurrent Systems, Specifica-
tion. – Berlin: Springer-Verlag, 1992. – 427 p.
15. Nikitchenko N. A Composition Nominative
Approach to Program Semantics. – Technical
Report IT-TR: 1998-020. – Technical
University of Denmark. – 1998. – 103 p.
16. Редько В.Н. Композиции программ и ком-
позиционное программирование // Про-
граммирование. – 1978. – № 5. – С. 3–24.
17. Редько В.Н. Основания композиционного
программирования // Программирование. –
1979. – № 3. – С. 3–13.
18. Басараб И.А., Никитченко Н.С., Редько
В.Н. Композиционные базы данных. –
Киев: Либідь, 1992. – 191 с.
19. Hoare C.A.R. An Axiomatic Basis for Com-
puter Programming // Communications of the
ACM. – 1969. – Vol. 12, N 10. – P. 576–583.
20. Heisel M., Reif W., Stephan W. Implementing
Verification Strategies in the KIV-System //
Lusk E., Overbeek R. (eds.) Proc. 9th
International Conference on Automated
Deduction // Lecture Notes in Computer
Science. – Berlin: Springer-Verlag, 1988. –
Vol. 310 – P. 216–231.
21. Reif W. The KIV-approach to Software
Verification // Broy M., Jähnichen S. (eds.)
KORSO: Methods, Languages, and Tools for
the Construction of Correct Software. Final
Report // Lecture Notes in Computer Science.
–Berlin: Springer-Verlag, 1995. – Vol. 1009.
– P. 339–368.
22. Панченко Т.В. Методологія доведення
властивостей програм в композиційних
мовах IPCL // Тези доп. Міжнар. конф.
“Теоретичні та прикладні аспекти
побудови програмних систем”
(TAAPSD’2004). – К.; 2004. – С. 62–67.
23. Winskel G. The Formal Semantics of Pro-
gramming Languages: An Introduction. –
London: MIT Press Foundations of
Computing Series, 1993. – 361 p.
24. Takaoka T. A systematic approach to parallel
program verification // Proc. Computing:
Australasian Theory Symposium (CATS 96).
– Melbourne (Australia), 1996. – P. 48–56.
25. Reisig W. The Expressive Power of Abstract-
State Machines // Computing and Informatics.
– 2003. – Vol. 22, N 3/4. – P. 209–219.
26. Панченко Т.В. Модель спрощеного стану
для методу доведення властивостей в мо-
вах IPCL та її застосування і переваги //
Тези міжнар. наук. конф. TAAPSD`2007,
Berdyansk, 4-9 September. – 2007. –
Р. 319–322.
27. Кривий С.Л., Матвєєва Л.Е. Формальні ме-
тоди аналізу властивостей систем // Кибе-
рнетика и системный анализ. – 2003. – № 2.
– С. 15–36.
28. Edmund M. Clarke, Jeannette M. Wing et al.
Formal methods: state of the art and future di-
rections // ACM Computing Surveys. – 1996.
– Vol. 28, N 4. – P. 626–643.
29. Gurevich Y. Sequential Abstract-State Ma-
chines Capture Sequential Algorithms // ACM
Transactions on Computational Logic. – 2000.
– Vol. 1, N 1. – P. 77–111.
30. Floyd R.W. Assigning Meanings to Programs
// Proc. Symposium on Applied Mathematics,
Mathematical Aspects of Computer Science. –
American Mathematical Society, 1967. –
Vol. 19. – P. 19–32.
31. Hoare C.A.R. An Axiomatic Basis for Com-
puter Programming // Communications of the
ACM. – 1969. – Vol. 12, N 10. – P. 576–583.
32. Dijkstra E.W. A personal summary of the
Gries-Owicki theory // Selected Writings on
Computing: A Personal Perspective. –
Springer-Verlag; NewYork; Heidelberg,
Berlin; 1982. – P. 188–199.
33. Lamport L. Control predicates are better than
dummy variables for reasoning about program
control // ACM Transactions on Programming
Languages and Systems (TOPLAS). – 1988. –
Vol. 10, N 2. – P. 267 – 281.
Отримано 11.12.2007
Про автора:
Панченко Тарас Володимирович.
Місце роботи автора:
Київський національний університет
імені Тараса Шевченка,
01033, Київ, вул. Володимирська 60.
Тел.: 259 0519.
e-mail: tpanchenko@issystems.com.ua
|
| id | nasplib_isofts_kiev_ua-123456789-329 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 1727-4907 |
| language | Ukrainian |
| last_indexed | 2025-12-07T18:16:43Z |
| publishDate | 2008 |
| publisher | Інститут програмних систем НАН України |
| record_format | dspace |
| spelling | Панченко, Т.В. 2008-03-31T15:57:56Z 2008-03-31T15:57:56Z 2008 Метод доведення властивостей програм в композиційно-номінативних мовах IPCL / Т.В. Панченко // Пробл. програмув. — 2008. — N 1. — С. 3-16. — Бібліогр.: 33 назв. — укр. 1727-4907 https://nasplib.isofts.kiev.ua/handle/123456789/329 681.3 Викладено композиційний метод верифікації систем спеціального класу – моделі багатоекземплярного
 виконання програм у серверному середовищі з паралелізмом у режимі почергового виконання з пере
 ключенням і взаємодією через спільну пам’ять. У роботі специфіковано задачу, побудовано відповідні
 моделі, сформульовано два варіанти часткової коректності програм на введених композиційних мовах та запропоновано методологію верифікації, що включає метод з лінійною складністю замість
 експоненційної. The compositional method for verification of special class systems, namely multi-instance program execution model in server environment with shared memory interleaving concurrency, is presented. The task is specified and appropriate models are developed here. Two types of partial correctness properties of programs in introduced compositional languages are formulated. Methodology of verification including method with linear complexity instead of exponential one is developed here. uk Інститут програмних систем НАН України №1 С. 3-16. Теоретичні та методологічні основи програмування Метод доведення властивостей програм в композиційно-номінативних мовах IPCL The Method for Program Properties Proof in Compositional Nominative Languages IPCL Article published earlier |
| spellingShingle | Метод доведення властивостей програм в композиційно-номінативних мовах IPCL Панченко, Т.В. Теоретичні та методологічні основи програмування |
| title | Метод доведення властивостей програм в композиційно-номінативних мовах IPCL |
| title_alt | The Method for Program Properties Proof in Compositional Nominative Languages IPCL |
| title_full | Метод доведення властивостей програм в композиційно-номінативних мовах IPCL |
| title_fullStr | Метод доведення властивостей програм в композиційно-номінативних мовах IPCL |
| title_full_unstemmed | Метод доведення властивостей програм в композиційно-номінативних мовах IPCL |
| title_short | Метод доведення властивостей програм в композиційно-номінативних мовах IPCL |
| title_sort | метод доведення властивостей програм в композиційно-номінативних мовах ipcl |
| topic | Теоретичні та методологічні основи програмування |
| topic_facet | Теоретичні та методологічні основи програмування |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/329 |
| work_keys_str_mv | AT pančenkotv metoddovedennâvlastivosteiprogramvkompozicíinonomínativnihmovahipcl AT pančenkotv themethodforprogrampropertiesproofincompositionalnominativelanguagesipcl |