22. Название проекта. Jil CSParser CSharpUtils Lucene.net SharpDevelop CodeContracts. Размер. 50 тыс. 60 тыс. 108 тыс. 256 тыс. 1213 тыс. 1534 тыс.


Чтобы посмотреть этот PDF файл с форматированием и разметкой, скачайте его и откройте на своем компьютере.
Íàïðàâàõðóêîïèñè
ÊîøåëåâÂëàäèìèðÊîíñòàíòèíîâè÷
ÌÅÆÏÐÎÖÅÄÓÐÍÛÉÑÒÀÒÈ×ÅÑÊÈÉÀÍÀËÈÇ
ÄËßÏÎÈÑÊÀÎØÈÁÎÊÂÈÑÕÎÄÍÎÌÊÎÄÅ
ÏÐÎÃÐÀÌÌÍÀßÇÛÊÅÑ#
Ñïåöèàëüíîñòü05.13.11
¾Ìàòåìàòè÷åñêîåèïðîãðàììíîåîáåñïå÷åíèåâû÷èñëèòåëüíûõ
ìàøèí,êîìïëåêñîâèêîìïüþòåðíûõñåòåé¿
Àâòîðåôåðàò
äèññåðòàöèèíàñîèñêàíèåó÷¼íîéñòåïåíè
êàíäèäàòàôèçèêî-ìàòåìàòè÷åñêèõíàóê
Ìîñêâà2017
ÐàáîòàâûïîëíåíàâÔåäåðàëüíîìãîñóäàðñòâåííîìáþäæåòíîìó÷ðåæäå
íèèíàóêèÈíñòèòóòñèñòåìíîãîïðîãðàììèðîâàíèÿÐîcñèéñêîéàêàäåìèè
íàóê.
Íàó÷íûéðóêîâîäèòåëü:
ÁåëåâàíöåâÀíäðåéÀíäðååâè÷
,êàíä.
ôèç.-ìàò.íàóê,âåäóùèéíàó÷íûéñîòðóäíèê
Îôèöèàëüíûåîïïîíåíòû:
ÃåðãåëüÂèêòîðÏàâëîâè÷,
äîêòîðòåõíè
÷åñêèõíàóê,ïðîôåññîð,äåêàíôàêóëüòåòà
âû÷èñëèòåëüíîéìàòåìàòèêèèêèáåðíåòèêè,
Íèæåãîðîäñêîãîãîñóäàðñòâåííîãîóíèâåðñè
òåòàèìåíèÍ.È.Ëîáà÷åâñêîãî,äèðåêòîðÍà
ó÷íî-èññëåäîâàòåëüñêîãîèíñòèòóòàïðèêëàä
íîéìàòåìàòèêèèêèáåðíåòèêè,ðóêîâîäèòåëü
Ïðèâîëæñêîãîíàó÷íî-îáðàçîâàòåëüíîãîÖåí
òðàñóïåðêîìïüþòåðíûõòåõíîëîãèé
ÏàâëîâÅâãåíèéÃåííàäüåâè÷,
êàíäèäàò
òåõíè÷åñêèõíàóê,ÎÎÎ"Èññëåäîâàòåëüñêèé
öåíòðÑàìñóíã",ñòàðøèéèíæåíåðïðîãðàì
ìèñò,ðóêîâîäèòåëüïðîåêòîâ
Âåäóùàÿîðãàíèçàöèÿ:Âû÷èñëèòåëüíûéöåíòðèì.À.À.Äîðîäíè
öûíàÔåäåðàëüíîãîèññëåäîâàòåëüñêîãîöåí
òðà¾Èíôîðìàòèêàèóïðàâëåíèå¿Ðîññèéñêîé
àêàäåìèèíàóê
Çàùèòàñîñòîèòñÿ25ìàÿ2017ã.â12:30íàçàñåäàíèèäèññåðòàöèîííîãî
ñîâåòàÄ002.087.01ïðèÈíñòèòóòåñèñòåìíîãîïðîãðàììèðîâàíèÿÐÀÍïî
àäðåñó:109004,Ìîñêâà,óë.À.Ñîëæåíèöûíà,ä.25.
ÑäèññåðòàöèåéìîæíîîçíàêîìèòüñÿâáèáëèîòåêåèíàñàéòåÔåäåðàëüíî
ãîãîñóäàðñòâåííîãîáþäæåòíîãîó÷ðåæäåíèÿíàóêèÈíñòèòóòñèñòåìíîãî
ïðîãðàììèðîâàíèÿÐîññèéñêîéàêàäåìèèíàóê.
Àâòîðåôåðàòðàçîñëàí¾¿àïðåëÿ2017ãîäà.
Ó÷åíûéñåêðåòàðü
äèññåðòàöèîííîãîñîâåòàÄ002.087.01,
êàíä.ôèç.-ìàò.íàóêÇåëåíîâÑ.Â.
Îáùàÿõàðàêòåðèñòèêàðàáîòû
Àêòóàëüíîñòüòåìû.
Íàðÿäóñòåñòèðîâàíèåìèäèíàìè÷åñêèìàíàëèçîì,ñòàòè÷åñêèéàíà
ëèçèñõîäíîãîêîäàøèðîêîèñïîëüçóåòñÿäëÿïîèñêàäåôåêòîââïðîãðàì
ìàõ.Ìíîãèåñîâðåìåííûåñòàíäàðòûñåðòèôèêàöèèòðåáóþò,÷òîáûïðî
ãðàììíîåîáåñïå÷åíèåáûëîïðîâåðåíîíàíàëè÷èåäåôåêòîâ,âòîì÷èñëå
ïðèïîìîùèèíñòðóìåíòîâñòàòè÷åñêîãîàíàëèçà.Íàïðèìåð,òàêèìñòàí
äàðòîìÿâëÿåòñÿÃÎÑÒÐ56939-2016äëÿðàçðàáîòêèáåçîïàñíîãîïðî
ãðàììíîãîîáåñïå÷åíèÿ,êîòîðûéíà÷àëäåéñòâîâàòüâÐÔ06.01.2017.
Îòñòàòè÷åñêèõàíàëèçàòîðîâäëÿïðèìåíåíèÿâïðîìûøëåííîìöèê
ëåðàçðàáîòêèòðåáóþòñÿ:âûñîêàÿñêîðîñòüàíàëèçà(íåáîëåå2-3÷àñîâ
äëÿïîëíîãîàíàëèçàïðîåêòîâèçíåñêîëüêèõìèëëèîíîâñòðîêêîäà);âûñî
êîåêà÷åñòâîàíàëèçà(âûñîêèéïðîöåíòèñòèííûõñðàáàòûâàíèé(50-70%)è
ïîääåðæêàïîèñêàïîïóëÿðíûõêëàññîâîøèáîê,âêëþ÷àþùàÿïîèñêòèïè÷
íûõîøèáî÷íûõñèòóàöèèâðàìêàõäàííûõêëàññîâ).Äëÿñîáëþäåíèÿýòèõ
òðåáîâàíèéñòàòè÷åñêèåàíàëèçàòîðûâûíóæäåííîèñïîëüçóþòíåñòðîãèé
àíàëèç,ïîçâîëÿþùèéäîñòè÷üêîìïðîìèññàìåæäóâðåìåíåìðàáîòû,êî
ëè÷åñòâîìïðîïóñêîâäåôåêòîâèïðîöåíòîìëîæíûõñðàáàòûâàíèé.Ïðè
ýòîìäëÿïîèñêàñëîæíûõìåæïðîöåäóðíûõäåôåêòîâíåîáõîäèìîèñïîëü
çîâàòüàíàëèçïðîãðàìì,ó÷èòûâàþùèéçàâèñèìîñòèïîäàííûì(÷óâñòâè
òåëüíîñòüêïîòîêó),óñëîâèÿïåðåõîäîâ(÷óâñòâèòåëüíîñòüêïóòÿì),êîí
òåêñòûâûçîâîâ(÷óâñòâèòåëüíîñòüêêîíòåêñòó)èðàáîòóñäèíàìè÷åñêîé
ïàìÿòüþ.
Âòå÷åíèåïîñëåäíèõäåñÿòèëåòÿçûêïðîãðàììèðîâàíèÿC
#
ñòàáèëü
íîâõîäèòâøåñòåðêóñàìûõðàñïðîñòðàíåííûõÿçûêîâïðîãðàììèðîâàíèÿ
ïðîâåðñèèTIOBE.Âíàñòîÿùèéìîìåíò÷óâñòâèòåëüíûéêêîíòåêñòó,ïî
òîêóèïóòÿìàíàëèçñöåëüþâûÿâëåíèÿäåôåêòîâäëÿÿçûêàïðîãðàììèðî
âàíèÿC
#
îñóùåñòâëÿþòëèøüçàêðûòûåêîììåð÷åñêèåèíñòðóìåíòû,äëÿ
êîòîðûõîòñóòñòâóåòäåòàëüíîåîïèñàíèåèñïîëüçóåìûõïîäõîäîâèàëãî
ðèòìîâ.Ñóùåñòâóþùèåîòêðûòûåðåøåíèÿäëÿïîèñêàäåôåêòîâîãðàíè
÷èâàþòñÿîáõîäîìàáñòðàêòíîãîñèíòàêñè÷åñêîãîäåðåâàèëèïðîñòûìâíóò
ðèïðîöåäóðíûìàíàëèçîì,íåïðîâîäÿäåòàëüíîãîàíàëèçàïîòîêîâóïðàâ
ëåíèÿèäàííûõ.
3
Ìåòîäûïðîâåäåíèÿñòàòè÷åñêîãîàíàëèçàïðîãðàììðàçðàáàòûâàþò
ñÿêàêâîìíîãèõíàó÷íûõöåíòðàõ,òàêèõêàêóíèâåðñèòåòÑòåíôîðä,óíè
âåðñèòåòÁåðêëè,óíèâåðñèòåòÁðèòàíñêîéÊîëóìáèè,ÈÑÏÐÀÍ,òàêèâ
ëàíñìåæäó÷èñëîìïðîïóñêîâîøèáîêèêîëè÷åñòâîìëîæíûõïðåäóïðå
æäåíèé.
Öåëèèçàäà÷èäèññåðòàöèîííîéðàáîòû:
ðàçðàáîòêàâíóòðèïðî
öåäóðíûõàëãîðèòìîâàíàëèçàèàëãîðèòìîâìåæïðîöåäóðíîãîàíàëèçà,
÷óâñòâèòåëüíûõêïîòîêó,êîíòåêñòóèïóòÿì,ìåòîäàîïðåäåëåíèÿêðèòå
ðèÿâûäà÷èïðåäóïðåæäåíèéîíàëè÷èèäåôåêòà,îáåñïå÷èâàþùèõïîèñê
äåôåêòîââèñõîäíîìêîäåïðîãðàìì,íàïèñàííûõíàÿçûêåC
#
.Ðàçðàáîòàí
íûåàëãîðèòìûäîëæíûîáåñïå÷èâàòüêà÷åñòâîàíàëèçà,ñîîòâåòñòâóþùåå
ñîâðåìåííûìòðåáîâàíèÿìäëÿïðîìûøëåííûõñòàòè÷åñêèõàíàëèçàòîðîâ,
âêëþ÷àÿìàñøòàáèðóåìîñòü,äîñòàòî÷íóþäëÿàíàëèçàïðîãðàìì,ñîñòîÿ
ùèõèçìèëëèîíîâñòðîêêîäà.
Äëÿäîñòèæåíèÿïîñòàâëåííûõöåëåéáûëèñôîðìóëèðîâàíûèðåøå
íûñëåäóþùèåçàäà÷è:
1.
Ðàçðàáîòêàâíóòðèïðîöåäóðíûõ÷óâñòâèòåëüíûõêïîòîêóèïóòÿì
àëãîðèòìîâàíàëèçà,ïîçâîëÿþùèõíàîñíîâåâû÷èñëåííîéèìèèí
ôîðìàöèèâûïîëíÿòüïîèñêøèðîêîãîêëàññàäåôåêòîâ;äîêàçà
òåëüñòâîêîððåêòíîñòèàëãîðèòìîâ.
2.
Ðàçðàáîòêàìåæïðîöåäóðíûõ÷óâñòâèòåëüíûõêïîòîêó,êîíòåêñòó
èïóòÿìàëãîðèòìîâàíàëèçà,âêëþ÷àþùèõàëãîðèòìïîñòðîåíèÿ
ðåçþìåìåòîäàïîðåçóëüòàòàìâíóòðèïðîöåäóðíîãîàíàëèçàèàë
ãîðèòìïðèìåíåíèÿðåçþìåâòî÷êàõâûçîâà.
3.
Ðàçðàáîòêàìåòîäàîïðåäåëåíèÿêðèòåðèÿâûäà÷èïðåäóïðåæäå
íèÿîíàëè÷èèäåôåêòàñó÷åòîìîñîáåííîñòåéïðîâîäèìîãîàíàëè
çà,ïîäõîäÿùåãîäëÿøèðîêîãîêëàññàäåôåêòîâ.Ðàçðàáîòêàêîí
êðåòíûõäåòåêòîðîâäëÿïðèâåäåííîãîêðèòåðèÿâûäà÷èïðåäóïðå
æäåíèÿ.
4.
Îöåíêàíàïðàêòèêåõàðàêòåðèñòèêïðåäëîæåííûõìåòîäîâèàë
ãîðèòìîâíàñîîòâåòñòâèåçàÿâëåííûìòðåáîâàíèÿì.
Íàó÷íàÿíîâèçíà.
Âðàáîòåáûëèïîëó÷åíûñëåäóþùèåðåçóëüòàòû,
îáëàäàþùèåíàó÷íîéíîâèçíîé:
1.
Ðàçðàáîòàíûàëãîðèòìûâíóòðèïðîöåäóðíîãîàíàëèçà,îáëàäàþ
ùèå÷óâñòâèòåëüíîñòüþêïîòîêóèïóòÿì,íåòåðÿþùèåèíôîð
ìàöèþâòî÷êàõîáúåäèíåíèÿ.
2.
Ðàçðàáîòàíûàëãîðèòìûìåæïðîöåäóðíîãîàíàëèçà,÷óâñòâèòåëü
íîãîêêîíòåêñòó,ïîòîêóèïóòÿì,îáîáùàþùèåðåçóëüòàòûâíóò
5
ðèïðîöåäóðíîãîàíàëèçàââèäåðåçþìåìåòîäà,èïðèìåíÿþùèå
ðåçþìåïðèîáðàáîòêåâûçîâàäàííîãîìåòîäà.
3.
Ðàçðàáîòàíìåòîäîïðåäåëåíèÿêðèòåðèÿâûäà÷èïðåäóïðåæäåíèé,
ó÷èòûâàþùèé÷óâñòâèòåëüíîñòüêïóòÿìïðèïîèñêåäåôåêòîâ,èñ
ïîëüçîâàíèåêîòîðîãîïîçâîëÿåòäîñòè÷üïðèåìëåìîãîóðîâíÿëîæ
íûõïðåäóïðåæäåíèé.
4.
Äîêàçàòåëüñòâàêîððåêòíîñòèïðåäëîæåííîãîàëãîðèòìàâíóòðè
ïðîöåäóðíîãîàíàëèçàèñîîòâåòñòâèÿðàçðàáîòàííûõäåòåêòîðîâ
âûáðàííîìóêðèòåðèþâûäà÷èïðåäóïðåæäåíèé.
Òåîðåòè÷åñêàÿèïðàêòè÷åñêàÿçíà÷èìîñòü.
Ïðåäëîæåíûàëãî
ðèòìû÷óâñòâèòåëüíîãîêïóòÿìâíóòðèïðîöåäóðíîãîèìåæïðîöåäóðíîãî
àíàëèçàäëÿçàäà÷èïîèñêàøèðîêîãîêëàññàäåôåêòîâ.Ðàçðàáîòàíìåòîä
îïðåäåëåíèÿêðèòåðèÿâûäà÷èïðåäóïðåæäåíèé,ó÷èòûâàþùèé÷óâñòâè
òåëüíîñòüêïóòÿì.
Âñåïðåäëîæåííûåàëãîðèòìûáûëèðåàëèçîâàíûâñòàòè÷åñêîìàíà
ëèçàòîðåSharpChecker.ÀíàëèçàòîðSharpCheckerïðåäïîëàãàåòïðîìûø
ëåííîåèñïîëüçîâàíèåïðèðàçðàáîòêåïðîãðàììíîãîîáåñïå÷åíèÿäëÿðàí
íåãîîáíàðóæåíèÿïðîãðàììíûõäåôåêòîâ.Äàííûéàíàëèçàòîðòàêæåìî
æåòáûòüèñïîëüçîâàíâñåðòèôèöèðóþùèõöåíòðàõäëÿîöåíêèêà÷å
ñòâàñåðòèôèöèðóåìîãîïðîãðàììíîãîîáåñïå÷åíèÿ.Ðàçðàáîòàííûéàíàëè
çàòîðSharpCheckerâíåäð¼íäëÿïðîìûøëåííîãîèñïîëüçîâàíèÿâêîìïà
íèèSamsung.
Ìåòîäîëîãèÿèìåòîäûèññëåäîâàíèé
.Ðåçóëüòàòûäèññåðòàöèè
áûëèïîëó÷åíûñèñïîëüçîâàíèåììåòîäîâèìîäåëåé,ïðèìåíÿåìûõïðè
ïðîâåäåíèèñòàòè÷åñêîãîàíàëèçà.Ìàòåìàòè÷åñêóþîñíîâóäàííîéðàáî
òûñîñòàâëÿþòòåîðèÿãðàôîâ,òåîðèÿìíîæåñòâ,ìàòåìàòè÷åñêàÿëîãèêà,
òåîðèÿàëãîðèòìîâ.
Îñíîâíûåïîëîæåíèÿ,âûíîñèìûåíàçàùèòó:
1.
àëãîðèòìâíóòðèïðîöåäóðíîãîàíàëèçà,îáëàäàþùèé÷óâñòâèòåëü
íîñòüþêïîòîêóèïóòÿì,ïðèýòîìíåòåðÿþùèéèíôîðìàöèþâ
òî÷êàõîáúåäèíåíèÿ;
2.
àëãîðèòììåæïðîöåäóðíîãîàíàëèçà,÷óâñòâèòåëüíîãîêêîíòåêñòó,
ïîòîêóèïóòÿì,îáîáùàþùèéðåçóëüòàòûâíóòðèïðîöåäóðíîãîàíà
ëèçàââèäåðåçþìåìåòîäàèïðèìåíÿþùèéðåçþìåïðèîáðàáîòêå
âûçîâàäàííîãîìåòîäà;
6
3.
ìåòîäîïðåäåëåíèÿêðèòåðèÿâûäà÷èïðåäóïðåæäåíèé,ó÷èòûâà
þùèé÷óâñòâèòåëüíîñòüêïóòÿìïðèïîèñêåäåôåêòîâ,èñïîëüçî
âàíèåêîòîðîãîïîçâîëÿåòäîñòè÷üïðèåìëåìîãîóðîâíÿëîæíûõ
ïðåäóïðåæäåíèé.
Àïðîáàöèÿðàáîòû.
Îñíîâíûåðåçóëüòàòûðàáîòûäîêëàäûâàëèñü
íàñëåäóþùèõêîíôåðåíöèÿõ:
1.
XXIÌåæäóíàðîäíàÿíàó÷íàÿêîíôåðåíöèÿñòóäåíòîâ,àñïèðàíòîâ
èìîëîäûõó÷¼íûõ¾Ëîìîíîñîâ-2014¿(Ìîñêâà,Ðîññèÿ2014);
2.
Âñåïðåäñòàâëåííûåâäèññåðòàöèèðåçóëüòàòûïî
ëó÷åíûëè÷íîàâòîðîì.
Ïóáëèêàöèè.
Îñíîâíûåðåçóëüòàòûïîòåìåäèññåðòàöèèèçëîæåíû
â6ïå÷àòíûõèçäàíèÿõ[
1

6
],5èçêîòîðûõèçäàíûâæóðíàëàõ,ðåêîìåí
äîâàííûõÂÀÊ.Âêëàäàâòîðàâðàáîòå[
2
]çàêëþ÷àåòñÿâðàçðàáîòêåàë
ãîðèòìîââíóòðèïðîöåäóðíîãîèìåæïðîöåäóðíîãîàíàëèçàèðàçðàáîòêå
äåòåêòîðàäëÿïîèñêàäîñòóïàêíóëåâîìóóêàçàòåëþ(
null
).Âñòàòüå[
3
]
âêëàäàâòîðàñîñòîèòâðàçðàáîòêåàëãîðèòìîâîïòèìèçàöèèðàçìåðàôîð
ìóëèðåàëèçàöèèèíôðàñòðóêòóðûèíñòðóìåíòàSharpChecker.Âðàáîòå[
4
]
âêëàäàâòîðàñîñòîèòâðàçðàáîòêåìåòîäàîïðåäåëåíèÿêðèòåðèÿâûäà÷è
ïðåäóïðåæäåíèé.Âïóáëèêàöèè[
5
]âêëàäàâòîðàçàêëþ÷àåòñÿâðàçðàáîòêå
ÿäðààíàëèçàïîìå÷åííûõäàííûõäëÿïðîãðàììíàÿçûêàõC/C++.
Ñòàòè÷åñêèéàíàëèçàòîðÿçûêàC
#
SharpChecker,âêîòîðîìðåàëè
çîâàíûïðåäëîæåííûåìåòîäûàíàëèçà,âêëþ÷åíâåäèíûéðååñòððîññèé
ñêèõïðîãðàììäëÿýëåêòðîííûõâû÷èñëèòåëüíûõìàøèíèáàçäàííûõïî
ÏðèêàçóÌèíêîìñâÿçèÐîññèèîò09.03.2017103,Ïðèëîæåíèå1,ïï.37,
ðååñòðîâûé2910.
Ñîäåðæàíèåðàáîòû
Âî
ââåäåíèè
îáîñíîâàíààêòóàëüíîñòüäèññåðòàöèîííîéðàáîòû,
ñôîðìóëèðîâàíàöåëüèàðãóìåíòèðîâàíàíàó÷íàÿíîâèçíàèññëåäîâàíèé,
7
ïîêàçàíàïðàêòè÷åñêàÿçíà÷èìîñòüïîëó÷åííûõðåçóëüòàòîâ,ïðåäñòàâëåíû
âûíîñèìûåíàçàùèòóíàó÷íûåïîëîæåíèÿ.
Âïåðâîéãëàâå
ðàññìàòðèâàåòñÿçàäà÷àïîèñêàîøèáîêâèñõîäíîì
êîäåïðîãðàììïðèïîìîùèìåòîäîâñòàòè÷åñêîãîàíàëèçà,èïðîèçâîäèòñÿ
îáçîðñóùåñòâóþùèõïîäõîäîâ.
Êëþ÷åâàÿñëîæíîñòüðàçðàáîòêèñòàòè÷åñêîãîàíàëèçàçàêëþ÷àåòñÿ
âïîèñêåêîìïðîìèññàìåæäóìàñøòàáèðóåìîñòüþ,êëàññîìîáíàðóæèâàå
ìûõîøèáîê,ïðîöåíòîìëîæíûõñðàáàòûâàíèéèïðîïóñêîìîøèáîêèäî
ïîëíèòåëüíûìèîãðàíè÷åíèÿìè,íàêëàäûâàåìûìèíààíàëèçèðóåìóþïðî
ãðàììó.Èäåàëüíûéñòàòè÷åñêèéàíàëèçàòîðäîëæåíõîðîøîìàñøòàáèðî
âàòüñÿ,îáíàðóæèâàòüâñåîøèáêèâðåìåíèâûïîëíåíèÿ,íåèìåòüëîæíûõ
ñðàáàòûâàíèéèïðîïóñêîâîøèáîêèïðèìåíÿòüñÿêîâñåìïðîãðàììàìáåç
îãðàíè÷åíèé.Ñîçäàíèåèäåàëüíîãîàíàëèçàòîðàíåâîçìîæíîâñèëóàëãî
ðèòìè÷åñêîéíåðàçðåøèìîñòèçàäà÷èïîòåîðåìåÐàéñà.
Âäàííîéðàáîòåðàññìàòðèâàåòñÿçàäà÷àïîèñêàäåôåêòîâ.Äîïîë
íèòåëüíûõîãðàíè÷åíèéíààíàëèçèðóåìûåïðîãðàììûíåíàêëàäûâàåòñÿ.
Çàäà÷ààíàëèçàïîèñêäåôåêòîââèñõîäíîìêîäå,ïðèâîäÿùèõêîøèáêàì
âðåìåíèâûïîëíåíèÿ.Äîïóñêàåòñÿíàëè÷èåëîæíûõñðàáàòûâàíèéèïðî
ïóñêîâîøèáîê.Ñëîæíîñòüðàçðàáîòêèçàêëþ÷àåòñÿâîáíàðóæåíèèïðàê
òè÷åñêèçíà÷èìîãîêëàññàîøèáîêïðèñîõðàíåíèèíèçêîãîïðîöåíòàëîæ
íûõñðàáàòûâàíèéèõîðîøåéìàñøòàáèðóåìîñòè.
Äàííàÿçàäà÷àðåøàëàñüâðÿäåíàó÷íî-èññëåäîâàòåëüñêèõèïðîìûø
ëåííûõèíñòðóìåíòîâ.Âäàííîéãëàâåðàññìàòðèâàþòñÿñëåäóþùèåíà
ó÷íî-èññëåäîâàòåëüñêèåèíñòðóìåíòûäëÿàíàëèçàïðîãðàììíàC/C++:
Prex,Saturn,Varvel.Êñîæàëåíèþ,ïóáëèêàöèèíàòåìóîðãàíèçàöèèìåæ
ïðîöåäóðíîãî÷óâñòâèòåëüíîãîêïóòÿìñòàòè÷åñêîãîàíàëèçàäëÿÿçûêà
C
#
,ðåøàþùåãîçàäà÷óïîèñêàäåôåêòîâ,îòñóòñòâóþò.Èçïðîìûøëåííûõ
ñòàòè÷åñêèõàíàëèçàòîðîâ,ïîääåðæèâàþùèõàíàëèçïðîãðàììíàÿçûêå
C
#
,ðàññìàòðèâàþòñÿCoverity,Klocwork,PVS-Studio,ReSharper.
Âðåçóëüòàòåàíàëèçàâîçìîæíîñòåéïðèâåäåííûõâûøåèíñòðóìåí
òîâäåëàåòñÿâûâîä,÷òîäëÿñîçäàíèÿìàñøòàáèðóåìîãîèíñòðóìåíòàñòà
òè÷åñêîãîàíàëèçàíåîáõîäèìîèñïîëüçîâàòü÷óâñòâèòåëüíûéêïóòÿìâíóò
ðèïðîöåäóðíûéàíàëèçâêîìáèíàöèèñìåæïðîöåäóðíûìàíàëèçîì,îñíî
âàííûìíàðåçþìå.
8
ÈíñòðóìåíòSvace,ðàçðàáîòàííûéâÈíñòèòóòåñèñòåìíîãîïðîãðàì
ìèðîâàíèÿÐÀÍ,ïîääåðæèâàåòìåæïðîöåäóðíûéàíàëèçíàîñíîâåðåçþìå,
îäíàêîïîääåðæêà÷óâñòâèòåëüíîñòèêïóòÿìîñòàâëåíàíàóñìîòðåíèåðàç
ðàáîò÷èêàäåòåêòîðà.Âäàííîéðàáîòåðàññìàòðèâàþòñÿìåæïðîöåäóðíûé
àíàëèç,ïîëíîñòüþ÷óâñòâèòåëüíûéêïóòÿì,èìåòîäîïðåäåëåíèÿêðèòå
ðèÿâûäà÷èïðåäóïðåæäåíèÿîáîøèáêå.
Âîâòîðîéãëàâå
ðàññìàòðèâàþòñÿîñîáåííîñòèàíàëèçàÿçûêàC
#
,
àòàêæåââîäèòñÿâíóòðåííååïðåäñòàâëåíèåäëÿïðîãðàììíàÿçûêåC
#
.
ßçûêïðîãðàììèðîâàíèÿC
#
îáúåêòíî-îðèåíòèðîâàííûéñòàòè÷å
ñêèòèïèçèðîâàííûéÿçûêâûñîêîãîóðîâíÿ.ÊîìïàíèÿMicrosoftàêòèâíî
ðàçâèâàåòÿçûêC
#
,âûïóñêàÿíîâóþâåðñèþêàæäûåäâà-òðèãîäà.Ñêàæ
äîéíîâîéâåðñèåéâÿçûêC
#
äîáàâëÿþòñÿíîâûåÿçûêîâûåâîçìîæíîñòè,
÷òîòðåáóåòîòèíñòðóìåíòîâñòàòè÷åñêîãîàíàëèçààäàïòèðîâàòüñÿêíèì.
Âäàííîéðàáîòåïîääåðæèâàþòñÿñëåäóþùèåâîçìîæíîñòè:äèíàìè÷åñêàÿ
ïàìÿòü,äèíàìè÷åñêàÿïðîâåðêàòèïà,èñêëþ÷åíèÿ,êîíñòðóêöèèóïðàâëå
íèÿðåñóðñàìè.×àñòè÷íîïîääåðæèâàþòñÿ:êîñâåííûåâûçîâû,ìíîãîïîòî÷
íîñòü,çàìûêàíèÿ,Linq-âûðàæåíèÿ.Íåðàññìàòðèâàåòñÿïîääåðæêàíåáåç
îïàñíûõñåêöèéèîòðàæåíèé.
Âêà÷åñòâåâíóòðåííåãîïðåäñòàâëåíèÿïðåäëàãàåòñÿèñïîëüçîâàòüíà
áîðãðàôîâïîòîêàóïðàâëåíèÿ(ÃÏÓ)äëÿàíàëèçèðóåìûõìåòîäîâ.
ÃÏÓñîñòîèòèçáàçîâûõáëîêîâ,ñîåäèí¼ííûõð¼áðàìè.Êàæäûéáàçî
âûéáëîêñîäåðæèòïîñëåäîâàòåëüíîñòüèíñòðóêöèé.Êàæäîéèíñòðóêöèè
ñîîòâåòñòâóåòäîïîëíèòåëüíàÿëîêàëüíàÿïåðåìåííàÿ,çíà÷åíèåêîòîðîé
ðàâíîðåçóëüòàòóâûïîëíåíèÿýòîéèíñòðóêöèè.Còî÷êèçðåíèÿÿçûêàC
#
,
äîïîëíèòåëüíûåëîêàëüíûåïåðåìåííûåñîîòâåòñòâóþòðåçóëüòàòàìâû÷èñ
ëåíèÿâûðàæåíèé.Äîïîëíèòåëüíûåëîêàëüíûåïåðåìåííûåìîãóòáûòüèñ
ïîëüçîâàíûâáàçîâûõáëîêàõ,äîìèíèðóåìûõáàçîâûìáëîêîì,ñîäåðæà
ùèìèíñòðóêöèþ.Ïåðåîïðåäåëåíèåäîïîëíèòåëüíûõëîêàëüíûõïåðåìåí
íûõíåäîïóñòèìî.
Êðîìåäîïîëíèòåëüíûõëîêàëüíûõïåðåìåííûõ,äëÿâñåãîÃÏÓîïðå
äåë¼ííàáîðïàðàìåòðîâìåòîäàèíàáîðëîêàëüíûõïåðåìåííûõ.Òèïïàðà
ìåòðîâçàäàíïðîòîòèïîììåòîäàâñîîòâåòñòâóþùåìêëàññå.Òèïëîêàëü
íûõïåðåìåííûõîïðåäåëÿåòñÿïîòèïóïåðåìåííûõ,êîòîðûìèîíèèíèöè
àëèçèðóþòñÿ.
9
Âäàííîéðàáîòåðàññìàòðèâàþòñÿñëåäóþùèåèíñòðóêöèèâíóòðåí
íåãîïðåäñòàâëåíèÿ:
val
:=
a:f
;
÷òåíèåïîëÿ
(1)
val
:=
a
[
i
];
÷òåíèåýëåìåíòàìàññèâà
(2)
val
:=
a
O
b
íåêîòîðàÿáèíàðíàÿîïåðàöèÿ
(3)
val
:=
O
a
íåêîòîðàÿóíàðíàÿîïåðàöèÿ
(4)
val
:=
a:f
=
b
;
çàïèñüâïîëå
(5)
val
:=
a
=
b
;
çàïèñüâëîêàëüíóþïåðåìåííóþ
(6)
val
:=
const
;
îïðåäåëåíèåêîíñòàíòû
(7)
val
:=
foo
(
params
);
âûçîâìåòîäà
(8)
ðàññìàòðèâàåòñÿâîïðîñèñïîëüçîâàíèÿñèìâîëüíî
ãîâûïîëíåíèÿäëÿïðîâåäåíèÿ÷óâñòâèòåëüíîãîêïóòÿìèêïîòîêóâíóò
ðèïðîöåäóðíîãîàíàëèçà.
Ïðèñèìâîëüíîìâûïîëíåíèèáóäåìñ÷èòàòü,÷òîêàæäûéìåòîäÿâ
ëÿåòñÿòî÷êîéâõîäàâïðîãðàììó.Âõîäíûåïàðàìåòðûìåòîäûèñîñòî
ÿíèåïàìÿòèìîãóòèìåòüïðîèçâîëüíûåçíà÷åíèÿ.Òîãäàïàðàìåòðèçóåì
íà÷àëüíîåñîñòîÿíèåâòî÷êåâõîäàâìåòîäíàáîðîìñèìâîëüíûõïåðåìåí
íûõ.Ñèìâîëüíûåïåðåìåííûåÿâëÿþòñÿòèïèçèðîâàííûìèâñîîòâåòñòâèè
ñòèïàìèèñõîäíûõïîëåéèïåðåìåííûõ.Äîïîëíèòåëüíîäëÿñèìâîëüíûõ
ïåðåìåííûõ,èìåþùèõññûëî÷íûéòèï,ïîòðåáóåì,÷òîáûèõçíà÷åíèÿíå
ÿâëÿëèñüïñåâäîíèìàìèäðóãäðóãà.Äàííîåïðåäïîëîæåíèå,ðàçóìååòñÿ,
îãðàíè÷èâàåòìíîæåñòâîðàññìàòðèâàåìûõñîñòîÿíèé.
Äëÿîïèñàíèÿïàðàìåòðèçàöèèââåäåìñëåäóþùèåìíîæåñòâà:

