Ýëåìåíòû äîêàçàòåëüíîãî ïðîãðàììèðîâàíèÿ - ÷àñòü 2
íà÷ cls
ââîä (à, b, ñ) input a, b, ñ
åñëè à > b òî if à > b then
òàõ := a max = a
èíåc b > ñ òî elseif b > ñ then
òàõ := b màõ = b
èíåc ñ > à òî elseif ñ > a then
òàõ:= ñ màõ = ñ
êåñëè end if
âûâîä («òàõ=»,òàõ) ? «màõ=»; màõ
êîí end
Çàïóñê ýòîé ïðîãðàììû íà ÝÂÌ ìîæíî ïðîâåðèòü íà ñëåäóþùèõ äàííûõ:
Tecò1 Òåñò2 Òåñò3
? 1 1 2 ? 1 2 3 ? 3 2 1
max = 2 max = 3 max = 3
Âñå òðè ðåçóëüòàòà ïðàâèëüíûå. Îòëàäêó ïðîãðàììû ïîñëå çàïóñêà ýòèõ ïðèìåðîâ ìîæíî áûëî áû ñ÷èòàòü çàâåðøåííîé. Îäíàêî åñòü êîíòðïðèìåð:
Êîíòðïðèìåð1
? 2 1 3
max = 2
Íî ýòîò ðåçóëüòàò - íåïðàâèëüíûé. Ñëåäîâàòåëüíî, àëãîðèòì è ïðîãðàììà ñîäåðæàò îøèáêè. Íî ñêîëüêî ýòèõ îøèáîê - îäíà, äâå, à ìîæåò áûòü áîëüøå?
Ïðè äîêàçàòåëüíîì ïîäõîäå ðàçðàáîòêà àëãîðèòìîâ è ïðîãðàìì ïðåäïîëàãàåò ñîñòàâëåíèå ñïåöèôèêàöèé è äîêàçàòåëüñòâî èõ ïðàâèëüíîñòè ïî îòíîøåíèþ ê ýòèì ñïåöèôèêàöèÿì. Ïðîöåññ ðàçðàáîòêè ïðîãðàìì ñ÷èòàåòñÿ çàâåðøåííûì ïîñëå ïðîâåðêè èõ íà ÝÂÌ è ïðåäîñòàâëåíèè äîêàçàòåëüñòâ îòñóòñòâèÿ îøèáîê.
Äîêàçàòåëüñòâà ïðàâèëüíîñòè àëãîðèòìîâ è ïðîãðàìì, ðàâíî êàê è ëþáûå äðóãèå äîêàçàòåëüñòâà, ñòðîÿòñÿ íà îñíîâå ñóæäåíèé è ðàññóæäåíèé.