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

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

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

Процедуралық программалау тілдерінде программалық бірлік болып программалық объектілерге қарапайым әрекет жасауды көрсететін және анықтамалары программалау тілінің интерпретациялау ережесінде дәл берілген қарапайым оператор немесе әрекеттер тізбегін сипаттайтын құрамында басқа операторлар болатын күрделі оператор есептелінеді. Яғни, кез келген программаны күрделі оператор деп қарастыруға болады.

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

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

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

2 Операторлардың семантикасын алатын болсақ, онда оларды келесі түрде анықтауымызға болады:

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

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

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

1) алғышартты қайталау күрделі S әрекеті белгілі В шарты ақиқат болып тұрғанша қайталау денесі S1 әрекетін орындауды қайталау керек, ал кері жағдайда еш нәрсе орындамау керек дегенді көрсетеді;

2) соңғышартты қайталау күрделі S әрекеті қайталау денесі болатын берілген S1 әрекетін орындауды белгілі В шарты шарты жалған болып тұрғанша қайталай беру керек, ал кері жағдайда қайталауды тоқтату дегенді көрсетеді.

Операторлар симантикасан білмей тұрып нақты программа жазылмайды және олардың верификациялау әдісі жасалмайды.

Төменде процедуралық программалау тілдеріндегі программаларды верификациялаудың үш әдісі қарастырылады.

Бірінші әдісі – Флойдтың индуктивті тұжырымдау әдісі (Floyd, 1967). Келесі әдіс – Маннаның редукциялық әдісі (Манн, 1969). Соңғы әдіс – Хоардың аксиоматикалық әдісі (Hoar, 1969).

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

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

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

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

1) Программаның түйін нүктелері анықталады: оларға программаның енгізу нүктесі, шығару нүктесі және аралық нәтеже шығатын барлық нүктелері жатады;

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

3) Программаның орындалу жолдары ерекшелінеді, ол үшін алдымен, егер программада қайталау операторлары болса, онда қайталау тілінде (қайталаудың қатпары тарқатылады),

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

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

11 Программаны верификациялаудың логика-математикалық әдістері

Флойд әдісі бойынша программаның дұрыстығын дәлелдеу дегенміз соңғышарттың ақиқаттығы алғышарт ақиқаттылығынан және барлық аралықшарттар ақиқаттылығынан шығатындығын дәлелдеу.

Сонымен талданатын Р программасы р₁, р₂, ..., р_n программалық бірліктерінен тұрғызылған болсын, яғни, әрбір программалық бірлік р₁(t=1,n) меншіктеу операторы, тармақталу операторы, тармақталу операторы, қайталану операторы немесе, топталу операторы болады. Р программасының верификациялау шарты cν (Р,і_р,о_р) арқылы белгіленсін, яғни,

