Программисттың логикалық мәдениетінің информатика-математикалық негіздері

1 слайд
Программисттың логикалық мәдениетінің информатика- математикалық негіздері Бағдарламалық қамтамасыз етудің сапасын қадағалау және қателерін табу - верификация мен валидацияның негізгі міндеті. Бұл процестер бір мақсатқа бағытталғанымен, әдістері мен ережелерінде айырмашылықтар бар. Верификация жұмыс барысында жасалған артефакттардың бұрын жасалған немесе негізге алынған артефакттарға, сондай-ақ ережелер мен стандарттарға сәйкестігін тексереді. GA by Gani Abdumalik

1 слайд

2 слайд
Верификация процесі Верификация бағдарламалық жасақтаманың әртүрлі аспектілерін тексереді. Бұл процесс стандарт нормаларының арасындағы сәйкестікті, бағдарламалық жасақтамаға қойылатын талаптарға сәйкестікті, жобалық шешімдердің, бастапқы кодтың және қолданылған құжаттардың сәйкестігін қамтиды. Сонымен қатар, қойылған талаптар, құжаттар және код белгілі бір мемлекеттің нормалары мен стандарттарына сай екендігі тексеріледі. 1 Стандарттарға сәйкестік Бағдарламалық жасақтаманың қолданыстағы стандарттарға сәйкестігін тексеру 2 Талаптарға сәйкестік Бағдарламалық жасақтаманың қойылған талаптарға сәйкестігін бағалау 3 Құжаттама мен кодты тексеру Жобалық шешімдердің, бастапқы кодтың және құжаттаманың өзара сәйкестігін тексеру

2 слайд

3 слайд
Программа спецификациясының айнымалылары Программаның спецификациясын құру үшін түрлі айнымалылар қажет. Олар үш негізгі топқа бөлінеді: енгізу, программалық және шығару айнымалылары. Енгізу айнымалылары алғашқы деректерді беруге арналған. Программалық айнымалылар аралық нәтижелерді сақтауға қолданылады. Ал шығару айнымалылары соңғы нәтижелерді беруге арналған. Енгізу айнымалылары Алғашқы деректерді сақтайды және программаны орындау кезінде өзгермейді Программалық айнымалылар Аралық нәтижелерді сақтайды және программаның орындалу барысында өзгереді Шығару айнымалылары Соңғы нәтижелерді сақтайды және программаның соңғы жағдайында анықталады

3 слайд

4 слайд
Айнымалылар векторлары Программа спецификациясындағы айнымалылар сәйкес векторларды құрайды. Енгізу векторы X=(x1, x2, ..., xk) алғашқы кезеңде белгілі болатын және программаны орындау кезінде өзгермейтін енгізу айнымалыларынан тұрады. Орындалу векторы Y=(y1, y2, ..., yl) программаның орындалу барысында анықталатын программалық айнымалылардан тұрады. Шығару векторы Z=(z1, z2, ..., zm) программаның соңғы жағдайында анықталатын шығару айнымалыларынан тұрады. Енгізу векторы (X) Алғашқы деректерді қамтиды және программа орындалу барысында өзгермейді Орындалу векторы (Y) Программаның орындалу барысында анықталатын аралық мәндерді сақтайды Шығару векторы (Z) Программаның соңғы нәтижелерін қамтиды

4 слайд

5 слайд
Программа жиындары Әрбір P программасы үшін үш негізгі жиын анықталады: inp(p) - енгізу векторлары мәндерінің жиыны, ran(p) - орындалу векторлары мәндерінің жиыны және out(p) - шығару векторлары мәндерінің жиыны. Бұл жиындардың барлығы бос емес. Әрбір программалық бірлік pt, t=1,n үшін inp(pt) және out(pt) жиындары анықталады, мұнда inp(p1)=inp(p) және out(pn)=out(p). Сонымен қатар, t=2,n-1 үшін inp(pt) ⊆ ran(p) және out(pt) ⊆ ran(p). inp(p) Енгізу векторлары мәндерінің жиыны ran(p) Орындалу векторлары мәндерінің жиыны out(p) Шығару векторлары мәндерінің жиыны

5 слайд

