Лекция 2. Общие принципы дедуктивной верификации программ. Логика Хоара, страница 4
Описание файла
PDF-файл из архива "Лекция 2. Общие принципы дедуктивной верификации программ. Логика Хоара", который расположен в категории "". Всё это находится в предмете "математические методы верификации схем и программ" из 10 семестр (2 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст 4 страницы из PDF
ψ0 = wpr (y ⇐ y − x; x ⇐ x + y ; y ⇐ x − y , ψ) =ÀÂÒÎÌÀÒÈ×ÅÑÊÀß ÏÐÎÂÅÐÊÀÏÐÀÂÈËÜÍÎÑÒÈ ÏÐÎÃÐÀÌÌÏðèìåð1. ψ0 = wpr (y ⇐ y − x; x ⇐ x + y ; y ⇐ x − y , ψ) =wpr (y ⇐ y − x, wpr (x ⇐ x + y , wpr (y ⇐ x − y , ψ))) =ÀÂÒÎÌÀÒÈ×ÅÑÊÀß ÏÐÎÂÅÐÊÀÏÐÀÂÈËÜÍÎÑÒÈ ÏÐÎÃÐÀÌÌÏðèìåð1. ψ0 = wpr (y ⇐ y − x; x ⇐ x + y ; y ⇐ x − y , ψ) =wpr (y ⇐ y − x, wpr (x ⇐ x + y , wpr (y ⇐ x − y , ψ))) =wpr (y ⇐ y − x, wpr (x ⇐ x + y , ψ{y /x − y })) =ÀÂÒÎÌÀÒÈ×ÅÑÊÀß ÏÐÎÂÅÐÊÀÏÐÀÂÈËÜÍÎÑÒÈ ÏÐÎÃÐÀÌÌÏðèìåð1.
ψ0 = wpr (y ⇐ y − x; x ⇐ x + y ; y ⇐ x − y , ψ) =wpr (y ⇐ y − x, wpr (x ⇐ x + y , wpr (y ⇐ x − y , ψ))) =wpr (y ⇐ y − x, wpr (x ⇐ x + y , ψ{y /x − y })) =wpr (y ⇐ y − x, ψ{y /x − y }{x/x + y }) =ÀÂÒÎÌÀÒÈ×ÅÑÊÀß ÏÐÎÂÅÐÊÀÏÐÀÂÈËÜÍÎÑÒÈ ÏÐÎÃÐÀÌÌÏðèìåð1. ψ0 = wpr (y ⇐ y − x; x ⇐ x + y ; y ⇐ x − y , ψ) =wpr (y ⇐ y − x, wpr (x ⇐ x + y , wpr (y ⇐ x − y , ψ))) =wpr (y ⇐ y − x, wpr (x ⇐ x + y , ψ{y /x − y })) =wpr (y ⇐ y − x, ψ{y /x − y }{x/x + y }) =ψ{y /x − y }{x/x + y }{y /y − x} =ÀÂÒÎÌÀÒÈ×ÅÑÊÀß ÏÐÎÂÅÐÊÀÏÐÀÂÈËÜÍÎÑÒÈ ÏÐÎÃÐÀÌÌÏðèìåð1. ψ0 = wpr (y ⇐ y − x; x ⇐ x + y ; y ⇐ x − y , ψ) =wpr (y ⇐ y − x, wpr (x ⇐ x + y , wpr (y ⇐ x − y , ψ))) =wpr (y ⇐ y − x, wpr (x ⇐ x + y , ψ{y /x − y })) =wpr (y ⇐ y − x, ψ{y /x − y }{x/x + y }) =ψ{y /x − y }{x/x + y }{y /y − x} =ψ{x/x + (y − x), y /(x + (y − x)) − (y − x)} =ÀÂÒÎÌÀÒÈ×ÅÑÊÀß ÏÐÎÂÅÐÊÀÏÐÀÂÈËÜÍÎÑÒÈ ÏÐÎÃÐÀÌÌÏðèìåð1.
ψ0 = wpr (y ⇐ y − x; x ⇐ x + y ; y ⇐ x − y , ψ) =wpr (y ⇐ y − x, wpr (x ⇐ x + y , wpr (y ⇐ x − y , ψ))) =wpr (y ⇐ y − x, wpr (x ⇐ x + y , ψ{y /x − y })) =wpr (y ⇐ y − x, ψ{y /x − y }{x/x + y }) =ψ{y /x − y }{x/x + y }{y /y − x} =ψ{x/x + (y − x), y /(x + (y − x)) − (y − x)} =(x = u2 ∧ y = u1 ){x/x + (y − x), y /(x + (y − x)) − (y − x)} =ÀÂÒÎÌÀÒÈ×ÅÑÊÀß ÏÐÎÂÅÐÊÀÏÐÀÂÈËÜÍÎÑÒÈ ÏÐÎÃÐÀÌÌÏðèìåð1. ψ0 = wpr (y ⇐ y − x; x ⇐ x + y ; y ⇐ x − y , ψ) =wpr (y ⇐ y − x, wpr (x ⇐ x + y , wpr (y ⇐ x − y , ψ))) =wpr (y ⇐ y − x, wpr (x ⇐ x + y , ψ{y /x − y })) =wpr (y ⇐ y − x, ψ{y /x − y }{x/x + y }) =ψ{y /x − y }{x/x + y }{y /y − x} =ψ{x/x + (y − x), y /(x + (y − x)) − (y − x)} =(x = u2 ∧ y = u1 ){x/x + (y − x), y /(x + (y − x)) − (y − x)} =x + (y − x) = u2 ∧ (x + (y − x)) − (y − x) = u1 ) ≡I0ÀÂÒÎÌÀÒÈ×ÅÑÊÀß ÏÐÎÂÅÐÊÀÏÐÀÂÈËÜÍÎÑÒÈ ÏÐÎÃÐÀÌÌÏðèìåð1.
ψ0 = wpr (y ⇐ y − x; x ⇐ x + y ; y ⇐ x − y , ψ) =wpr (y ⇐ y − x, wpr (x ⇐ x + y , wpr (y ⇐ x − y , ψ))) =wpr (y ⇐ y − x, wpr (x ⇐ x + y , ψ{y /x − y })) =wpr (y ⇐ y − x, ψ{y /x − y }{x/x + y }) =ψ{y /x − y }{x/x + y }{y /y − x} =ψ{x/x + (y − x), y /(x + (y − x)) − (y − x)} =(x = u2 ∧ y = u1 ){x/x + (y − x), y /(x + (y − x)) − (y − x)} =x + (y − x) = u2 ∧ (x + (y − x)) − (y − x) = u1 ) ≡I0y = u2 ∧ x = u1ÀÂÒÎÌÀÒÈ×ÅÑÊÀß ÏÐÎÂÅÐÊÀÏÐÀÂÈËÜÍÎÑÒÈ ÏÐÎÃÐÀÌÌÏðèìåð2. Àíàëîãè÷íîψ1 = wpr (x ⇐ x + y ; y ⇐ x − y ; x ⇐ x − y , ψ) ≡I0x = u1 ∧ y = u2ÀÂÒÎÌÀÒÈ×ÅÑÊÀß ÏÐÎÂÅÐÊÀÏÐÀÂÈËÜÍÎÑÒÈ ÏÐÎÃÐÀÌÌÏðèìåð2.
Àíàëîãè÷íîψ1 = wpr (x ⇐ x + y ; y ⇐ x − y ; x ⇐ x − y , ψ) ≡I0x = u1 ∧ y = u23. wpr (π, ψ) = (x > y ∧ ψ1 ) ∨ (¬(x > y ) ∧ ψ0 ) ≡(x = u1 ) ∧ (y = u2 ).ÀÂÒÎÌÀÒÈ×ÅÑÊÀß ÏÐÎÂÅÐÊÀÏÐÀÂÈËÜÍÎÑÒÈ ÏÐÎÃÐÀÌÌÏðèìåð2. Àíàëîãè÷íîψ1 = wpr (x ⇐ x + y ; y ⇐ x − y ; x ⇐ x − y , ψ) ≡I0x = u1 ∧ y = u23. wpr (π, ψ) = (x > y ∧ ψ1 ) ∨ (¬(x > y ) ∧ ψ0 ) ≡(x = u1 ) ∧ (y = u2 ).4. Î÷åâèäíî, |= ϕ → wpr (π, ψ).Çíà÷èò, π êîððåêòíàÿ ïðîãðàììà ïåðåàäðåñàöèè.ÀÂÒÎÌÀÒÈ×ÅÑÊÀß ÏÐÎÂÅÐÊÀÏÐÀÂÈËÜÍÎÑÒÈ ÏÐÎÃÐÀÌÌÍåóæåëè âñå òàê ïðîñòî?ÀÂÒÎÌÀÒÈ×ÅÑÊÀß ÏÐÎÂÅÐÊÀÏÐÀÂÈËÜÍÎÑÒÈ ÏÐÎÃÐÀÌÌÍåóæåëè âñå òàê ïðîñòî?Óâû, íåò.
Ãëàâíóþ òðóäíîñòü ïðåäñòàâëÿåò îïåðàòîð öèêëàwhile C do π od. Åäèíñòâåííûé ñïîñîá âåðèôèöèðîâàòü ýòîòîïåðàòîð ýòî âîñïîëüçîâàòüñÿ ïðîèçâîäíûì ïðàâèëîì:WHILE-GEN:ϕ {while C do π od} ψ.ϕ → χ, (χ&C ) {π} χ, (χ&¬C ) → ψÀÂÒÎÌÀÒÈ×ÅÑÊÀß ÏÐÎÂÅÐÊÀÏÐÀÂÈËÜÍÎÑÒÈ ÏÐÎÃÐÀÌÌÍåóæåëè âñå òàê ïðîñòî?Óâû, íåò. Ãëàâíóþ òðóäíîñòü ïðåäñòàâëÿåò îïåðàòîð öèêëàwhile C do π od. Åäèíñòâåííûé ñïîñîá âåðèôèöèðîâàòü ýòîòîïåðàòîð ýòî âîñïîëüçîâàòüñÿ ïðîèçâîäíûì ïðàâèëîì:WHILE-GEN:ϕ {while C do π od} ψ.ϕ → χ, (χ&C ) {π} χ, (χ&¬C ) → ψÝòî ïðàâèëî òðåáóåò ââåäåíèÿ âñïîìîãàòåëüíîé ôîðìóëû χ,êîòîðàÿ íàçûâàåòñÿ èíâàðèàíòîì öèêëà . Èíâàðèàíò öèêëàçàâèñèò îò òåëà öèêëà π è óñëîâèÿ C .Àâòîìàòè÷åñêàÿ ãåíåðàöèÿ èíâàðèàíòîâ öèêëà ýòî êëþ÷åâàÿçàäà÷à â ðåøåíèè ïðîáëåìû àâòîìàòè÷åñêîé âåðèôèêàöèèïðîãðàìì.ÊÎÍÅÖ ËÅÊÖÈÈ 2..