cν (Р,і_р,о_р) → (і_р(Х,) ∩ r_р1(х,у)|_р2 ) & (r_р1(х,у) ∩ r_р2(х,у)_р2) &...& (r_рn-1(х,у) ∩ о_р(X,y)

Мұнда енгізу векторы Х(х₁,х₂), x₁ - бөлінгіш, х₂ - бөлгіш; аралық векторы (у₁,у₂), у₁ - аралық бөлінді, у₂ – аралық қалдық;

Шығару векторы Z=(z₁,z₂), z₁ - бөлінді, z₂ - қалдық.

a, b және c - программаның түйін нүктелері, бұл нүктелерде келесі тұжырымдар құрылады:
a: і_р (х₁,х₂)х₁ 0х₂0

b: r_p1(x₁,x₂,y₁,y₂)x₁=y₁*x₂+y₂y₂0

c: o_p(x_1,x₂,z₁,z₂)x₁=z₁*x₂+z₂z₂0x₂z₂
b түйін нүктесінде қайталау тілінеді, нәтижесінде программа үш жолға бөлінеді: бірінші жол а-дан b-ға дейін (1-ші және 2-ші жол кесінділері), екінші жол қайталау бойынша b-дан b-ға дейін (2-ші, 3-ші және 4-ші жол кесінділері), үшінші жол b-дан c-ға дейін (2-ші, 5-ші және 6-шы жол кесінділері).

Верификациялау шарттарын құру жол операторларын кері бағытта (ретте) қарастыру нәтижесінде жүзеге асырылады.

Бірінші жол үшін:

І_р(х₁,х₂,)  (х₁,х₂,у₁,у₂,)_у10,_у2  х₁

яғни, х₁0х₂0  х₁0*х₁+х₂х₁0

Екінші жол үшін:

rp1(х1,х2,у1,у2,)  (у2х2  rp2(х1,х2,у1,у2,)у1у+1,у2у2-х2

Үшінші жол үшін:

r_p2(X_1, X_2, y_1, y₂)  (x₂ y₂  o_p(x_1,x_2,z_1,z₂)z₁₌y₁ ),

z₂₌y₂

яғни,

x₁₌y₁x₂₊y₂y₂ O  (x₂y₂  x₁₌y₁* x₂₊y₂ y₂ Ox₂y₂) (3)

(1) – формуладан арифметикалық амалдард орындап біткен соң мынадай x₁x₂o  x₁=x₁x₁o логикалық өрнек шығады, мұндағы x₁=x₁- 2h әр қашанда ақиқат (тавтология), сондықтан оны қысқартып тастап өрнектен мынадай X₁O  x₂O  x₁O формула алуға болады.

(2) – формуладан арифметикалық амалдарды орындап біткен соң және (С) және С түріндегі формулалардың логикалық теңмәнділігін, сондай-ақ, конъюнкцияның коммутативтілігін ескере отырып,  түріндегі аксиоманы (мәні әрқашан ақиқат формуланы) алуға болады, яғни,
x₁=y₁* x₂+y₂ y₂x₂ y₂ O x₁=y₁ * x₂+y₂x₂

(3) – формуланы түрлендіре отырып D  D түріндегі аксиоманы алуға болады, мұнда D арқылы мына х₁=y₁ *x₂+y₂ y₂ x₂ y₂ өрнегі белгіленеді.

Енді алынған (1), (2) және (3) верификациялау шарттарының ақиқаттығын тексеру үшін мән орнату функциясы VAL-ң көмегімен х₁ және х₂ енгізу айнымалылары үшін нақты тестілік деректер алайық, мысалы, VAL (х_1, х₂) = (7,3) болсын. Сонда верификациялау шарттары бойынша айнымалылар үшін келесі мәндерді аламыз:
7О 3О 7=О*7+7  7О; (1)

7=1*3+4 & 4O(43 Й 7=(1+1)* 3+4-3 & 43; (2)

7=2*3+1& 1O(317=2*3+1&31) (3)
(1), (2) және (3) өрнектердің ақиқаттығы көрініп тұр, яғни, P программасын верификациялау шарты сv(Р, і, о ) ақиқат болады, ол жоғарыдағы теорема бойынша і_р {p}o_p-ң ақиқаттығын көрсетеді. Ендеше, біз қарастырған бүтін санды бүтін санға бөлуді орындайтын 3 программасы дербес дұрыс.

Практикалық жұмыстарды орындауға әдістемелік нұсқаулар

1-2 практикалық жұмыс. Негізгі интеллектуалдық құралдардың математикалық алғышарттары

		(1-ші ереже: ақиқат)
		(2-ші ереже: жалған)
		(3-ші ереже: идентификатор)
		(4-ші ереже: теріске шығару)
		(5- ші ереже: дизъюнкция)
		(6- ші ереже: шартты Немесе)
		(7- ші ереже: конъюнкция)
		(8- ші ереже: шарттыЖәне)
		(9- ші ереже: импликация)
	e	(10- ші ереже: эквиваленттілік)

Аталған грамматиканың жалғыз метасимволы _ болып табылады, ал алфавиті











2-кесте – Ақиқаттық кестесі

_