6 слайд
Программаның шарттары Программаның спецификациясында үш түрлі шарт анықталады: алғышарт, аралықшарт және соңғы шарт. Алғышарт ip(x) енгізу векторының мәні туралы және P программасының бастапқы жағдайын анықтайды. Аралықшарт rpt(x,y), t=2,n-1 енгізу және шығару векторларының байланысы туралы және программаның аралық жағдайын анықтайды. Соңғы шарт op(x,z) программаның соңғы нәтижесін анықтайды. 1 Алғышарт (ip(x)) Программаның бастапқы жағдайын анықтайды 2 Аралықшарт (rpt(x,y)) Программаның аралық жағдайын анықтайды 3 Соңғы шарт (op(x,z)) Программаның соңғы нәтижесін анықтайды

6 слайд

7 слайд
Программаның аяқталуы және дұрыстығы Программаның аяқталуы мен дұрыстығы үш негізгі анықтамамен сипатталады. Біріншіден, P программасы ip(x)-те аяқталады, егер кез-келген x үшін ip(x) ақиқат болса және P программасын орындау оның соңғы жағдайына алып келсе. Екіншіден, P программасы ip(x)-те анықталмаған, егер программада шексіз орындауды талап ететін құрылым болса. Үшіншіден, P программасы ip(x) мен op(x,z)-ке қатысты дербес дұрыс, егер ip(x) ақиқат болуынан және P программасының ip(x)-те аяқталуынан op(x,z)-нің ақиқаттығы шықса. Аяқталу Программа соңғы жағдайға жетеді Анықталмағандық Программада шексіз орындалу бар Дербес дұрыстық Алғышарттан соңғы шарт шығады

7 слайд

8 слайд
Программаның толық дұрыстығы P программасы ip(x) мен op(x,z)-ке қатысты толық дұрыс деп аталады, егер кез-келген x үшін ip(x) ақиқат болуынан P программасын орындау ip(x)-те аяқталатындығы және op(x,z)-нің ақиқаттығы шықса. Бұл анықтама программаның дербес дұрыстығынан күштірек, өйткені ол программаның аяқталуын да талап етеді. Толық дұрыстықты формалды түрде ip{P}op деп белгілейді және ол келесідей анықталады: ip{P}op ⇔ [(ip(x) & P(x)=z) ⇒ op(x,z)]. Дербес дұрыстық Толық дұрыстық Тек соңғы шарттың ақиқаттығын талап етеді Аяқталуды және соңғы шарттың ақиқаттығын талап етеді Әлсіз шарт Күшті шарт

8 слайд

9 слайд
Программаның дұрыстығын дәлелдеу әдістері Программаның дұрыстығын дәлелдеудің үш негізгі әдісі бар: Флойд әдісі, Манна әдісі және Хоар әдісі. Бұл әдістер процедуралық программалау тілдеріне арналған. Олардың барлығы программалық бірліктердің семантикасын сипаттауды талап етеді. Флойдтың индуктивті тұжырымдау әдісі блок-схема тілінде берілген программаларға қолданылады. Маннаның редукциялық әдісі программаны логикалық формулаға түрлендіреді. Хоардың аксиоматикалық әдісі программаның дұрыстығын аксиомалар мен ережелер жүйесі арқылы дәлелдейді. Флойд әдісі Индуктивті тұжырымдау Манна әдісі Редукциялық әдіс Хоар әдісі Аксиоматикалық әдіс

9 слайд

10 слайд
Флойдтың индуктивті тұжырымдау әдісі Флойдтың әдісі бес негізгі қадамнан тұрады. Бірінші қадамда программаның түйін нүктелері анықталады. Екінші қадамда түйін нүктелер тұжырымдармен жабдықталады. Үшінші қадамда программаның орындалу жолдары ерекшелінеді. Төртінші қадамда верификациялау шарттары құрылады. Соңғы қадамда барлық верификациялау шарттарының ақиқаттылығы дәлелденеді. Бұл әдіс программадағы қателерді анықтауға мүмкіндік береді, егер верификациялау шарттарының қарама-қайшылығы табылса. 1 Түйін нүктелерді анықтау Программаның маңызды нүктелерін табу 2 Тұжырымдарды орналастыру Түйін нүктелерге тұжырымдарды қою 3 Орындалу жолдарын анықтау Программаның мүмкін жолдарын табу 4 Верификациялау шарттарын құру Әр жол үшін шарттарды анықтау 5 Шарттарды дәлелдеу Барлық шарттардың ақиқаттығын тексеру

10 слайд