Верификация программ: состояние, проблемы, результаты. I
Представлено аналiтичний огляд сучасних методiв верифiкацiї програмного забезпечення послiдовних, функцiональних, паралельних та розподiлених систем. Основну увагу придiлено методам верифiкацiї на основi властивостей абстрактних iнтерпретацiй, транзицiйних систем, мереж Петрi....
Gespeichert in:
| Datum: | 2013 |
|---|---|
| Hauptverfasser: | , |
| Format: | Artikel |
| Sprache: | Russian |
| Veröffentlicht: |
Інститут кібернетики ім. В.М. Глушкова НАН України
2013
|
| Schriftenreihe: | Кибернетика и системный анализ |
| Schlagworte: | |
| Online Zugang: | https://nasplib.isofts.kiev.ua/handle/123456789/86285 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Zitieren: | Верификация программ: состояние, проблемы, результаты. I / С.Л. Крывый, А.Н. Максимец // Кибернетика и системный анализ. — 2013. — Т. 49, № 6. — С. 3-14. — Бібліогр.: 20 назв. — рос. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| id |
nasplib_isofts_kiev_ua-123456789-86285 |
|---|---|
| record_format |
dspace |
| spelling |
nasplib_isofts_kiev_ua-123456789-862852025-02-09T14:24:05Z Верификация программ: состояние, проблемы, результаты. I Верифікація програм: стан, проблеми, результати Program verification: State of the art, problems, results Крывый, С.Л. Максимец, А.Н. Кибернетика Представлено аналiтичний огляд сучасних методiв верифiкацiї програмного забезпечення послiдовних, функцiональних, паралельних та розподiлених систем. Основну увагу придiлено методам верифiкацiї на основi властивостей абстрактних iнтерпретацiй, транзицiйних систем, мереж Петрi. An analytical survey of the modern verification methods for sequential functional, reactive, and distributed systems is presented. The main attention is given to the methods that are based on the properties of abstract interpretation, transition systems, and Petri nets. 2013 Article Верификация программ: состояние, проблемы, результаты. I / С.Л. Крывый, А.Н. Максимец // Кибернетика и системный анализ. — 2013. — Т. 49, № 6. — С. 3-14. — Бібліогр.: 20 назв. — рос. 0023-1274 https://nasplib.isofts.kiev.ua/handle/123456789/86285 51.681.3 ru Кибернетика и системный анализ application/pdf Інститут кібернетики ім. В.М. Глушкова НАН України |
| institution |
Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| collection |
DSpace DC |
| language |
Russian |
| topic |
Кибернетика Кибернетика |
| spellingShingle |
Кибернетика Кибернетика Крывый, С.Л. Максимец, А.Н. Верификация программ: состояние, проблемы, результаты. I Кибернетика и системный анализ |
| description |
Представлено аналiтичний огляд сучасних методiв верифiкацiї програмного забезпечення послiдовних, функцiональних, паралельних та розподiлених систем. Основну увагу придiлено методам верифiкацiї на основi властивостей абстрактних iнтерпретацiй, транзицiйних систем, мереж Петрi. |
| format |
Article |
| author |
Крывый, С.Л. Максимец, А.Н. |
| author_facet |
Крывый, С.Л. Максимец, А.Н. |
| author_sort |
Крывый, С.Л. |
| title |
Верификация программ: состояние, проблемы, результаты. I |
| title_short |
Верификация программ: состояние, проблемы, результаты. I |
| title_full |
Верификация программ: состояние, проблемы, результаты. I |
| title_fullStr |
Верификация программ: состояние, проблемы, результаты. I |
| title_full_unstemmed |
Верификация программ: состояние, проблемы, результаты. I |
| title_sort |
верификация программ: состояние, проблемы, результаты. i |
| publisher |
Інститут кібернетики ім. В.М. Глушкова НАН України |
| publishDate |
2013 |
| topic_facet |
Кибернетика |
| url |
https://nasplib.isofts.kiev.ua/handle/123456789/86285 |
| citation_txt |
Верификация программ: состояние, проблемы, результаты. I / С.Л. Крывый, А.Н. Максимец // Кибернетика и системный анализ. — 2013. — Т. 49, № 6. — С. 3-14. — Бібліогр.: 20 назв. — рос. |
| series |
Кибернетика и системный анализ |
| work_keys_str_mv |
AT kryvyjsl verifikaciâprogrammsostoânieproblemyrezulʹtatyi AT maksimecan verifikaciâprogrammsostoânieproblemyrezulʹtatyi AT kryvyjsl verifíkacíâprogramstanproblemirezulʹtati AT maksimecan verifíkacíâprogramstanproblemirezulʹtati AT kryvyjsl programverificationstateoftheartproblemsresults AT maksimecan programverificationstateoftheartproblemsresults |
| first_indexed |
2025-11-26T20:11:47Z |
| last_indexed |
2025-11-26T20:11:47Z |
| _version_ |
1849885104063643648 |
| fulltext |
Ñ.Ë. ÊÐÛÂÛÉ, À.Í. ÌÀÊÑÈÌÅÖ
ÓÄÊ 51.681.3 ÂÅÐÈÔÈÊÀÖÈß ÏÐÎÃÐÀÌÌ: ÑÎÑÒÎßÍÈÅ,
ÏÐÎÁËÅÌÛ, ÐÅÇÓËÜÒÀÒÛ. I
Êëþ÷åâûå ñëîâà: âåðèôèêàöèÿ, àáñòðàêòíûå èíòåðïðåòàöèè, òðàíçèöèîí-
íûå ñèñòåìû, ñåòè Ïåòðè, âåðèôèêàöèÿ íà ìîäåëÿõ.
Äàííàÿ ðàáîòà ÿâëÿåòñÿ ïðîäîëæåíèåì îáçîðîâ, íà÷àòûõ â [1, 2], ãäå ðàññìàò-
ðèâàëèñü ìåòîäû âåðèôèêàöèè ïðîãðàìì ïðîöåäóðíîãî òèïà c îðèåíòàöèåé íà
èñïîëüçîâàíèå ïðîãðàììíûõ äèíàìè÷åñêèõ ëîãèê (â ÷àñòíîñòè, ëîãèêè Õîàðà).
 ïåðâîé ÷àñòè íàñòîÿùåé ïóáëèêàöèè îïèñûâàåòñÿ ìåòîä àáñòðàêòíûõ èíòåð-