V
ìíîæåñòâîïåðåìåííûõ,îïðåäåëÿåìûõâìåòîäå;

P;P

V
ìíîæåñòâîïàðàìåòðîâìåòîäà;

S
ìíîæåñòâîñèìâîëüíûõïåðåìåííûõ;

S
R
;S
R

S
ìíîæåñòâîñèìâîëüíûõïåðåìåííûõññûëî÷íîãîòèïà;
10

~s
âåêòîð,ñîñòîÿùèéèçâñåõñèìâîëüíûõïåðåìåííûõ;

F
ìíîæåñòâîïîëåé,ïîêîòîðûìîñóùåñòâëÿåòñÿäîñòóï.
Òîãäàìíîæåñòâîíà÷àëüíûõñîñòîÿíèéïðîãðàììûíàâõîäåâìåòîä
áóäåòîïèñûâàòüñÿñëåäóþùèìîáðàçîì:

P
entry
:
P
!
S
ñèìâîëüíàÿïàðàìåòðèçàöèÿïàðàìåòðîâìåòîäà;

H
entry
:
S
R

F*S
ñèìâîëüíàÿïàðàìåòðèçàöèÿñîñòîÿíèÿêó÷è.
Çäåñüèäàëåå
entry
òî÷êàâõîäàâìåòîä.
Ïàðóîòîáðàæåíèé
P
entry
è
H
entry
,çàäàþùóþñèìâîëüíóþïàðàìåò
ðèçàöèþíàâõîäåâìåòîä,áóäåìíàçûâàòüíà÷àëüíûìñèìâîëüíûìñîñòî
ÿíèåìèëè
State
entry
.Ïîäñòàâëÿÿâìåñòîñèìâîëüíûõïåðåìåííûõ,ñîäåð
æàùèõñÿâ
~s
,èõäîïóñòèìûåêîíêðåòíûåçíà÷åíèÿ,ïîëó÷èììíîæåñòâî
ñïîñîáîâçàïóñòèòüìåòîä.Îáîçíà÷èìäàííîåìíîæåñòâîêàê

