Конструювання та верифікація програм на основі специфікацій у композиційно-номінативній мові CNLS
Ця робота продовжує цикл попередніх досліджень, головною метою яких було створення ефективних мов, підходів та програмних
 засобів розробки якісних програмних систем з використанням формальних методів. На основі побудованих раніше мов
 специфікації, програмування та математичного апа...
Збережено в:
| Дата: | 2010 |
|---|---|
| Автори: | , |
| Формат: | Стаття |
| Мова: | Українська |
| Опубліковано: |
Інститут програмних систем НАН України
2010
|
| Теми: | |
| Онлайн доступ: | https://nasplib.isofts.kiev.ua/handle/123456789/14631 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Цитувати: | Конструювання та верифікація програм на основі специфікацій у композиційно-номінативній мові CNLS / М.А. Безверха, П.П. Процик// Пробл. програмув. — 2010. — № 2-3. — С. 340-348. — Бібліогр.: 15 назв. — укр. |
Репозитарії
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1860164116030685184 |
|---|---|
| author | Безверха, М.А. Процик, П.П. |
| author_facet | Безверха, М.А. Процик, П.П. |
| citation_txt | Конструювання та верифікація програм на основі специфікацій у композиційно-номінативній мові CNLS / М.А. Безверха, П.П. Процик// Пробл. програмув. — 2010. — № 2-3. — С. 340-348. — Бібліогр.: 15 назв. — укр. |
| collection | DSpace DC |
| description | Ця робота продовжує цикл попередніх досліджень, головною метою яких було створення ефективних мов, підходів та програмних
засобів розробки якісних програмних систем з використанням формальних методів. На основі побудованих раніше мов
специфікації, програмування та математичного апарата представляються практичні підходи автоматизованої побудови та
верифікації програм на основі специфікацій. Зокрема, методи перетворення специфікацій у код програми, використання
спеціальних засобів мови для автоматичного створення тестових прикладів та можливостей мови по застосуванню методів
верифікації під час виконання.
This work continues the series of previous studies whose primary purpose was creating efficient languages, approaches and software tools
for development of quality software systems using formal methods. On the basis of developed specification and programming languages we
present new practical approaches for automated construction and verification of programs based on formal specifications. In particular,
methods of conversion specifications in the program code, the use of special means of language to automatically create test cases and
language capabilities for the application of run-time verification.
|
| first_indexed | 2025-12-07T17:56:06Z |
| format | Article |
| fulltext |
Формальні методи програмування
© М.А. Безверха, П.П. Процик, 2010
340 ISSN 1727-4907. Проблеми програмування. 2010. № 2–3. Спеціальний випуск
УДК 681.3.06
КОНСТРУЮВАННЯ ТА ВЕРИФІКАЦІЯ ПРОГРАМ
НА ОСНОВІ СПЕЦИФІКАЦІЙ
У КОМПОЗИЦІЙНО-НОМІНАТИВНІЙ МОВІ CNLS
М.А. Безверха, П.П. Процик
Національний авіаційний університет, Київ, проспект Космонавта Комарова, 1, корп. 6.
E-mail: mariya.bezverkha@livenau.net
ЗАТ «СІКЛУМ», 03680, Київ, вул. Антоновича, 172, офіс 19.
Тел. +38 044 545 7745 ext. 821
piter.protsyk@gmail.com
Ця робота продовжує цикл попередніх досліджень, головною метою яких було створення ефективних мов, підходів та програмних
засобів розробки якісних програмних систем з використанням формальних методів. На основі побудованих раніше мов
специфікації, програмування та математичного апарата представляються практичні підходи автоматизованої побудови та
верифікації програм на основі специфікацій. Зокрема, методи перетворення специфікацій у код програми, використання
спеціальних засобів мови для автоматичного створення тестових прикладів та можливостей мови по застосуванню методів
верифікації під час виконання.
This work continues the series of previous studies whose primary purpose was creating efficient languages, approaches and software tools
for development of quality software systems using formal methods. On the basis of developed specification and programming languages we
present new practical approaches for automated construction and verification of programs based on formal specifications. In particular,
methods of conversion specifications in the program code, the use of special means of language to automatically create test cases and
language capabilities for the application of run-time verification.
Вступ
Процес верифікації – це важливий етап розробки програмних систем. Мета процесу верифікації –
встановлення того, що поведінка програми збігається з очікуваною поведінкою. Це інтуїтивно зрозуміле
визначення не уточнює, що таке виконання програми, її поведінка – реальна та очікувана, і як впевнитись, що
вони збігаються. В залежності від обраних визначень процес верифікації буде суттєво різним. Так, при ручній
верифікації (тестуванні), під поведінкою найчастіше розуміють те, що користувач бачить на екрані при роботі
програми разом з результатами, які вона виробляє: файли, друковані документи тощо. Часто очікувану
поведінку програми описують лише неформально у вигляді результатів її виконання та проміжних станів.
На практиці використання формальних, тобто заснованих на математичних методах, засобів верифікації
є досить складним [1]. Однією з причин такого стану справ – є недостатній рівень автоматизації формальних
методів, складність їх інтеграції в існуючі процеси.
Ця робота продовжує цикл досліджень [2 – 4], головною метою яких було створення ефективних мов,
підходів та програмних засобів розробки якісних програмних систем з використанням формальних методів. На
основі побудованих у попередніх роботах мов специфікації [2, 4], програмування та математичного апарата
представляються практичні підходи автоматизованої побудови та верифікації програм на основі специфікацій.
Зокрема, методи перетворення специфікацій у код програми, використання спеціальних засобів мови для
автоматичного створення тестових прикладів та можливостей мови по застосуванню методів верифікації під
час виконання.
У проведених дослідженнях широко застосовуються принципи та математичний апарат композиційно-
номінативного підходу [5]. Визначення використаних у даній роботі понять взяті з роботи [6].
Специфікація програм
Верифікації програмних системи не можлива без чіткого опису очікуваної поведінки системи, що витікає
з мети цього процесу. Такий опис поведінки може виконуватись різними способами – за допомогою вимог,
тестових сценаріїв (test cases), формальних специфікацій тощо.
У контексті даної роботи для специфікації поведінки буде використовуватись підхід, що ґрунтується на
використанні мови Z-Notation [7] та композиційно-номінативної семантики, які запропоновані у роботах [3, 4].
У рамках цього підходу система описується в термінах станів та переходів з одного стану в інший.
Функціонування системи починається з деякого початкового стану та продовжується (можливо, нескінченно
довго), поки існує можливість переходу в інший стан. Іноді виділяють множину станів, яку називають
заключною, і при переході системи в один з таких станів її виконання припиняється. Кожна програмна система
повинна мати хоча б один початковий стан. Тому для кожної специфікації має виконуватись наступне
твердження
teInitialStaStateSpace .
Формальні методи програмування
341
Специфікація програмної системи у Z-Notation – це набір схем разом з тестовими поясненнями. Схеми
описують поведінку та властивості системи. Схема у Z-Notation – це засіб структурування специфікації. Схема
складається з декларативної та предикативної частин. У декларативній частині описуються змінні, які
приймають участь у схемі. Предикативна частина накладає на змінні обмеження, описує їх властивості,
встановлює взаємовідношення між ними у формі предикатів логіки першого порядку. Існує три типи змінних:
вхідні, вихідні та змінні стану системи. Синтаксично схема має такий вигляд: [ Declaration | Predicates].
У специфікаціях можна використовувати схеми в наступних випадках: для завдання типів даних,
у визначеннях, у предикатах.
У загальному випадку схема має таку структуру:
Scheme = [ x1 : S1 ; … ; xn : Sn;
x’1 : S1 ; … ; x’n : Sn;
i1? : T1 ; … ; im? : Tm;
o1! : U1 ; … ; op! : Up |
Prek (i1 , … , im , x1 ,…, xn );
Invl (x1 , … , xn ); Invo (x’1 , …. , x’n);
Opj (i1,…,im,x1,…,xn,x’1,…,x’n ,o1,…,op)],
де
x1 : S1 ; … ; xn : Sn – змінні стану до виконання операції,
x’1 : S1 ; … ; x’n : Sn – змінні стану після виконання операції,
i1? : T1 ; … ; im? : Tm – вхідні змінні,
o1! : U1 ; … ; op! : Up – вихідні змінні,
Prek – предикати, які задають передумови операції,
Invl, Invo – інваріантні відношення, які накладаються на змінні,
Opj – предикати, які задають операцію, тобто пов’язують поточний та наступний стан системи.
На практиці використовуються різні рівні деталізації поняття стану та переходу. Будемо представляти
стани системи за допомогою номінативної множини [5, 6]. Вона складається з компонентів вигляду
ім’язначення. Переходи тлумачаться як номінативні операції, що відображають одні стани системи в інші.
Схеми поділяються на три типи: схеми станів, ініціалізації та операцій.
SchemaText = StateSchemaText | InitSchemaText | OpSchemaText;
StateSchemaText = [ x1 ,…, xn | P(x1 ,…, xn) ];
InitSchemaText = [x1' ,…, xn' | Init(x1' ,…, xn') ];
OpSchemaText = [x1,…,xn,x1',…,xn' | Pre(x1 ,…, xn);Op(x1 ,…, xn, x1' ,…, xn'); Post(x1' ,…, xn') ].
Зафіксуємо множину доступних імен
Names == {x1 ,…, xm}.
За необхідності множину імен можна буде поповнювати. Але вона завжди буде містити лише скінчену
кількість елементів. Достатньо розглядати схеми у такій синтаксичній формі:
S = [x1,…,xn,x1',…,xn' | P(x1 ,…, xn), Q(x1 ,…, xn, x1' ,…, xn'), R(x1' ,…, xn')].
Тоді введемо такі позначення: Names(S) = { x1,…,xn } та Names'(S) = { x1',…,xn' }, відповідно.
Тепер можемо надати формальне визначення специфікації. Отже, синтаксичною специфікацією
програмної системи у Z назвемо впорядкований текст, що складається з довільного скінченого числа схем
станів ST1,…,STk, однієї або декількох схем ініціалізації I1,…,Im, довільного скінченого числа схем операцій
Op1,…,Opn та довільного числа допоміжних схем-визначень C1,…Cp. Схеми визначення вводяться як
синтаксичні скорочення. При цьому, при переході до семантики, вони об’єднуються з семантикою схеми, в якій
вони використовуються. Схеми можна синтаксично об’єднувати за допомогою операції синтаксичного
об’єднання схем.
Як було показано у [4], кожна схема Sch буде визначати клас номінативних множин S(Sch) такий, що
кожен елемент цього класу буде задовольняти умовам специфікованим у відповідній схемі. Детальні викладки
семантики схем були представлені в [3, 4].
Враховуючи попередні міркування, специфікацією програмної системи у Z-Notation будемо називати
наступну четвірку Spec=(ST,I,OP,C), де ST={ ST1,…,STk } – множина схем станів; I={ I1,…,Im } – множина схем
ініціалізації; OP={Op1,…,Opn } – множина схем операцій; C={ C1,…Cp } – множина допоміжних схем.
Формальні методи програмування
342
Моделлю Z-специфікації, (або моделлю, яку індукує специфікація) будемо називати трійку, що
визначається наступним чином:
),,(
)(...)()(
);...(
);...(
21
21
21
OPIST
OpSOpSOpS
IIIS
STSTSTS
Model
n
m
k
.
Зазначимо, що OP фактично задає часткову багатозначну функцію з множини всіх номінативних даних
ND у ND.
Зрозуміло, що не кожна специфікація визначає програмну систему здатну щось обчислювати. Для цього
необхідно (але не достатньо), щоб отримана модель системи задовольняла наступним умовам:
1. ST , тобто простір станів не вироджений;
2. STI та I , тобто існує хоча б один початковий стан;
3. STstOpstOPSTst )()(: , тобто операції системи не виходять за межі простору станів.
Стан st системи називається заключним, якщо )(stOP .
З наведених визначень випливає, що кожна коректна Z специфікація задає транзиційну систему. Ця
транзиційна система і буде описувати поведінку досліджуваної програмної системи. При чому, на кожному
кроці виконання вона буде задовольняти умовам специфікації.
Отже, наступним кроком, у роботі буде досліджуватись перехід від цієї формальної моделі до коду
програми та побудові засобів її верифікації.
Математичний інструментарій мови CNLS
Перейдемо до розгляду мови програмування, яка буде використовуватись для досягнення поставленої
мети. Ця мова була вперше представлена у роботі [2] і з того часу зазнала активного розвитку. Згодом її назва
була змінена на «композиційно-номінативну мову специфікації програмних систем» (Composition-Nominative
Language for program Specification) або скорочено CNLS.
Найбільший інтерес для даної роботи буде являти так званий математичний інструментарій мови. Тобто
формалізми, запозичені з математики та розвинуті, враховуючи потреби програмування [5].
Множини
Поняття множини широко використовується у мові CNLS. Основний тип даних у мові – номінативний
об’єкт, який на семантичному рівні моделюється номінативною множиною. Окрім пар «ім’я»-«значення»,
номінативний об’єкт містить пари спеціального вигляду – «ім’я»-«функція», що не суперечить загальному
визначенню номінативної множини, але суттєво розширює семантику мови. У мові кожна обчислювана
функція може розглядатись як дане і як функція. Можливість тлумачення функції як даного важлива для
побудови ефективних методів верифікації.
Математичний інструментарій мови CNLS дає можливість оперувати наступними, дещо умовними,
класами множин:
- множини чисел: N, Z, D;
- мовні множини – це множини слів деякого алфавіту, множини, що задаються регулярними виразами;
- номінативні множини – це множини пар ім’я-значення ND = [v–>1, y–>[z–>4]];
- скінчені множини деяких об’єктів;
- множини, що задаються предикатом належності, наприклад, }0,12|{ NkkkxNxOdd ;
- типи даних: кожен тип даних задає множину об’єктів (клас).
Для множин визначені класичні теоретико-множинні операції – об’єднання, перетину, різниці тощо.
Функції
На семантичному рівні програма у мові CNLS трактується як функція над номінативним даним (станом),
побудована з більш простих функцій за допомогою композицій, та відображає вхідні дані програми у вихідні.
Результат виконання програми може бути невизначеним або символічно – . Тому, кожна програма в
загальному випадку задає часткову функцію над множиною номінативних даних.
Кожна синтаксична конструкція визначає номінативну функцію певного рівня, що належить класу всіх
відображень вигляду ND → ND.
Зрозуміло, що всі функції на рівні семантики – квазіарні [6], для зручності будемо допускати такі
синтаксичні скорочення для позначення застосування функції до відповідного номінативного даного [8]. Або,
що те саме, але більш звично для програмування – виклику тіла функції з параметром. Тут символьний запис
t1~t2 означає, що «терм t1 є скороченим записом семантичного терму t2»:
- fst() ~ f(st);
- fst(v1)~f(st [v1→ x1]), для деякого значення параметру x1;
- fst(v1,...,vn) ~ f(st [v1 → x1 ,…, vn → xn]), для деяких значень параметрів x1 ,…, xn.
Формальні методи програмування
343
Найпростішими є константні функції
- відсутнє значення – Null ~ null() ≡ null;
- константа нуль – 0 ~ 0 ≡ 0;
- числові константи – n ~ n ≡ n, n N, або Z, або R.
Зауважимо, що числові проміжки, які є областю значення числових констант є, як правило, обмеженими
і скінченими (навіть для дійсних чисел) в силу об’єктивних причин, що накладаються можливостями
обчислювальних пристроїв.
Запис sem(t) буде позначати семантичний об’єкт, що відповідає синтаксичному терму t.
Розглянемо синтаксичне визначення функції, основного об’єкту мови CNLS, за допомогою форм Бекуса-
Наура:
functionDefinition := f(v1,…, vn ) global(a1,…, am){functionBody}
functionBody := functionCall ’;’ functionBody | empty
functionCall := id ‘(‘ functionCall ,…, functionCall ‘)’.
Як бачимо, визначення складається з
- імені – f;
- списку обов’язкових імен-аргументів – v1,…, vn;
- списку змінних стану, які функція може змінити – a1,…, an;
- визначення тіла функції functionBody, що являє собою послідовність викликів функцій.
Спочатку визначимо семантику для виклику тіла (обчисленні значення) функції над заданими
значеннями параметрів. Нехай існує визначення функції у формі f(v1,…, vn) global(a1,…, am) { functionBody }.
Тоді терм f(x1,…,xn) позначає результат обчислення функції f на даному st [v1 → x1 ,…, vn → xn]. Цей результат
отримується послідовним виконанням обчислень заданих термом functionBody
f(v1,…, vn )
global(a1,…, am) {
g1(v1,…, vn , a1,…, am);
g2(v1,…, vn , a1,…, am);
. . .
gk(v1,…, vn , a1,…, am);
}
t = f(x1,…,xn).
Тоді 1 1( ) [ ( ), ( ),..., ( )]m msem t state result result body a a body a a body
при ))'((...))'(( 1 stategsemstategsembody k та ],...,[' 11 nn xvxvstatestate .
Розглянемо представлення базових номінативно обчислюваних функцій у CNLS:
- константи нуль 0, – 0, один 1, – 1 та інші;
- порожнє дане [] D – empty;
- функція вибору іменованої компоненти – D – d.v;
- предикат належності – (WD)(a, d1) – (d1.Has(a));
- існування імені – (!v)(d) – (d.HasName(v));
- бінарна композиція присвоювання (іменування) – asD(f,g)(d) – (empty.[ f (d)→ g(d)]);
- взяття значення (роз’іменування) – cnD(f,g)(d) – (g(d)[f(d)]);
- перейменування (реномінації) – RD(a,b)(d) – ([b→d.a]+(d – [a→d.a])).
Синтаксичний спектр функцій мови значно ширший, ніж набір базових, але на семантичному рівні вони
можуть бути зведеними до вказаних базових.
Функції з перевірками
Мова володіє потужним механізмом, який дозволяє в декларативній формі накладати умови на функції і
на програму. Ці специфікації мають форму перед-, після- та інваріантних умов.
Крім того, існує можливість використовувати булеві вирази (предикати), які будуть обчислюватись під
час виконання програми, що забезпечить додатковий контроль при розробці, тестуванні та використанні
програми.
Синтаксично функція з перевірками задається наступним чином:
function name(…) global (…)
[ pre(boolExpr1); post(boolExpr2); inv(boolExpr3);]
{
Body;
}.
Вираз, заданий як передумова (pre), обчислюється над станом безпосередньо перед початком обчислення
тіла функції. Відповідно вираз, заданий у післяумові (post), обчислюється одразу після тіла функції. Інваріантні
умови (inv) обчислюються кожен раз при зміні значень у стані та одразу після обчислення виразу передумови.
Обчислення умов не має змінювати значень стану.
Формальні методи програмування
344
У роботі [8] подібні механізми накладання умов на функцію носять назву контракту. Існують мови,
в яких у тій чи іншій мірі реалізується цей механізм Eiffel [9], Spec# [10] та інші.
Звичайно, що при написанні програми, у контракті можна використовувати тільки обчислювані
предикати. У CNLS до них належать такі:
- предикати номінативної належності;
- предикат існування імені у даному;
- логіко-функціональні предикати: порівняння, рівності, порожності даного;
- агрегатні предикати: any(d,p) – хоча б один, all(d,p) – кожен, та їх похідні;
- усі булеві функції мови (функції, що мають областю значень множину {T,F}).
Концепція контракту, окрім суто практичної користі, відіграє суттєву методологічну роль у сучасному
програмуванні [8–10]. За допомогою контрактів можна декларативно
- фіксувати припущення розробника цього коду, щодо вхідних, вихідних даних та перетвореннях стану в
процесі обчислення;
- формувати базис тверджень про програму для формального аналізу її поведінки під час виконання;
- утворювати зв’язок між програмою та її специфікацією.
Розглянемо реалізацію концепції контракту у мові CNLS. При переході до семантики функції будемо
використовувати такі визначення:
)),...,(( 1 nxxfsem
[ ( )],якщо виконуються співвідношення
,інакше.
state result result body
невизначено
.))'((
))];((['
;)(
,))((
2
1
truestateboolExprsemresult
statebodyresultresultstatestate
statebody
truestateboolExprsemresult
(1)
При цьому, семантика операції присвоєння зміниться наступним чином
)),...,(( 1 nxxfvsem
=
' [ ( ')],якщо виконуються співвідношення
невизначено,інакше.
state v result state
.)''()(
)];'(['''
;)),...,((
));,...,(('
33
1
1
truestateboolExprstateboolExpr
stateresultvstatestate
xxfsem
xxfsemstatestate
n
n
(2)
Враховуючи представлену семантику Z-Notation, можна провести аналогію між визначенням операцій за
допомогою схем та функціями з перевірками у CNLS: у рамках семантики Хоара/Мейера схеми операцій
визначають контракт методу.
В цьому контексті цілком природною і практично обумовленою постає задача побудови процедури
перетворення специфікації з Z-Notation у шаблон виконуваною програми CNLS. При цьому, за рахунок
контрактів досягається узгодженість програми з специфікацією.
Предикати
Предикати – це вирази, які приймають значення з двозначної множини, наприклад, {істина, фальш}.
У випадку часткових предикатів враховується також можливість невизначеного значення. У своїй статті [11]
А. Мартін окреслює проблему невизначеності в контексті семантики Z-Notation, як одну із складних проблем, з
якою стикаються дослідники. Тут буде розглядатись випадок, коли невизначеність вводиться як деяке
спеціальне значення, скажімо undef.
У CNLS є такі оператори булевої алгебри: and (&), or (|), not (!). Оператори приналежності до множини –
in, до типу – is. Крім того, предикатом буде також функція, яка повертає значення true (істина) або false(фальш).
Функцію можна додатково позначати як предикат за допомогою такого контракту: function pred(x,y,…) [ pre();
post(result is Boolean); invariant(unchanged(state, x,y,..,)) ] {…}. Тут unchanged(…) – системний предикат, який
вказує на те, що обчислення тіла функції не призводить до змін у стані змінних.
Якщо при обчисленні предикату виникає невизначена ситуація, наприклад, один з аргументів є
невизначеним, то значення предикату автоматично приймається невизначеним. Крім того, результат виконання
програми у такому випадку теж буде невизначеним.
Перетворення специфікації у CNLS програму
При використанні традиційних мов програмування розв’язання задачі перетворення специфікації у
виконуваний код є нетривіальною проблемою. Крім того, результуючий код програми слабко зв’язаний з
початковою специфікацією і можливість відслідковувати обернені зв’язки та виконувати взаємні корективи
(специфікації-коду) втрачається.
Формальні методи програмування
345
Проте існують спеціалізовані мови програмування, такі як Spec#, Eiffel та інші, які за рахунок
розширених мовних конструкцій дозволяють зберігати зв’язок між кодом програми та специфікацією і далі
використовувати ці зв’язки при формальному аналізі програми. Наприклад, у роботі [12] представлена
процедура побудови програми Spec# на основі специфікації. До мов такого класу належать і CNLS.
Опишемо процес, який дозволяє автоматизовано перетворювати коректні специфікації у формі
(ST,I,OP,C) в програми на мові CNSL. Специфікації може відповідати багато синтаксично різних програм,
проте поведінка кожної з них буде збігатися з властивостям, заданими у специфікації.
Процес перетворення у виконуваний код відбувається поступово, шляхом послідовних кроків уточнення.
Перший крок – створення початкової програми може виконуватись автоматично. При цьому, змінні описані у
схемах станів (ST), перетворяться у змінні стану програми. Вхідні дані та початковий стан програми мають
задовольняти умовам схем ініціалізації (I). Без втрати загальності можна вважати, що множини ST та I є
одноелементними. Якщо це не так, то їх можна отримати шляхом застосування операції об’єднання схем за
всіма елементами множин. Кожна схема з множини OP визначає функцію на станах системи.
При цьому структурно програма буде складатись з функцій Init(), Inv(st), Op1(st)…Opn(st). Припустимо,
що S = [ x1 ,…, xn | P(x1 ,…, xn) ]; I = [x1' ,…, xn' | I(x1' ,…, xn') ]. Тоді функція Init(), що задає початковий стан,
будується за схемою I наступним чином:
function Init() [pre(empty(st)); post(pred_I(result)); invariant(Inv(st))] {
st = [
x1→null, x2→null, . . . xn→null];
}.
Предикат, що задає після умови у контракті pred_I, будується на основі визначення I(x1' ,…, xn') у схемі.
При чому можливі два випадки, перший, коли визначення I(x1' ,…, xn') задає вираз, що можна автоматично
перетворити у вираз мови та більш складний, коли автоматичне перетворення не можливе. У другому випадку,
будується пуста функція pred_I, яка повинна обчислювати значення предикату. Розробка алгоритму
обчислення, в цьому випадку, віддається на розсуд розробника, так само, як і тіла функції Init.
Функція, що обчислює значення предикату Inv, будується на основі визначення схеми S таким чином:
function Inv(st)[pre(); post(result is Boolean); inv(unchanged(st))]{
return (Names(st).Subset([x1 ,…, xn])) && pred_P(st);
}.
При цьому, ситуація з функцією pred_P, яка обчислює значення предикату, аналогічна попередньому
випадку. Для кожної схеми, що задає операцію Op = [x1,…,xn,x1',…,xn' | Pre(x1 ,…, xn);Op(x1 ,…, xn, x1' ,…, xn');
Post(x1' ,…, xn') ], будується окрема функція програми:
function Op(st)[pre(pred_Pre(st)); post(pred_Post(result)&pred_Op(st, result)); invariant(Inv(st))]{
throw NotImplementedException();
}.
Розглянемо типовий приклад схеми, що задає операцію та функцію, яка може бути отримана за нею
- схема f = [x:Z, x’:Z| x>0; x’ mod 2 == 0],
- функція function f(st) [ pre(st(x)>0); post(result(x) % 2 == 0); invariant(st(x) is int); ] { обчислення }.
Отримана за специфікацією програма не містить тексту обчислення, вона є шаблоном для подальшого
уточнення розробником. Важливість цього шаблону полягає в тому, що він дозволяє в подальшому будувати
програми, які задовольняють вимогам, накладеним специфікацією.
Наступні кроки уточнення творчі. Вони виконуються розробником системи та полягають у реалізації
виконуваної частини програми, яку неможливо отримати з декларативних специфікацій на першому кроці. Так,
за допомогою предикатів, можна виразити складні твердження про властивості функції. Задати обчислення цієї
функції можна різними способами – це і є задача розробника.
Створена таким чином програма, відкриває ряд нових можливостей для верифікації, серед яких
- застосовування засобів верифікації, характерних для Z-Notation, коли властивості програми будуть
відповідати властивостям специфікації за рахунок контрактів, з одним обмеженням, – контракт програми є
істинним;
- автоматизована генерація тестових прикладів та їх виконання;
- використання методик верифікації під час виконання.
Автоматизоване тестування CNLS програм
Розглянемо процес побудови тестових прикладів та верифікації програм, створених за представленою
методикою. Завдяки тісному зв’язку отриманої програми з формальною специфікацією, цей процес добре
піддається автоматизації. Це робить його також потужним засобом тестування.
Розглянемо функцію з попереднього прикладу
function f(x) [ pre(x>0); post(x % 2 == 0); invariant(x is int); ] {
x = x*4 ;
return x;
}.
Формальні методи програмування
346
Умови, що накладаються за допомогою контракту, мають виділяти серед усіх даних ті, які належать
області визначеності та області значень функції. Цю інформацію можна використовувати для побудови
прикладів, які б задовольняли накладеним умовам. Існує спеціальний клас програмних засобів, здатних
виконувати цю задачу – це Satisfiability Modulo Theory (SMT) солвери, серед яких – Yices, Z3 [13, 14].
Покажемо на прикладі солверу Yices, яким чином можна використовувати контракти для побудови
тестових даних. Для цього перетворимо умови контракту в предикати, записані на мові солвера
Контракт CNLS Yices
invariant(x is int) (define f1::(-> int int))
(define x::int)
pre(x>0); (assert (> x 0))
post(x % 2 == 0); (assert (= (mod (f1 x) 2) 0)).
Отримаємо такий вхідний текст:
(define x::int)
(define f::(-> int int))
(assert (> x 0))
(assert (= (mod (f x) 2) 0))
(check).
Розглянемо протокол роботи програми після запуску з такими параметрами:
yices.exe -e 1.txt
Результат Опис
Sat Тестовий приклад знайдено
(= x 1) При x = 1
(= (f x) 0) якщо f(x) = 0 тоді
(= (mod 0 2) 0) умова контракту x%2 == 0
задовольняється.
Цей результат було отримано лише на основі предикатів з контракту, тому значення функції f(x) = 0
може відрізнятись від реального значення функції на цьому даному. Поки що це не є важливим, оскільки мета
кроку – отримати вхідні дані, які б задовольнили умови контракту. Далі виконується обчислення функції f(x)
при x=1. Отримаємо такий результат f([x→1]) = x*4 = 4.
Тепер модифікуємо текст для солвера враховуючи нову інформацію
(define x::int)
(define f1::(-> int int))
(assert (> x 0))
(assert (= (mod (f1 x) 2) 0))
(check)
(assert (= x 1))
(assert (= (f1 x) 4))
(check).
Після запуску буде одержано такий результат:
sat
(= x 1)
(= (f1 1) 4)
(= (mod 4 2) 0).
Тобто, отримане в результаті обчислень функції значення (стан системи) теж задовольняє умовам
контракту. А отже, функція на цьому конкретному даному задовольняє умови початкової специфікації, і її
поведінку можна вважати такою, що не суперечить вимогам.
Метод побудови тестових прикладів складається з таких кроків.
Крок 1. Використовуючи умови контракту, побудувати набір даних – d1, що буде його задовольняти.
Крок 2. Отриманий набір даних підставити на вхід функції, та обчислити її значення – y1. Якщо
значення функції невизначене (функція зациклилась, виникла виключна ситуація тощо), тоді вважаємо, що
програма обчислення функції містить помилку, і необхідно або посилити умови у специфікації, або виправити
помилку та перейти до першого кроку.
Крок 3. До умов, що були побудовані на першому кроці, додаємо нове твердження: f(d1) = y1.
Та перевіряємо, що отримана система тверджень не містить суперечностей. Якщо суперечність існує,
тоді модифікуємо код програми або її специфікації.
Крок 4. Далі продовжуємо процедуру пошуку нових тестових даних, додаючи на кожному кроці умову
txx або (assert (/= x xt)), де xt – значення змінної отримане на попередньому кроці. Та переходимо до
другого кроку.
Формальні методи програмування
347
При цьому, якщо на деякому кроці процедура призведе до негативного результату на етапі перевірки
значення функції, це одразу означає, що програма, яка обчислює значення функції не відповідає умовам
специфікації, а отже містить помилку.
За рахунок автоматизації цю процедуру можна використовувати для перевірки відповідності реалізації
початковій специфікації на великих об’ємах даних, тим самим суттєво зменшуючи ризик появи дефектів у коді.
Верифікація під час виконання
Верифікація програми в процесі виконання (або Run-time верифікація) [15] – це підхід, при якому
тестування вхідної програми на відповідність специфікації відбувається власними засобами програми під час її
виконання з використанням формальних підходів. Run-time верифікація виступає як додатковий засіб, що
гарантує коректність програми. В окремому випадку верифікації під час виконання можна розглядати модульне
тестування (UnitTesting), яке полягає у виконанні тестових прикладів та порівнянні результатів з еталонними
даними. Недоліком модульного тестування є те, що і тестові приклади, і еталонні результати створюються
програмістами на основі власних міркувань, які не є формальними. Тому вважається, що верифікація в процесі
виконання є більш надійним засобом гарантування коректності програми ніж тестування (включаючи модульне
тестування), та менш надійним ніж формальні методи [15].
При запропонованому підході створення програми із формальної специфікації, контракти виступають
одним з ключових елементів верифікації під час виконання. Кожен раз при обчислені функції або модифікації
змінних стану програма перевіряє валідність цих дій шляхом обчислення значень предикатів. Крім цього,
система веде протокол усього процесу обчислення, який при порушенні умов контракту можна
використовувати для аналізу та налагодження програми.
Розглянемо наступний приклад. Нехай потрібно розробити функцію, яка з масиву натуральних чисел
виділяє ті, що повторюються. Цей приклад носить лише демонстраційний характер, але він є достатньо
показовим.
Розпочнемо із Z специфікації. Простір станів буде складатись із двох множин. Множини чисел, що не
повторюються – Unique, та тих, що повторюються – Repeated. Очевидно, вони не мають перетинатися.
StateSpace = [ )(:),(: NPRepeatedNPUnique | {}RepeatedUnique ].
При додаванні нового елемента до стану, він буде спочатку долучатися до множини Unique елементів, а
при повторному додаванні вилучатись з цієї множини і долучатись до множини Repeated:
AddItem(x)=[ NxPRepeatedUniquePRepeatedUnique :?);(:',');(:, |
}{' xUniqueUniqueUniquex ;
}{'}{\' xRepeatedRepeatedxUniqueUniqueUniquex ]
Відповідна програма буде складатись із двох частин: блоку ініціалізації та функції додавання нового
елемента.
Блок ініціалізації:
Unique = new Set();
Repeated = new Set();.
Функція додавання елемента:
function AddItem(x)
[ pre(Naturals.Contains(x)); // відповідає Nx
post(Unique.Contains(x)|Repeated.Contains(x)); // відповідає peatedxUniquex Re
invariant(Unique.Intersect(Repeated)==Sets.Empty); // відповідає {}Re peatedUnique
]
{ if (!Unique.Contains(x)) Unique.Add(x);
else { Unique.Remove(x); Repeated.Add(x); }
}.
З прикладу варто звернути увагу на блок інваріанта, де специфікуються умови порожності перетину
множин (з умови схеми StateSpace), а також післяумову, яка гарантує, що елемент буде долучено хоча б в одну
множину. На рис. 1 показано обробку описаного прикладу в системі CNLS.
Зазначимо також, що зміна порядку операцій вилучення та додавання елемента до множини призведе до
порушення умови інваріанта: зміна Unique.Remove(x); Repeated.Add(x); на Repeated.Add(x); Unique.Remove(x). Від
моменту додавання елемента до множини Repeated і до моменту його вилучення із множини Unique, ці дві
множини будуть мати непорожній перетин. Результат виконання функції від цього не зміниться, такий стан
програми може призводити до небажаних сторонніх ефектів, наприклад, у випадку багатопоточності.
Це зауваження показує, що навіть достатньо тривіальні приклади програм, можуть містити в собі важко
передбачувані аспекти, які легко ідентифікуються при використанні формальних підходів. Все це говорить на
користь запропонованого методу, хоча його використання і не гарантує відсутності інших помилок.
Запропонований підхід може застосовуватись як додатковий засіб перевірки часткової коректності програм, та
бути додатковим «ременем безпеки» при розробці програмного забезпечення.
Формальні методи програмування
348
Рисунок. Унікальні та повторювані елементи
Висновки
Результатом роботи є розвиток підходів автоматизованої верифікації програм, створених за допомогою
мови програмування CNLS. Запропоновані методи перетворення формальних специфікацій у код програми.
Розроблено методи побудови тестових прикладів за допомогою солверів. Представлено засоби, що підтримають
методи верифікації під час виконання.
Важливість отриманих результатів полягає в їх практичній значимості. Кожен з представлених методів
добре підлягає автоматизації та може використовуватись при розробці програмних систем. Крім того, в рамках
цієї роботи були розроблені діючі прототипи для обробки представлених мов специфікації та програмування.
1. J.C. Knight, C.L. Dejong, M.S. Gibble, L.G. Nakano. Why Are Formal Methods Not Used More Widely // Fourth NASA Formal Methods
Workshop. – 1997. P. 1–12.
2. Процик П.П. Композиційно–номінативна мова програмування Script.NET // “Проблеми програмування”. № 2–3 (спеціальний випуск).
Київ – 2008. –С. 323–331.
3. Процик П.П. Композиційно-номінативний підхід до побудови семантики Z-Notation // Вісник київського університету. Сер.: Фізико-
математичні науки. – 2008. – № 1. – С. 116–120.
4. Процик П.П. Композиційно-номінативний підхід до специфікації програмних систем у мові Z-Notation // Вісник Київського
університету. Сер.: Фізіко-математичні науки.–2009.–№ 1. –С. 133–138.
5. Никитченко Н.С. Композиционно-номинативный подход к уточнению понятия программы. // Проблеми программування. – 1999.–№ 1.
– C. 16– 31.
6. Нікітченко Н.С., Шкільняк С.С. Математична логіка та теорія алгоритмів:підручник – К.: Видавничо-поліграфічний центр «Київський
університет», 2008. – 528 с.
7. Jim Woodcock, Jim Davies: Using Z. Specification, Refinement, and Proof // Prentice Hall, New York – 1996. – 523 p.
8. B. Meyer. Object-oriented software construction – New York: Prentice–Hall International Series of Computer Science, 2000. – 1296 p.
9. B. Meyer Eiffel: The Language– New York: Prentice–Hall International Series of Computer Science, 1992. – 296 p.
10. M. Barnett, K. Rustan, M. Leino, W. Schulte. The Spec# programming system: An Overview // CASSIS 2004 Proceedings – 2004. – P. 29–69.
11. Martin Andrew Relating Z and First-Order Logic // Journal of Formal Methods. – 1999. – Volume II. – P. 1266–1280.
12. Shengchao Qin; Guanhua He, Linking Object-Z with Spec# //Proc. of 12th IEEE International Conference on Engineering Complex Computer
Systems, 11–14 July 2007. – P. 185 – 196.
13. L. Moura N. Bjørner, Z3: An Efficient SMT Solver, Conference on Tools and Algorithms for the Construction and Analysis of Systems
(TACAS), Budapest, Hungary, 2008. – P. 1–10.
14. B. Dutertre and L. Moura. The YICES SMT Solver. In SMTCOMP: Satisfiability Modulo Theories Competition, 2006. http://yices.csl.sri.com/.
15. M. Barnett and W. Schulte. Contracts, Components, and their Runtime Verification. Technical Report MSR–TR–2002–38, Microsoft Research,
April 2002. ftp://ftp.research.microsoft.com/pub/tr/tr–2002–38.pdf
|
| id | nasplib_isofts_kiev_ua-123456789-14631 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 1727-4907 |
| language | Ukrainian |
| last_indexed | 2025-12-07T17:56:06Z |
| publishDate | 2010 |
| publisher | Інститут програмних систем НАН України |
| record_format | dspace |
| spelling | Безверха, М.А. Процик, П.П. 2010-12-27T13:44:15Z 2010-12-27T13:44:15Z 2010 Конструювання та верифікація програм на основі специфікацій у композиційно-номінативній мові CNLS / М.А. Безверха, П.П. Процик// Пробл. програмув. — 2010. — № 2-3. — С. 340-348. — Бібліогр.: 15 назв. — укр. 1727-4907 https://nasplib.isofts.kiev.ua/handle/123456789/14631 681.3.06 Ця робота продовжує цикл попередніх досліджень, головною метою яких було створення ефективних мов, підходів та програмних
 засобів розробки якісних програмних систем з використанням формальних методів. На основі побудованих раніше мов
 специфікації, програмування та математичного апарата представляються практичні підходи автоматизованої побудови та
 верифікації програм на основі специфікацій. Зокрема, методи перетворення специфікацій у код програми, використання
 спеціальних засобів мови для автоматичного створення тестових прикладів та можливостей мови по застосуванню методів
 верифікації під час виконання. This work continues the series of previous studies whose primary purpose was creating efficient languages, approaches and software tools
 for development of quality software systems using formal methods. On the basis of developed specification and programming languages we
 present new practical approaches for automated construction and verification of programs based on formal specifications. In particular,
 methods of conversion specifications in the program code, the use of special means of language to automatically create test cases and
 language capabilities for the application of run-time verification. uk Інститут програмних систем НАН України Формальні методи програмування Конструювання та верифікація програм на основі специфікацій у композиційно-номінативній мові CNLS Specification Based Program Construction and Verification in Composition-Nominative Language CNLS Article published earlier |
| spellingShingle | Конструювання та верифікація програм на основі специфікацій у композиційно-номінативній мові CNLS Безверха, М.А. Процик, П.П. Формальні методи програмування |
| title | Конструювання та верифікація програм на основі специфікацій у композиційно-номінативній мові CNLS |
| title_alt | Specification Based Program Construction and Verification in Composition-Nominative Language CNLS |
| title_full | Конструювання та верифікація програм на основі специфікацій у композиційно-номінативній мові CNLS |
| title_fullStr | Конструювання та верифікація програм на основі специфікацій у композиційно-номінативній мові CNLS |
| title_full_unstemmed | Конструювання та верифікація програм на основі специфікацій у композиційно-номінативній мові CNLS |
| title_short | Конструювання та верифікація програм на основі специфікацій у композиційно-номінативній мові CNLS |
| title_sort | конструювання та верифікація програм на основі специфікацій у композиційно-номінативній мові cnls |
| topic | Формальні методи програмування |
| topic_facet | Формальні методи програмування |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/14631 |
| work_keys_str_mv | AT bezverhama konstruûvannâtaverifíkacíâprogramnaosnovíspecifíkacíiukompozicíinonomínativníimovícnls AT procikpp konstruûvannâtaverifíkacíâprogramnaosnovíspecifíkacíiukompozicíinonomínativníimovícnls AT bezverhama specificationbasedprogramconstructionandverificationincompositionnominativelanguagecnls AT procikpp specificationbasedprogramconstructionandverificationincompositionnominativelanguagecnls |