ïðåòàöèé àíàëèçà ñåìàíòè÷åñêèõ ñâîéñòâ ïîñëåäîâàòåëüíûõ ïðîãðàìì, âî âòî-
ðîé — ìåòîäû è èõ ïðèëîæåíèÿ, îðèåíòèðîâàííûå íà âåðèôèêàöèþ ðåàêòèâ-
íûõ è ðàñïðåäåëåííûõ ñèñòåì. Âûáîð ýòèõ íàïðàâëåíèé îáúÿñíÿåòñÿ òåì, ÷òî
â íàñòîÿùåå âðåìÿ â îáëàñòè âåðèôèêàöèè àêòèâíî ðàçâèâàþòñÿ è ïðèìåíÿþò-
ñÿ íà ïðàêòèêå èìåííî ýòè íàïðàâëåíèÿ.
Ñåìàíòè÷åñêèé àíàëèç ïðîãðàìì çàêëþ÷àåòñÿ â ðàçðàáîòêå àíàëèçàòîðà ïðî-
ãðàìì. Ïîä àíàëèçàòîðîì ïîíèìàåòñÿ ïðîãðàììà, êîòîðàÿ, ïîëó÷àÿ íà ñâîé âõîä
â êà÷åñòâå âõîäíûõ äàííûõ ïðîãðàììó (âîçìîæíî, àííîòèðîâàííóþ), âûäàåò íà
âûõîäå îòâåòû íà âîïðîñû î åå ñâîéñòâàõ, êîòîðûå èìåþò ìåñòî íà âñåì ïðîòÿ-
æåíèè âûïîëíåíèÿ ýòîé ïðîãðàììû. Èç-çà àëãîðèòìè÷åñêîé íåðàçðåøèìîñòè
ïðîáëåìû âåðèôèêàöèè èëè èç-çà îãðîìíîé ñëîæíîñòè ïðîöåññà âåðèôèêàöèè
ýòè îòâåòû íåèçáåæíî áóäóò ÷àñòè÷íûìè, íî è îíè âñåãäà î÷åíü âàæíû. Îäèí èç
ïîäõîäîâ ê ïðîáëåìå âåðèôèêàöèè — ìåòîä àáñòðàêòíûõ èíòåðïðåòàöèé,
îñíîâíûå ïîëîæåíèÿ êîòîðîãî îïèñàíû â äàííîé ðàáîòå.
1. ÀÁÑÒÐÀÊÒÍÛÅ ÈÍÒÅÐÏÐÅÒÀÖÈÈ
Àáñòðàêòíûå èíòåðïðåòàöèè âïåðâûå áûëè ââåäåíû Ì. Ñèíòöîâûì [3] äëÿ àâ-
òîìàòèçàöèè ïðîöåññà àíàëèçà ïðîãðàìì, çàòåì áûëè ðàçâèòû â ðàáîòàõ [4–6]
è [7, 8]. Ãëàâíàÿ èäåÿ àáñòðàêòíûõ èíòåðïðåòàöèé ñîñòîèò â íàõîæäåíèè òàêèõ
îãðàíè÷åíèé àáñòðàêòíîãî õàðàêòåðà íà ñåìàíòè÷åñêèå ñòðóêòóðû ïðîãðàìì, ÷òî-
áû ìîæíî áûëî ïðèìåíÿòü ñðåäñòâà àâòîìàòè÷åñêîãî äîêàçàòåëüñòâà óòâåðæäåíèé
â ëîãè÷åñêèõ ÿçûêàõ è ñðåäñòâà êîìïüþòåðíîé àëãåáðû.  ýòîì ñìûñëå ìåòîä
àáñòðàêòíûõ èíòåðïðåòàöèé îòíîñÿò ê òàêèì ìåòîäàì, êàê àíàëèç ïîòîêîâ äàí-
íûõ â ïðîãðàììàõ, ñìåøàííûå âû÷èñëåíèÿ, òðàíñôîðìàöèè ïðîãðàìì â ïðîöåñ-
ñå ãåíåðàöèè êîäà [9].
Ñâîéñòâà è èõ àáñòðàêöèè. Ïóñòü Q — íåêîòîðîå ìíîæåñòâî îáúåêòîâ (íà-
ïðèìåð, ñîñòîÿíèé ïðîãðàììû, âûïîëíÿåìûõ òðàññ è ò.ï.), P — ìíîæåñòâî îáú-
åêòîâ, èìåþùèõ îïðåäåëåííîå ñâîéñòâî, ò.å. P B Q� ( ), ãäå B Q( ) — áóëåàí ìíî-
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2013, ¹ 6 3
© Ñ.Ë. Êðûâûé, À.Í. Ìàêñèìåö, 2013
æåñòâà Q. Ïîñêîëüêó ñâîéñòâà îïðåäåëÿþò ïîäìíîæåñòâà èç B Q( ), òî îíè îáðà-
çóþò ïîëíóþ áóëåâóþ ðåøåòêó G B Q Q� � �( ( ), , , , , , ' )� � îòíîñèòåëüíî
òåîðåòèêî-ìíîæåñòâåííûõ îïåðàöèé, ýëåìåíòû êîòîðîé ÷àñòè÷íî óïîðÿäî÷åíû
îòíîøåíèåì âêëþ÷åíèÿ (�) äëÿ ìíîæåñòâ.
Íàïîìíèì, ÷òî ïîëíîé ðåøåòêîé íàçûâàåòñÿ àëãåáðà R � �( ,{ , , , , })� � � �� ,
ãäå � — ÷àñòè÷íî óïîðÿäî÷åííîå ìíîæåñòâî îòíîøåíèåì ÷àñòè÷íîãî ïîðÿäêà (� ),
à îïåðàöèè íàçûâàþòñÿ îïåðàöèÿìè âçÿòèÿ âåðõíåé ãðàíè (� ) è íèæíåé ãðàíè
(�) íåêîòîðîé ñîâîêóïíîñòè ýëåìåíòîâ èç � [10]. Ýëåìåíòû � è� ñîîòâåòñòâó-
þò íóëþ è åäèíèöå ïîëíîé ðåøåòêè. Ýòî îçíà÷àåò, ÷òî � � � �a a�( )�
� ( )a �� è äëÿ ëþáîãî ïîäìíîæåñòâà H � � ñóùåñòâóåò åäèíñòâåííûé ýëå-
ìåíò a �� òàêîé, ÷òî a b
b H
�
�
� (äëÿ îïåðàöèè � òàêîé ýëåìåíò îïðåäåëÿåòñÿ
äâîéñòâåííûì îáðàçîì).
Äàëåå áóäåì ïîëàãàòü, ÷òî èìååòñÿ ïîëíàÿ ðåøåòêà ( ,{ , , , , })� � � �� � ,
â òåðìèíàõ êîòîðîé áóäóò îïðåäåëÿòüñÿ âñå íåîáõîäèìûå ïîíÿòèÿ.
Íåôîðìàëüíî ïîä àáñòðàêöèåé ïîíèìàåòñÿ âûâîä èëè (ìåõàíè÷åñêîå) âû-
÷èñëåíèå íà îáúåêòàõ, òàêèõ ÷òî òîëüêî íåêîòîðûå ñâîéñòâà ýòèõ îáúåêòîâ ìîãóò
èñïîëüçîâàòüñÿ. Ïóñòü A — ìíîæåñòâî êîíêðåòíûõ ñâîéñòâ, A � � — ìíîæåñò-
âî àáñòðàêòíûõ ñâîéñòâ, êîòîðûå ìîãóò èñïîëüçîâàòüñÿ â âûâîäàõ èëè âû÷èñëå-
íèÿõ. Òàêèì îáðàçîì, àáñòðàêöèÿ ñîñòîèò â àïïðîêñèìèðîâàíèè êîíêðåòíûõ
ñâîéñòâ ñ ïîìîùüþ èõ àáñòðàêòíûõ ñâîéñòâ.
Ñóùåñòâóåò äâà âîçìîæíûõ íàïðàâëåíèÿ àïïðîêñèìàöèè: àïïðîêñèìàöèÿ
ñâåðõó è àïïðîêñèìàöèÿ ñíèçó. Àïïðîêñèìàöèÿ ñâåðõó ìíîæåñòâà ñâoéñòâ P A�
ñ ïîìîùüþ ìíîæåñòâà àáñòðàêòíûõ ñâîéñòâ P �� âëå÷åò P P� .  àïïðîêñèìà-
öèè ñíèçó ìíîæåñòâà ñâîéñòâ P A� ñ ïîìîùüþ ìíîæåñòâà àáñòðàêòíûõ ñâîéñòâ
P �� ïîëó÷àåì P P� . Î÷åâèäíî, ÷òî àïïðîêñèìàöèè ñâåðõó è ñíèçó äâîéñòâåí-
íûå îäíà äðóãîé. Ýòî çíà÷èò, ÷òî àïïðîêñèìàöèÿ ñâåðõó/ñíèçó äëÿ P ÿâëÿåòñÿ
àïïðîêñèìàöèåé ñíèçó/ñâåðõó äëÿ P, à îòñþäà âûòåêàåò, ÷òî ìîæíî ðàññìàòðè-
âàòü òîëüêî îäíó èç íèõ, íàïðèìåð àïïðîêñèìàöèþ ñâåðõó.
Äàëåå, ýëåìåíò �, ÿâëÿÿñü ýëåìåíòîì � , îáîçíà÷àåò ñëó÷àé, êîãäà íåêîòî-
ðûå ñâîéñòâà íå èìåþò àáñòðàêöèè (íàïðèìåð, êîãäà � � �). Ñëåäîâàòåëüíî, ëþ-
áîå êîíêðåòíîå ñâîéñòâî P �� âñåãäà ìîæåò áûòü àïïðîêñèìèðîâàíî ñâåðõó
(ñ ïîìîùüþ�, ò.å. Q èñòèííî èëè íåò). Äëÿ áîëåå òî÷íîé àïïðîêñèìàöèè èñïîëü-
çóåòñÿ íàèìåíüøàÿ àáñòðàêöèÿ P �� òàêàÿ, ÷òî P P� è íå ñóùåñòâóåò
�
P P P� : � .
Èìååòñÿ íåñêîëüêî ðàçëè÷íûõ àïïðîêñèìàöèé äëÿ ðàçëè÷íûõ ñâîéñòâ. Âî
èçáåæàíèå ðàññìîòðåíèÿ âñåõ âîçìîæíûõ àïïðîêñèìàöèé íåîáõîäèìî, ÷òîáû
ëþáîå êîíêðåòíîå ñâîéñòâî P A� èìåëî íàèëó÷øóþ àáñòðàêöèþ P �� , ò.å. åñëè
P P� , òî �
�P � äîëæíî âûïîëíÿòüñÿ P P P P� �
�
. Èç îïðåäåëåíèÿ îïåðà-
öèè � ñëåäóåò, ÷òî òðåáîâàíèå íàèëó÷øåé àáñòðàêöèè ýêâèâàëåíòíî ïåðåñå÷å-
íèþ àáñòðàêòíûõ ñâîéñòâ P P P P�
�
�� �{ : }� � . Äðóãàÿ òî÷êà çðåíèÿ
îïèñàíà â ðàáîòàõ [11, 12].
Ïðîèëëþñòðèðóåì ñêàçàííîå ïðèìåðîì èç ðàáîòû [9].
Ïðèìåð 1. Ðàññìîòðèì àðèôìåòè÷åñêîå âûðàæåíèå ( )8 5� . Ñëåäóåò îïðåäå-
ëèòü, áóäåò ðåçóëüòàò ÷åòíûì èëè íå÷åòíûì ÷èñëîì. Ýòî ìîæíî âûÿñíèòü ñ ïî-
ìîùüþ êîíêðåòíîãî âû÷èñëåíèÿ ÷èñëà 13, êîòîðîå íå÷åòíî, à ìîæíî òàêæå
àáñòðàãèðîâàòüñÿ îò êîíêðåòíûõ çíà÷åíèé 8 è 5 ïóòåì ââåäåíèÿ ñâîéñòâà ÷åòíîñ-
òè: even (÷åòíîå) è odd (íå÷åòíîå), è äàëåå ðàññìàòðèâàòü çàäà÷ó ñëîæåíèÿ
even odd� . Ýòî âû÷èñëåíèå àáñòðàêöèè äàåò ðåçóëüòàò odd.
4 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2013, ¹ 6
ßñíî, ÷òî ìîæíî áûëî áû ðàñ-
ñìàòðèâàòü äðóãèå àáñòðàêöèè, ïîëó-
÷àÿ ðàçëè÷íóþ èíôîðìàöèþ î âûðà-
æåíèÿõ, íàïðèìåð, êàêîé áóäåò çíàê â
ðåçóëüòàòå âû÷èñëåíèÿ âûðàæåíèÿ?
Òîãäà ðàññìàòðèâàëàñü áû àáñòðàêöèÿ
positive positive positive� � .
Ãëàâíûì çäåñü ÿâëÿåòñÿ òî, ÷òî ìû èìååì àáñòðàêöèè ïîíÿòèÿ çíà÷åíèÿ (5)
è îïåðàöèè íà íèõ ( �). Îáîáùàÿ ýòè àáñòðàêöèè, çàïèøåì àáñòðàêòíûå îïåðàöèè
ñëîæåíèÿ è óìíîæåíèÿ íà ìíîæåñòâå { , }even odd ñëåäóþùèì îáðàçîì (ðèñ. 1).
Îáîçíà÷èì ýòó àáñòðàêöèþ ÏÍ è ðàññìîòðèì óñëîâíîå âûðàæåíèå if è then
3 else 4. Åñëè çíà÷åíèå u íåèçâåñòíî, òî è ðåçóëüòàò ýòîãî âûðàæåíèÿ íåèçâåñòåí.
Äëÿ ïîëó÷åíèÿ àáñòðàêöèè òàêèõ âûðàæåíèé è ââîäèòñÿ íîâîå àáñòðàêòíîå çíà-
÷åíèå� �ÏÍ äëÿ îáîçíà÷åíèÿ îòñóòñòâèÿ çíàíèÿ î çíà÷åíèè. Îíî óäîâëåòâîðÿåò
óñëîâèÿì even �� è odd ��. Îòñþäà ñëåäóåò, ÷òî åñëè s t� , ò.å. s ìåíüøå èëè
ðàâíî t, òî s áîëåå èíôîðìàòèâíî, ÷åì t.
Ïóñòü s t, — äâà àáñòðàêòíûõ çíà÷åíèÿ. Òîãäà s t� — íàèìåíüøàÿ âåðõíÿÿ
ãðàíü ýëåìåíòîâ s è t â íàøåé ðåøåòêå, îçíà÷àþùàÿ íàèìåíüøèé ýëåìåíò, êîòî-
ðûé áîëüøå èëè ðàâåí s è t. Íàïðèìåð, äëÿ ïðèâåäåííîãî âûøå óñëîâíîãî âûðà-
æåíèÿ even odd� �� áóäåò àáñòðàêòíûì çíà÷åíèåì ýòîãî óñëîâíîãî âûðàæåíèÿ.
Ðàññìîòðèì òåïåðü òàêèå äâå ôóíêöèè:
f x x( ) � �1 è g x x x g x( ) ( )�
�if then else5 8 5 .
Äëÿ ôóíêöèè f x( ) èìååì àáñòðàêòíóþ èíòåðïðåòàöèþ f X odda X( ) � � , à äëÿ
ôóíêöèè g x( ) ïîñòðîåíèå àáñòðàêöèè íåñêîëüêî ñëîæíåå, òàê êàê åå àáñòðàêöèÿ
g a äîëæíà îòâåòèòü íà âîïðîñ, èìååò ëè ðåøåíèå ðåêóðñèâíîå îïðåäåëåíèå:
g X even g odd Xa X( ) ( ( ))� � �� .
Îòâåò áóäåò yes, åñëè ââåñòè íîâîå çíà÷åíèå � äëÿ îáîçíà-
÷åíèÿ «íåò çíà÷åíèÿ» èëè «íå îïðåäåëåíî». Òàêèì îáðàçîì,
� �ÏÍ è � � s äëÿ âñåõ àáñòðàêòíûõ çíà÷åíèé s�ÏÍ.  ðå-
çóëüòàòå ïîëó÷àåì ðåøåòêó G even odd� �({ , , , }� , { , ,� � �,
� �, }). Ïðè ýòîì äèàãðàììà Õàññå èìååò ñëåäóþùèé âèä
(ðèñ. 2).
Çàïèøåì àáñòðàêòíûå îïåðàöèè ñëîæåíèÿ è óìíîæåíèÿ (ðèñ. 3).
Èç-çà óñëîâíûõ âûðàæåíèé è ðåêóðñèâíûõ îïðåäåëåíèé ôóíêöèé ïðèõîäèò-
ñÿ ââîäèòü äâà àáñòðàêòíûõ çíà÷åíèÿ (� è �) äëÿ îáîçíà÷åíèÿ «íå îïðåäåëåíî»
è «íåò èíôîðìàöèè».
Ïîäâîäÿ ïåðâûå èòîãè, îòìåòèì, ÷òî ïðîãðàììû ìîãóò áûòü èíòåðïðåòèðî-
âàíû êîíêðåòíî èëè àáñòðàêòíî. Èçó÷àÿ ñâîéñòâà àáñòðàêòíîé èíòåðïðåòàöèè
ïðîãðàììû, ìû èçó÷àåì ñâîéñòâà ñàìîé ïðîãðàììû.
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2013, ¹ 6 5
Îïåðàöèÿ � even odd
even odd
odd even
even
odd
Îïåðàöèÿ � even odd
even even
even odd
even
odd
Ðèñ. 1
even odd
�
�
Ðèñ. 2
Îïåðàöèÿ � even odd�
even odd
�
even
�
� � � �
� �
odd evenodd � �
� � �� �
Îïåðàöèÿ � even odd�
even even
�
even
�
� � � �
�
even oddodd � �
� � ��
even
even
Ðèñ. 3
Àáñòðàêòíûå è êîíêðåòíûå îòîáðàæåíèÿ. Óòî÷íèì ââåäåííûå â ïðèìå-
ðå 1 ïîíÿòèÿ àáñòðàêöèè è êîíêðåòèçàöèè ôóíêöèè. Îáà òèïà ýòèõ îòîáðàæåíèé
ìîãóò áûòü ôîðìàëèçîâàíû ñ ïîìîùüþ ôóíêöèè àáñòðàêöèè � è ôóíêöèè êîí-
êðåòèçàöèè �. Ïóñòü N � { , , , }0 1 2 � — ìíîæåñòâî íàòóðàëüíûõ ÷èñåë, B N( ) —
åãî áóëåàí, ÷àñòè÷íî óïîðÿäî÷åííûé îòíîøåíèåì âêëþ÷åíèÿ (�).
Ôóíêöèÿ êîíêðåòèçàöèè � : ( )ÏÍ � B N îòîáðàæàåò àáñòðàêòíîå çíà÷åíèå s
â ìíîæåñòâî � ( )s êîíêðåòíûõ ÷èñåë, ïðåäñòàâëåííûõ çíà÷åíèåì s. Ôóíêöèÿ
àáñòðàêöèè � : ( )B N � ÏÍ, íàîáîðîò, îòîáðàæàåò ìíîæåñòâî ÷èñåë V â (íàè-
ìåíüøåå) àáñòðàêòíîå çíà÷åíèå s V( ) , ïðåäñòàâëÿþùåå âñå ÷èñëà ýòîãî
ìíîæåñòâà.
Îò ôóíêöèé êîíêðåòèçàöèè è àáñòðàêöèè òðåáóåòñÿ âûïîëíåíèå òàêèõ
óñëîâèé:
1) îáå ôóíêöèè ìîíîòîííû;
2) � � �s V s s� �( ( )) ;
3) � � �V B A V V( ) ( ( ))� � .
Óñëîâèå ìîíîòîííîñòè îçíà÷àåò, ÷òî áîëüøàÿ àáñòðàêöèÿ ïðåäñòàâëÿåò
áîëüøåå ìíîæåñòâî êîíêðåòíûõ çíà÷åíèé. Èç óñëîâèå 2) ñëåäóåò, ÷òî êàæäîå
àáñòðàêòíîå çíà÷åíèå ïðåäñòàâëÿåò ñàìî ñåáÿ è íå äîïóñêàåò ïóòàíèöû ñðåäè
àáñòðàêòíûõ çíà÷åíèé. Óñëîâèå 3) îçíà÷àåò, ÷òî àáñòðàãèðîâàíèå è êîíêðåòèçè-
ðîâàíèå ìíîæåñòâà V êîíêðåòíûõ çíà÷åíèé äàåò ìíîæåñòâî, ñîäåðæàùåå
ìíîæåñòâî V .
Âûïîëíåíèå âñåõ ýòèõ óñëîâèé âìåñòå ãàðàíòèðóåò, ÷òî àáñòðàêöèÿ ìíîæåñò-
âà V ñîõðàíÿåò ïðåäñòàâëåíèå âñåõ ýëåìåíòîâ èç V .
Ïðèìåð 2. Â ðåøåòêå ÏÍ èç ïðèìåðà 1 ôóíêöèÿ êîíêðåòèçàöèè èìååò âèä:
� ( )� � � — ïóñòîå ìíîæåñòâî;
� ( ) { , , , }even � 0 2 4 � — ìíîæåñòâî ÷åòíûõ ÷èñåë;
� ( ) { , , , }odd � 1 2 5 � — ìíîæåñòâî íå÷åòíûõ ÷èñåë;
� ( )� � N — ìíîæåñòâî íàòóðàëüíûõ ÷èñåë,
à ôóíêöèÿ àáñòðàêöèè áóäåò òàêîé:
�( )� � � ; �({ , , , })0 2 4 � � even; �({ , , , })1 3 5 � � odd ; �( )N �� .
Èñïîëüçóÿ ôóíêöèè � è � , ìîæíî îïðåäåëèòü ïîíÿòèå àáñòðàêòíîé ôóíêöèè
f Aa : � � . Íàïðèìåð, ïóñòü � � ÏÍ è f N N: � — êîíêðåòíàÿ ôóíêöèÿ,
n N� è �({ })n — åãî àáñòðàêòíîå çíà÷åíèå. Òîãäà îò ôóíêöèè f a òðåáóåòñÿ,
÷òîáû êîíêðåòíîå çíà÷åíèå f n( ) ýòîé ôóíêöèåé ïðåäñòàâëÿëîñü êàê àáñòðàêò-
íîå çíà÷åíèå f na ( {( )})� , ò.å. � � �n N f n f na( ( ) ( ( ({ }))))� � .
Àáñòðàêòíàÿ îïåðàöèîííàÿ ñåìàíòèêà ïðîãðàìì. Íàïîìíèì îñíîâíûå
ïîíÿòèÿ �-èñ÷èñëåíèÿ è ñäåëàåì íåêîòîðûå çàìå÷àíèÿ îá àáñòðàêòíîì ñèíòàêñè-
ñå ïðîãðàììû. �-èñ÷èñëåíèå ïðåäñòàâëÿåò ñîáîé èñ÷èñëåíèå íåèìåíîâàííûõ
ôóíêöèé, îíî äàåò ñèíòàêñè÷åñêîå îïèñàíèå ôóíêöèé è ñèíòàêñè÷åñêèå ïðàâèëà
èõ ïðåîáðàçîâàíèÿ. Òàê, â �-âûðàæåíèè �x f x.[ ( )], ñèìâîë � ÷èòàåòñÿ êàê «ôóíê-
öèÿ îò», à òî÷êà — êàê «êîòîðàÿ âîçâðàùàåò». Íàïðèìåð, �x x. [*( , )]2 îçíà÷àåò
ôóíêöèþ, êîòîðàÿ âîçâðàùàåò 2x . Ïðè ýòîì ñèìâîë x íàçûâàåòñÿ ñâÿçàííîé ïåðå-
ìåííîé �-àáñòðàêöèè, à âûðàæåíèå ñïðàâà îò òî÷êè — òåëîì �-àáñòðàêöèè. Òåëî
�-àáñòðàêöèè îïèñûâàåò òî, ÷òî íóæíî ñäåëàòü ñ ïàðàìåòðàìè, ïîñòóïèâøèìè íà
âõîä ôóíêöèè. Òåëî �-àáñòðàêöèè ìîæåò ñîäåðæàòü è äðóãóþ �-àáñòðàêöèþ, íà-
ïðèìåð � �x y x y.[ .[*( ( , ), )]]� 2 . Ýòî îçíà÷àåò, ÷òî ôóíêöèÿ îò x âîçâðàùàåò ôóíê-
öèþ îò y, êîòîðàÿ âîçâðàùàåò 2( )x y� è ÿâëÿåòñÿ �-âûðàæåíèåì.
6 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2013, ¹ 6
Âû÷èñëåíèå �-âûðàæåíèé îñóùåñòâëÿåòñÿ ñ ïîìîùüþ ïðàâèë âûâîäà �-èñ÷èñ-
ëåíèÿ. Ïðîñòåéøèé òèï �-âûðàæåíèé — ýòî êîíñòàíòû, êîòîðûå ñ÷èòàþòñÿ ñàìîîï-
ðåäåëåííûìè, ò.å. èõ íåëüçÿ ïðåîáðàçîâàòü ê áîëåå ïðîñòûì �-âûðàæåíèÿì. Âû÷èñ-
ëåíèå êîíñòàíòû 3 äàåò òó æå êîíñòàíòó 3. Ïðåîáðàçîâàíèå �-âûðàæåíèÿ � ( , )1 3
â êîíñòàíòó 4 âûïîëíÿåòñÿ ñ ïîìîùüþ âñòðîåííûõ �-ïðàâèë, íàïðèìåð
* ( ( , ))( ( , )) * ( ( , ), ) * ( , )� � � �� � � �� � ��1 2 4 1 1 2 3 3 3 9
� � �
.
Âòîðàÿ ãðóïïà ïðàâèë íàçûâàåòñÿ �-ïðàâèëàìè. Ðàññìîòðèì ïðèìåð �-âûðà-
æåíèÿ �x x x.[ ( , )]� 2 . Çäåñü ñèòóàöèÿ àíàëîãè÷íà òîé, êîòîðàÿ âîçíèêàåò ïðè âûçî-
âå ïðîöåäóðû èëè ôóíêöèè ñ ôàêòè÷åñêèì ïàðàìåòðîì, çàìåíÿþùèì åå ôîð-
ìàëüíûé ïàðàìåòð. Ñëåäîâàòåëüíî, ñíà÷àëà íóæíî çàìåíèòü ôîðìàëüíûé ïàðà-
ìåòð x ôàêòè÷åñêèì ïàðàìåòðîì 2.  äàííîì �-âûðàæåíèè ïîëó÷àåì:
�
� �
x x x.[* ( , )] * ( , )2 2 2 4� �� � �� .
Ðåäóêöèÿ �-àáñòðàêöèè, ïðèìåíåííàÿ ê íåêîòîðîìó àðãóìåíòó, ìîæåò äàòü
äðóãóþ �-àáñòðàêöèþ, è â ýòîì ñëó÷àå ïðîöåññ ìîæåò áûòü ïðîäîëæåí. Íàïðè-
ìåð, âû÷èñëåíèå �-âûðàæåíèÿ � �x y x y.[ .[ ( , )] ]� 7 8 ìîæíî íà÷àòü ñ ïîäñòàíîâêè
÷èñëà 7 âìåñòî x â òåëî âíåøíåé àáñòðàêöèè, ò.å. � y x y.[ ( , )]� .  ðåçóëüòàòå ïî-
ëó÷àåì � y y.[ ( , )]� 7 8, è çàêàí÷èâàÿ ïðèìåíåíèå, ïîëó÷àåì âûðàæåíèå � ( , )7 8 , ÷òî
äàåò îêîí÷àòåëüíîå çíà÷åíèå 15.
Ïðåäñòàâëåíèå ïðîãðàìì. Ïðåäñòàâèì ïðîãðàììó â âèäå ðàçìå÷åííîãî îðãðà-
ôà ñ îäíîé íà÷àëüíîé âåðøèíîé è îäíîé çàêëþ÷èòåëüíîé âåðøèíîé. Äóãè (îðèåí-
òèðîâàííûå ðåáðà) ãðàôà ïîìå÷åíû îïåðàòîðàìè ÿçûêà ïðîãðàììèðîâàíèÿ.
Ãðàôîì ïðîãðàììû íàçûâàåòñÿ ÷åòâåðêà G V a a Ep � ( , , , )*
0 , ãäå V — êîíå÷-
íîå ìíîæåñòâî âåðøèí, E V V� � — êîíå÷íîå ìíîæåñòâî äóã, a V0 � — íà÷àëü-
íàÿ âåðøèíà, a V* � — çàêëþ÷èòåëüíàÿ âåðøèíà, ïðè÷åì a a0 � * . Åñëè
( , )a b E� , òî ñ÷èòàþò, ÷òî äóãà ( , )a b âûõîäèò èç âåðøèíû a è âõîäèò â âåðøèíó b.
Íà÷àëüíàÿ âåðøèíà õàðàêòåðèçóåòñÿ òåì, ÷òî â íåå íå âõîäèò íè îäíà äóãà, à èç
çàêëþ÷èòåëüíîé âåðøèíû íå âûõîäèò íè îäíà äóãà, à âñå äðóãèå âåðøèíû èç V
íàõîäÿòñÿ íà íåêîòîðîì ïóòè èç a0 â a * .
Ïóñòü � — âåêòîð, êîîðäèíàòàìè êîòîðîãî ÿâëÿþòñÿ ïàðû ( , )� i im , ãäå � i —
ïåðåìåííàÿ, à mi — åå çíà÷åíèå, êîòîðîå áåðåòñÿ èç íåêîòîðîãî óíèâåðñàëüíîãî
ìíîæåñòâà U . Ìíîæåñòâî îïåðàòîðîâ Q U( ) äåëèòñÿ íà äâà ïîäìíîæåñòâà:
� ïîäìíîæåñòâî O Us ( ) îïåðàòîðîâ ïðèñâàèâàíèÿ;
� ïîäìíîæåñòâî O Ut ( ) îïåðàòîðîâ ïðîâåðêè óñëîâèé.
Îïåðàòîð ïðèñâàèâàíèÿ � �: ( )� y ïðåäñòàâëÿåò ñîáîé ÷àñòè÷íîå îòîáðà-
æåíèå èç ìíîæåñòâà U â U , à ïðîâåðêà óñëîâèé — ÷àñòè÷íîå îòîáðàæåíèå èç
U â B true false� { , }.
Ïðîãðàììîé íàçûâàåòñÿ òðîéêà � � ( , , )G U L , ãäå G — ãðàô ïðîãðàììû,
U — óíèâåðñàëüíîå ìíîæåñòâî è L E O U: ( )� — ôóíêöèÿ îòìåòîê äóã ãðàôà G.
Âåðøèíû ýòîãî ãðàôà áóäóò òàêæå íàçûâàòüñÿ ñîñòîÿíèÿìè ïðîãðàììû. Ôóíê-
öèÿ L òàêàÿ, ÷òî äëÿ êàæäîé âåðøèíû a V� , îòëè÷íîé îò a * , ëèáî èç a âûõîäèò
åäèíñòâåííàÿ äóãà, îòìå÷åííàÿ íåêîòîðûì îïåðàòîðîì ïðèñâàèâàíèÿ y, ëèáî äâå
äóãè, îòìå÷åííûå óñëîâèÿìè u è u ñîîòâåòñòâåííî.  ðàáîòàõ [1, 2] òàêàÿ ìî-
äåëü ïðîãðàììû íàçâàíà U Y� -ñõåìîé ïðîãðàììû.
Îïåðàöèîííàÿ ñåìàíòèêà. Îïåðàöèîííàÿ ñåìàíòèêà ñèíòàêñè÷åñêè ïðà-
âèëüíîé ïðîãðàììû p ñîïîñòàâëÿåò ïîñëåäîâàòåëüíîñòü äîñòèæèìûõ ñîñòîÿíèé
ïðè âû÷èñëåíèÿõ, îïðåäåëÿåìûõ ýòîé ïðîãðàììîé.
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2013, ¹ 6 7
Ìíîæåñòâî ñîñòîÿíèé S ñîñòîèò èç ïàð ( , )a m , ãäå a V� � { }� — ñîñòîÿíèå
ïðîãðàììû, m U� — ñîñòîÿíèå ïàìÿòè, à � �V — âåðøèíà, íàçûâàåìàÿ ñîñòîÿ-
íèåì îøèáêè. Ñîñòîÿíèÿ a a0 , ,* � õàðàêòåðèçóþòñÿ òàêèìè �-âûðàæåíèÿìè:
� � � � � � ��a ac m c a c m c a c m c
0 0� � � � � �( , ) . ( ), ( , ) . ( ), ( , ) . (*
* ) .
Ïðîãðàììà � ( , , )G U L îïðåäåëÿåò ôóíêöèþ ïåðåõîäîâ
: S S� ñëåäóþùèì
îáðàçîì:
1)
� �(( , )) ( , )m m� ;
2)
(( , )) ( , )* *a m a m� ;
3) åñëè ( , )a m S1 � , ãäå a V1 � èìååò îäíó âûõîäíóþ äóãó ( , )a a E1 2 � , îòìå-
÷åííóþ îïåðàòîðîì ïðèñâàèâàíèÿ y O Us� ( ), òî ïðè m y�dom ( ) èìååì
(( , )) ( , ( ))a m a y m1 2� , èíà÷å
�(( , )) ( , )a m m1 � ;
4) åñëè ( , )a m S1 � , ãäå a V1 � , èìååò äâå âûõîäíûå äóãè: ( , )a a1 2 ,
( , )a a E1 3 � , îòìå÷åííûå u è �u u O Ut, ( ) ñîîòâåòñòâåííî, òî m u�dom ( ) ïðè
�(( , )) ( , )a m m1 � , èíà÷å åñëè u m( ), òî
(( , )) ( , )a m a m1 2� , èíà÷å
(( , )) ( , )a m a m1 3� .
Îòíîøåíèå ïåðåõîäîâ
� �S S , îïðåäåëÿåìîå ïðîãðàììîé , èìååò âèä
�
( , ) . ( ( )a a a a1 2 2 1� .
Íàïîìíèì îïðåäåëåíèå ðåôëåêñèâíîãî è òðàíçèòèâíîãî çàìûêàíèé áèíàð-
íîãî îòíîøåíèÿ. Äëÿ ëþáîãî íàòóðàëüíîãî ÷èñëà n
1 ñòåïåíü áèíàðíîãî îòíî-
øåíèÿ � � �S S îïðåäåëÿåòñÿ ðåêóðñèâíî: � � � �0 1� ��iS
n n, * , ãäå iS — òîæ-
äåñòâåííîå îòíîøåíèå íà S (äèàãîíàëü ìíîæåñòâà S), à * — îïåðàöèÿ óìíîæåíèÿ
áèíàðíûõ îòíîøåíèé. Ðåôëåêñèâíûì è òðàíçèòèâíûì çàìûêàíèåì áèíàðíîãî
îòíîøåíèÿ � íàçûâàåòñÿ îáúåäèíåíèå � � � �* � iS
n
� � �� � ��
2
Âûïîëíåíèå ñèíòàêñè÷åñêè ïðàâèëüíîé ïðîãðàììû , íà÷èíàþùååñÿ â íà-
÷àëüíîì ñîñòîÿíèè ( , )a m S0 � , íàçûâàåòñÿ âåäóùèì ê ñîñòîÿíèþ îøèáêè òîãäà
è òîëüêî òîãäà, êîãäà � � �a S a a a1 0 1 1: ( , ) ( )*
� � , è òåðìèíàëüíûì òîãäà è òîëü-
êî òîãäà, êîãäà � � �a S a a aa1 0 1 1: ( , ) ( )*
*
� .  ïðîòèâíîì ñëó÷àå ãîâîðÿò, ÷òî
âû÷èñëåíèå ïðîãðàììû ðàñõîäèòñÿ. Ðåçóëüòàò âûïîëíåíèÿ ñèíòàêñè÷åñêè ïðà-
âèëüíîé ïðîãðàììû , íà÷èíàþùåãîñÿ â íà÷àëüíîì ñîñòîÿíèè ( , )a m0 , îïðåäå-
ëåí òîãäà è òîëüêî òîãäà, êîãäà ýòî âûïîëíåíèå çàêàí÷èâàåòñÿ ñî çíà÷åíèåì
�m U òàêèì, ÷òî
* *(( , ), ( , ))a m a m0
è
m — ýòîò ðåçóëüòàò.
Äèñêðåòíàÿ äèíàìè÷åñêàÿ ñèñòåìà (ÄÄÑ) èñïîëüçóåòñÿ â êà÷åñòâå ìîäåëè
äëÿ èññëåäîâàíèÿ ñåìàíòè÷åñêèõ ñâîéñòâ ïðîãðàìì.
ÄÄÑ íàçûâàåòñÿ ïÿòåðêà ( , , , , )*S a a
� � �
0
òàêàÿ, ÷òî S — íåïóñòîå ìíîæåñòâî
ñîñòîÿíèé,
� �S S — îòíîøåíèå ïåðåõîäîâ, �a S B
0
: � õàðàêòåðèçóåò íà÷àëüíîå
ñîñòîÿíèå, �
a
S B* : � — çàêëþ÷èòåëüíîå ñîñòîÿíèå, à � � : S B� — ñîñòîÿíèå
îøèáêè, ïðè÷åì âñå ñîñòîÿíèÿ a a0 , ,* � ðàçëè÷íû.
ÄÄÑ íàçûâàåòñÿ òîòàëüíîé, åñëè � � � �c S c S c c1 1( ( , ))
, è äåòåðìèíèðîâàí-
íîé, åñëè � � � � �c c c S c c c c c c, , ( ( , ) ( , )) ( )1 2 1 2 1 2
.
Ïðîãðàììà , îïðåäåëåííàÿ âûøå, çàäàåò íåêîòîðóþ ÄÄÑ. Áîëåå òîãî, âû-
ïîëíÿþòñÿ ñëåäóþùèå ñâîéñòâà:
� � � c c S c c ca, ( , ) ( ( ))1 1 10
� ,
� � � � �c c S c c c c ca, ( , ) ( )*1 1 1
� ,
� � � �c c S c c c c, ( , ) ( ) ( )1 1 1
� �� � .
8 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2013, ¹ 6
ÄÄÑ íàçûâàåòñÿ èíúåêòèâíîé, åñëè
�1 äåòåðìèíèðîâàíî, è èíâåðòèðóåìîé,
åñëè îíà èíúåêòèâíà è
�1 — òîòàëüíîå îòíîøåíèå (â îáùåì ñëó÷àå ïðîãðàììà
íå âñåãäà îïðåäåëÿåò èíúåêòèâíóþ ÄÄÑ).
2. ÕÀÐÀÊÒÅÐÈÑÒÈÊÀ ÄÄÑ Ñ ÏÎÇÈÖÈÉ ÍÅÏÎÄÂÈÆÍÛÕ ÒÎ×ÅÊ
Òåîðåìû î íåïîäâèæíîé òî÷êå îòîáðàæåíèé â ïîëíûõ ðåøåòêàõ. Ïðèâå-
äåì íåêîòîðûå îïðåäåëåíèÿ è ïîíÿòèÿ èç òåîðèè ïîëíûõ ðåøåòîê. Ïóñòü
R � �( ,{ , , , , })� � � �� — ïîëíàÿ ðåøåòêà è f R R: � — îòîáðàæåíèå.
Îòîáðàæåíèå f íàçûâàåòñÿ ñòðîãèì, åñëè f ( )� � � , è èçîòîííûì, åñëè
� � �a b G a b f a f b, [( ) ( ( ) ( )]� � .
Ýëåìåíò a R� íàçûâàåòñÿ íåïîäâèæíîé òî÷êîé îòîáðàæåíèÿ f R R: � ,
åñëè f a a( ) � . Ïîñêîëüêó ïîëíàÿ ðåøåòêà ÿâëÿåòñÿ ÷àñòè÷íî óïîðÿäî÷åííûì
ìíîæåñòâîì, òî íåïîäâèæíàÿ òî÷êà ìîæåò áûòü íå åäèíñòâåííîé, è òîãäà åñòåñ-
òâåííî ââåñòè ïîíÿòèå íàèìåíüøåé (l f p ) è äâîéñòâåííîå ïîíÿòèå íàèáîëüøåé
íåïîäâèæíîé òî÷êè (gf p ). Èñõîäÿ èç îïðåäåëåíèÿ îïåðàöèè � , ìîæåì çàïèñàòü
l fp f x R f x x( ) { : ( ) }� �� � è g fp f x R x f x( ) { : ( )}� �� � .
Èìåþò ìåñòî ñëåäóþùèå óòâåðæäåíèÿ [10].
Òåîðåìà 1 (î íåïîäâèæíîé òî÷êå). Åñëè R � �( ,{ , , , , })� � � �� — ïîëíàÿ
ðåøåòêà è f R R: � — èçîòîííîå îòîáðàæåíèå, òî ñóùåñòâóåò ýëåìåíò a R� òà-
êîé, ÷òî f a a( ) � .
Òåîðåìà 2 (Òàðñêîãî). Ìíîæåñòâî íåïîäâèæíûõ òî÷åê èçîòîííîãî îòîáðà-
æåíèÿ ïîëíîé ðåøåòêè R � �( ,{ , , , , })� � � �� ÿâëÿåòñÿ ïîëíîé ðåøåòêîé îòíî-
ñèòåëüíî òîãî æå ïîðÿäêà � .
Èç òåîðåìû Òàðñêîãî âûòåêàåò ñëåäóþùåå óòâåðæäåíèå.
Òåîðåìà 3 (î ðåêóðñèâíîì ïðèíöèïå èíäóêöèè). Åñëè R � �( ,{ , , , , })� � � �� —
ïîëíàÿ ðåøåòêà, òî � � �x R f x x lfp f x(( ( ) ) ( ( ) ))� � è äâîéñòâåííî � �x R
(( ( )) ( ( ))x f x x g fp f� �� .
Åñëè R � �( ,{ , , , , })� � � �� è R1 �
�
( ,{ , , , , })� � � �� — ïîëíûå ðå-
øåòêè, òî ìíîæåñòâî F îòîáðàæåíèé èç R â R1 ÿâëÿåòñÿ ïîëíîé ðåøåòêîé
R F�
�
( ,{ , , , , })� � �� îòíîñèòåëüíî îòíîøåíèÿ � �
f g F f g, ( )� òîãäà
è òîëüêî òîãäà, êîãäà � �
x R f x g x( ( ) ( ))� .
Ìíîæåñòâî n-îê ýëåìåíòîâ ïîëíîé ðåøåòêè R îáðàçóþò ñíîâà ïîëíóþ ðå-
øåòêó îòíîñèòåëüíî îòíîøåíèÿ ïîêîìïîíåíòíîãî ñðàâíåíèÿ, ò.å.
( , , , ( , , , ))a a a b b bn n1 2 1 2� �� òîãäà è òîëüêî òîãäà, êîãäà a bi i� äëÿ
i n�1 2, , ,� . Áóëåàí B R( ) ïîëíîé ðåøåòêè R ñíîâà áóäåò ïîëíîé ðåøåòêîé
( ( ), , , , , , )B R R� � � � ' . Îòîáðàæåíèå f R R: � 1 ðàñøèðÿåòñÿ íà ðåøåòêè R n è
R n
1
î÷åâèäíûì îáðàçîì: f a a f a f an n(( , , )) ( ( ), , ( ))1 1� �� è íà áóëåàíû
f B R B R: ( ) ( )� 1 , ãäå f S f x x S( ) { ( ) : }� � , S B R� ( ) , f S B R( ) ( )� 1 .
Ïîñëåäîâàòåëüíîñòü ýëåìåíòîâ x x xn0 1, , , ,� � ÷àñòè÷íî óïîðÿäî÷åííîãî
ìíîæåñòâà ( , )R � íàçûâàåòñÿ âîçðàñòàþùåé öåïüþ, åñëè x x xn0 1� � � �� �
Ôóíêöèÿ f R R: � íà ðåøåòêå R � �( ,{ , , , , })� � � �� íàçûâàåòñÿ ïîëó-� -íå-
ïðåðûâíîé òîãäà è òîëüêî òîãäà, êîãäà äëÿ ëþáîé öåïè C x i I Ri� � �{ | } âûïîë-
íÿåòñÿ ðàâåíñòâî f C f C( ) ( )� �� . Èìååò ìåñòî ñëåäóþùàÿ òåîðåìà.
Òåîðåìà 4 (Êëèíè). Íàèìåíüøàÿ ôèêñèðîâàííàÿ òî÷êà ïîëó-�-íåïðåðûâíîé
ôóíêöèè f íà R � �( ,{ , , , , })� � � �� ñîâïàäàåò ñî çíà÷åíèåì � f i , ãäå f i
îïðåäåëÿåòñÿ ðåêóððåíòíîé çàâèñèìîñòüþ f x x0 � � . [ ], f i� �1 �x f f xi. [ ( ( ))].
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2013, ¹ 6 9
×àñòè÷íî óïîðÿäî÷åííîå ìíîæåñòâî íàçûâàåòñÿ ìíîæåñòâîì, óäîâëåòâîðÿ-
þùèì óñëîâèþ îáðûâà âîçðàñòàþùèõ öåïåé, åñëè ëþáàÿ âîçðàñòàþùàÿ öåïü êî-
íå÷íà, ò.å. ñóùåñòâóåò òàêîé èíäåêñ m, ÷òî
x x x x x xm m m0 1 2 1 2� � � �� �� � �� �
Î÷åâèäíî, ÷òî ïîëó-� -íåïðåðûâíàÿ ôóíêöèÿ áóäåò èçîòîííûì îòîáðàæåíè-
åì, íî îáðàòíîå â îáùåì ñëó÷àå íåâåðíî. Îäíàêî åñëè f — èçîòîííîå îòîáðàæå-
íèå ïîëíîé ðåøåòêè â ñåáÿ, óäîâëåòâîðÿþùåé óñëîâèþ îáðûâà âîçðàñòàþùèõ
öåïåé, òî f áóäåò ïîëó-� -íåïðåðûâíîé ôóíêöèåé.  ýòîì ñëó÷àå òàêàÿ ôóíêöèÿ
áóäåò ïîëíûì-� -ìîðôèçìîì, ò.å. � �H R f H f H( ) ( )� �� , à îòñþäà î÷åâèä-
íûì îáðàçîì ñëåäóåò ïîëó-� -íåïðåðûâíîñòü f .
Äâîéñòâåííûì îáðàçîì îïðåäåëÿþòñÿ óáûâàþùèå öåïè, óñëîâèå îáðûâà
óáûâàþùèõ öåïåé, ïîëó-� -íåïðåðûâíîñòü è ïîëíûé � -ìîðôèçì.
Åñëè R � �( ,{ , , , , })� � � �� è R1 �
�
( ,{ , , , , })� � � �� — ïîëíûå ðå-
øåòêè, f R R: � è g R R:
�
— èçîòîííûå îòîáðàæåíèÿ, à h R R: '� — ñòðîãîå
ïîëó-� -íåïðåðûâíîå îòîáðàæåíèå (ò.å. h( )� �
� ), òî h lfp f lfp g( ( )) ( )� .
Åñëè a — ýëåìåíò ïîëíîé ðåøåòêè, òî åãî äîïîëíåíèåì íàçûâàåòñÿ òàêîé
ýëåìåíò b, ÷òî a b� �� è a b� � � .  îáùåì ñëó÷àå äîïîëíåíèå ýëåìåíòà â ïîë-
íîé ðåøåòêå íååäèíñòâåííî, íî åñëè îíî åäèíñòâåííî, òî òàêàÿ ðåøåòêà íàçûâà-
åòñÿ ðåøåòêîé ñ åäèíñòâåííûì äîïîëíåíèåì è îáîçíà÷àåòñÿ
R � � ( ,{ , , , , , })� � � �� , à äîïîëíåíèå ýëåìåíòà a îáîçíà÷àåòñÿ a .
Òåîðåìà 5 (Ïàðèê). Åñëè f R R: � — èçîòîííîå îòîáðàæåíèå ïîëíîé ðå-
øåòêè R ñ åäèíñòâåííûì äîïîëíåíèåì, òî f x( ) òîæå áóäåò èçîòîííûì îòî-
áðàæåíèåì R è gf p f l fp x f x( ) ( . [ ( )])� � .
Ïóñòü R � �( ,{ , , , , })� � � �� — ïîëíàÿ ðåøåòêà, n � 1 è F R Rn n: � —
ïîëó-� -íåïðåðûâíîå îòîáðàæåíèå. Ïóñòü X X X n� ( , , )1 � — âåêòîð èç R n .
Ñèñòåìà óðàâíåíèé
X F X� ( ) (ò.å. X F X X j nj j n� �( , , ), , , )1 1� �
èìååò ïî êðàéíåé ìåðå îäíî ðåøåíèå, êîòîðîå ÿâëÿåòñÿ íàèìåíüøåé âåðõíåé
ãðàíüþ ïîñëåäîâàòåëüíîñòè { | }X ii � 0 , ãäå X 0 � � �( , , )� è X F Xi i� �1 ( ) ,
ò.å. X F X Xj
i
j
i
n
i� �1
1
( , , )� , j n�1, ,� .
Õàðàêòåðèñòèêà ñâîéñòâ ÄÄÑ. Ïóñòü ( , , , , )*S a a
� � � �0
— ÄÄÑ è ìíî-
æåñòâî äîñòèæèìûõ ñîñòîÿíèé, óäîâëåòâîðÿþùèõ óñëîâèþ �, îïðåäåëÿåòñÿ ñëå-
äóþùèì îáðàçîì:
� �
�s s S s l s s post2 1 1 1 2.[ : ( ( ) ( , )] ( ( )* *� � � � ,
ãäå post s s S s s s� � � ��� �� � � �. [ . [ : ( ) ( , )]]].2 1 1 1 2 .
Ïðèìåð 3. Ïóñòü — ïðîãðàììà, êîòîðîé ñîîòâåòñòâóåò ïîëíîñòüþ îïðåäå-
ëåííàÿ ÄÄÑ ( , , , , )*S a a
� � � �0
, à � è
— íåêîòîðûå óñëîâèÿ. Òîãäà ÷àñòè÷íàÿ
êîððåêòíîñòü ïðîãðàììû çàïèñûâàåòñÿ â âèäå âûðàæåíèÿ
�
� �
a apost* ( )( )*� � �
0
,
êîòîðîå îçíà÷àåò, ÷òî êàæäîå âûïîëíåíèå ïðîãðàììû , íà÷èíàþùååñÿ â íà-
÷àëüíîì ñîñòîÿíèè a0 , ãäå èñòèííî óñëîâèå �, çàêàí÷èâàåòñÿ â çàêëþ÷èòåëü-
íîì ñîñòîÿíèè a * , ãäå èñòèííî óñëîâèå
. Âîïðîñ òåðìèíàëüíîñòè ïðîãðàì-
ìû íå ðàññìàòðèâàåòñÿ, ÷åì îïðàâäûâàåòñÿ ñëîâî «÷àñòè÷íàÿ» êîððåêòíîñòü.
Ñëåäóþùåå óòâåðæäåíèå ïîêàçûâàåò, ÷òî post ( )( )*
� ÿâëÿåòñÿ ðåøåíèåì
óðàâíåíèÿ � �
�� � post( )( ) íà ïîëíîé ðåøåòêå R false true� � � � ( , { , , , , , })� .
10 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2013, ¹ 6
Òåîðåìà 6: à) ðåøåòêà R false true� � � � ( , { , , , , , })� — ïîëíàÿ ðåøåòêà ñ
åäèíñòâåííûì äîïîëíåíèåì;
á) äëÿ ëþáîãî � îòîáðàæåíèå post( )� ÿâëÿåòñÿ ïîëíûì ñòðîãèì �-ìîðôèç-
ìîì, è äëÿ ëþáîãî óñëîâèÿ � îòîáðàæåíèå �� � �. [ ( )( )]post — òîæå ñòðîãèé ïîë-
íûé �-ìîðôèçì;
â) äëÿ ëþáîãî
è ëþáîãî � èìååò ìåñòî
post post l fp post
n
n( )( ) ( )( ) ( . [ ( )( )])*
�
� �� �
�� � ��
�0
.
Ïðèìåð 4.  ìåòîäå Ôëîéäà–Íàóðà ïðè äîêàçàòåëüñòâå ÷àñòè÷íîé ïðàâèëü-
íîñòè ïðîãðàììû îòíîñèòåëüíî íà÷àëüíûõ óñëîâèé � è çàêëþ÷èòåëüíûõ óñëî-
âèé
êîððåêòíîñòü èíäóêòèâíûõ ïðåäïîëîæåíèé ñâîäèòñÿ ê äîêàçàòåëüñòâó
óòâåðæäåíèé ((( ) ) ( )( ) ) (( ) ))*� �
�
a at post t t t
0
� � � � � � � ïðè óñëîâèè
ñïðàâåäëèâîñòè óòâåðæäåíèÿ t.
Ïðèìåíÿÿ ðåêóðñèâíûé èíäóêòèâíûé ïðèíöèï, ïîëó÷àåì, ÷òî èç
((( ) ) ( ( )( ) ))� �
a t post t t
0
� � � � ñëåäóåò l fp post ta( . [( ) ( )( )]) )�� � �
�
0
� � �
â ñèëó ï. â) ïðåäûäóùåé òåîðåìû. Äåéñòâèòåëüíî, ñîãëàñíî ýòîìó ñâîéñòâó
( ( )( )) ( )* *
*�
� � �
a a apost t� � � � �
0
.
Íàîáîðîò, åñëè — ÷àñòè÷íî ïðàâèëüíàÿ ïðîãðàììà îòíîñèòåëüíî óñëîâèé
� è
, òî ýòî ìîæåò áûòü äîêàçàíî ñ ïîìîùüþ ìåòîäà Ôëîéäà–Íàóðà. Ýòî ñëåäó-
åò èç òîãî, ÷òî ìîæíî âûáðàòü t êàê l fp posta( . [ ) ( )( )])�� � �
�
0
� � .
Ðàññìîòðåííàÿ âûøå õàðàêòåðèñòèêà ÄÄÑ âûïîëíÿëàñü ñ ïîìîùüþ post-îòî-
áðàæåíèÿ, íî õàðàêòåðèçîâàòü ÄÄÑ ìîæíî è ñ ïîìîùüþ pre-îòîáðàæåíèÿ.
Ïóñòü � — íåêîòîðîå óñëîâèå âèäà
�
�
�s s S s s s pre1 2 1 2 2.[ : ( , ) ( )] ( )( )* *� � � � .
Ìîæåì çàïèñàòü, ÷òî
pre s s S s s s� � � ��� �� �
�. [ . [ [ : ( , ) ( )]]]*
1 2 1 2 2 .
Ïðèìåð 5. Ïóñòü ïðîãðàììà îïðåäåëÿåò ïîëíóþ äåòåðìèíèðîâàííóþ
ÄÄÑ ( , , , , )*S a a
� � � �0
, à � è
ÿâëÿþòñÿ âõîäíûì è âûõîäíûì óñëîâèÿìè ñîîò-
âåòñòâåííî.Òîãäà äîêàçàòåëüñòâî òîòàëüíîé êîððåêòíîñòè ïðîãðàììû ñâîäèòñÿ
ê äîêàçàòåëüñòâó èìïëèêàöèè
( ) ( )( )*
*� �
�
a apre
0
� � � .
Äðóãèìè ñëîâàìè, êàæäîå âû÷èñëåíèå ïðîãðàììû , íà÷èíàþùååñÿ â ñîñòîÿ-
íèè a0 , ãäå âûïîëíÿåòñÿ óñëîâèå �, ïðèâîäèò ê ñîñòîÿíèþ a * , ãäå âûïîëíÿåò-
ñÿ óñëîâèå
.
Ìàòåìàòè÷åñêèå ñâîéñòâà îòîáðàæåíèÿ pre ïîëó÷àþòñÿ äâîéñòâåííûì îáðàçîì
èç ñâîéñòâ post, ïîñêîëüêó pre post( )( ) ( )( )� � � �� �1 è post pre( )( ) ( )( )� � � �� �1 .
Èìååò ìåñòî ñëåäóþùàÿ òåîðåìà.
Òåðåìà 7: à) äëÿ ëþáîãî � îòîáðàæåíèå pre( )� ÿâëÿåòñÿ ïîëíûì ñòðîãèì
�-ìîðôèçìîì è äëÿ ëþáîãî óñëîâèÿ � îòîáðàæåíèå �� � �. [ ( )( )]pre — òîæå ñòðî-
ãèé ïîëíûé �-ìîðôèçì;
á) äëÿ ëþáîãî
è ëþáîãî � èìååò ìåñòî
pre pre lfp pre
n
n( )( ) ( )( ) ( . [ ( )( )])*
�
� �� �
�� � ��
�0
.
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2013, ¹ 6 11
Âû÷èñëåíèÿ â äåòåðìèíèðîâàííîé ÄÄÑ ( , , , , )*S a a
� � � �0
, êîòîðûå íå âåäóò
â ñîñòîÿíèå îøèáêè, óäîâëåòâîðÿþò óñëîâèþ �
�� �� pre( )( )* . Îòñþäà ñëå-
äóåò òåoðåìà 8.
Òåîðåìà 8. Ïóñòü
— òîòàëüíîå äåòåðìèíèðîâàííîå îòíîøåíèå ïåðåõîäîâ.
Òîãäà äëÿ ëþáîãî óñëîâèÿ � èìååò ìåñòî
� �pre g fp pre( )( ) ( . [ ( )( )])*
� �� �
� .
Òàêèì îáðàçîì, ïîâåäåí÷åñêèå ñâîéñòâà äåòåðìèíèðîâàííîé ÄÄÑ, êîòîðàÿ
ñîîòâåòñòâóåò ïðîãðàììå , ïîëó÷àþòñÿ êàê ðåøåíèÿ â âèäå íåïîäâèæíûõ òî÷åê
ñëåäóþùèõ óðàâíåíèé: ïóñòü � è
— âõîäíîå è âûõîäíîå óñëîâèÿ äëÿ äåòåðìè-
íèðîâàííîé ÄÄÑ ( , , , , )*S a a
� � � �0
, òîãäà:
1) äëÿ ìíîæåñòâà ñîñòîÿíèé, êîòîðûå óäîâëåòâîðÿþò íà÷àëüíîìó óñëîâèþ �,
post l lfp posta a( )( ) ( .[( ) ( )( )])*
� � �� � �
�
0 0
� � � � ;
2) äëÿ ìíîæåñòâà ñîñòîÿíèé, êîòîðûå óäîâëåòâîðÿþò çàêëþ÷èòåëüíîìó
óñëîâèþ
,
pre lfp prea a( )( ) ( .[( ) ( )( )])*
* *
�
�� �
�� � � � ;
3) äëÿ ìíîæåñòâà ñîñòîÿíèé, êîòîðûå ïðèâîäÿò ê ñîñòîÿíèþ îøèáêè,
pre lfp pre( )( ) ( . [ ( )( )])*
� �� �
�� �� � ;
4) äëÿ ìíîæåñòâà ñîñòîÿíèé, êîòîðûå íå ïðèâîäÿò ê ñîñòîÿíèþ îøèáêè,
� �pre g fp pre( )( ) ( . [ ( )( )])*
� �� �
�� � ;
5) äëÿ ìíîæåñòâà ñîñòîÿíèé, êîòîðûå ïðèâîäÿò ê íåîïðåäåëåííîñòè,
pre g fp prea a( )( ) ( . [ ( )( )])*
* *
� � �� � �
�� �� � � � .
3. ÇÀÊËÞ×ÈÒÅËÜÍÛÉ ÏÐÈÌÅÐ
Ïðîèëëþñòðèðóåì íà ïðèìåðå òåîðèè ïðîãðàììíûõ èíâàðèàíòîâ ïîñòðîåíèå
èåðàðõèè àáñòðàêöèé, êîòîðûå âîçíèêàþò ïðè ïîèñêå ñîîòíîøåíèé â ïðîãðàì-
ìàõ. Â ïðîöåññå ïîèñêà ñîîòíîøåíèé â ïðîãðàììàõ èìååì äåëî ñî ñëåäóþùè-
ìè îáúåêòàìè:
à) ïðîãðàììîé â íåêîòîðîì ÿçûêå ïðîãðàììèðîâàíèÿ è åå îáëàñòüþ äàííûõ;
á) ÿçûêîì ñîîòíîøåíèé;
â) ãåíåðàòîðîì ñîîòíîøåíèé (àëãîðèòìîì ïîèñêà ñîîòíîøåíèé) [1, 2].
Àáñòðàêöèè, êàñàþùèåñÿ ïðîãðàììû è åå äàííûõ, ñîñòîÿò â ñëåäóþùåì:
à1) àáñòðàãèðîâàíèå îò ñòðóêòóðíûõ ïåðåìåííûõ ïðîãðàììû (ìàññèâîâ,
êóðñîðîâ, óêàçàòåëåé è ò.ï.) è ó÷åò òîëüêî ïðîñòûõ ïåðåìåííûõ è äåéñòâèé íàä
íèìè;
à2) àáñòðàêöèÿ îáëàñòè äàííûõ (íàïðèìåð, ïðèíèìàåòñÿ, ÷òî îáëàñòü äàííûõ
ÿâëÿåòñÿ àáåëåâîé ãðóïïîé èëè âåêòîðíûì ïðîñòðàíñòâîì).
Àáñòðàêöèè, êàñàþùèåñÿ ÿçûêà ñîîòíîøåíèé, ñîñòîÿò â òîì, ÷òî ïðèíèìàåò-
ñÿ ñîãëàøåíèå î ÿçûêå òîëüêî ðàâåíñòâ èëè òîëüêî ëèíåéíûõ ðàâåíñòâ è íåðà-
âåíñòâ. Ñðåäè ýòèõ àáñòðàêöèé èìååòñÿ èåðàðõèÿ ñëåäóþùåãî âèäà:
á1) ÿçûê ïîëèíîìèàëüíûõ ðàâåíñòâ [13];
á2) ÿçûê ïîëèíîìèàëüíûõ ðàâåíñòâ îãðàíè÷åííîé ñòåïåíè [14];
á3) ÿçûê ëèíåéíûõ ðàâåíñòâ è íåðàâåíñòâ [15];
12 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2013, ¹ 6
á4) ÿçûê ëèíåéíûõ ðàâåíñòâ [16];
á5) ÿçûê ðàâåíñòâ âèäà r c� , ãäå r — ïåðåìåííàÿ, à c — êîíñòàíòà [17].
Àáñòðàêöèè, êàñàþùèåñÿ ãåíåðàòîðà èíâàðèàíòîâ, âûòåêàþò èç àáñòðàêöèé
ÿçûêà ñîîòíîøåíèé è àëãåáðû äàííûõ. Åñëè ïðèíèìàåòñÿ àáñòðàêöèÿ ÿçûêà ëè-
íåéíûõ ðàâåíñòâ, òî ãåíåðàòîð íå ó÷èòûâàåò óñëîâèé â óñëîâíûõ îïåðàòîðàõ, íå
ÿâëÿþùèõñÿ ëèíåéíûìè ðàâåíñòâàìè.
Íåîáõîäèìîñòü â òàêèõ àáñòðàêöèÿõ ñîñòîèò â òîì, ÷òî ïðè íàëè÷èè òîé èëè
èíîé àáñòðàêöèè ïðîöåññ ïîèñêà ñîîòíîøåíèé ìîæåò óñïåøíî çàêàí÷èâàòüñÿ,
à íå ïðîäîëæàòüñÿ áåñêîíå÷íî. Ïðè ýòîì ãåíåðàòîð ñîîòíîøåíèé âû÷èñëÿåò íàè-
ìåíüøóþ íåïîäâèæíóþ òî÷êó. Òàê, ãåíåðàòîð, ðåàëèçóþùèé ìåòîä âåðõíåé àï-
ïðîêñèìàöèè (àëãîðèòì ÌÂÀ [1, 2]), âû÷èñëÿåò íàèìåíüøóþ íåïîäâèæíóþ
òî÷êó, ÿâëÿþùóþñÿ ðåøåíèåì ñèñòåìû óðàâíåíèé
X
N a a
X ef X ya a
a u y a S
a
�
��
�
�
�� �
0 0, ,
( , )
( , , )
åñëè
'
'�
äëÿ âñåõ ñîñòîÿíèé a a,
è ïåðåõîäîâ ( , , , )
�a u y a S ïðîãðàììû, ãäå a0 — íà-
÷àëüíîå ñîñòîÿíèå, N 0 — ìíîæåñòâî ñîîòíîøåíèé â íà÷àëüíîì ñîñòîÿíèè,
à ôóíêöèÿ ef âû÷èñëÿåò ìíîæåñòâî ñîîòíîøåíèé íà âûõîäå îïåðàòîðà ïðèñâà-
èâàíèÿ y ñ ó÷åòîì íà åãî âõîäå ìíîæåñòâà ñîîòíîøåíèé X a' . Ñîîòíîøåíèÿ,
âõîäÿùèå â ðåçóëüòèðóþùèå ìíîæåñòâà, è áóäóò èíâàðèàíòíûìè ñîîòíîøåíè-
ÿìè àíàëèçèðóåìîé ïðîãðàììû.
Ïðè ýòîì ïîëó÷àåìûå â ïðîöåññå ïîèñêà ñîîòíîøåíèÿ ñîñòàâëÿþò ðåøåòêó
îòíîñèòåëüíî îïåðàöèé îáúåäèíåíèÿ è ïåðåñå÷åíèÿ. Ïîëíîòà ìíîæåñòâà ñîîòíî-
øåíèé çàâèñèò îò òîãî, áóäåò ëè äèñòðèáóòèâíîé ôóíêöèÿ ef îòíîñèòåëüíî
îïåðàöèè ïåðåñå÷åíèÿ.
 ñâÿçè ñî ñêàçàííûì âûøå çàìåòèì, ÷òî ñåìàíòè÷åñêèé àíàëèç ïðîãðàìì