.Ïðåäïîëà
ãàåòñÿ,÷òîçíà÷åíèÿñèìâîëüíûõïåðåìåííûõïîëíîñòüþîïðåäåëÿþòðå
çóëüòàòûâû÷èñëåíèÿâñåõáóëåâûõâûðàæåíèé,à,ñëåäîâàòåëüíî,èïóòü
âûïîëíåíèÿ.Åñëèðåçóëüòàòáóëåâûõâûðàæåíèéçàâèñèòîòíåèçâåñòíûõ
çíà÷åíèé,òîäëÿäàííûõçíà÷åíèéòàêæåââåä¼ìñèìâîëüíûåïåðåìåííûå,
îïðåäåëÿåìûåâòî÷êåâõîäà.Òàêêàêâåêòîðêîíêðåòíûõçíà÷åíèé
~

2

îäíîçíà÷íîîïðåäåëÿåòïóòüâûïîëíåíèÿ,òîîáîçíà÷èìêàê
L
(
~

)
ïóòüâû
ïîëíåíèÿ,ñîîòâåòñòâóþùèéâåêòîðóêîíêðåòíûõçíà÷åíèé
~

.
Ââåäåìâñïîìîãàòåëüíûåîáîçíà÷åíèÿ:

L
(
~

)
e
çíà÷åíèÿïåðåìåííûõèñîñòîÿíèåïàìÿòèíàðåáðå
e
ïóòè
âûïîëíåíèÿ
L
(
~

)
;


