Лекция 2. Общие принципы дедуктивной верификации программ. Логика Хоара (1185524), страница 3
Текст из файла (страница 3)
. . }, {+, −, ×}, <, >, =, ≥, ≤i.Äëÿ ýòîãî äîñòàòî÷íî óñòàíîâèòü èñòèííîñòü â èíòåðïðåòàöèèI0 âñåõ ôîðìóë, ñòîÿùèõ â ëèñòüÿõ ïîñòðîåííîãî âûâîäà.ËÎÃÈÊÀ ÕÎÀÐÀÏðèìåðÏîêàæåì, ÷òî ïîñòðîåííûé âûâîä â ëîãèêå Õîàðà ÿâëÿåòñÿóñïåøíûì äëÿ ñòàíäàðòíîé àðèôìåòè÷åñêîé èíòåðïðåòàöèèI0 = hDI0 = {0, 1, 2, .
. . }, {+, −, ×}, <, >, =, ≥, ≤i.Äëÿ ýòîãî äîñòàòî÷íî óñòàíîâèòü èñòèííîñòü â èíòåðïðåòàöèèI0 âñåõ ôîðìóë, ñòîÿùèõ â ëèñòüÿõ ïîñòðîåííîãî âûâîäà.1. I0 |= ϕ(x, y , z) → ϕ(x, y , z)Î÷åâèäíî.ËÎÃÈÊÀ ÕÎÀÐÀÏðèìåðÏîêàæåì, ÷òî ïîñòðîåííûé âûâîä â ëîãèêå Õîàðà ÿâëÿåòñÿóñïåøíûì äëÿ ñòàíäàðòíîé àðèôìåòè÷åñêîé èíòåðïðåòàöèèI0 = hDI0 = {0, 1, 2, .
. . }, {+, −, ×}, <, >, =, ≥, ≤i.Äëÿ ýòîãî äîñòàòî÷íî óñòàíîâèòü èñòèííîñòü â èíòåðïðåòàöèèI0 âñåõ ôîðìóë, ñòîÿùèõ â ëèñòüÿõ ïîñòðîåííîãî âûâîäà.1. I0 |= ϕ(x, y , z) → ϕ(x, y , z)Î÷åâèäíî.2. I0 |= ϕ0 (x, y , z)&¬¬(x = y ) → (z = x), ò. å.I0 |= (x > 0)&(y > 0)&(x = y )&GCD(x, y , z) → (z = x).Âåðíî.ËÎÃÈÊÀ ÕÎÀÐÀÏðèìåð3. I0 |= ϕ0 (x, y , z)&¬(x = y )&(x > y ) →→ ϕ0 (x − y , y , z), ò. å.I0 |= (x > 0)&(y > 0)&(x > y )&GCD(x, y , z) →→ (x − y > 0)&(y > 0)&GCD(x − y , y , z).Âåðíî.ËÎÃÈÊÀ ÕÎÀÐÀÏðèìåð3. I0 |= ϕ0 (x, y , z)&¬(x = y )&(x > y ) →→ ϕ0 (x − y , y , z), ò. å.I0 |= (x > 0)&(y > 0)&(x > y )&GCD(x, y , z) →→ (x − y > 0)&(y > 0)&GCD(x − y , y , z).Âåðíî.4.
I0 |= ϕ0 (x, y , z)&¬(x = y )&¬(x > y ) →→ ϕ0 (x, y − x, z), ò. å.I0 |= (x > 0)&(y > 0)&(y > x)&GCD(x, y , z) →→ (x > 0)&(y − x > 0)&GCD(x, y − x, z).Âåðíî.5. I0 |= true.Î÷åâèäíî.ËÎÃÈÊÀ ÕÎÀÐÀÏðèìåð3. I0 |= ϕ0 (x, y , z)&¬(x = y )&(x > y ) →→ ϕ0 (x − y , y , z), ò. å.I0 |= (x > 0)&(y > 0)&(x > y )&GCD(x, y , z) →→ (x − y > 0)&(y > 0)&GCD(x − y , y , z).Âåðíî.4.
I0 |= ϕ0 (x, y , z)&¬(x = y )&¬(x > y ) →→ ϕ0 (x, y − x, z), ò. å.I0 |= (x > 0)&(y > 0)&(y > x)&GCD(x, y , z) →→ (x > 0)&(y − x > 0)&GCD(x, y − x, z).Âåðíî.5. I0 |= true.Î÷åâèäíî.Òàêèì îáðàçîì, âñå ëèñòîâûå ôîðìóëû âûâîäà èñòèííû âèíòåðïðåòàöèè I0 . Çíà÷èò, âûâîä òðèïëåòà ϕ0 {π0 } ψ0 ÿâëÿåòñÿóñïåøíûì âûâîäîì â èíòåðïðåòàöèè I0 .ËÎÃÈÊÀ ÕÎÀÐÀÒåîðåìà êîððåêòíîñòèÄëÿ ëþáîé èíòåðïðåòàöèè I è äëÿ ëþáîãî ïðàâèëà âûâîäàëîãèêè ÕîàðàΦ,Ψåñëè I |= Ψ,òî I |= Φ.I |= ϕ,Φ,ϕΦ,Ψ1 , Ψ2I |= Ψ1 ,I |= Ψ2 ,Φ,ϕ, Ψ, ψ I |= ϕ,I |= Ψ,I |= ψ,ËÎÃÈÊÀ ÕÎÀÐÀÒåîðåìà êîððåêòíîñòèÄëÿ ëþáîé èíòåðïðåòàöèè I è äëÿ ëþáîãî ïðàâèëà âûâîäàëîãèêè ÕîàðàΦ,Ψåñëè I |= Ψ,I |= ϕ,Φ,ϕΦ,Ψ1 , Ψ2I |= Ψ1 ,I |= Ψ2 ,Φ,ϕ, Ψ, ψ I |= ϕ,I |= Ψ,I |= ψ,òî I |= Φ.Äîêàçàòåëüñòâî.Ðàññìîòðèì ïîî÷åðåäíî âñå ïðàâèëà âûâîäà ëîãèêè Õîàðà.ËÎÃÈÊÀ ÕÎÀÐÀÄîêàçàòåëüñòâî.Ïðàâèëîϕ{x/t} {x ⇐ t} ϕASS:.trueÏîêàæåì, ÷òî â ëþáîé èíòåðïðåòàöèè I âåðíîI |= ϕ{x/t} {x ⇐ t} ϕ.(∗)Ïóñòü θ ïðîèçâîëüíàÿ îöåíêà ïåðåìåííûõ, è ïóñòüI |= ϕ{x/t}θ.Òîãäà ñîãëàñíî îïåðàöèîííîé ñåìàíòèêå èìïåðàòèâíûõïðîãðàìì èìååòñÿ åäèíñòâåííîå âû÷èñëåíèåhx ⇐ t, θi −→I h∅, ηi,è ïðè ýòîì η = {x/t}θ.Î÷åâèäíî, I |= ϕη , è ýòî äîêàçûâàåò (∗).ËÎÃÈÊÀ ÕÎÀÐÀÄîêàçàòåëüñòâî.Äëÿ îñòàëüíûõ ïðàâèë äîêàçàòåëüñòâî êîððåêòíîñòèïðîâîäèòñÿ ïî òîé æå ñõåìå.ËÎÃÈÊÀ ÕÎÀÐÀÄîêàçàòåëüñòâî.Äëÿ îñòàëüíûõ ïðàâèë äîêàçàòåëüñòâî êîððåêòíîñòèïðîâîäèòñÿ ïî òîé æå ñõåìå.Ñëåäñòâèå.Åñëè òðèïëåò ϕ{π}ψ èìååò óñïåøíûé â èíòåðïðåòàöèè I âûâîä,òî ïðîãðàììà π ÷àñòè÷íî êîððåêòíà â èíòåðïðåòàöèè Iîòíîñèòåëüíî ïðåäóñëîâèÿ ϕ è ïîñòóñëîâèÿ ψ . ÷àñòíîñòè, ýòî îçíà÷àåò, ÷òî èññëåäîâàííàÿ íàìè ïðîãðàììàâû÷èñëåíèÿ íàèáîëüøåãî îáùåãî ÷àñòè÷íî êîððåêòíà âàðèôìåòè÷åñêîé èíòåðïðåòàöèè I0 .ÀÂÒÎÌÀÒÈ×ÅÑÊÀß ÏÐÎÂÅÐÊÀÏÐÀÂÈËÜÍÎÑÒÈ ÏÐÎÃÐÀÌÌÊàê àâòîìàòèçèðîâàòü âåðèôèêàöèþ ïðîãðàìì?Äëÿ ýòîãî íóæíî âûÿñíèòü1.
Ïîëíà ëè ñèñòåìà ïðàâèë âûâîäà ëîãèêè Õîàðà?2. Ñóùåñòâóåò ëè àëãîðèòì ïîñòðîåíèÿ óñïåøíîãî âûâîäà?ÀÂÒÎÌÀÒÈ×ÅÑÊÀß ÏÐÎÂÅÐÊÀÏÐÀÂÈËÜÍÎÑÒÈ ÏÐÎÃÐÀÌÌÂîïðîñ î ïîëíîòå ïðàâèë âûâîäà Õîàðà.Íà ñàìîì äåëå, çäåñü íå îäèí, à òðè âîïðîñà.ÀÂÒÎÌÀÒÈ×ÅÑÊÀß ÏÐÎÂÅÐÊÀÏÐÀÂÈËÜÍÎÑÒÈ ÏÐÎÃÐÀÌÌÂîïðîñ î ïîëíîòå ïðàâèë âûâîäà Õîàðà.Íà ñàìîì äåëå, çäåñü íå îäèí, à òðè âîïðîñà.1. Âåðíî ëè, ÷òî äëÿ êàæäîé èíòåðïðåòàöèè I ñóùåñòâóåòñèñòåìà ïðàâèë âûâîäà, ïîçâîëÿþùàÿ äëÿ êàæäîãî òðèïëåòàΦ = ϕ{π}ψ ïîñòðîèòü óñïåøíûé âûâîä òðèïëåòà Φ âèíòåðïðåòàöèè I è äîêàçàòü åãî óñïåøíîñòü â ñëó÷àå I |= Φ?ÀÂÒÎÌÀÒÈ×ÅÑÊÀß ÏÐÎÂÅÐÊÀÏÐÀÂÈËÜÍÎÑÒÈ ÏÐÎÃÐÀÌÌÂîïðîñ î ïîëíîòå ïðàâèë âûâîäà Õîàðà.Íà ñàìîì äåëå, çäåñü íå îäèí, à òðè âîïðîñà.1.
Âåðíî ëè, ÷òî äëÿ êàæäîé èíòåðïðåòàöèè I ñóùåñòâóåòñèñòåìà ïðàâèë âûâîäà, ïîçâîëÿþùàÿ äëÿ êàæäîãî òðèïëåòàΦ = ϕ{π}ψ ïîñòðîèòü óñïåøíûé âûâîä òðèïëåòà Φ âèíòåðïðåòàöèè I è äîêàçàòü åãî óñïåøíîñòü â ñëó÷àå I |= Φ?Îòâåò îòðèöàòåëüíûé . Ñëåäóåò èç òåîðåìû Ãåäåëÿ î íåïîëíîòåâñÿêîé ðåêóðñèâíî ïåðå÷èñëèìîé ñèñòåìû àêñèîì àðèôìåòèêèíàòóðàëüíûõ ÷èñåë.ÀÂÒÎÌÀÒÈ×ÅÑÊÀß ÏÐÎÂÅÐÊÀÏÐÀÂÈËÜÍÎÑÒÈ ÏÐÎÃÐÀÌÌÂîïðîñ î ïîëíîòå ïðàâèë âûâîäà Õîàðà.À ÷òîáû áûëî ñîâñåì ïîíÿòíî, ïîïðîáóéòå óáåäèòüñÿ ñàìè, ÷òîäîêàçàòåëüñòâî êîððåêòíîñòè ïðîãðàììûπ : if x ∗ ∗n + y ∗ ∗n = z ∗ ∗n then u ⇐ 0 else u ⇐ 1 îòíîñèòåëüíî ïðåäóñëîâèÿϕ = (x > 0)&(y > 0)&(z > 0)&(n > 2)è ïîñòóñëîâèÿψ = (u > 0)ðàâíîñèëüíî äîêàçàòåëüñòâó Âåëèêîé Òåîðåìû Ôåðìà,ðàçîáðàòüñÿ â êîòîðîì ïîä ñèëó ëèøü î÷åíü íåìíîãèììàòåìàòèêàìÀÂÒÎÌÀÒÈ×ÅÑÊÀß ÏÐÎÂÅÐÊÀÏÐÀÂÈËÜÍÎÑÒÈ ÏÐÎÃÐÀÌÌÂîïðîñ î ïîëíîòå ïðàâèë âûâîäà Õîàðà.2.
Âåðíî ëè, ÷òî äëÿ êàæäîé èíòåðïðåòàöèè I ñóùåñòâóåòñèñòåìà ïðàâèë âûâîäà, ïîçâîëÿþùàÿ äëÿ êàæäîãî òðèïëåòàΦ = ϕ{π}ψ ïîñòðîèòü óñïåøíûé âûâîä Φ â èíòåðïðåòàöèè I(íî íå ãàðàíòèðóþùàÿ äîêàçàòåëüñòâà åãî óñïåøíîñòè) âñëó÷àå I |= Φ?ÀÂÒÎÌÀÒÈ×ÅÑÊÀß ÏÐÎÂÅÐÊÀÏÐÀÂÈËÜÍÎÑÒÈ ÏÐÎÃÐÀÌÌÂîïðîñ î ïîëíîòå ïðàâèë âûâîäà Õîàðà.2. Âåðíî ëè, ÷òî äëÿ êàæäîé èíòåðïðåòàöèè I ñóùåñòâóåòñèñòåìà ïðàâèë âûâîäà, ïîçâîëÿþùàÿ äëÿ êàæäîãî òðèïëåòàΦ = ϕ{π}ψ ïîñòðîèòü óñïåøíûé âûâîä Φ â èíòåðïðåòàöèè I(íî íå ãàðàíòèðóþùàÿ äîêàçàòåëüñòâà åãî óñïåøíîñòè) âñëó÷àå I |= Φ?Îòâåò îòðèöàòåëüíûé .
Áàçîâûå ïðåäèêàòû ñèãíàòóðû σ ìîãóòáûòü íåäîñòàòî÷íî âûðàçèòåëüíûìè äëÿ ïðåäñòàâëåíèÿ âñåõòåõ îòíîøåíèé ìåæäó ïåðåìåííûìè ïðîãðàììû, êîòîðûåíóæíû äëÿ ïîñòðîåíèÿ óñïåøíîãî âûâîäà. ðåçóëüòàòå íå íàéäåòñÿ íóæíûõ ôîðìóë ϕ0 , ψ 0 äëÿïðèìåíåíèÿ ïðàâèëàϕ{π}ψCONS:.ϕ → ϕ0 , ϕ0 {π}ψ 0 , ψ 0 → ψÀÂÒÎÌÀÒÈ×ÅÑÊÀß ÏÐÎÂÅÐÊÀÏÐÀÂÈËÜÍÎÑÒÈ ÏÐÎÃÐÀÌÌÂîïðîñ î ïîëíîòå ïðàâèë âûâîäà Õîàðà.3. Âåðíî ëè, ÷òî äëÿ íåêîòîðûõ èíòåðïðåòàöèé I ñóùåñòâóåòñèñòåìà ïðàâèë âûâîäà Õîàðà, êîòîðàÿ ïîçâîëÿåò äëÿ êàæäîãîòðèïëåòà Φ = ϕ{π}ψ ïîñòðîèòü óñïåøíûé âûâîä Φ âèíòåðïðåòàöèè I â ñëó÷àå I |= Φ?ÀÂÒÎÌÀÒÈ×ÅÑÊÀß ÏÐÎÂÅÐÊÀÏÐÀÂÈËÜÍÎÑÒÈ ÏÐÎÃÐÀÌÌÂîïðîñ î ïîëíîòå ïðàâèë âûâîäà Õîàðà.3.
Âåðíî ëè, ÷òî äëÿ íåêîòîðûõ èíòåðïðåòàöèé I ñóùåñòâóåòñèñòåìà ïðàâèë âûâîäà Õîàðà, êîòîðàÿ ïîçâîëÿåò äëÿ êàæäîãîòðèïëåòà Φ = ϕ{π}ψ ïîñòðîèòü óñïåøíûé âûâîä Φ âèíòåðïðåòàöèè I â ñëó÷àå I |= Φ?Îòâåò ïîëîæèòåëüíûé . Äîñòàòî÷íî, ÷òîáû äëÿ ëþáîãî öèêëàπ = while C do π 0 od ñóùåñòâîâàë òàêîé òåðì tπ , ÷òî äëÿëþáîé îöåíêè ïåðåìåííûõ θ çíà÷åíèå òåðìà tπ θ ðàâíî n + 1òîãäà è òîëüêî òîãäà, êîãäà öèêë π â âû÷èñëåíèè hπ, θiñîâåðøàåò n èòåðàöèé.ÀÂÒÎÌÀÒÈ×ÅÑÊÀß ÏÐÎÂÅÐÊÀÏÐÀÂÈËÜÍÎÑÒÈ ÏÐÎÃÐÀÌÌ×òî íóæíî äëÿ ïîñòðîåíèÿ óñïåøíîãî âûâîäà?ÀÂÒÎÌÀÒÈ×ÅÑÊÀß ÏÐÎÂÅÐÊÀÏÐÀÂÈËÜÍÎÑÒÈ ÏÐÎÃÐÀÌÌ×òî íóæíî äëÿ ïîñòðîåíèÿ óñïåøíîãî âûâîäà?IÍåîáõîäèìî èìåòü ýôôåêòèâíûé ïðóâåð äëÿ ïðîâåðêèèñòèííîñòè ôîðìóë â ðàçíûõ èíòåðïðåòàöèÿõ:I |= ϕ .ÀÂÒÎÌÀÒÈ×ÅÑÊÀß ÏÐÎÂÅÐÊÀÏÐÀÂÈËÜÍÎÑÒÈ ÏÐÎÃÐÀÌÌ×òî íóæíî äëÿ ïîñòðîåíèÿ óñïåøíîãî âûâîäà?IÍåîáõîäèìî èìåòü ýôôåêòèâíûé ïðóâåð äëÿ ïðîâåðêèèñòèííîñòè ôîðìóë â ðàçíûõ èíòåðïðåòàöèÿõ:I |= ϕ .IÍåîáõîäèìî âûðàáîòàòü ñòðàòåãèþ àâòîìàòè÷åñêîãîïîñòðîåíèÿ âûâîäà â ëîãèêå Õîàðà.
Íàèáîëüøóþ òðóäíîñòüñîçäàåò ïðàâèëîCONS:ϕ{π}ψ,ϕ → ϕ0 , ϕ0 {π}ψ 0 , ψ 0 → ψïîñêîëüêó íåÿñíî, êàêèå ôîðìóëû ϕ0 , ψ 0 íóæíî âûáèðàòü âêàæäîì ñëó÷àå.ÀÂÒÎÌÀÒÈ×ÅÑÊÀß ÏÐÎÂÅÐÊÀÏÐÀÂÈËÜÍÎÑÒÈ ÏÐÎÃÐÀÌÌÑòðàòåãèÿ âûâîäà â ëîãèêå Õîàðà.ÎïðåäåëåíèåÏóñòü çàäàíû èíòåðïðåòàöèÿ I , èìïåðàòèâíàÿ ïðîãðàììà π èïîñòóñëîâèå ψ . Òîãäà ôîðìóëà ϕ0 íàçûâàåòñÿ ñëàáåéøèìïðåäóñëîâèåì (weakest precondition) äëÿ ïðîãðàììû π èïîñòóñëîâèÿ ψ , åñëèÀÂÒÎÌÀÒÈ×ÅÑÊÀß ÏÐÎÂÅÐÊÀÏÐÀÂÈËÜÍÎÑÒÈ ÏÐÎÃÐÀÌÌÑòðàòåãèÿ âûâîäà â ëîãèêå Õîàðà.ÎïðåäåëåíèåÏóñòü çàäàíû èíòåðïðåòàöèÿ I , èìïåðàòèâíàÿ ïðîãðàììà π èïîñòóñëîâèå ψ . Òîãäà ôîðìóëà ϕ0 íàçûâàåòñÿ ñëàáåéøèìïðåäóñëîâèåì (weakest precondition) äëÿ ïðîãðàììû π èïîñòóñëîâèÿ ψ , åñëè1.
I |= ϕ0 {π}ψ ,ÀÂÒÎÌÀÒÈ×ÅÑÊÀß ÏÐÎÂÅÐÊÀÏÐÀÂÈËÜÍÎÑÒÈ ÏÐÎÃÐÀÌÌÑòðàòåãèÿ âûâîäà â ëîãèêå Õîàðà.ÎïðåäåëåíèåÏóñòü çàäàíû èíòåðïðåòàöèÿ I , èìïåðàòèâíàÿ ïðîãðàììà π èïîñòóñëîâèå ψ . Òîãäà ôîðìóëà ϕ0 íàçûâàåòñÿ ñëàáåéøèìïðåäóñëîâèåì (weakest precondition) äëÿ ïðîãðàììû π èïîñòóñëîâèÿ ψ , åñëè1. I |= ϕ0 {π}ψ ,2. äëÿ ëþáîé ôîðìóëû ϕ , åñëè I |= ϕ{π}ψ , òî I |= ϕ → ϕ0 .Ñëàáåéøåå ïðåäóñëîâèå äëÿ ïðîãðàììû π è ïîñòóñëîâèÿ ψóñëîâèìñÿ îáîçíà÷àòü wpr (π, ψ) .ÀÂÒÎÌÀÒÈ×ÅÑÊÀß ÏÐÎÂÅÐÊÀÏÐÀÂÈËÜÍÎÑÒÈ ÏÐÎÃÐÀÌÌÊàêàÿ ïîëüçà îò ñëàáåéøåãî ïðåäóñëîâèÿ?ÒåîðåìàI |= ϕ{π}ψ ⇐⇒I |= wpr (π, ψ){π}ψ,I |= ϕ → wpr (π, ψ).Òàêèì îáðàçîì, çàäà÷à ïîñòðîåíèÿ óñïåøíîãî âûâîäà ñâîäèòñÿê çàäà÷å âû÷èñëåíèÿ wpr (π, ψ).ÀÂÒÎÌÀÒÈ×ÅÑÊÀß ÏÐÎÂÅÐÊÀÏÐÀÂÈËÜÍÎÑÒÈ ÏÐÎÃÐÀÌÌÀ êàê âû÷èñëÿòü ñëàáåéøåå ïðåäóñëîâèå?Òåîðåìàwpr (x ⇐ t, ψ) = ψ{x/t},wpr (π1 ; π2 , ψ) = wpr (π1 , wpr (π2 , ψ)),wpr (if C then π1 else π2 fi, ψ) =C &wpr (π1 , ψ) ∨ ¬C &wpr (π2 , ψ),ÄîêàçàòåëüñòâîÑàìîñòîÿòåëüíî.Òàêèì îáðàçîì, äëÿ ìíîãèõ îïåðàòîðîâ (ïðîãðàìì) ñëàáåéøååïðåäóñëîâèå âû÷èñëÿåòñÿ àâòîìàòè÷åñêè.ÀÂÒÎÌÀÒÈ×ÅÑÊÀß ÏÐÎÂÅÐÊÀÏÐÀÂÈËÜÍÎÑÒÈ ÏÐÎÃÐÀÌÌÏðèìåðÏîêàæåì, ÷òî ïðîãðàììàπ:ifx>ythen x ⇐ x + y ; y ⇐ x − y ; x ⇐ x − yelse y ⇐ y − x; x ⇐ x + y ; y ⇐ x − yïðîâîäèò êîððåêòíóþ ïåðåàäðåñàöèþ äàííûõ.ÀÂÒÎÌÀÒÈ×ÅÑÊÀß ÏÐÎÂÅÐÊÀÏÐÀÂÈËÜÍÎÑÒÈ ÏÐÎÃÐÀÌÌÏðèìåðÏðåäóñëîâèå ϕ :Ïîñòóñëîâèå ψ :,x = u2 ∧ y = u1 ,x = u1 ∧ y = u2ÀÂÒÎÌÀÒÈ×ÅÑÊÀß ÏÐÎÂÅÐÊÀÏÐÀÂÈËÜÍÎÑÒÈ ÏÐÎÃÐÀÌÌÏðèìåðÏðåäóñëîâèå ϕ : x = u1 ∧ y = u2 ,Ïîñòóñëîâèå ψ : x = u2 ∧ y = u1 ,×òîáû óáåäèòüñÿ â êîððåêòíîñòè ïðîãðàììûäîñòàòî÷íîâû÷èñëèòü wpr (π, ψ) ,Ïðîâåðèòü âûïîëíèìîñòü I0 |= ϕ → wpr (π, ψ).ÀÂÒÎÌÀÒÈ×ÅÑÊÀß ÏÐÎÂÅÐÊÀÏÐÀÂÈËÜÍÎÑÒÈ ÏÐÎÃÐÀÌÌÏðèìåð1.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
