Жұмыс бағдарламасы мамандықтың жұмыс оқу жоспары және 20 ж бекітілген элективті пәндер каталогы негізінде әзірленген


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



жүктеу 3,94 Mb.
бет19/25
Дата14.12.2017
өлшемі3,94 Mb.
#4102
түріЖұмыс бағдарламасы
1   ...   15   16   17   18   19   20   21   22   ...   25

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


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

- Операторлардың семантикасы

- Флойд әдісі

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

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

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

<программа>: : = <оператор> | <оператор><программа>

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

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

<меншіктеу>: : = <айнымалы><өрнек>

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

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

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



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

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

- Тармақталу операторы үш түрге бөлінеді:

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 Программаны верификациялаудың логика-математикалық әдістері

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

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

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

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

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

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

b: rp1(x1,x2,y1,y2)x1=y1*x2+y2y20

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

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

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

Ір12,)  (х1212,)у10,у2  х1

яғни, х10х20  х10*х12х10

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



rp1(х1,х2,у1,у2,) (у2х2 rp2(х1,х2,у1,у2,)у1у+1,у2у2-х2

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

rp2(X1, X2, y1, y2)  (x2 y2  op(x1,x2,z1,z2)z1=y1 ),

z2=y2

яғни,

x1=y1x2+y2y2 O  (x2y2  x1=y1* x2+y2 y2 Ox2y2) (3)



Берілген программаның дербес дұрыстығын дәлелдеу, осы программадағы барлық жолдарға арнап құрылған (1), (2) және (3) верификациялау шарттарының ақиқаттығын орнатуға келіп тіреледі.

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

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

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

Енді алынған (1), (2) және (3) верификациялау шарттарының ақиқаттығын тексеру үшін мән орнату функциясы VAL-ң көмегімен х1 және х2 енгізу айнымалылары үшін нақты тестілік деректер алайық, мысалы, VAL (х1, х2) = (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}op-ң ақиқаттығын көрсетеді. Ендеше, біз қарастырған бүтін санды бүтін санға бөлуді орындайтын 3 программасы дербес дұрыс.

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

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



Предикаттар жиынтығы – келесі грамматикадан құралған тіл (1 кесте):

1-кесте – Предикаттар жиынтығы





(1-ші ереже: ақиқат)





(2-ші ереже: жалған)





(3-ші ереже: идентификатор)





(4-ші ереже: теріске шығару)





(5- ші ереже: дизъюнкция)





(6- ші ереже: шартты Немесе)





(7- ші ереже: конъюнкция)





(8- ші ереже: шарттыЖәне)





(9- ші ереже: импликация)



e

(10- ші ереже: эквиваленттілік)

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




болып табылады, мұндағы  жиыны программаның логикалық типті айнымалыларынан тұрады.

Анықтама 1  предикаты  (Жалған), ал  предикаты  (Ақиқат) білдіреді.

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

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





























































































Формулалар:



























, теріске шығарудың инволютивтілігі, екі ретті теріске шығарудың заңы
















жүктеу 3,94 Mb.

Достарыңызбен бөлісу:
1   ...   15   16   17   18   19   20   21   22   ...   25




©g.engime.org 2024
әкімшілігінің қараңыз

    Басты бет
рсетілетін қызмет
халықаралық қаржы
Астана халықаралық
қызмет регламенті
бекіту туралы
туралы ережені
орталығы туралы
субсидиялау мемлекеттік
кеңес туралы
ніндегі кеңес
орталығын басқару
қаржы орталығын
қаржы орталығы
құрамын бекіту
неркәсіптік кешен
міндетті құпия
болуына ерікті
тексерілу мемлекеттік
медициналық тексерілу
құпия медициналық
ерікті анонимді
Бастауыш тәлім
қатысуға жолдамалар
қызметшілері арасындағы
академиялық демалыс
алушыларға академиялық
білім алушыларға
ұйымдарында білім
туралы хабарландыру
конкурс туралы
мемлекеттік қызметшілері
мемлекеттік әкімшілік
органдардың мемлекеттік
мемлекеттік органдардың
барлық мемлекеттік
арналған барлық
орналасуға арналған
лауазымына орналасуға
әкімшілік лауазымына
инфекцияның болуына
жәрдемдесудің белсенді
шараларына қатысуға
саласындағы дайындаушы
ленген қосылған
шегінде бюджетке
салығы шегінде
есептелген қосылған
ұйымдарға есептелген
дайындаушы ұйымдарға
кешен саласындағы
сомасын субсидиялау