l
ìíîæåñòâîâåêòîðîâêîíêðåòíûõçíà÷åíèé,äëÿêîòîðûõ
L
(
~

)
ñîîòâåòñòâóåòïóòèíàÃÏÓ
l
.
Äëÿîïðåäåëåíèÿñèìâîëüíîãîñîñòîÿíèÿâïðîèçâîëüíîéòî÷êåÃÏÓ
ââåäåì
SE
ìíîæåñòâîñèìâîëüíûõâûðàæåíèé.Ñèìâîëüíûìèâûðàæåíè
ÿìèÿâëÿþòñÿñèìâîëüíûåïåðåìåííûåèêîíñòàíòû,àòàêæåâûðàæåíèÿ,
ïîñòðîåííûåèçñèìâîëüíûõâûðàæåíèéñïîìîùüþóíàðíûõ,áèíàðíûõè
óñëîâíîãîîïåðàòîðîâ.
Äëÿçàäàíèÿîãðàíè÷åíèé,ó÷èòûâàþùèõóñëîâèÿïåðåõîäîâ,âñèì
âîëüíîìñîñòîÿíèèÿâíîââîäèòñÿïðåäèêàòïóòè.Ïðåäèêàòîìïóòèáóäåì
íàçûâàòüñèìâîëüíîåâûðàæåíèå
G
ëîãè÷åñêîãîòèïà,çàäàþùååìíîæåñòâî
äîïóñòèìûõçíà÷åíèéâåêòîðàñèìâîëüíûõïåðåìåííûõ

G
,
~

2

G
()
G
(
~

)
.
11
ÒîãäàñèìâîëüíîåñîñòîÿíèåâêîíêðåòíîéâåðøèíåïóòèÃÏÓáóäåì
îïèñûâàòüíàáîðîì
State
=
hV
;
H
;
Gi
,ãäå:

V
:
V
!
SE
ïàðàìåòðèçîâàííûåçíà÷åíèÿëîêàëüíûõïåðåìåí
íûõ;

H
:
S
R

F*
SE
ïàðàìåòðèçîâàííîåñîñòîÿíèåêó÷è;

G
ïðåäèêàòïóòè.
Ââåä¼ìôóíêöèþêîíêðåòèçàöèèäëÿñèìâîëüíîãîñîñòîÿíèÿ
'
(
State
=
hV
;
H
;
Gi
;
~

)
,êîòîðàÿâñëó÷àå,åñëè
~

2

G
,ñòðîèòêîíêðåòíîå
ñîñòîÿíèåäëÿëîêàëüíûõïåðåìåííûõèïàìÿòè,ïîäñòàâëÿÿâ
V
è
H
âìåñòîñèìâîëüíûõïåðåìåííûõêîíêðåòíûåçíà÷åíèÿ,ñîîòâåòñòâóþùèå
~

.
Çàäà÷àñèìâîëüíîãîâûïîëíåíèÿçàêëþ÷àåòñÿâïîñòðîåíèèñèìâîëü
íîãîñîñòîÿíèÿäëÿâûáðàííîãîïóòèíàÃÏÓ.Ôîðìàëüíîäàííàÿçàäà÷à
ñòàâèòñÿñëåäóþùèìîáðàçîì:äëÿçàäàííîãîïóòè
l
íàÃÏÓ,íà÷èíàþùåãî
ñÿâ
entry
èçàêàí÷èâàþùåãîñÿðåáðîì
e
,íåîáõîäèìîâû÷èñëèòüñèìâîëü
íîåñîñòîÿíèå
State
e
òàêîå,÷òî:
G
=
l
^8
~

2

l
(
L
(
~

)
e
=
'
(
State
e
;
~

))
:
(11)
Çäåñüèäàëååîïåðàöèÿ
]
îáîçíà÷àåòïåðåîïðåäåëåíèåîòîáðàæåíèÿ
äëÿçàäàííûõçíà÷åíèé:
(
A
]
B
)(
x
)=
8

:
B
(
x
)
;
åñëè
x
2
domain
(
B
);
A
(
x
)
;
èíà÷å
(12)
Äëÿïîñòðîåíèÿñèìâîëüíûõñîñòîÿíèéäëÿòî÷åêíàïóòè
l
îïðåäå
ëèìïðàâèëàèíòåðïðåòàöèèèíñòðóêöèéîòíîñèòåëüíîíà÷àëüíîãîñîñòî
ÿíèÿâñîîòâåòñòâèèñèõñåìàíòèêîé.Ïóñòü
e
pred
;e
succ
ðåáðàïóòèíà
ÃÏÓäîèïîñëåèíñòðóêöèè
I
ñîîòâåòñòâåííî.Òîãäàââåäåìñëåäóþùèå
ïðàâèëàèíòåðïðåòàöèèäëÿñîîòâåòñòâóþùèõèíñòðóêöèé.
h
e
pred
ij
=
hV
;
H
;
GiI
="
a
=
b
;"
h
e
succ
ij
=
hV]f
a
7!V
(
b
)
g
;
H
;
Gi
h
e
pred
ij
=
hV
;
H
;
GiI
="
a
=
const
;"
h
e
succ
ij
=
hV]f
a
7!
const
g
;
H
;
Gi
12
h
e
pred
ij
=
hV
;
H
;
GiI
="
a
=
b

c
;"
h
e
succ
ij
=
hV]f
a
7!V
(
b
)
V
(
c
)
g
;
H
;
Gi
h
e
pred
ij
=
hV
;
H
;
GiI
="
a
=
O
b
;"
h
e
succ
ij
=
hV]f
a
7!
O
b
g
;
H
;
Gi
h
e
pred
ij
=
hV
;
H
;
GiI
="
assume
(
c
);"
h
e
succ
ij
=
hV
;
H
;
G^V
(
c
)
i
)
h
e
pred
ij
=
hV
;
H
;
GiI
="
a
=
b:f
;"
h
e
succ
ij
=
hV]
a
7!H
(
V
(
b
)
;f
)
;
H
;
Gi
)
h
e
pred
ij
=
hV
;
H
;
GiI
="
a:f
=
b
;"
h
e
succ
ij
=
hV
;
H]hV
(
a
)
;f
i7!V
(
b
)
;
Gi
)
Ïðèçàäàíèèïðàâèëèíòåðïðåòàöèèíåáûëèðàññìîòðåíûèíñòðóê
öèèâûçîâàìåòîäàèäîñòóïàêìàññèâó.Èíòåðïðåòàöèÿèíñòðóêöèéâûçîâà
ñó÷åòîìðåçþìåâûçâàííûõìåòîäîâáóäåòðàññìîòðåíàäàëåå.
Âäàííîéãëàâåðàññìàòðèâàåòñÿïîäõîä,ïîçâîëÿþùèéïðîâîäèòüàíà
ëèçöèêëîâñôèêñèðîâàííûì÷èñëîìèòåðàöèé.Äàííûéïîäõîäïðåäëàãàåò
ïîäìåíÿòüðåçóëüòàòûàðèôìåòè÷åñêèõîïåðàöèéââíóòðèöèêëàíàíîâûå
íåèçâåñòíûåñèìâîëüíûåçíà÷åíèÿ.Òàêèìîáðàçîì,ñòàíîâèòñÿâîçìîæíûì
âûõîäèçöèêëîâñôèêñèðîâàííûì÷èñëîìèòåðàöèé.
Ëåììà3.1.
Äëÿâñåõñèìâîëüíûõñîñòîÿíèé,ïîëó÷åííûõâðåçóëüòà
òåïðèìåíåíèÿïðàâèëèíòåðïðåòàöèè,íà÷èíàÿèçíà÷àëüíîãîñèìâîëüíîãî
ñîñòîÿíèÿäëÿçàäàííîãîïóòèíàÃÏÓ
l
,âûðàæåíèå(
11
)âåðíî.
Òàêêàêñèìâîëüíîåâûïîëíåíèåìîæåòïðîàíàëèçèðîâàòüëèøüîïðå
äåë¼ííûéíàáîðïóòåéâûïîëíåíèÿ,ñðàçóîïðåäåëèìïóòè,êîòîðûåáóäóò
ïîäâåðãàòüñÿàíàëèçó.Äëÿýòîãîââåäåìïîíÿòèåãðàôàðàçâåðòêè.
ÃðàôîìðàçâåðòêèäëÿÃÏÓ
G
=
h
V;E;v
entry
;v
exit
i
áóäåìíàçûâàòü
àöèêëè÷åñêèéîðèåíòèðîâàííûéñâÿçàííûéãðàôñâûäåëåííûìèèñòîêîì
èñòîêîì
G
0
=
h
V
0
;E
0
;v
0
entry
;v
0
exit
i
,äëÿêîòîðîãîîïðåäåëåíàôóíêöèÿñîîò
âåòñòâèÿ
'
:
V
0
!
V
òàêàÿ,÷òîâåðíî:
'
(
v
0
entry
)=
v
entry
'
(
v
0
exit
)=
v
exit
(13)
8
v
0
2
V
0
nf
v
0
entry
;v
0
exit
g
:
'
(
v
0
)
62f
v
entry
;v
exit
g
(14)
h
v
0
;u
0
i2
E
0
=
)h
'
(
v
0
)
;
'
(
u
0
)
i2
E
0
(15)
h
v
0
;u
0
i2
E
0
^h
v
0
;w
0
i2
E
0
^
u
0
6
=
w
0
=
)
'
(
u
0
)
6
=
'
(
w
0
)
(16)
13
ÄëÿïåðåõîäàîòàíàëèçàêîíêðåòíîãîïóòèÃÏÓêàíàëèçóãðàôà
ðàçâåðòêèíåîáõîäèìîîïðåäåëèòüîïåðàöèèîáúåäèíåíèÿñèìâîëüíûõñî
ñòîÿíèé,àòàêæåïåðåîïðåäåëèòüïðàâèëàâûâîäàäëÿ÷òåíèÿèçàïèñèâ
ïàìÿòü.Íåíàðóøàÿîáùíîñòè,ìîæíîñ÷èòàòü,÷òîîáúåäèíÿþòñÿâñåãäà
ëèøüäâàñîñòîÿíèÿ.Âòîìñëó÷àå,åñëèâáàçîâûéáëîêâõîäèòáîëååäâóõ
ð¼áåð,äîáàâëåíèåìïóñòûõáàçîâûõáëîêîâìîæíîäîáèòüñÿòîãî,÷òîîáú
åäèíåíèþáóäóòïîäâåðãàòüñÿíåáîëååäâóõáëîêîâ.
Òîãäàçàäà÷óîáúåäèíåíèÿñèìâîëüíûõñîñòîÿíèéñôîðìóëèðóåìñëå
äóþùèìîáðàçîì.Ïóñòüäàíàòðîéêàâåðøèí
h
l;r;j
i
òàêèõ,÷òîåñòüðåáðà
h
l;j
i
è
h
r;j
i
.Äëÿâåðøèí
l
è
r
èçâåñòíûñîñòîÿíèÿ
hV
l
;
H
l
;
G
l
i
è
hV
r
;
H
r
;
G
r
i
.
Íåîáõîäèìîïîñòðîèòüñèìâîëüíîåñîñòîÿíèåäëÿâåðøèíû
j
,îáúåäèíÿþ
ùååèíôîðìàöèþîïóòÿõ,ïðèøåäøèõïîðåáðàì
h
l;j
i
è
h
r;j
i
.
Ïðåäèêàòïðèîáúåäèíåíèèâû÷èñëÿåòñÿñëåäóþùèìîáðàçîì:
G
j
=
G
l
_G
r
.Ïîïîñòðîåíèþäàííûéïðåäèêàòäîïóñêàåòâñåâîçìîæíûåçíà÷åíèÿ
íà÷àëüíûõñîñòîÿíèé,ñîîòâåòñòâóþùèõïðåäèêàòàì
G
l
è
G
r
.
Äëÿïîñòðîåíèÿ
V
j
è
H
j
íåîáõîäèìîíàéòèòàêîåñèìâîëüíîåâûðàæå
íèå
C
,÷òîîäíîâðåìåííî:

