Search for invariants of U-Y-programs by an interactive algorithm over completely free data algebras
The problem of generating program invariants on free algebras is considered. Modern provers need program invariants as input to get more relevant results for software verification. Implementation of iterative algorithm for generating invariants on absolutely free algebras is presented. We show that...
Gespeichert in:
| Datum: | 2015 |
|---|---|
| 1. Verfasser: | |
| Format: | Artikel |
| Sprache: | Ukrainian |
| Veröffentlicht: |
Інститут програмних систем НАН України
2015
|
| Schlagworte: | |
| Online Zugang: | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/73 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| Назва журналу: | Problems in programming |
Institution
Problems in programming| id |
pp_isofts_kiev_ua-article-73 |
|---|---|
| record_format |
ojs |
| resource_txt_mv |
ppisoftskievua/be/3f8c9e0dbf08e002cd0bc3bb96ba29be.pdf |
| spelling |
pp_isofts_kiev_ua-article-732018-09-18T14:26:22Z Search for invariants of U-Y-programs by an interactive algorithm over completely free data algebras Поиск инвариантов U-Y- программ интерацийним алгоритмом над совершенно свободными алгебрами данных Пошук інваріантів U-Y- програм інтераційним алгоритмом над абсолютно вільними алгебрами данних Maksymets, O.M. UDC 51.681.3 УДК 51.681.3 УДК 51.681.3 The problem of generating program invariants on free algebras is considered. Modern provers need program invariants as input to get more relevant results for software verification. Implementation of iterative algorithm for generating invariants on absolutely free algebras is presented. We show that the algorithm generates relevant invariants corresponding to free algebras. Рассматривается проблема поиска программных инвариантов в программах над свободными алгебрами данных. Для получения более релевантных результатов при верификации программного обеспечения современным «Прувер» необходимы инварианты программ. Представлены реализацию итерационного алгоритма генерации инвариантов на совершенно свободных алгебры. Показано, что алгоритм генерирует релевантные инварианты для соответствующей свободной алгебры. Розглядається проблема пошуку програмних інваріантів у програмах над вільними алгебрами даних. Для отримання більш релевантних результатів при верифікації програмного забезпечення сучасним «пруверам» необхідні інваріанти програм. Представлено реалізацію ітераційного алгоритму генерації інваріантів на абсолютно вільних алгебрах. Показано, що алгоритм генерує релевантні інваріанти для відповідної вільної алгебри. Інститут програмних систем НАН України 2015-09-10 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/73 PROBLEMS IN PROGRAMMING; No 2-3 (2012) ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 2-3 (2012) ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 2-3 (2012) 1727-4907 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/73/75 Copyright (c) 2015 ПРОБЛЕМИ ПРОГРАМУВАННЯ |
| institution |
Problems in programming |
| baseUrl_str |
https://pp.isofts.kiev.ua/index.php/ojs1/oai |
| datestamp_date |
2018-09-18T14:26:22Z |
| collection |
OJS |
| language |
Ukrainian |
| topic |
UDC 51.681.3 |
| spellingShingle |
UDC 51.681.3 Maksymets, O.M. Search for invariants of U-Y-programs by an interactive algorithm over completely free data algebras |
| topic_facet |
UDC 51.681.3 УДК 51.681.3 УДК 51.681.3 |
| format |
Article |
| author |
Maksymets, O.M. |
| author_facet |
Maksymets, O.M. |
| author_sort |
Maksymets, O.M. |
| title |
Search for invariants of U-Y-programs by an interactive algorithm over completely free data algebras |
| title_short |
Search for invariants of U-Y-programs by an interactive algorithm over completely free data algebras |
| title_full |
Search for invariants of U-Y-programs by an interactive algorithm over completely free data algebras |
| title_fullStr |
Search for invariants of U-Y-programs by an interactive algorithm over completely free data algebras |
| title_full_unstemmed |
Search for invariants of U-Y-programs by an interactive algorithm over completely free data algebras |
| title_sort |
search for invariants of u-y-programs by an interactive algorithm over completely free data algebras |
| title_alt |
Поиск инвариантов U-Y- программ интерацийним алгоритмом над совершенно свободными алгебрами данных Пошук інваріантів U-Y- програм інтераційним алгоритмом над абсолютно вільними алгебрами данних |
| description |
The problem of generating program invariants on free algebras is considered. Modern provers need program invariants as input to get more relevant results for software verification. Implementation of iterative algorithm for generating invariants on absolutely free algebras is presented. We show that the algorithm generates relevant invariants corresponding to free algebras. |
| publisher |
Інститут програмних систем НАН України |
| publishDate |
2015 |
| url |
https://pp.isofts.kiev.ua/index.php/ojs1/article/view/73 |
| work_keys_str_mv |
AT maksymetsom searchforinvariantsofuyprogramsbyaninteractivealgorithmovercompletelyfreedataalgebras AT maksymetsom poiskinvariantovuyprogramminteracijnimalgoritmomnadsoveršennosvobodnymialgebramidannyh AT maksymetsom pošukínvaríantívuyprogramínteracíjnimalgoritmomnadabsolûtnovílʹnimialgebramidannih |
| first_indexed |
2025-07-17T10:08:48Z |
| last_indexed |
2025-07-17T10:08:48Z |
| _version_ |
1837888363329224704 |
| fulltext |
Формальні методи програмування
УДК 51.681.3
ПОШУК ІНВАРІАНТІВ U-Y-ПРОГРАМ ІТЕРАЦІЙНИМ
АЛГОРИТМОМ НАД АБСОЛЮТНО ВІЛЬНИМИ АЛГЕБРАМИ
ДАННИХ
О.М. Максимець
Київський національний університет ім. Тараса Шевченка,
03680, м. Київ, проспект Глушкова, 2, корпус 6,
E-mail: maksymets@gmail.com
Розглядається проблема пошуку програмних інваріантів у програмах над вільними алгебрами даних. Для отримання більш
релевантних результатів при верифікації програмного забезпечення сучасним «пруверам» необхідні інваріанти програм.
Представлено реалізацію ітераційного алгоритму генерації інваріантів на абсолютно вільних алгебрах. Показано, що алгоритм
генерує релевантні інваріанти для відповідної вільної алгебри.
The problem of generating program invariants on free algebras is considered. Modern provers need program invariants as input to get
more relevant results for software verification. Implementation of iterative algorithm for generating invariants on absolutely free algebras
is presented. We show that the algorithm generates relevant invariants corresponding to free algebras.
Вступ
В стані програми інваріант являє собою твердження щодо змінних програми, яке є вірним завжди, коли
процес обчислень потрапляє у цей стан. Будь-який прогрес у проблемах пошуку інваріантів є важливим для
перевірки правильності програм у теорії верифікації [1]. Пошук інваріантів є полем для застосування
алгоритмів на алгебрах, автоматичних «пруверів», абстрактних методів представлення і перевірки моделей.
Особливої уваги заслуговує задача пошуку інваріантів для циклів. Розв’язок цієї задачі дозволяє
знаходити вічні цикли на етапі компіляції і перевіряти більш складні програми [2].
У даній роботі розглянута узагальнена задача пошуку інваріантів, не фокусуючись на інваріантах
циклів. Вибрана мова виразів не дозволяє покрити множину виразів, які використовуються в сучасних мовах
програмування, але є наближенням до них. Новизною цієї роботи є реалізація ітераційного алгоритму [3] і
демонстрація його на прикладі.
Визначення
Розглянемо U-Y програму на пам'яті змінних { }1,..., mR r r= , які визначені на алгебрі даних ( ),D Ω .
є клас алгебр, який включає в себе алгебру ( ,K D Ω) ( ),D Ω і визначається набором рівностей [4]. Eq ( ),T RΩ
є вільною алгеброю термів, на з класу R ( ),K D Ω . Ми розглядаємо абсолютно вільну алгебру, тому множина
відомих співвідношень є пустою . Eq = ∅
Нехай { 0 1 *, ,..., }A a a a= – множина вершин U-Y програми. – множини базисів
співвідношень, які є вірними в відповідній вершині програми на поточному кроці виконання методу.
0 1, ,...,a a aN N N *
Розглядається задача пошуку інваріантів на мові . складається з термів визначених як рівності
виду , де , .
L L
( ):ir h r= ( ) ( ),h r T R∈ Ω ( )1,..., mr r r=
Для демонстрації структур даних і алгоритму розглянемо приклад програми, яка обчислює суму
1
1
1
m
y
n
z
y
y
z
m
−
=
=
∑
∑ по вхідних цілих , . Одна з U-Y програм, яка розв’язує цю задачу (рис. 1). m n
Ребро U-Y програми складаються з умов переходу u , які знаходяться зліва від ребра на рис. 1 і опера-
торів присвоєння , що знаходяться справа від ребра. позначає базис співвідношень для вершини програ-
ми , який справджується на конкретному кроці алгоритму.
y aN
a
Розглядається метод верхньої апроксимації (МВА) [5] для генерації інваріантів на вище наведеному
прикладі. МВА ігнорує умови на ребрах, а ті які мають вигляд u ( )ir h r= переносяться в присвоєння цього
ребра у вигляді . Таким чином, ребро між вершинами і , яке складається з
y
( ):ir h r= 3a 4a ( )u z m= = і
буде враховано, як 2 2 1( : ^ , : / )y x m y sum sum sum x= = = + 2 2 1( : ^ , : / , : )y x m y sum sum sum x z m= = = + = .
©О.М. Максимець, 2012
ISSN 1727-4907. Проблеми програмування. 2012. № 2-3. Спеціальний випуск 228
Формальні методи програмування
a2
a1
a0
a3
: ,input m n
1
1
1
:
m
y
n
z
y
y
z
result
m
−
=
=
∑
∑ y := 1
sum2 := 0
z := 1
sum1 := 0
x := z ^ y;
sum1 := sum1 + x
a4
x := m ^ y
sum2 := sum2 + sum1/x z = m
z:=z+1 z != m
y:=y+1 y != n
a*
y = n
Рис. 1. Приклад U-Y програми
Метод використовує три нетривіальні операції над базисами: перетин, ефект і порівняння.
Операція перетину базисів будує найбільший базис простору, який є підпростором і
( ,aef N y)
BAN NI AN BN .
Оператор за базисом співвідношень , які вірні перед виконанням операторів присвоювання ,
будує базис співвідношень, які вірні на перетвореному оператором стані пам’яті. Оператор порівняння двох
базисів співвідношень
( ,aef N y)
B
aN y
y
AN N<> перевіряє чи збігаються простори співвідношень описані цими базисами,
враховуючи, що в базисах можуть використовуватися різні набори змінних. Більш детально ці операції і їхня
оцінка складності описані в [6].
Початкове наближення
За означенням U-Y програма має тільки одну початкову вершину a0. На початкову вершину може
подаватися вхідний базис співвідношень , який є правильним до виконання програми. Решту вершин мають
порожні базиси співвідношень . Для розглядуваного прикладу
0aN
1,...,aN N *a 0aN = ∅ . Метод називається методом
верхньої апроксимації тому, що ми будуємо початкові базиси співвідношень, які з кожним кроком звужуються.
Початкове наближення цих базисів і є верхньою границею. Початкове наближення отримується в результаті
виконання першого етапу методу.
Далі приведена послідовність дій виконання першого етапу МВА (рис. 2) для пошуку початкового
наближення:
Na0 := N0
ToVisit.push(a0)
Visited := {}
while (ToVisit <> ) ∅
c := ToVisit.pop()
Visited := Visited + c
for every (c, y, a’)
if Not a’ in Visited
Na’:=ef(Nc, y)
ToVisit.push(a’)
Рис. 2. Перший етап МВА
229
Формальні методи програмування
На кожному кроці зберігається стек вершин, які потрібно відвідати і множину, які вже були
відвідані . На першому кроці методу стек складається з , а множина порожня. На
кожній ітерації методу розглядається одна з вершин стеку . Розглядаються всі ребра
ToVisit
Visited ToVisit 0a Visited
ToVisit c ( ), ,c y a′ , які
виходять з цієї вершини і присвоюються aN ′ результуючий базис ефекту ( ),cef N y . Додаємо до множини
для розгляду на наступних кроках. Етап закінчується, коли множина розглядуваних вершин є
порожньою.
a′
ToVisit ToVisit
Проведемо обчислення методу для розглянутого прикладу U-Y програми:
Беремо вершину з стеку , розглянемо ребро ,
, бо
0a ToVisit ( )( )1, 2 : 0; : 1 ,aca sum y= =
( )( ) ( )1 0: , 2 : 0; : 1 : 2 : 0; :N ef N sum y sum y= = = = = 1 0N= ∅ . =
Додаємо до множини Visite , до стеку T . 0a d 1a oVisit
Беремо вершину з стеку T , розглянемо ребро 1a oVisit ( )( )1 2, 1: 0; : 1 ,aa sum z= = :
( )1 : 2 : 0; :N sum y= = =1
=
,
( )( ) ( )2 1: , 1: 0; : 1 : 2 : 0; 1: 2; : 1; :N ef N sum z sum sum sum z y z= = = = = = = .
Додаємо до множини Visite , до стеку To . 1a d 2a Visit
Беремо вершину з стеку To , розглянемо ребро 2a Visit ( )( )2 3, 1: 1 ^ ; : ^ ,aa sum sum z y x z y= + = .
Продовжуючи виконання далі за методом отримуємо наступні базиси співвідношень, що приведені в табл. 1.
Таблиця 1. Базиси початкового наближення
Вершина Базис співвідношень
0aN ∅
1aN
2 : 0
: 1
sum
y
=
=
2 : 0
1: 2
: 1
:
sum
sum sum
z
y z
=
=
=
=
2aN
2 : 0
1: 2
: 1
:
: ^
sum
sum sum x
z
y z
x z z
=
= +
=
=
=
3aN
2 : 0 1
1: 0 ^
:
: 1
: ^
sum sum
sum z z
z m
y
x z y
= +
= +
=
=
=
4aN
2 : 0 0 ^
1: 0 ^
:
:
: ^1
sum z z
sum z z
z m
y n
x z
= + +
= +
=
=
=
*aN
Етап стабілізації розв’язку
На кожному кроці зберігається множина вершин, які потрібно відвідати . На першому кроці
методу множина складається з усіх вершин множини
ToVisit
ToVisit A окрім . На кожній ітерації методу
розглядається одна з вершин стеку . Базис поточної множини співвідношень присвоюється базис
множини співвідношень вершини : . Розглядаються всі ребра
0a
ToVisit c
c : cN N= ( ), ,a y c′ , які входять в вершину і для
кожного ребра поточний базис множини співвідношень перетинається з базисом . Після проходу
по всім перерахованим ребрам , то множина поповнюється всіма вершинами, для яких є
c
N ( ,cef N y)
cN N<> ToVisit
230
Формальні методи програмування
ребра, які ведуть з : , де – множина ребер U-Y програми. Етап методу закінчує виконання,
якщо множина розглядуваних вершин To є порожньою.
c ( ){ }| , ,a c y a S∈ S
Visit
Послідовність дій виконання другого етапу МВА (рис. 3).
ToVisit := A\{a0}
while (ToVisit <> ) ∅
c := take from ToVisit
if (Nc <> ) ∅
N := Nc
for every (a’, y, c)
N := NI ef(Nc, y)
if (N <> Nc)
Nc := N
ToVisit := ToVisit + {a | for every (c, y, a)}
Рис. 3. Другий етап МВА
Розглянемо виконання 2-го етапу методу (рис. 3) на розглядуваному прикладі програми (рис. 1).
Множина To містить { } . Visit 1 2 3 4 *, , , ,a a a a a
Розглянемо вершину , . 1a 1:N N=
Розглянемо ребро : ( )( )0, 2 : 0; : 1 ,1sum y= =
( )( ) ( )0 , 2 : 0; : 1 2 : 0; : 1ef N sum y sum y= = = = = .
Присвоюємо:
( ) ( ) ( ): 2 : 0; : 1 2 : 0; : 1 : 2 : 0; : 1N sum y sum y sum y= = = ∩ = = = = =
Розглянемо ребро ( )4 1, : 1,a y y a= + :
( )4 : 2 : 0 1; 1: 0 ^ ; : ; : 1; : ^N sum sum sum z z z m y x z y= = + = + = = = ,
( ) (4 , : 1 2 : 0 0 ^ ; 1: 0 ^ ; : ; : 1 1; : ^1ef N y y sum z z sum z z z m y x z= + = = + + = + = = + = )
) ∅
N
.
Присвоюємо:
( ) (: 2 : 0; : 1 2 : 0 0 ^ ; 1: 0 ^ ; : ; : 1 1; : ^1N sum y sum z z sum z z z m y x z= = = = + + = + = = + = =I .
Базис , тому до розгляду додаються, вершини до яких є ребра з вершини : 1N <> 1a { }2:ToVisit ToVisit a= + .
Вершина уже знаходиться в To . 2a Visit
Розглянемо вершину , . 2a 2:N N=
Розглянемо ребро : ( )( )1, 1: 0; : 1 , 2sum z= =
( ) ( )1, 1: 0, : 1 1: 0; : 1ef N sum z sum z= = = = = ,
( ) ( ) ( )2 : 2 : 0; 1: 2; : 1; : 1: 0; : 1 : 1: 0; : 1N sum sum sum z y z sum z sum z= = = = = = = = = =I .
Розглянемо ребро : ( )3, : 1,2z z= +
( )3 : 2 : 0; 1: 2 ; : 1; : ; : ^N sum sum sum x z y z x z z= = = + = = = ,
( ) (3 , : 1 2 : 0; 1: 2 ^ ; : ; : 1; : ^ef N z z sum sum sum z z z y y y x y y= + = = = + = + = = )
) ∅
N
,
( ) (2 : 1: 0; : 1 2 : 0; 1: 2 ^ ; : ; : 1; : ^ :N sum z sum sum sum z z z y y y x y y= = = = = + = + = = =I .
Базис , тому до розгляду додаються, вершини до яких є ребра з вершини : 2N <> 2a { }3:ToVisit ToVisit a= + .
Вершина уже знаходиться в To . 3a Visit
Розглянемо вершину , . 3a 3:N N=
Розглянемо ребро ( )2, 1: 1 ^ ; : ^ ,3sum sum z y z z y= + = :
( ) (2 , 1: 1 ^ ; : ^ 1: 1 ; : ^ef N sum sum z y x z y sum sum x x z y= + = = = + = )
Присвоюємо:
( ) ( ) ( ): 2 : 0; 1: 2 ; : 1; : ; : ^ 1: 1 ; : ^ : ^N sum sum sum x z y z x z z sum sum x x z y x z y= = = + = = = = + = = =I
Базис , тому до розгляду додаються, вершини до яких є ребра з вершини :
. Вершина уже знаходиться в To , а ні.
3N <> N
},
3a
{ 2 4:ToVisit ToVisit a a= + 4a Visit 2a
Розглянемо вершину , . 2a 2:N N=
Так як переходимо до наступної вершини. 2 :N = ∅
231
Формальні методи програмування
Розглянемо вершину , . 4a 4:N N=
Розглянемо ребро ( )2, 1: 1 ^ ; : ^ ,4sum sum z y x z y= + = :
( ) ( )3 , 2 : 2 1; : ; : ^ 2 : 2 1 ; : ; : ^ef N sum sum sum z m x m y sum sum sum x z m x z y= + = = = = + + = =
Присвоюємо:
( ) ( ): 2 : 0 1; 1: 0 ^ ; : ; : 1; : ^ 2 : 2 1; : ; : ^N sum sum sum z z z m y x z y sum sum sum z m x z y= = + = + = = = = + = =I
( ): ; : ^z m x z y= = =
=
},
.
Базис , тому додаємо до розгляду вершини до яких є виходи з вершини
: . Вершина уже знаходиться в To , а буде додана.
4N N<>
4N { 1 5:ToVisit ToVisit a a= + 5a Visit 1a
Розглянемо вершину , . 2a 1:N N=
Так як переходимо до наступної вершини. 1 :N = ∅
Розглянемо вершину , . Розглянемо ребро 5a 5:N N= ( )4, : ,5y n= :
( ) (4 , : : , : ; : ^ef N y n z m y n x z y= = = = = ) .
Присвоюємо:
( ) ( ) ( ): 2 : 0 0 ^ ; 1: 0 ^ ; : ; : ; : ^1 : ; : ; : ^ : ; :N sum z z sum z z z m y n x z z m y n x z y z m y n= = + + = + = = = = = = = = =I .
Базис , але з вершини немає виходів, тому що ця вершина кінцева. 5N <> N 5a
Множина To порожня, робота методу закінчилась. Visit
Результатом виконання методу є наступна множина базисів інваріантів (табл. 2).
Таблиця 2. Базиси інваріантів
Вершина Базис інваріантів
0aN ∅
1aN ∅
2aN ∅
3aN ^x z y=
^x z y=
z m= 4aN
y n=
z m= *aN
Індуктивне доведення інваріантів
Як бачимо з прикладу вище отримати доведення вірності U-Y програми не вдається, оскільки з базису
інваріантів неможливо вивести вираз, який обчислює програма.
Розглянемо приклад програми, яка обчислює добуток матриць , де
:
:C A B= ×
( ) ( ) (
1
, , *
n
r
c i j a i r b r j
=
= ∑ ),
( ): 1;for i n=
( ): 1;for j n=
( ): 1;for l n=
( ) ( ) ( ) ( ), : , , * ,c i j c i j a i l b l j= +
Рис. 4. Приклад програми множення матриць
МВА на даному прикладі не вдається отримати інших інваріантів, окрім умов виходу з циклів.
Скористаємося аналітичним методом для доведення інваріантів. Методом математичної індукції доведемо, що
в рядку 4, гнізді циклів, виконується інваріант . ( ) ( ) (
1
, , *
l
r
c i j a i r b r j
=
= ∑ ),
Для твердження індукції виконується 1l = ( ) ( ) ( ), ,1 1c i j a i b j= ⋅ , .
Для твердження індукції виконується 2l = ( ) ( ) ( ) ( ) ( ), ,1 1, , 2 2c i j a i b j a i b j= ⋅ + ⋅ , .
Нехай твердження виконується на кроці l k= : . Розглянемо співвідношення
на кроці : .
( ) ( ) (
1
, , *
k
r
c i j a i r b r j
=
= ∑ ),
,1l k= + ( ) ( ) ( ) ( ) ( ) ( ) ( )
1
1 1
, , , , 1 1, ,
k k
r r
c i j a i r b r j a i k b k j a i r b r j
+
= =
= ⋅ + + ⋅ + = ⋅∑ ∑
232
Формальні методи програмування
Таким чином, на всіх кроках в рядку 4 виконується . Отже, після
закінчення виконання циклу за умовою його закінчення
1..l = n ),( ) ( ) (
1
, , *
l
r
c i j a i r b r j
=
= ∑
l n= і справджується , що і
доводить правильність програми.
( ) ( ) (
1
, , *
n
r
c i j a i r b r j
=
= ∑ ),
Одна з особливостей МВА – це можливість при генерації інваріантів ураховувати більш складні
інваріанти, виведені експертом, наприклад, методом математичної індукції. У такому випадку ці інваріанти
додаються до вхідного базису співвідношень . 0aN
Висновки
У даній роботі описується реалізація алгоритму МВА [1]. Представлений результат виконання
генерації інваріантів програмою, яка реалізує метод верхньої апроксимації для U-Y програм над вільною
алгеброю.
Отримана множина базисів інваріантів може слугувати вхідними параметрами для «прувера», який
перевіряє правильність програми. Оскільки в вершині виконується основна операція сумування 3a
1: 1sum sum x= + , то інваріант ^x z y= вказує на те, що сума рахується правильно. У вершині виконується
операцію ділення на
4a
x і справджуються умови ^x z y= і z m= , тобто ділення правильне щодо постановки
задачі. Інваріанти в вершині надають змогу перевірити умови виходу з програми. 5a
Змінюючи три операції: порівняння, перетину базисів і ефект , які використовуються в методі,
відповідно до алгебри даних U-Y програми, можна отримати більш складні інваріанти. В наступних працях
планується розширити алгебру до алгебри лінійних многочленів і дослідити паралелізацію ітераційних
методів [7].
ef
1. Hoare T. The Verifying Compiler: A Grand Challenge for Computing Research // Journal of the ACM.– 2003.– N. 50(1). – P. 63–69.
2. Kovacs L., Voronkov A. Finding loop invariants for programs over arrays using a theorem prover. Proceedings of the 12th International
Conference on Fundamental Approaches to Software Engineering of Lecture Notes in Computer Science, Springer.– 2009. – Vol. 5503.–
P. 470.
3. Кривий С.Л. Проблеми розробки програмного забезпечення. Формалізація, модель, алгоритми, програма, верифікація.– К., 2010.
4. Maksymets O.M. Application of minimization algorithm for finite acyclic automata in finding condition’s basis for program invariant search //
Proceedings of International Conference on Theoretical and Applied Aspects of Cybernetics. Informatics and Computer Science Section.–
2011.– P. 35–37.
5. Годлевский А.Б., Капитонова Ю.В., Кривой С.Л., Летичевский А.А. Итеративные методы анализа программ // Кибернетика.– 1989.–
№ 2.– С. 9–19.
6. Годлевский А.Б., Кривой С.Л. Трансформационный синтез еффективных алгоритмов с учетом дополнительной информации //
Кибернетика.– 1989.– № 2.– С. 9–19.
7. Кривой С.Л., Ракша С.Г. Поиск инвариантных линейных зависимостей в программах // Кибернетика.– 1984.– № 6.– С. 23–28.
233
Вступ
Визначення
Початкове наближення
Етап стабілізації розв’язку
Індуктивне доведення інваріантів
Висновки
|