òðåáóåò èçó÷åíèÿ äèñöèïëèí, êîòîðûå èññëåäóþò ðàçíîðîäíûå ñåìåéñòâà ìåòî-
äîâ è àëãîðèòìîâ. Ýòî ñâÿçàíî ñ òåì, ÷òî ìåòîäû àíàëèçà ïðîãðàìì íåçàâèñèìî
ìîãóò ïðèìåíÿòüñÿ ê ÿçûêàì, îáúåêòíîìó êîäó, ñåìàíòèêå, ñâîéñòâàì ñïåöèôè-
êàöèé, ñâîéñòâàì îáúåêòíîãî êîäà, àáñòðàêöèÿì è ò.ï. Òàêîé àíàëèç âîçìîæåí íà
àïïðîêñèìàöèÿõ ñòðóêòóð, âõîäÿùèõ â ñåìàíòè÷åñêèå ñïåöèôèêàöèè. Ñ ïðàêòè-
÷åñêîé òî÷êè çðåíèÿ, ýòà ìåòîäîëîãèÿ ìîæåò ïðèìåíÿòüñÿ â ïðîöåññå ðàçðàáîòêè
èåðàðõèè ñåìàíòèê è èåðàðõèè àáñòðàêòíûõ àëãåáð íà ðàçíûõ óðîâíÿõ àáñòðàê-
öèè [18]. Öåëü òàêîé ìåòîäîëîãèè — ñîçäàíèå ñðåäñòâ òàêîé ñåìàíòè÷åñêîé
ñèñòåìû àíàëèçàòîðîâ, êîòîðàÿ (ïî âîçìîæíîñòè) àâòîìàòè÷åñêè âûïîëíÿëà áû
àíàëèç ñïåöèôèêàöèé.
Äàëüíåéøèå èññëåäîâàíèÿ ïðîáëåìû è ðåçóëüòàòû â ýòîé îáëàñòè ìîæíî
íàéòè â ðàáîòàõ [6, 11, 12, 19, 20].
ÑÏÈÑÎÊ ËÈÒÅÐÀÒÓÐÛ
1. Ì à ê ñ è ì å ö À . Í . Ïîèñê ïðîãðàììíûõ èíâàðèàíòîâ â âèäå ïîëèíîìîâ // Äîêë. ÍÀÍ
Óêðàèíû. — 2013. — ¹ 9. — Ñ. 44–50.
2. Ê ð û â û é Ñ . Ë . , Ì à ê ñ è ì å ö À . Í . Ôîðìàëüíûå ìåòîäû âåðèôèêàöèè íà îñíîâå ñåòåé
Ïåòðè // Òð. 10-é ìåæäóíàð. êîíô. «Òåîðåòèêî-ïðèêëàäíûå àñïåêòû ïîñòðîåíèÿ ïðîãðàì.
ñèñòåì. TAAbD’2013». — ßëòà, 2013. — Ñ. 75–80.
3. S i n t z o f f F . Calculating properties of programs by variations on specific models // ACM Conf. on
Proving Assertions about Programs; Sigplan Notices. — 1972. — 7, N 1. — P. 203–207.
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2013, ¹ 6 13
â ïðîòèâíîì ñëó÷àå,
4. C o u s o t P . Semantic foundations of program analysis // S.S. Muchnik and N.D. Jones, editors,
Program Flow Analysis: Theory and Appl. — Prentice-Hall, 1981. — 10. — P. 303–342.
5. C o u s o t P . Abstract interpretation: a unified lattice model for static analysis of programs by con-
struction of fixpoints. // 4-th ACM Symposium on Principles on Program. Languages. — Los An-
geles: ACM, 1977. — P. 238–252.
6. C o u s o t P . Verification by abstract Interpretation // Lecture Notes in Comput. Sci. — 2003. —
N 2772. — P. 243–268.
7. N i e l s o n F . A denotation framework for data flow analisys // Acta Inform. — 1982. — N 18. —
P. 265–287.
8. N i e l s o n F . Two-level semantics and abstract interpretation // Theor. Comput. Sci. (Fundamental
Studies). — 1989.— N 69. — P. 117–242.
9. J o n e s N . D . , G o m a r d C . K . , S e s t o f t P . Partial evaluation and automatic program genera-
tion. — Techn. Un-t of Denmark, 1993. — 414 p.
10. Á è ð ê ã î ô Ã . Òåîðèÿ ðåøåòîê. — M.: Íàóêà, 1984. — 564 c.
11. C o u s o t P . , C o u s o t R . Abstract Interpretation frameworks // Journ. of Logic and Comput. —
1992. — 2, N 4. — P. 511–547.
12. C o u s o t P . , C o u s o t R . Modular static program analysis. Invited paper // Lecture Notes in
Comput. Sci. — 2002. — N 2304. — P. 159–178.
13. R o d r i g u e z - C a r b o n e l l E . , K a p u r D . An abstract interpretation approach for automatic
generation of polynomial invariants // Proc. Static Analysis Sympos. (SAS). — Italy. — August
2004. — P. 1–8.
14. L v o v M . S . About one algorithm of program polynomial invariants generation // Proc. Workshop
on Invariant Generation: (Techn. rep.) Univ. of Linz; Eds. M. Giese, T. Jebelean. N 0707 (RISC
Rep. Ser.). Linz (Austria), 2007. — P. 85–99.
15. Ê ð è â î é Ñ . Ë . , Ð à ê ø à Ñ . Ã . Ïîèñê ëèíåéíûõ èíâàðèàíòíûõ çàâèñèìîñòåé â ïðîãðàììàõ
// Êèáåðíåòèêà. — 1984. — ¹ 6. — Ñ. 23–28.
16. K r i v o i S . L . About one invariant search algorithm in programs // Cybernetics and Systems
Analysis. — 1981. — N 5. — P. 12–18.
17. K i l d a l l G . A . A unified approach to program optimization // Conf. Rec. of ACM Symp. on Prin-
ciples of Program Languages. — Boston. — Oñtober 1–3. — 1973. — P. 194–206.
18. C o u s o t P . Abstract Interpretation Persective // ACM Workshop on Strategic Directions in
Comput. Res. MIT Laboratory for Comput. Sci.: Cambridge, Massachusetts, USA,1996. — P. 1–8.
19. C o u s o t P . Abstract interpretation based formal methods and future challenges. —
http://www.di.ens.fr/~cousot/. — 2003. — P. 131–151. Chap. 10. — P. 303–342.
20. S a d d e k B . , G r a f S . , L a k h n e c h Y . Abstraction as the key for invariant verification // Lec-
ture Notes in Comput. Sci. — 2003. — N 2772. — P. 67–99.
Ïîñòóïèëà 15.04.2013
14 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2013, ¹ 6
|