G
l


C
;

G
r
\

C
=
?
(17)
Åñëèâûïîëíåíèåäîøëîäîâåðøèíû
j
èçíà÷àëüíîãîñîñòîÿíèÿ,ñî
îòâåòñòâóþùåãîçíà÷åíèÿì
~

,òîìîæíîãàðàíòèðîâàòü,÷òîåñëè
~

2

C
,
òîáûëîïðîéäåíîðåáðî
h
l;j
i
,èíà÷å
h
r;j
i
.Òîãäàñîñòîÿíèåïàìÿòèèïå
ðåìåííûõìîæåòáûòüâûðàæåíîïðèïîìîùèóñëîâíîãîîïåðàòîðàîò
C
ñëåäóþùèìîáðàçîì:
V
j
(
v
)=
8

:
V
l
(
v
)
;
åñëè
V
l
(
v
)=
V
r
(
v
)
(
C
)?(
V
l
(
v
)):(
V
r
(
v
))
;
èíà÷å
(18)
H
j
(
s;f
)=
8

:
H
l
(
s;f
)
;
åñëè
H
l
(
s;f
)=
H
r
(
s;f
)
(
C
)?(
H
l
(
s;f
)):(
H
r
(
s;f
))
;
èíà÷å
(19)
Âêà÷åñòâå
C
ìîæåòáûòüèñïîëüçîâàíïðåäèêàò
G
l
.Äåéñòâèòåëüíî,
äëÿïðåäèêàòà
G
l
âûïîëíÿåòñÿòðåáîâàíèå(
17
).
Ââåä¼ìîïåðàöèþ
Decompose
:
SE
!
2
S

SE
,êîòîðàÿäëÿñèìâîëüíî
ãîâûðàæåíèÿññûëî÷íîãîòèïàñòðîèòíàáîðïàðèçñèìâîëüíîéïåðåìåí
14
íîéèóñëîâèÿ,ïðèêîòîðîìèñõîäíîåâûðàæåíèåðàâíîäàííîéñèìâîëü
íîéïåðåìåííîé.Âñåóñëîâèÿÿâëÿþòñÿïîïàðíîíåñîâìåñòíûìè.Ðåçóëüòàò
Decompose
ìîæåòáûòüâû÷èñëåíñïîìîùüþîáõîäàäåðåâàâûðàæåíèé,ñî
äåðæàùèõóñëîâíûåîïåðàòîðû.
Ââåä¼ìîïåðàöèþâçÿòèÿïîëÿ
DEREF
:
SE

F
!
SE
,êîòîðàÿïðî
èçâîäèò÷òåíèåèçñèìâîëüíîãîâûðàæåíèÿ
SE
ïîïîëþ
f
:
Decompose
(
se
)=
fh
s
i
;c
i
ij
i
2
[1
:::n
]
g
j
Decompose
(
se
)
j
=
n
h
i
=
H
(
s
i
;f
)
DEREF
(
se;f
)=
8

:
ite
(
c
1
;h
1
;ite
(
c
2
;h
2
;:::ite
(
c
n

1
;h
n

1
;h
n
)))
;
äëÿ
n�
1
h
1
;
äëÿ
n
=1
Ïðèïîìîùèäàííûõîïåðàöèéçàäàäèìèíòåðïðåòàöèþäëÿèíñòðóê
öèé÷òåíèÿèçàïèñèïîëÿ.
h
e
pred
ij
=
hV
;
H
;
GiI
="
a
=
b:f
;"
h
e
succ
ij
=
hV]f
a
7!
DEREF
(
V
(
b
)
;f
)
g
;
H
;
Gi
(20)
h
e
pred
ij
=
hV
;
H
;
GiI
="
a:f
=
b
;"
Decompose
(
V
(
a
))=
f
s
i
;c
i
g
h
e
succ
ij
=
hV
;
H]
n
i
=1
ff
s
i
;f
g7!
ite
(
c
i
;
V
(
b
)
;
H
(
s
i
;f
))
g
;
G
(21)
Áóäåìãîâîðèòü,÷òîñèìâîëüíîåñîñòîÿíèå
hV
;
H
;
Gi
îòíîñèòåëüíî
òî÷êè
e
îïðåäåëåíîêîððåêòíî,åñëè

G
ñîäåðæèòâòî÷íîñòèâñå
~

,èçêîòî
ðûõ
e
äîñòèæèìà,èäëÿêàæäîãî
~

2

G
âåðíî,÷òî
'
(
hV
;
H
;
Gi
;
~

)=
L
(
~

)
e
Òåîðåìà3.1
.Îïðåäåë¼ííûåâûøåïðàâèëàèíòåðïðåòàöèèñòðîÿò
êîððåêòíûåñèìâîëüíûåñîñòîÿíèÿ.
Àëãîðèòì3.1
.Âûáåðåìêîíêðåòíóþâåðøèíóâãðàôåðàçâåðòêè

u
.Áóäåìñ÷èòàòü,÷òîâñåâåðøèíû,êîòîðûåòîïîëîãè÷åñêèìåíüøå
u
,
óæåîáðàáîòàíûèèõïðåäèêàòûïóòèïîñ÷èòàíû.Íàéäåìäëÿ
u
å¼îáëàñòü
ïîñòäîìèíèðîâàíèÿ.Ïóòüuíåïîñòäîìèíèðóåòòî÷êóâõîäà.Ðàññìîòðèì
ãðàôâåðøèí,òîïîëîãè÷åñêèìåíüøèõëèáîðàâíûõ
u
,íàçîâ¼ìåãî
G
0
.Ïî
ñòðîèìðàçðåç
h
S;T
i
òàêîé,÷òîê
S
îòíîñÿòñÿâñåâåðøèíû
G
0
,êîòîðûå
15
âèñõîäíîìãðàôåíåïîñòäîìèíèðóåòäàííàÿâåðøèíà,àê
T
âñåâåð
øèíûèçîáëàñòèïîñòäîìèíèðîâàíèÿ.Ïóñòü
h
s
i
;t
i
i
ñïèñîêðåáåð,ëåæà
ùèõíàðàçðåçå.Òîãäàïðåäèêàòïóòèäëÿ
u
ïîñòðîèìñëåäóþùèìîáðàçîì:
h_
i
(
G
(
s
i
)
^
Cond
(
s
i
;t
i
))
;
i
,ãäå
G
(
s
i
)
ïðåäèêàòïóòèäëÿâåðøèíû
s
i

Cond
(
s
i
;t
i
)
óñëîâèåïåðåõîäàïîðåáðó.Âäàííîìñëó÷àåïîäóñëîâèåì
ïåðåõîäàïîðåáðóïîíèìàåòñÿóñëîâèåâèíñòðóêöèè
assume
áàçîâîãîáëî
êà,âêîòîðûéâõîäèòðåáðî.Åñëèóáëîêàîòñóòñòâóåò
assume
,òîóñëîâèå
ñ÷èòàåòñÿòîæäåñòâåííûìèñòèíå.
Òåîðåìà3.2
.Àëãîðèòì3.1êîððåêòíîâû÷èñëÿåòïðåäèêàòïóòè.
Àëãîðèòì3.2
.Ïóñòü
dom
ýòîíåïîñðåäñòâåííûéäîìèíàòîðâåð
øèí
lhs
è
rhs
,òîãäàðàññìîòðèììíîæåñòâîâåðøèí,òîïîëîãè÷åñêèìåíü
øåëèáîðàâíûõ
lhs
èáîëüøåëèáîðàâíûõ
dom
,íàçîâ¼ìåãî
L
.Ðàññìîòðèì
àíàëîãè÷íîåìíîæåñòâîäëÿ
rhs
,íàçîâåìåãî
R
.Ðàññìîòðèìòîãäà
L
\
R
è
L
n
R
,áåçîãðàíè÷åíèÿîáùíîñòèáóäåìñ÷èòàòü,÷òî
L
n
R
íåïóñòî.Òîãäà
Interpol
=
_
i
(
G
dom;u
i
^
Cond
(
u
i
;v
i
))
,ãäå
h
u
i
;v
i
i
ðåáðà,ëåæàùèåíàðàç
ðåçå
h
L
\
R;L
n
R
i

