Лекция 2. Общие принципы дедуктивной верификации программ. Логика Хоара
Описание файла
PDF-файл из архива "Лекция 2. Общие принципы дедуктивной верификации программ. Логика Хоара", который расположен в категории "". Всё это находится в предмете "математические методы верификации схем и программ" из 10 семестр (2 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст из PDF
Ìàòåìàòè÷åñêèåìåòîäûâåðèôèêàöèèïðîãðàìì è ñõåìËÅÊÒÎÐÛ:Âëàäèìèð Àíàòîëüåâè÷ Çàõàðîâ,Âëàäèñëàâ Âàñèëüåâè÷ ÏîäûìîâËåêöèÿ 2.Îáùèå ïðèíöèïû äåäóêòèâíîéâåðèôèêàöèè ïðîãðàìì.Îïåðàöèîííàÿ ñåìàíòèêàèìïåðàòèâíûõ ïðîãðàìì.Ôîðìàëüíàÿ ïîñòàíîâêà çàäà÷èâåðèôèêàöèè ïðîãðàìì.Ëîãèêà Õîàðà: ïðàâèëà âûâîäà èñâîéñòâà.Àâòîìàòèçàöèÿ ïðîâåðêèïðàâèëüíîñòè ïðîãðàìì.ÏÐÈÍÖÈÏÛ ÄÅÄÓÊÒÈÂÍÎÃÎ ÀÍÀËÈÇÀÏÐÎÃÐÀÌÌ1. Ïðîãðàììà π âû÷èñëÿåò îòíîøåíèå Rπ ìåæäóäàííûìè íà âõîäå è íà âûõîäå ïðîãðàììû;ÏÐÈÍÖÈÏÛ ÄÅÄÓÊÒÈÂÍÎÃÎ ÀÍÀËÈÇÀÏÐÎÃÐÀÌÌ1.
Ïðîãðàììà π âû÷èñëÿåò îòíîøåíèå Rπ ìåæäóäàííûìè íà âõîäå è íà âûõîäå ïðîãðàììû;2. Òåêñò ïðîãðàììû ôîðìàëüíîå îïèñàíèåîòíîøåíèÿ Rπ ;ÏÐÈÍÖÈÏÛ ÄÅÄÓÊÒÈÂÍÎÃÎ ÀÍÀËÈÇÀÏÐÎÃÐÀÌÌ1. Ïðîãðàììà π âû÷èñëÿåò îòíîøåíèå Rπ ìåæäóäàííûìè íà âõîäå è íà âûõîäå ïðîãðàììû;2. Òåêñò ïðîãðàììû ôîðìàëüíîå îïèñàíèåîòíîøåíèÿ Rπ ;3. Cïåöèôèêàöèÿ ïðîãðàììû Φ ýòî îïèñàíèåòîãî îòíîøåíèÿ, êîòîðîå äîëæíàðåàëèçîâûâàòü ïðîãðàììà, íî íà äðóãîì ÿçûêå(èëè â äðóãîé ôîðìå);ÏÐÈÍÖÈÏÛ ÄÅÄÓÊÒÈÂÍÎÃÎ ÀÍÀËÈÇÀÏÐÎÃÐÀÌÌ1.
Ïðîãðàììà π âû÷èñëÿåò îòíîøåíèå Rπ ìåæäóäàííûìè íà âõîäå è íà âûõîäå ïðîãðàììû;2. Òåêñò ïðîãðàììû ôîðìàëüíîå îïèñàíèåîòíîøåíèÿ Rπ ;3. Cïåöèôèêàöèÿ ïðîãðàììû Φ ýòî îïèñàíèåòîãî îòíîøåíèÿ, êîòîðîå äîëæíàðåàëèçîâûâàòü ïðîãðàììà, íî íà äðóãîì ÿçûêå(èëè â äðóãîé ôîðìå);4. Ïðîâåðêà ïðàâèëüíîñòè ïðîãðàììû πîòíîñèòåëüíî ñïåöèôèêàöèè Φ ýòîäîêàçàòåëüñòâî òîãî, ÷òî Rπ ⇒ Φ .ÏÐÈÍÖÈÏÛ ÄÅÄÓÊÒÈÂÍÎÃÎ ÀÍÀËÈÇÀÏÐÎÃÐÀÌÌ×òîáû óìåòü äîêàçûâàòü ïðàâèëüíîñòü ïðîãðàììíóæíî1.
ñòðîãî îïðåäåëèòü îïåðàöèîííóþ ñåìàíòèêóïðîãðàìì: ñèñòåìó ïðàâèë, çàäàþùèõçàâèñèìîñòü ìåæäó âõîäíûìè è âûõîäíûìèäàííûìè ïðîãðàìì;ÏÐÈÍÖÈÏÛ ÄÅÄÓÊÒÈÂÍÎÃÎ ÀÍÀËÈÇÀÏÐÎÃÐÀÌÌ×òîáû óìåòü äîêàçûâàòü ïðàâèëüíîñòü ïðîãðàììíóæíî1. ñòðîãî îïðåäåëèòü îïåðàöèîííóþ ñåìàíòèêóïðîãðàìì: ñèñòåìó ïðàâèë, çàäàþùèõçàâèñèìîñòü ìåæäó âõîäíûìè è âûõîäíûìèäàííûìè ïðîãðàìì;2.
âûáðàòü ôîðìàëüíûé ÿçûê äëÿ îïèñàíèÿòðåáîâàíèé ïðàâèëüíîñòè ïðîãðàìì;ÏÐÈÍÖÈÏÛ ÄÅÄÓÊÒÈÂÍÎÃÎ ÀÍÀËÈÇÀÏÐÎÃÐÀÌÌ×òîáû óìåòü äîêàçûâàòü ïðàâèëüíîñòü ïðîãðàììíóæíî1. ñòðîãî îïðåäåëèòü îïåðàöèîííóþ ñåìàíòèêóïðîãðàìì: ñèñòåìó ïðàâèë, çàäàþùèõçàâèñèìîñòü ìåæäó âõîäíûìè è âûõîäíûìèäàííûìè ïðîãðàìì;2. âûáðàòü ôîðìàëüíûé ÿçûê äëÿ îïèñàíèÿòðåáîâàíèé ïðàâèëüíîñòè ïðîãðàìì;3. ïîñòðîèòü ëîãè÷åñêîå èñ÷èñëåíèå (ñèñòåìóïðàâèë âûâîäà) äëÿ äîêàçàòåëüñòâà ñâîéñòâïðàâèëüíîñòè ïðîãðàììÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌÄâà îñíîâíûõ ñïîñîáà ôîðìàëüíîãî îïèñàíèÿ ñåìàíòèêêîìïüþòåðíûõ ïðîãðàìì: äåíîòàöèîííûé è îïåðàöèîííûé .ÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌÄâà îñíîâíûõ ñïîñîáà ôîðìàëüíîãî îïèñàíèÿ ñåìàíòèêêîìïüþòåðíûõ ïðîãðàìì: äåíîòàöèîííûé è îïåðàöèîííûé .Äåíîòàöèîííûé : ïðîãðàììà îïèñûâàåò ôóíêöèþ; îíàîïðåäåëÿåòñÿ êàê êîìïîçèöèÿ ôóíêöèé äëÿ îòäåëüíûìôðàãìåíòîâ ïðîãðàììû;Ïðèìåíÿåòñÿ ïðåèìóùåñòâåííî äëÿÿçûêîâ ôóíêöèîíàëüíîãî ïðîãðàììèðîâàíèÿ.ÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌÄâà îñíîâíûõ ñïîñîáà ôîðìàëüíîãî îïèñàíèÿ ñåìàíòèêêîìïüþòåðíûõ ïðîãðàìì: äåíîòàöèîííûé è îïåðàöèîííûé .Äåíîòàöèîííûé : ïðîãðàììà îïèñûâàåò ôóíêöèþ; îíàîïðåäåëÿåòñÿ êàê êîìïîçèöèÿ ôóíêöèé äëÿ îòäåëüíûìôðàãìåíòîâ ïðîãðàììû;Ïðèìåíÿåòñÿ ïðåèìóùåñòâåííî äëÿÿçûêîâ ôóíêöèîíàëüíîãî ïðîãðàììèðîâàíèÿ.Îïåðàöèîííûé : ïðîãðàììà îïèñûâàåò îòíîøåíèå ïåðåõîäàâû÷èñëåíèÿ èç îäíîãî ñîñòîÿíèÿ â äðóãîå.Ïðèìåíÿåòñÿ ïðåèìóùåñòâåííî äëÿÿçûêîâ èìïåðàòèâíîãî ïðîãðàììèðîâàíèÿ.ÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌÎïðåäåëèì ñèíòàêñèñ è îïåðàöèîííóþ ñåìàíòèêóèìïåðàòèâíûõ ïðîãðàìì.Ïóñòü çàäàíà ñèãíàòóðà σ = hConst, Func, Predi , â êîòîðîéîïðåäåëåíî ìíîæåñòâî òåðìîâ Term è ìíîæåñòâî àòîìàðíûõôîðìóë Atom .Óñëîâèìñÿ, ÷òî ⇐ ýòî ñëóæåáíûé ñèìâîë, íåïðèíàäëåæàùèé ñèãíàòóðå σ .ÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌÎïðåäåëèì ñèíòàêñèñ è îïåðàöèîííóþ ñåìàíòèêóèìïåðàòèâíûõ ïðîãðàìì.Ïóñòü çàäàíà ñèãíàòóðà σ = hConst, Func, Predi , â êîòîðîéîïðåäåëåíî ìíîæåñòâî òåðìîâ Term è ìíîæåñòâî àòîìàðíûõôîðìóë Atom .Óñëîâèìñÿ, ÷òî ⇐ ýòî ñëóæåáíûé ñèìâîë, íåïðèíàäëåæàùèé ñèãíàòóðå σ .Îïðåäåëåíèåïðèñâàèâàíèå ::= ¾ïåðåìåííàÿ¿ ⇐ ¾òåðì¿óñëîâèå::= ¾àòîì¿ | (¬óñëîâèå ) |(óñëîâèå & óñëîâèå ) | (óñëîâèå ∨ óñëîâèå )ïðîãðàììà::= ïðèñâàèâàíèå |ïðîãðàììà ; ïðîãðàììà |if óñëîâèå then ïðîãðàììà else ïðîãðàììà |while óñëîâèå do ïðîãðàììà odÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌÏðèìåðÏðîãðàììà âû÷èñëåíèÿ íàèáîëüøåãî îáùåãî äåëèòåëÿ äâóõíàòóðàëüíûõ ÷èñåë.Const = {0, 1, 2, .
. . },Func = {+(2) , −(2) },Pred = {=(2) , >(2) , <(2) }while ¬(x = y )doif x > yodthen x ⇐ x − yelse y ⇐ y − xÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌÇíà÷åíèåì èìïåðàòèâíîé ïðîãðàììû ÿâëÿåòñÿ îòíîøåíèåâõîäâûõîä ìåæäó âõîäíûìè äàííûìè è ðåçóëüòàòîìâû÷èñëåíèÿ.Îòíîøåíèå âõîäâûõîä ïðîãðàììû îïðåäåëÿåòñÿ ïðè ïîìîùèîòíîøåíèÿ ïåðåõîäîâ ìåæäó ñîñòîÿíèÿìè âû÷èñëåíèÿïðîãðàììû.Ñîñòîÿíèå âû÷èñëåíèÿ ïðîãðàììû îïðåäåëÿåòñÿ äâóìÿêîìïîíåíòàìè ñîñòîÿíèåì óïðàâëåíèÿ è ñîñòîÿíèåìäàííûõ .ÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌÎïðåäåëåíèå (ñîñòîÿíèÿ âû÷èñëåíèÿ)Ïóñòü Var ýòî ìíîæåñòâî ïåðåìåííûõ, à GTerm ýòîìíîæåñòâî îñíîâíûõ òåðìîâ ñèãíàòóðû σ .ÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌÎïðåäåëåíèå (ñîñòîÿíèÿ âû÷èñëåíèÿ)Ïóñòü Var ýòî ìíîæåñòâî ïåðåìåííûõ, à GTerm ýòîìíîæåñòâî îñíîâíûõ òåðìîâ ñèãíàòóðû σ .Îöåíêîé ïåðåìåííûõ (ñîñòîÿíèåì äàííûõ) áóäåì íàçûâàòüâñÿêîå îòîáðàæåíèå (ïîäñòàíîâêó) θ : Var → GTerm .ÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌÎïðåäåëåíèå (ñîñòîÿíèÿ âû÷èñëåíèÿ)Ïóñòü Var ýòî ìíîæåñòâî ïåðåìåííûõ, à GTerm ýòîìíîæåñòâî îñíîâíûõ òåðìîâ ñèãíàòóðû σ .Îöåíêîé ïåðåìåííûõ (ñîñòîÿíèåì äàííûõ) áóäåì íàçûâàòüâñÿêîå îòîáðàæåíèå (ïîäñòàíîâêó) θ : Var → GTerm .Ñîñòîÿíèåì óïðàâëåíèÿ áóäåì íàçûâàòü âñÿêóþ ïðîãðàììó, àòàêæå ñïåöèàëüíûé ñèìâîë ∅ .ÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌÎïðåäåëåíèå (ñîñòîÿíèÿ âû÷èñëåíèÿ)Ïóñòü Var ýòî ìíîæåñòâî ïåðåìåííûõ, à GTerm ýòîìíîæåñòâî îñíîâíûõ òåðìîâ ñèãíàòóðû σ .Îöåíêîé ïåðåìåííûõ (ñîñòîÿíèåì äàííûõ) áóäåì íàçûâàòüâñÿêîå îòîáðàæåíèå (ïîäñòàíîâêó) θ : Var → GTerm .Ñîñòîÿíèåì óïðàâëåíèÿ áóäåì íàçûâàòü âñÿêóþ ïðîãðàììó, àòàêæå ñïåöèàëüíûé ñèìâîë ∅ .Ñîñòîÿíèåì âû÷èñëåíèÿ áóäåì íàçûâàòü âñÿêóþ ïàðó hπ, θi ,ãäå π ñîñòîÿíèå óïðàâëåíèÿ, à θ îöåíêà ïåðåìåííûõ.Çàïèñü Stateσ áóäåò îáîçíà÷àòü ìíîæåñòâî âñåâîçìîæíûõñîñòîÿíèé âû÷èñëåíèé ñèãíàòóðû σ .ÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌÎïðåäåëåíèå (îòíîøåíèÿ ïåðåõîäîâ)Ïóñòü I ýòî èíòåðïðåòàöèÿ ñèãíàòóðû σ .ÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌÎïðåäåëåíèå (îòíîøåíèÿ ïåðåõîäîâ)Ïóñòü I ýòî èíòåðïðåòàöèÿ ñèãíàòóðû σ .Òîãäà îòíîøåíèå ïåðåõîäîâ äëÿ èìïåðàòèâíûõ ïðîãðàìì ýòîáèíàðíîå îòíîøåíèå −→I íà ìíîæåñòâå ñîñòîÿíèé âû÷èñëåíèÿStateσ , óäîâëåòâîðÿþùåå ñëåäóþùèì òðåáîâàíèÿì:ÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌÎïðåäåëåíèå (îòíîøåíèÿ ïåðåõîäîâ)Ïóñòü I ýòî èíòåðïðåòàöèÿ ñèãíàòóðû σ .Òîãäà îòíîøåíèå ïåðåõîäîâ äëÿ èìïåðàòèâíûõ ïðîãðàìì ýòîáèíàðíîå îòíîøåíèå −→I íà ìíîæåñòâå ñîñòîÿíèé âû÷èñëåíèÿStateσ , óäîâëåòâîðÿþùåå ñëåäóþùèì òðåáîâàíèÿì:ASS: hx ⇐ t, θi −→I h∅, {x/t}θi;ÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌÎïðåäåëåíèå (îòíîøåíèÿ ïåðåõîäîâ)Ïóñòü I ýòî èíòåðïðåòàöèÿ ñèãíàòóðû σ .Òîãäà îòíîøåíèå ïåðåõîäîâ äëÿ èìïåðàòèâíûõ ïðîãðàìì ýòîáèíàðíîå îòíîøåíèå −→I íà ìíîæåñòâå ñîñòîÿíèé âû÷èñëåíèÿStateσ , óäîâëåòâîðÿþùåå ñëåäóþùèì òðåáîâàíèÿì:ASS: hx ⇐ t, θi −→I h∅, {x/t}θi;COMP∅ : hπ1 ; π2 , θi −→I hπ2 , ηiòîãäà è òîëüêî òîãäà, êîãäà hπ1 , θi −→I h∅, ηi;ÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌÎïðåäåëåíèå (îòíîøåíèÿ ïåðåõîäîâ)Ïóñòü I ýòî èíòåðïðåòàöèÿ ñèãíàòóðû σ .Òîãäà îòíîøåíèå ïåðåõîäîâ äëÿ èìïåðàòèâíûõ ïðîãðàìì ýòîáèíàðíîå îòíîøåíèå −→I íà ìíîæåñòâå ñîñòîÿíèé âû÷èñëåíèÿStateσ , óäîâëåòâîðÿþùåå ñëåäóþùèì òðåáîâàíèÿì:ASS: hx ⇐ t, θi −→I h∅, {x/t}θi;COMP∅ : hπ1 ; π2 , θi −→I hπ2 , ηiòîãäà è òîëüêî òîãäà, êîãäà hπ1 , θi −→I h∅, ηi;COMP: hπ1 ; π2 , θi −→I hπ10 ; π2 , ηiòîãäà è òîëüêî òîãäà, êîãäà hπ1 , θi −→I hπ10 , ηi è π10 6= ∅;ÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌÎïðåäåëåíèå (îòíîøåíèÿ ïåðåõîäîâ)IF1 : hif C then π1 else π2 , θi −→I hπ1 , θiòîãäà è òîëüêî òîãäà, êîãäà I |= C θ;ÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌÎïðåäåëåíèå (îòíîøåíèÿ ïåðåõîäîâ)IF1 : hif C then π1 else π2 , θi −→I hπ1 , θiòîãäà è òîëüêî òîãäà, êîãäà I |= C θ;IF0 : hif C then π1 else π2 , θi −→I hπ2 , θiòîãäà è òîëüêî òîãäà, êîãäà I 6|= C θ;ÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌÎïðåäåëåíèå (îòíîøåíèÿ ïåðåõîäîâ)IF1 : hif C then π1 else π2 , θi −→I hπ1 , θiòîãäà è òîëüêî òîãäà, êîãäà I |= C θ;IF0 : hif C then π1 else π2 , θi −→I hπ2 , θiòîãäà è òîëüêî òîãäà, êîãäà I 6|= C θ;WHILE1 : hwhile C do π od, θi −→I hπ; while C do π od, θiòîãäà è òîëüêî òîãäà, êîãäà I |= C θ;ÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌÎïðåäåëåíèå (îòíîøåíèÿ ïåðåõîäîâ)IF1 : hif C then π1 else π2 , θi −→I hπ1 , θiòîãäà è òîëüêî òîãäà, êîãäà I |= C θ;IF0 : hif C then π1 else π2 , θi −→I hπ2 , θiòîãäà è òîëüêî òîãäà, êîãäà I 6|= C θ;WHILE1 : hwhile C do π od, θi −→I hπ; while C do π od, θiòîãäà è òîëüêî òîãäà, êîãäà I |= C θ;WHILE0 : hwhile C do π od, θi −→I h∅, θiòîãäà è òîëüêî òîãäà, êîãäà I 6|= C θ.ÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌÎïðåäåëåíèå (îòíîøåíèÿ ïåðåõîäîâ)IF1 : hif C then π1 else π2 , θi −→I hπ1 , θiòîãäà è òîëüêî òîãäà, êîãäà I |= C θ;IF0 : hif C then π1 else π2 , θi −→I hπ2 , θiòîãäà è òîëüêî òîãäà, êîãäà I 6|= C θ;WHILE1 : hwhile C do π od, θi −→I hπ; while C do π od, θiòîãäà è òîëüêî òîãäà, êîãäà I |= C θ;WHILE0 : hwhile C do π od, θi −→I h∅, θiòîãäà è òîëüêî òîãäà, êîãäà I 6|= C θ.Îòíîøåíèå ïåðåõîäîâ −→I îïðåäåëÿåò, êàê èçìåíÿåòñÿñîñòîÿíèå âû÷èñëåíèÿ çà îäèí øàã ðàáîòû èíòåðïðåòàòîðàèìïåðàòèâíûõ ïðîãðàìì.ÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌÎïðåäåëåíèå (âû÷èñëåíèÿ ïðîãðàììû)Ïóñòü π0 ýòî èìïåðàòèâíàÿ ïðîãðàììà, θ0 îöåíêàïåðåìåííûõ.ÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌÎïðåäåëåíèå (âû÷èñëåíèÿ ïðîãðàììû)Ïóñòü π0 ýòî èìïåðàòèâíàÿ ïðîãðàììà, θ0 îöåíêàïåðåìåííûõ.×àñòè÷íûì âû÷èñëåíèåì ïðîãðàììû π0 íà îöåíêå ïåðåìåííûõθ0 â èíòåðïðåòàöèè I íàçûâàåòñÿ ïîñëåäîâàòåëüíîñòü(êîíå÷íàÿ èëè áåñêîíå÷íàÿ) ñîñòîÿíèé âû÷èñëåíèÿhπ0 , θ0 i, hπ1 , θ1 i, .
. . , hπn−1 , θn−1 i, hπn , θn i, . . . ,â êîòîðîé äëÿ ëþáîãî n, n ≥ 1, âûïîëíÿåòñÿ îòíîøåíèåhπn−1 , θn−1 i −→I hπn , θn i.ÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌÎïðåäåëåíèå (âû÷èñëåíèÿ ïðîãðàììû)Ïóñòü π0 ýòî èìïåðàòèâíàÿ ïðîãðàììà, θ0 îöåíêàïåðåìåííûõ.×àñòè÷íûì âû÷èñëåíèåì ïðîãðàììû π0 íà îöåíêå ïåðåìåííûõθ0 â èíòåðïðåòàöèè I íàçûâàåòñÿ ïîñëåäîâàòåëüíîñòü(êîíå÷íàÿ èëè áåñêîíå÷íàÿ) ñîñòîÿíèé âû÷èñëåíèÿhπ0 , θ0 i, hπ1 , θ1 i, . .
. , hπn−1 , θn−1 i, hπn , θn i, . . . ,â êîòîðîé äëÿ ëþáîãî n, n ≥ 1, âûïîëíÿåòñÿ îòíîøåíèåhπn−1 , θn−1 i −→I hπn , θn i.Âû÷èñëåíèåì ïðîãðàììû π0 íà îöåíêå ïåðåìåííûõ θ0 âèíòåðïðåòàöèè I íàçûâàåòñÿ âñÿêîå ìàêñèìàëüíîå ÷àñòè÷íîåâû÷èñëåíèå (âû÷èñëåíèå, êîòîðîå íåëüçÿ ïðîäîëæèòü).ÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌÏðèìåðÏóñòü I èíòåðïðåòàöèÿ ñèãíàòóðû σ = hConst, Func, Predi:Const = {0, 1, 2, . . . , }, Func = {+(2) , −(2) },Pred = {=(2) , >(2) , <(2) },ïðåäìåòíîé îáëàñòüþ êîòîðîé ÿâëÿåòñÿ ìíîæåñòâîíàòóðàëüíûõ ÷èñåë N0 ñ îáû÷íûìè àðèôìåòè÷åñêèìèîïåðàöèÿìè è îòíîøåíèÿìè.ÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌÏðèìåðÏóñòü I èíòåðïðåòàöèÿ ñèãíàòóðû σ = hConst, Func, Predi:Const = {0, 1, 2, .
. . , }, Func = {+(2) , −(2) },Pred = {=(2) , >(2) , <(2) },ïðåäìåòíîé îáëàñòüþ êîòîðîé ÿâëÿåòñÿ ìíîæåñòâîíàòóðàëüíûõ ÷èñåë N0 ñ îáû÷íûìè àðèôìåòè÷åñêèìèîïåðàöèÿìè è îòíîøåíèÿìè.Ðàññìîòðèì âû÷èñëåíèå ïðîãðàììûπ0 : while ¬(x = y )do if x > y then x ⇐ x − y else y ⇐ y − x odíà îöåíêå ïåðåìåííûõ θ0 = {x/4, y /6}.ÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌπ0 : while ¬(x = y )do if x > y then x ⇐ x − y else y ⇐ y − x odθ0 = {x/4, y /6}ÏðèìåðÊîììåíòàðèè:hπ0 , {x/4, y /6}iÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌπ0 : while ¬(x = y )do if x > y then x ⇐ x − y else y ⇐ y − x odθ0 = {x/4, y /6}ÏðèìåðÊîììåíòàðèè: WHILE1 , ò. ê. I |= ¬(4 = 6).hπ0 , {x/4, y /6}i↓Ihif x > y then x ⇐ x − y else y ⇐ y − x ; π0 , {x/4, y /6}iÎÏÅÐÀÖÈÎÍÍÀß ÑÅÌÀÍÒÈÊÀ ÏÐÎÃÐÀÌÌπ0 : while ¬(x = y )do if x > y then x ⇐ x − y else y ⇐ y − x odθ0 = {x/4, y /6}ÏðèìåðÊîììåíòàðèè: IF0 , ò. ê.
