Лекция 18 Тақырыбы: Программаның дұрыстығын дәлелдеу әдістері

Лекция 18

Тақырыбы: Программаның дұрыстығын дәлелдеу әдістері

1. 
   Програманың дұрыстығын дәлелдеу әдісі
   
2. 
   Операторлардың семантикасы
   
3. 
   Флоид әдісі
   

1. Программалардың дұрыстығын дәлелдеу әдістерінің алғашқылары Флойд әдісі, Манна әдісі және Хоар әдісі. Олар процедуралық программалық тілдерге арналған.

Процедуралық программалау тілдерінде программалық бірлік болып программалық объектілерге қарапайым әрекет жасауды көрсететін және анықтамалары программалау тілінің интерпретациялау ережесінде дәл берілген қарапайым оператор немесе әрекеттер тізбегін сипаттайтын құрамында басқа операторлар болатын күрделі оператор есептелінеді. Яғни, кез келген программаны күрделі оператор деп қарастыруға болады.
Қарапайым әрекет болып меншіктеу, ал күрделі әрекет ретінде тізбектеу, тармақталу немесе қайталау саналады. Сонда программаның синтаксисін Бэкус-Наур формуласының (БНФ) көмегімен жазуға болады:
<прорамма> : : = <оператор> | <оператор> <программа>

<оператор> : : = <меншіктеу> | <тізбектеу>| <тармақталу>|

<қайталау>| stop

<меншіктеу> : : = <айнымалы> <өрнек>
Анықтамаларын басқа ереже арқылы анықтауды талап ететін объектілердің атауы бұрыштама жақша “<” және “>” арасында жазылады. Олар ереженің сол жағында да, оң жағында да кездеседі. Басқа ереже арқылы анықтауды қажет етпейтін өздігінен анықталған объектілер ереженің оң жағынан орын алады, мысалы, stop.

Жоғарыда, программа синтаксисіне толық мәлімет берілмегендігін, нақты программалау тілімен сипатталатын кейбір операторлардың анықтамасы жоқ екендігі айтқан жөн. Себебі, олардың толық анықтамасы жоқ бейнеленуі нақты программалау тілімен анықталады. Дегенмен, “айнымалы”, “өрнек ”, (шарт( сияқты объектілерінің анықтамасы төменде тақырыптың мазмұны жазу барысында беріледі.

1. 
   <айнымалы> ← <өрнек>түрінде берілген меншіктеу операторын қарастырайық, мұнда “←” –меншіктеу амалының белгісі болады, ол әр программалау тілінде әр түрлі белгімен берілуі мүмкін, мысалы, “:=” –Pascal тілінде, “=”- Basic тілінде. Мнешіктеу операторының орындалуы екі этапта өтеді: алдымен өрнектің мәні есептелінеді, сонда кейін осы есептелінген мән айнымалыға меншіктеледі. Осылай, меншіктеу операторы айнымалы мәнін анықтау немесе қайта анықтау қызметін атқарады. Өрнектің мәнін есептегенде оған қатысатын айнымалының соңғы меншіктелінген мәні алынады;
   
2. 
   Тізбектеу операторы күрделі S әрекеті өзінің құрамына кіретін және орындалулары бірінен кейін бірі болатын саны шекті S1,S2,…,SN операторларының тізімі анықтайды.
   
3. 
   Тармақталу операторы үш түрге бөлінеді:
   

-балама тармақталу күрделі S әрекет белгілі бір В шартына байланысты берілген S1 әрекетін немесе S2 әрекетін орындау керек дегенді көрсетеді;

-көп мәнді тармақталу кұрделі S әрекеті белгілі айнымалы шама V өзінің әр түрлі мүмкін 1,2,..., N мәндерінің біреуін міндетті түрде қабылдауына сәйкес берілген әр түрлі S1,S2,…,SN әрекетінің біреуі міндетті түрде орындалуы қажет дегенді көрсетеді.

4) Қайталау операторы екі түрі бар:

• 
  алѓышартты ќайталау к‰рделі S єрекеті белгілі В шарты аќиќат болып т±рѓанша ќайталау денесі S1 єрекетін орындауды ќайталау керек, ал кері жаѓдайда еш нєрсе орындамау керек дегенді кµрсетеді;
  
• 
  соњѓышарты ќайталау к‰рделі S єрекеті ќайталау денесі болатын берілген S1 єрекетін орындауды белгілі В шарты шарты жалѓан болып т±рѓанша ќайталау беру керек, ал кері жаѓдайда ќайталауды тоќтату дегенді кµрсетеді.
  

3. Тµменде процедуралыќ программалау тілдеріндегі программаларды верификациялаудыњ ‰ш єдісі ќарастырылады.

Бірінші єдісі- флойдтыњ индуктивті т±жырымдау єдісі (Floyd 1967). Келесі єдіс – Маннаныњ редукциялыќ єдісі ( Манн 1969). Соњѓы єдіс- Хоардыњ аксиоматикалыќ єдісі (Hoar 1969).

Б±л єдістердіњ барлыѓы программмалыќ бірліктердіњ семантикасыныњ сипаттауѓа талап етеді. Сондыќтан осы єдістерде ќолданылѓан идеяны т‰сіну жєне оларда ќолданылѓан формалды ќ±рлымдарды білу программалаудыњ теориясыныњ айналушыларѓа µте пайдалы.

Флойдтың индуктивті тұжырымдау әдісі

Қарастырылып отырған обьектілер блок -схема тілінде берілген меншіктеу,тізбектеу, тармақталу, қайталау операторларынан тұратын программаның стандартты схемасына жататын программалар.

Әдістің негізгі мәні мынада:

1. 
   Программаның түйін нүктелері анықталады: оларға программаның енгізу нүктесі, шығару нүктесі және аралық нәтеже шығатын барлық нүктелері жатады;
   
2. 
   Түйін нүктелер программанның айнымалыларына байланысты тұжырымдармен жабдықталады: енгізу нүктесінде- алғышарт, аралық нүктелерде – аралықшарттар, ал шығару нүктесі- соңғы шарт, мұнда алғышарт әрқашан ақиқат болады деп саналады, ал аралық шарттар мен соңғы шарт программаның орындалуы осыларға сәйкес нүктелерге жеткенде ғана ақиқат бола алады;
   
3. 
   Программанын орындалу жолдары ерекшелінеді, ол үшін алдымен, егер программада қайталау операторлары болса, онда қайталау тілінде (қайкалаудың қатпары тарқатылады),
   

4. 
   Соңғы қадамда жасалынған түрлендіруді ескере отырып соңғы шарттывң ақиқаттығын дәлелдегенге шейін барлық верификатциялау шарттарының ақиқаттылығы біртінгдеп дәлелденеді. Мұнда кез келген қадамда пайда болған верификациялау шартының қарама- қайшылығы, егер верификациялау шартының өзі дұрыс құрылған болса, программада қателер барлығын дәлелдейді.