G
dom;u
i
óñëîâèåòîãî,÷òîïóòüâûïîëíåíèÿäîéäåò
äî
u
i
,ïðîéäÿ
dom
.
Òåîðåìà3.3
.Àëãîðèòì3.2êîððåêòíîâû÷èñëÿåòóñëîâèå
Interpol
.
Â÷åòâåðòîéãëàâå
ðàññìàòðèâàåòñÿâîïðîñó÷åòàâûçîâîâïðèñèì
âîëüíîìâûïîëíåíèè.Âûäåëÿþòñÿòðèòèïàâûçîâîâ:ïðÿìûåâûçîâûèç
âåñòíûõìåòîäîâ,êîñâåííûåâûçîâûèâûçîâûìåòîäîâèçñòîðîííèõáèá
ëèîòåê.
Äëÿìîäåëèðîâàíèÿïðÿìûõâûçîâîâíåîáõîäèìîðàçðàáîòàòüïðîöå
äóðóïîñòðîåíèÿðåçþìåìåòîäà.Âäàííîéðàáîòåïðåäëàãàåòñÿõðàíèòüâ
ðåçþìåñîñòîÿíèåïàìÿòèäîèïîñëåâûïîëíåíèÿìåòîäà.
hV
PRE
;
H
PRE
;
V
POST
;
H
POST
i
(22)
Äëÿïîñòðîåíèÿðåçþìåòàêîãîâèäàìîãóòáûòüèñïîëüçîâàíûðå
çóëüòàòûâíóòðèïðîöåäóðíîãîñèìâîëüíîãîâûïîëíåíèÿ.Âêà÷åñòâå
V
PRE
è
H
PRE
ïðåäëàãàåòñÿèñïîëüçîâàòüíà÷àëüíîåñèìâîëüíîåñîñòîÿíèå,àâ
êà÷åñòâå
V
POST
è
H
POST
ñèìâîëüíîåñîñòîÿíèå,ïîëó÷åííîåâòî÷êåâû
õîäà.
Îäíàêîîòñóòñòâèåäîïîëíèòåëüíûõîãðàíè÷åíèéíàðàçìåðïðèâåäåò
êíåîãðàíè÷åííîìóðàçðàñòàíèþêàêðåçþìå,òàêèñèìâîëüíûõñîñòîÿíèé,
16
÷òîïðèâåäåòêñóùåñòâåííîéäåãðàäàöèèïðîèçâîäèòåëüíîñòèàíàëèçàòî
ðà.Ñëåäîâàòåëüíî,íåîáõîäèìîîãðàíè÷èòüìàêñèìàëüíûéðàçìåððåçþìå.
Âäàííîéðàáîòåïðåäëàãàåòñÿââåñòèîãðàíè÷åíèÿíàðàçìåðãðàôàïàìÿòè
H
èíàðàçìåðãðàôàñèìâîëüíûõâûðàæåíèé.Äàëååðàññìàòðèâàþòñÿàë
ãîðèòìû,ïîçâîëÿþùèåïðîèçâåñòèñæàòèåäàííûõãðàôîââñîîòâåòñòâèè
ñðàññìîòðåííûìèîãðàíè÷åíèÿìè.
Äëÿïðèìåíåíèÿðåçþìåâòî÷êåâûçîâàìåòîäàíåîáõîäèìîïîñòðî
èòüñîîòâåòñòâèåìåæäóïàìÿòüþâòî÷êåâûçîâàèñîñòîÿíèÿìèïàìÿ
òè
hV
PRE
;
H
PRE
i
è
hV
POST
;
H
POST
i
.Ïóñòüìåòîäâûçûâàåòñÿñíàáî
ðîìïàðàìåòðîâ
f
se
i
g
,ãäå
se
i
ñèìâîëüíîåâûðàæåíèå,ñîîòâåòñòâóþ
ùååi-òîìóàðãóìåíòóâûçîâà.Áóäåìñ÷èòàòü,÷òîïîñòðîåíîîòîáðàæåíèå
Formal
2
Actual
,îòîáðàæàþùååñèìâîëüíûåïåðåìåííûå,ñîîòâåòñòâóþùèå
ôîðìàëüíûìïàðàìåòðàììåòîäà,âñèìâîëüíûåâûðàæåíèÿ,ñêîòîðûìè
äàííûéìåòîäáûëâûçâàí.
Îïèøåìïðîöåäóðó,ïîçâîëÿþùóþïîñòðîèòüñîïîñòàâëåíèåìåæäó
ñèìâîëüíûìèâûðàæåíèÿìèâûçâàííîãîèâûçûâàþùåãîìåòîäîâ.Äëÿíà
÷àëàñîïîñòàâèìíà÷àëüíîåñîñòîÿíèåâûçûâàåìîãîìåòîäà,çàäàííîåïàðîé
hV
PRE
;
H
PRE
i
,èòåêóùååñèìâîëüíîåñîñòîÿíèå
hV
;
Hi
.Äëÿýòîãîâîñïîëü
çóåìñÿàëãîðèòìîì,ïðèâåä¼ííûìíàëèñòèíãå
1
.
Èñïîëüçóþùàÿñÿôóíêöèÿ
DEREF
àíàëîãè÷íàïîñâîåéñåìàíòèêå
ôóíêöèè
(
20
)
.
Áëàãîäàðÿïîñòðîåííîìóîòîáðàæåíèþèçñèìâîëüíûõïåðåìåííûõ
âûçâàííîãîìåòîäàâñèìâîëüíûåâûðàæåíèÿâûçûâàþùåãî,âîçìîæíîîñó
ùåñòâèòüòðàíñëÿöèþñèìâîëüíûõâûðàæåíèéâûçâàííîãîìåòîäàâñèì
âîëüíûåâûðàæåíèÿâûçûâàþùåãî.Äëÿýòîãîäîñòàòî÷íîçàìåíèòüâñå
âõîæäåíèÿñèìâîëüíûõïåðåìåííûõâûçâàííîãîìåòîäàíàñîîòâåòñòâóþ
ùèåâûðàæåíèÿâûçûâàþùåãî.Ôóíêöèþ,îñóùåñòâëÿþùóþòàêóþòðàíñ
ëÿöèþ,îïðåäåëèìêàê
Translate
:
SE
callee
!
SE
caller
.Âñëó÷àå,åñëèäëÿ
ñèìâîëüíîãîâûðàæåíèÿâûçâàííîãîìåòîäàíåòàíàëîãè÷íîãîñèìâîëüíî
ãîâûðàæåíèÿââûçûâàþùåé,òîçàâîäèòñÿíîâàÿíåèçâåñòíàÿñèìâîëüíàÿ
ïåðåìåííàÿ,ñîîòâåòñòâóþùàÿâûðàæåíèþâûçâàííîãîìåòîäà.
Äëÿçàâåðøåíèÿïðèìåíåíèÿðåçþìåíåîáõîäèìîîáíîâèòüñîñòîÿíèå
ïàìÿòèâòî÷êåâûçîâàâñîîòâåòñòâèèñ
hV
POST
;
H
POST
i
.Äëÿýòîãîïðåä
ëàãàåòñÿèñïîëüçîâàòüàëãîðèòì,àíàëîãè÷íûé
1
.Îíïîçâîëÿåòïðèâåñòè
ñîäåðæèìîåïàìÿòèâñîîòâåòñòâèåñîáíîâëåíèÿìè,ïðîèçîøåäøèìèââû
17
PROCGetCallee2Caller(Callee2Caller:ArrayofSExSE,
CallerHeap:SxF�SE,CalleeHeap:SxF�S):SE�SE
BEGIN
5
result:SE�SE=Empty
visited:SetofSE=Empty
queue:QueueofSE,SErS8;-16;,-8;US8;=Empty
FOREACHcallee,caller&#x-106; -17; -1;pl-;Űl;&#x-169;-17;-5; ,-;၁ -17;z-1;xl-;Ÿl;&#x-177;-17;r-2;�inCallee2Caller;DO
visited.Add(callee)
10
queue.Add(callee,caller&#x-181; -17; -1;pl-;Űl;&#x-169;-17;-5; ,-;၁ -17;z-1;xl-;Ÿl;&#x-177;-17;r-3;�)
result.Add(callee,caller&#x-181; -16;š-1;pl-;Űl;&#x-170;-17;-5; ,-;၁ -17;z-1;xl-;ŷl;&#x-178;-17;r-3;�)
DONE
WHILEQueue.Size�0DO
callee,caller&#x-105; -17; -1;pl-;Űl;&#x-170;-17;-5; ,-;၀ -17;Š-1;xl-;ŷl;&#x-178;-17;r-2;�=Queue.Dequeue();
15
FOREACHfieldinCallerHeap.Keys.Where(s==caller)DO
pointsToCallee=CalleeHeap.Get(callee,field&#x-180; -17; -1;pl-;Űl;&#x-170;-17;-5; ,-;၅-18;i-1;࠮-;Ƃl;&#x-183; -37;Ө)
pointsToCaller=DEREF(CalleeHeap,caller,field)
result.Add(pointsToCallee,pointsToCaller);
visited.Add(pointsToCallee);
20
queue.Enqueue(pointsToCallee,pointsToCaller&#x-141;&#xp-13;�o-1;0i-;İn;&#x-130;&#xt-13;�s-1;0T-;İo;&#x-130; -13; -1;0l-;İl;&#x-130;-13;-4;@,-;গp;&#x-134;&#xo-13;i-1;4n-;Ĵt;&#x-133;&#xs-13;T-1;4o-;ፌ&#x-134; -13;l-1;4l-;ጾ&#x-134;&#xr-28;�);
DONE
DONE
returnresult
END
Ëèñòèíã1Àëãîðèòìïîñòðîåíèÿôóíêöèè
Translate
çâàííîììåòîäå.Ïîñëåâûïîëíåíèÿäàííîãîîáíîâëåíèÿ,îñíîâíîåðåçþìå
ìåòîäàñ÷èòàåòñÿïðèìåí¼ííûì,èíà÷èíàåòñÿïðèìåíåíèåâñïîìîãàòåëü
íûõ÷àñòåéðåçþìå,îïðåäåë¼ííûõàíàëèçàòîðàìè.
Âýòîéãëàâåòàêæåðàññìàòðèâàåòñÿïîäõîäêàíàëèçó÷èñòûõìåòî
äîâ.Ìåòîäñ÷èòàåòñÿ÷èñòûì,åñëèîííåìåíÿåòäèíàìè÷åñêóþïàìÿòüè
äëÿîäíîãîèòîãîæåâõîäíîãîñîñòîÿíèÿâîçâðàùàåòîäíîèòîæåçíà
÷åíèå.Òàêàÿïîääåðæêàòðåáóåòñÿ,íàïðèìåð,ïðèàíàëèçåèñïîëüçîâàíèÿ
êîëëåêöèé,èâ÷àñòíîñòèìàññèâîâ.Ïîääåðæêó÷èñòûõìåòîäîâïðåäëàãà
åòñÿîñóùåñòâëÿòüñïîìîùüþêåøèðîâàíèÿñîñòîÿíèé,ñêîòîðûìèäàííûå
ìåòîäûáûëèâûçâàíû.Åñëèìåòîäóæåâûçûâàëñÿñíåêîòîðûìñèìâîëü
íûìñîñòîÿíèåì,òîðåçóëüòàòâûçîâàáåðåòñÿèçêåøà.
Äëÿìåæïðîöåäóðíîãîàíàëèçàïîìå÷åííûõäàííûõïðåäëàãàåòñÿèñ
ïîëüçîâàòüïîäõîä,êîìáèíèðóþùèéñëàéñèíãèâíóòðèïðîöåäóðíûé÷óâ
ñòâèòåëüíûéêïóòÿìàíàëèç.Ñëàéñèíãïðåäëàãàåòñÿîñóùåñòâëÿòü,ñâî
äÿçàäà÷óðàñïðîñòðàíåíèÿïîìå÷åííûõäàííûõêIFDS-çàäà÷å.Ðåçóëüòà
òîìñëàéñèíãàÿâëÿåòñÿíàáîðìåæïðîöåäóðíûõïóòåéâìåæïðîöåäóðíîì
18
ÃÏÓ,ïîêîòîðûìïîìå÷åííûåäàííûåðàñïðîñòðàíÿþòñÿîòèñòîêàêñòîêó
áåçó÷åòàóñëîâèéïåðåõîäîâ.Äàëååäàííûåïóòèïîäâåðãàþòñÿîïèñàííî
ìó÷óâñòâèòåëüíîìóêïóòÿìâíóòðèïðîöåäóðíîìóàíàëèçó,âèíñòðóêöèÿõ
âûçîâàòðàíñëÿöèÿñèìâîëüíûõñîñòîÿíèéîñóùåñòâëÿåòñÿïîàíàëîãèèñ
àëãîðèòìàìèïðèìåíåíèÿðåçþìå.
Âïÿòîéãëàâå
ðàññìàòðèâàåòñÿìåòîäîïðåäåëåíèÿêðèòåðèÿâûäà
÷èïðåäóïðåæäåíèÿîíàëè÷èèäåôåêòà.Äëÿâûáðàííîãîêðèòåðèÿïðåä
ëàãàþòñÿàëãîðèòìûýôôåêòèâíîãîïîèñêàñîîòâåòñòâóþùèõäåôåêòîâíà
ïðèìåðåîøèáîêòèïàäîñòóïïîíóëåâîìóóêàçàòåëþèóòå÷êàðåñóðñîâ.Ïî
êàçûâàåòñÿñîîòâåòñòâèåîáíàðóæèâàåìûõàëãîðèòìàìèîøèáîêâûáðàííî
ìóêðèòåðèþ.
Äëÿïîñòðîåíèÿêðèòåðèÿâûäà÷èïðåäóïðåæäåíèé,ðàññìîòðèììíî
æåñòâî
f

i
g
2

,ãäå

i


.Ýëåìåíò

i
íàçîâ¼ì
àáñòðàêöèåé

f

i
g
ìíîæåñòâîìàáñòðàêöèé.Áóäåìãîâîðèòü,÷òîââåðøèíåãðàôàðàçâåðò
êè
B
ñîäåðæèòñÿîøèáêà,åñëèíàéäåòñÿòàêàÿàáñòðàêöèÿ

i
,÷òîíàâñåõ
íàáîðàõçíà÷åíèéïåðåìåííûõ
~

2

i
ïðîèçîéä¼òîøèáêàâòî÷êåB.
Ïóñòü

i
âûðàæàåòñÿíåêîòîðûìîáðàçîì÷åðåçñèìâîëüíûåïåðåìåí
íûå
~s
.Òîãäàîáîçíà÷èìêàê
P

i
B
(
~s
)
ôîðìóëóîòñèìâîëüíûõïåðåìåííûõ,
çàäàþùóþóñëîâèåòîãî,÷òî
~s
îäíîâðåìåííîïðèíàäëåæèòàáñòðàêöèè

i
,
èóïðàâëåíèåäîéä¼òäîòî÷êè
B
.Êàê
Err
B
(
~s
)
îáîçíà÷èìóñëîâèåòîãî,
÷òîâòî÷êå
B
ïðîèçîéäåòîøèáêà.Òîãäàäàäèìîïðåäåëåíèåîøèáêèäëÿ
àáñòðàêöèè

i
ñëåäóþùèìîáðàçîì:
Err

i
B
=(
9
~s
:
P

i
B
(
~s
))
^
(
8
~s
:
P

i
B
(
~s
)
!
Err
B
(
~s
))
(23)
Òîãäàíàëè÷èåîøèáêèâòî÷êåBîïðåäåëèìêàêñóùåñòâîâàíèåàá
ñòðàêöèè,íàêîòîðîéïðîèçîéä¼òîøèáêà:
9

i
:
Err

i
B
(24)
Îïðåäåëåíèå(
24
)áóäåìíàçûâàòüîáùèìîïðåäåëåíèåìîøèáêè,
hf

i
g
;Err
B
i
îïðåäåëåíèåìîøèáêè,ïîëó÷åííûìïîäñòàíîâêîé
f

i
g
è
Err
B
âîáùååîïðåäåëåíèåîøèáêè.Âçàâèñèìîñòèîòâûáîðàìíîæåñòâà
àáñòðàêöèé
f

i
g
áóäóòðàçëè÷àòüñÿìíîæåñòâàîáíàðóæèâàåìûõîøèáîê.
Âíåêîòîðûõñëó÷àÿõìîæíîïîêàçàòü,÷òîèìååòìåñòîâëîæåíèåìíî
æåñòâîáíàðóæèâàåìûõîøèáîê.Ðàññìîòðèìäâàðàçëè÷íûõìíîæåñòâààá
19
ñòðàêöèé
A
0
=
f

0
i
g
è
A
00
=
f

00
i
g
;
A
0
;
A
00
2
2

òàêèõ,÷òî:
8
i
9
~
J
:
0
i
=
[
j
2
~
J

00
j
(25)
Ëåììà5.1
.Ïóñòü
Err
A
0
B
ìíîæåñòâîîøèáîêâòî÷êå
B
ïðèèñïîëüçîâàíèè
àáñòðàêöèé
A
0

Err
A
00
B
ïðèèñïîëüçîâàíèèàáñòðàêöèé
A
00
,òîãäàâåðíî:
8
B
:
Err
A
0
B

Err
A
00
B
(26)
Ðàññìîòðèìðàçëè÷íûåêðèòåðèèîøèáî÷íûõñèòóàöèé,ïîëó÷àþùèõ
ñÿâçàâèñèìîñòèîòâûáîðàìíîæåñòâààáñòðàêöèé.
Ïîñòðîèìàáñòðàêöèþ,ñîîòâåòñòâóþùóþçàäà÷åïîèñêàîøèáî÷íûõ
âõîäíûõäàííûõ.Äëÿýòîãîïðîíóìåðóåìâñåçíà÷åíèÿìíîæåñòâà
=
f
~

i
g
èîïðåäåëèììíîæåñòâîàáñòðàêöèéêàê

i
=
~

i
.Äëÿäàííûõàáñòðàêöèé
îïðåäåëåíèåîøèáêè(
24
)áóäåòçàïèñàíîââèäå:
9
~

i
:
G
B
(
~

i
)
^
Err
B
(
~

i
)
.
Ñäðóãîéñòîðîíû,ðàññìîòðèì

1
=
.Òîãäàîïðåäåëåíèå(
24
)ïðè
íèìàåòâèä:
9
~s
(
G
B
(
~s
))
^8
~s
(
G
B
(
~s
)
!
Err
B
(
~s
))
(27)
Îïðåäåëåíèå(
27
)óòâåðæäàåò,÷òîåñëèòî÷êà
B
òàêîâà,÷òîîíàäî
ñòèæèìàõîòÿáûíàîäíîìêîíêðåòíîìñîñòîÿíèèèâíåéâñåãäàïðîèñõî
äèòîøèáêà,òîòî÷êà
B
îøèáî÷íà.Äàííîåîïðåäåëåíèåÿâëÿåòñÿñàìûì
ñòðîãèìèçðàññìàòðèâàåìûõ,ïîýòîìóåìóñâîéñòâåíåíïðîïóñêðåàëüíûõ
îøèáîê.
Ââåäåìíàáîðáóëåâûõïåðåìåííûõ
b
j
=
b
j
(
~s
)
äëÿêàæäîãîâûðàæå
íèÿâãðàôåðàçâåðòêè,èìåþùåãîëîãè÷åñêèéòèï.Ïðîíóìåðóåìâñåïóòè
âãðàôåðàçâåðòêè
f
l
i
g
.Äëÿêîíêðåòíîãîïóòè
l
i
îáîçíà÷èìíàáîðïåðåìåí
íûõ
b
j
,âû÷èñëåííûõâèñòèíó,êàê
B
+
i
,àíàáîðïåðåìåííûõ,âû÷èñëåííûõ
âëîæü,êàê
B

i
.

i
=
^
j
8







:
b
j
;b
j
2
B
+
i
:
b
j
;b
j
2
B

i
true;
èíà÷å
=
~
l
i
(
~s
)
Òàêèìîáðàçîì,êàæäàÿ

i
îïðåäåëÿåòðåçóëüòàòâû÷èñëåíèÿâñåõ
áóëåâûõâûðàæåíèé,êîòîðûåâñâîþî÷åðåäüîïðåäåëÿþòïóòü
l
0
i
.Ôîðìó
ëà(
24
)äëÿäàííîéàáñòðàêöèèèìååòñëåäóþùèéâèä:
20
9
~
l
i
:(
9
~s
:(
G
~
l
i
B
(
~s
)))
^8
~s
:((
G
~
l
i
B
(
~s
)
!
Err
B
(
~s
))
(28)
ãäå
G
~
l
i
B
(
~s
)=(
8
j
:
~
l
i;j
=
~
l
i;j
(
~s
))
^G
B
.
Òàêæåðàññìàòðèâàþòñÿàáñòðàêöèèäëÿêðèòè÷åñêîéòî÷êè

i
=
G
B
èçíà÷åíèéâåêòîðà
~
b


i
=
~
b
i
.
Çàìåòèì,÷òîäëÿââåä¼ííûõàáñòðàêöèéâåðíîñëåäóþùååñîîòíîøå
íèå:
Err

i
=

Err

i
=
G
B
i

Err

i
=
~
l
i

Err

i
=
~
b
i

Err

i
=
~

i
(29)
Ðàññìàòðèâàþòñÿïðèìåðûîøèáî÷íûõñèòóàöèéäëÿââåä¼ííûõàá
ñòðàêöèé.
Äàëååâäàííîéãëàâåðàññìàòðèâàþòñÿ÷óâñòâèòåëüíûåêïóòÿìàëãî
ðèòìûïîèñêàîøèáîêäîñòóïàê
null
èóòå÷êèðåñóðñîâ.Èäåÿàëãîðèòìà
ïîèñêàäîñòóïàê
null
çàêëþ÷àåòñÿâïîñòðîåíèèäëÿâñåõñèìâîëüíûõâû
ðàæåíèéäëÿêàæäîéòî÷êèïðîãðàììû
e
ôîðìóë
IsNull
se
e
(
~
b
i
)
òàêèõ,÷òî
IsNull
se
e
(
~
b
i
)
!
se
==
null
.Òîãäà,åñëèâòî÷êå,ãäåïðîèñõîäèòäîñòóïê
se
,ôîðìóëà
G
e
^
IsNull
se
e
(
~
b
i
)
âûïîëíèìà,òîâûäàåòñÿîøèáêàîâîçìîæíîì
äîñòóïåê
null
.
Òåîðåìà5.1
.Èçâûïîëíèìîñòèôîðìóëû
G
e
^
IsNull
se
e
(
~
b
)
ñëåäóåò
íàëè÷èåîøèáêèïîîïðåäåëåíèþ
Err

i
=
~
b
i
.
Ïóñòü
IsNull
se
e;l
(
~
b
i
)
óñëîâèåòàêîãî,÷òîâòî÷êå
e
äëÿâñåõ
~

2

l
,
se
==
null
.
Òåîðåìà5.2
.Îøèáî÷íûåñèòóàöèè,ñîîòâåòñòâóþùèåâûïîëíèìîñòè
ôîðìóëû
G
l
e
^
IsNull
se
e;l
(
~
b
)
âòî÷êàõäîñòóïàêñèìâîëüíîìóâûðàæåíèþ
se
äëÿâñåõâîçìîæíûõïóòåé
l
,ñîâïàäàþòññèòóàöèÿìèïîîïðåäåëåíèþ(
28
).
Èñïîëüçóÿðåçóëüòàòòåîðåìû5.2,âêàæäîéòî÷êåäîñòóïàìîæíîïî
ñòðîèòüóñëîâèå
G
e
^
IsNull
se
e
(
~
b
)
òàêîå,÷òîåãîâûïîëíèìîñòüýêâèâàëåíòíà
(
28
).Äàëååâäàííîéãëàâåðàññìàòðèâàþòñÿïðàêòè÷åñêèåàñïåêòûðåàëè
çàöèèòàêîéïðîâåðêèèâîïðîñûìåæïðîöåäóðíîãîïîèñêàäîñòóïàê
null
.
Ìåæïðîöåäóðíûéïîèñêïðåäëàãàåòñÿîðãàíèçîâûâàòü,ñîõðàíÿÿâðåçþìå
óñëîâèÿ,ïðèêîòîðûõêñèìâîëüíûìïåðåìåííûìîñóùåñòâëÿåòñÿäîñòóï.
Àëãîðèòìïîèñêàóòå÷åêðåñóðñîâóñòðîåíñõîæèìîáðàçîì.Äëÿêàæ
äîãîðåñóðñà,ïðåäñòàâëåííîãîñèìâîëüíîéïåðåìåííîé,âû÷èñëÿåòñÿóñëî
âèååãîóòå÷êè
LC
s
(
~
b
i
)
.Âñëó÷àå,åñëèâìîìåíòâûõîäàèçìåòîäàôîð
ìóëà
LC
se
(
~
b
i
)
^G
âûïîëíèìà,âûäàåòñÿïðåäóïðåæäåíèåîáóòå÷êåðåñóðñà.
21
Ðàññìàòðèâàþòñÿïðè÷èíû,ïîêîòîðûìïîñòðîåííûéàëãîðèòìïîèñ
êàÿâëÿåòñÿíåñòðîãèì:

ðàçâåðòêàöèêëîâ;

çàìåíàðåçóëüòàòîâàðèôìåòè÷åñêèõâûðàæåíèéâöèêëåíàíåèç
âåñòíûåçíà÷åíèÿ;

ïðåäïîëîæåíèåîáîòñóòñòâèèïñåâäîíèìîââòî÷êàõâõîäà;

íåòî÷íîñòüïîñòðîåíèÿðåçþìå.
Âøåñòîéãëàâå
îïèñûâàåòñÿèíñòðóìåíòñòàòè÷åñêîãîàíàëèçà
SharpChecker,âêîòîðîìðåàëèçîâàííûïðåäëàãàåìûåâäàííîéðàáîòå
àëãîðèòìû.Ïðîâîäèòñÿîöåíêàïðîèçâîäèòåëüíîñòèèàíàëèçðåçóëüòàòîâ
èíñòðóìåíòàSharpChecker.
Ñðåäèàëãîðèòìîâïîèñêàîøèáîê,ðåàëèçîâàííûõâèíñòðóìåíòå
SharpChecker,åñòüêàêèñïîëüçóþùèåèñêëþ÷èòåëüíîñèíòàêñè÷åñêèéàíà
ëèç,òàêèàíàëèçïîòîêîâäàííûõ,àòàêæåíàèáîëååìîùíûé,îïèñàííûé
âäàííîéðàáîòå,÷óâñòâèòåëüíûéêêîíòåêñòóèïóòÿìâûïîëíåíèÿìåæ
ïðîöåäóðíûéàíàëèç.
Âäàííîéãëàâåîñîáîåâíèìàíèåóäåëÿåòñÿîñîáåííîñòÿìðåàëèçàöèè,
ñâÿçàííûìíåïîñðåäñòâåííîñÿçûêîìC
#
,àèìåííîïîñòðîåíèþãðàôàâû
çîâîâèãðàôàïîòîêàóïðàâëåíèÿ.Îáñóæäàþòñÿîñîáåííîñòèïîñòðîåíèÿ
ðåçþìåäëÿâíåøíèõìåòîäîâèñòàíäàðòíîéáèáëèîòåêèÿçûêàC
#
.Ðàñ
ñìàòðèâàåòñÿïîñòðîåíèåïîñèìâîëüíûìâûðàæåíèÿìçàïðîñîâêSMT
ðåøàòåëþ.
Ïðèâîäèòñÿâûïîëíåííàÿîöåíêàýôôåêòèâíîñòèîïòèìèçàöèèðàçìå
Íàçâàíèå
ïðîåêòà
Ðàçìåð
Âðåìÿ
àíàëèçà
NRE
Óòå÷êà
ðåñóðñîâ
Jil
50òûñ.
3ìèí.
32
2
CSParser
60òûñ.
1ìèí.
7
0
CSharpUtils
108òûñ.
2ìèí.
21
107
256òûñ.
19ìèí.
33
876
SharpDevelop
1213òûñ.
23ìèí.
140
182
CodeContracts
1534òûñ.
14ìèí.
64
23
Òàáëèöà1ÐåçóëüòàòûòåñòèðîâàíèÿèíñòðóìåíòàSharpChecker.
ìèðîâàíûâûáîðêè,ïîêîòîðûìïðîâîäèëàñüîöåíêàîòíîøåíèÿèñòèííûõ
èëîæíûõñðàáàòûâàíèé.Îöåíêàïîêàçàëà,÷òîäëÿãðóïïûNREïðîöåíò
èñòèííûõñðàáàòûâàíèéíàõîäèòñÿâ95-ïðîöåíòíîìäîâåðèòåëüíîìèíòåð
âàëå57-74%,àäëÿãðóïïûóòå÷êàðåñóðñîââèíòåðâàëå72-87%.
Â
çàêëþ÷åíèè
ñôîðìóëèðîâàíûðåçóëüòàòûäèññåðòàöèîííîéðàáî
òûèïðèâîäÿòñÿíàïðàâëåíèÿäàëüíåéøèõèññëåäîâàíèé.
Îñíîâíûåðåçóëüòàòûäèññåðòàöèîííîéðàáîòû
1.
Ðàçðàáîòàíàëãîðèòìâíóòðèïðîöåäóðíîãîàíàëèçà,îáëàäàþùèé
÷óâñòâèòåëüíîñòüþêïîòîêóèïóòÿì,ïðèýòîìíåòåðÿþùèéèí
ôîðìàöèþâòî÷êàõîáúåäèíåíèÿ.
2.
Ðàçðàáîòàíàëãîðèòììåæïðîöåäóðíîãîàíàëèçà,÷óâñòâèòåëüíîãî
êêîíòåêñòó,ïîòîêóèïóòÿì,îáîáùàþùèéðåçóëüòàòûâíóòðèïðî
öåäóðíîãîàíàëèçàââèäåðåçþìåìåòîäàèïðèìåíÿþùèéðåçþìå
ïðèîáðàáîòêåâûçîâàäàííîãîìåòîäà.
3.
Ðàçðàáîòàíêðèòåðèéâûäà÷èïðåäóïðåæäåíèé,ó÷èòûâàþùèé÷óâ
ñòâèòåëüíîñòüêïóòÿìïðèïîèñêåäåôåêòîâ,èñïîëüçîâàíèåêî
òîðîãîïîçâîëÿåòäîñòè÷üïðèåìëåìîãîóðîâíÿëîæíûõïðåäóïðå
æäåíèé.Äëÿäàííîãîêðèòåðèÿðàçðàáîòàíûäåòåêòîðû,ïîçâîëÿ
þùèåîáíàðóæèòüîøèáêèâèäà¾äîñòóïïîíóëåâîìóóêàçàòåëþ¿
è¾óòå÷êàðåñóðñîâ¿.
4.
Äîêàçàíàêîððåêòíîñòüïðåäëîæåííîãîàëãîðèòìàâíóòðèïðîöå
äóðíîãîàíàëèçàèñîîòâåòñòâèåðàçðàáîòàííûõäåòåêòîðîââû
áðàííîìóêðèòåðèþâûäà÷èïðåäóïðåæäåíèé.
23
5.
Ðàçðàáîòàíèíñòðóìåíòñòàòè÷åñêîãîàíàëèçà,ðåàëèçóþùèéðàçðà
áîòàííûåàëãîðèòìûäëÿàíàëèçàïðîãðàììíàÿçûêåC
#
.Äëÿäàí
íîãîèíñòðóìåíòàïðîâåäåíàýêñïåðèìåíòàëüíàÿîöåíêàåãîõàðàê
òåðèñòèêíàñîîòâåòñòâèåçàÿâëåííûìòðåáîâàíèÿì.Ïðåäëîæåí
íûåàëãîðèòìûèìåòîäûïîçâîëÿþòïðîâîäèòüàíàëèçïðîåêòîâ,
ñîñòîÿùèõèçáîëååìèëëèîíàñòðîêêîäà,âîòâåä¼ííîåâðåìÿ.Ïðè
ýòîìêà÷åñòâîðåçóëüòàòîâàíàëèçàñîîòâåòñòâóåòçàÿâëåííûìòðå
áîâàíèÿì(áîëåå50%èñòèííûõñðàáàòûâàíèéäëÿðåàëèçîâàííûõ
äåòåêòîðîâ).
Ïóáëèêàöèèíàòåìóäèññåðòàöèè
1.
ÊîøåëåâÂ.Ê.
Ôîðìàëèçàöèÿîïðåäåëåíèÿîøèáîêïðèñòàòè÷åñêîì
ñèìâîëüíîìâûïîëíåíèè//
ÒðóäûÈíñòèòóòàñèñòåìíîãîïðîãðàììè
ðîâàíèÿÐÀÍ
.2016.Ò.28,5.Ñ.105118.
2.
×óâñòâèòåëüíûéêïóòÿìïîèñêäåôåêòîââïðîãðàììàõíàÿçûêåC#
íàïðèìåðåðàçûìåíîâàíèÿíóëåâîãîóêàçàòåëÿ/ÊîøåëåâÂ.Ê.,Äóäè
íàÈ.À.,ÈãíàòüåâÂ.Í.,ÁîðçèëîâÀ.È.//
ÒðóäûÈíñòèòóòàñèñòåì
íîãîïðîãðàììèðîâàíèÿÐÀÍ
.2015.Ò.27,5.Ñ.5986.
3.
Â.Ê.Êîøåëåâ,Â.Í.Èãíàòüåâ,À.È.Áîðçèëîâ
.Èíôðàñòðóêòóðàñòàòè
÷åñêîãîàíàëèçàïðîãðàììíàÿçûêåC#//
ÒðóäûÈíñòèòóòàñèñòåì
íîãîïðîãðàììèðîâàíèÿÐÀÍ
.2016.Ò.28,1.Ñ.2140.
4.
È.À.Äóäèíà,Â.Ê.Êîøåëåâ,À.Å.Áîðîäèí
.Ïîèñêîøèáîêäîñòóïàêáó
ôåðóâïðîãðàììàõíàÿçûêåC/C++//
ÒðóäûÈíñòèòóòàñèñòåìíîãî
ïðîãðàììèðîâàíèÿÐÀÍ
.2016.Ò.28,4.Ñ.149168.
5.
KoshelevV.K.,IzbyshevA.O.,DudinaI.A.
InterproceduralTaintAnalysis
forLLVM-bitcode//
ProgrammingandComputerSoftware
.2015.
Vol.41,no.4.Pp.237245.
6.
ÊîøåëåâÂ.Ê.
Ñòàòè÷åñêèéìàñøòàáèðóåìûéìåæïðîöåäóðíûéàíàëèç
ïîìå÷åííûõäàííûõ//ÌàòåðèàëûÌåæäóíàðîäíîãîìîëîäåæíîãîíà
ó÷íîãîôîðóìà¾ËÎÌÎÍÎÑÎÂ-2014¿.2014.
24

Приложенные файлы

  • pdf 9452326
    Размер файла: 346 kB Загрузок: 0

Добавить комментарий