Лекция 2. Общие принципы дедуктивной верификации программ. Логика Хоара (1185524)

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла

Ìàòåìàòè÷åñêèåìåòîäûâåðèôèêàöèèïðîãðàìì è ñõåìËÅÊÒÎÐÛ:Âëàäèìèð Àíàòîëüåâè÷ Çàõàðîâ,Âëàäèñëàâ Âàñèëüåâè÷ ÏîäûìîâËåêöèÿ 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 , ò. ê.

Характеристики

Тип файла PDF

PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.

Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.

Список файлов лекций