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

Лекция 10

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

Мұндай математикалық әдістерді жасаудың екі жолы бар. Бірінші жол дайын рограмманың дұрыстығын дәлелдеуге үмкіндік береді, және ол программаны верификациялау деп аталады. Екінші жолы программаны синтездеу деп аталады және дұрыстығы авлдын ала дәлелденген программаны құруға мүмкіндік береді. Программаны верификациялауды программаны дәлелдеу деп, ал програманы синтездеуді дәлелдеуді программалау деп те атауға болады. Екі консепцияның ұқсастығы формалды жүйелерде (програмалық, логикалық жүйелерде ) негізделуі және олардың “ спецификация ”деген ұғымды қолдану.

Белгілі бі есепті шешуге арналған программаны жазбастан бұрын алдымен осы есепті түсініп алу қажет, содан кейін оның и Спецификациясын құру керек. Програманы Спецификациялау деп программа арқылы шешілітін есептің формалді сипаттамасын айтады, спецификация тілінде құрылады. Программамен спецификация айырмашылығы : программа – программалаушының компьютерге берген бұйрығы, ал спецификация- програмалаушыға берілген бұйрық. Пракимка жүзінде программаны спецификациялау, программалаумен қатар жүреді. Көп жағдайда спецификация тілі программалау тіліне байланысты. Егер спецификация тілі жасалынып және оны түсінетін программалар жүйесі құрылса, онда бұл тіл программалау тіліне айналады.

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

Бұл түсінік екіге бөлінеді: “ дербес дұрыстық ” ( егер нәтиже шықса, онда ол дұрыс)

Кез-келген программаны программалық бірліктеғріне композиция операциясын қолдану қөмегімен құру мүмкін екені белгілі. Программалық бірліктер программа жазылған тілдің мооделіне байланысты. әдетте программалық бірлік ретінгде программалау тілінің се мантикасымен анықталатын анық мәнге ие тілдің синтаксистік бірлігі алынады. Мұндай бірліктер мысалы, Pascal сияқты императивті ( процерадуралық) тілдерді – операторлар Lisp сияқты функционалдық тілдерде – функциялар Refal сияқты алмастырымдылық тіілдерде – алмастырым ережелері, ал, Prolog сияқты логикалық тілдерде – логикалық тұжырымдар болып табылады.

Яғни, қарастырылып отырған Р программасы р_1, р_2,..., р_п программалық бірліктер композитциясынан тұрады. Бұл жағдайда, Р программасының орындалуы Р_1, Р_2,..., Р_п программалық бірліктерінің тізбектеліп орындалуына әкеледі. Яғни, Р программасы Р _1, орындалмастан бұрын шешілетін есептің барлық алғашқы деректерінің мәндері белгілі болатын бастапқы күйінде болады, ал Р_п орындалғаннан кейін осы есептің барлық нәтижесі анықталған соңғы күйінде болуы қажет.

Лекция 11

Тақырыбы: Программаның спецификациясын құру

Енгізу айнымалылары алғашқы деректерді, программалық айнымалылары арқылы нәтижелерді, ал шығару айнымалылары соңғы нәтижелерді, беруге арналған. Осы айнымалылар сәйкес векторларды топатаса алады:

1. 
   мәндері алғашқы кезеңде белгілі болатын және программаны орындау кезінде өзгермейтін енгізу айнымалыларынан тұратын енгізу векторы. Х=( х_1, х_2,..., х_к );
   
2. 
   мәндері программаның орындалу барысында арлық жағдайда айқындалатын, программалық айнымалылардан тұратын орындалу векторы; y= (y, y₂,…, y₁ );
   
3. 
   мәндері программаның соңғы жағдайында айқындалатын, шығару айнымалыларынан тұратын шығару векторы, Z=(z₁,z₂,…, z_m ).
   

Inp(p)

Сәйкесінше, әр программалық бірлік р_t, tn, үшін бос емес жиын inp (p)6 out (p₁), белгілеуге болады.Мұнда,

Ip (p₁)=inp out(p_n) = out (p)

Сонымен қатар, үшін

Inp(p₁) ran (p), out(p₁) ran(p)

Егер осы векторлардың мәнін анықтайтын функция val болса, онда:

Val (x) =,val (y) = , val (x)=,

Мұнда inp (p), out (p).

Енгізу векторының мәні туралы және Р програмасының бастапқы жағдайын анықтайтын і_р(х) тұжырымды алғышарт деп атайды яғни, і_р (х): inp (p) {0,1},

Мұнда 0- логикалық “жалған” мән, ал, 1- логикалық “ақиқат” мән.

Енгізу және шығару векторларының байланысы туралы және программаның аралық жағдайын анықтайтын r_p(x,y), t=2,n- 1

Тұжырымды аралықшарттар деп атайды, яғни,

R_p1(x,y): inp (p) {0,1}

Р программасы і_р (х) – те аяқталады дейді, егер кез- келген Х үшін і_р (х) ақиқат болса және Р программасын орындау оның соңғы жағдайына алып келетін болса, яғни, Р(Х) анықталған.

Р программасы і_р (х) анықталмаған дейді, егер Р программасында шексіз орындауды талап ететін қандай-да бір құрылым бар болса, яғни, Р(х) анықталмаған.

Р программасы і_р (х) мен о_р (Х,Z) – ке қатысты дербес дұрыс дейді, егер кез- келген Х үшін і_р (х) ақиқат болатындығынан және Р программасын орындау і_р (Х) –те аяқталатындығынан о_р (x,z) -ң ақиқаттығы шығатын болса.

Егер Р программасының і_р (х) мен о_р (Х,Z) – ке қатысты дербес дұрыстығын і_р {P} o_p деп белгілесек, онда ол формалды түрде былай анықтайды.

і_р {P} o_p [( і_р (х) & p(x)=z) o_p (x,z)]

мұнда - анықтама бойынша деген таңба.

4 Анықтама.

Р программасы і_р (х) мен о_р (Х,Z) – ке қатысты толық дұрыс дейді, егер кез- келген Х үшін і_р (х) ақиқат болатындығынан Р программасын орындау і_р (х)- те аяқталатындығы және о_р (Х,Z) –ң ақиқаттығы шықса.