- Қарастырылып отырған обьектілер есепті шешуге мүмкіндікберетін, нақты, толық және бірмәнді жазылғанпрограмма болыптабылады. Есепті шешу мағынасында оның алғашқы деректермәндерімен аралықнәтижелер алубарысында соңғы нәтижесін табу процесіжатыр. Бұлпроцесспрограмманыорындау арқылыжүзеге асады. Егер программаны орындау күтілген нәтжеге дұрысалып келсе, онда олпрограмма дұрыс деп саналады. Сондықтан, программаны орындау программаның дұрыстығыныңкритерийі қызметінатқарады. Бірақпрограммалау практикасыкөбінесе,алғашқы деректердің кейбірмәндерімен алынған дұрыс нәтижелі программалардың да қателері барлығын көрсетеді. Сондықтанпрограманың дұрыстығындәлелдеу мақсатында (тестілеу) программанынақтыдеректер мәндерімен (тестермен) орындау, практикада ешкөмегін тигізбейді. Толданатынпрограммаға арналғантолықтестілер құрылғаны дәлелденбесе, тестілеуәдісі программадағықатені тауыпбергенімен, оныңжоқтығынешқашан дәлелдей алмайды. Бұлжағдайпрогграмманың дұрыстығын дәлелдейтін әр түрліматематикалық әдістерді ойлаптабуға әкеледі.
Мұндай математикалық әдістердіжасаудың екіжолыбар.Бірінші жол дайынрограмманың дұрыстығын дәлелдеугеүмкіндікбереді, жәнеолпрограмманыверификациялау депаталады. Екінші жолыпрограмманы синтездеу депаталады және дұрыстығы авлдынала дәлелденген программанықұруға мүмкіндікбереді. Программаны верификациялауды программаныдәлелдеу деп, алпрограманы синтездеуді дәлелдеуді программалау деп те атауғаболады. Екі консепцияның ұқсастығы формалды жүйелерде (програмалық, логикалықжүйелерде ) негізделуі жәнеолардың “ спецификация ”дегенұғымдықолдану.
- “Спецификация” (specification) сөзі сипаттама дегендің, ал Спецификациялау сипаттауды білдіреді.
Белгілі бі есепті шешуге арналған программаныжазбастан бұрыналдымен осыесепті түсініп алуқажет, содан кейін оның иСпецификациясын құру керек.Програманы Спецификациялаудеп программа арқылышешілітін есептің формалді сипаттамасын айтады, спецификация тілінде құрылады. Программамен спецификация айырмашылығы : программа – программалаушының компьютерге бергенбұйрығы, ал спецификация- програмалаушыға берілген бұйрық. Пракимка жүзінде программаныспецификациялау, программалауменқатаржүреді. Көпжағдайда спецификация тіліпрограммалаутілінебайланысты. Егерспецификациятілі жасалынып жәнеонытүсінетін программаларжүйесіқұрылса, ондабұлтілпрограммалаутіліне айналады.
Программаның спецификацияғақатыстыдұрыстығы деп,егер программакірісінде өзінеқажетдеректерді алып шығысында қойылған есепке байланысты құрылғанқатынастарды қанағаттандыратын нәтижелер шығаратындығынайтады.
Бұлтүсінікекігебөлінеді: “ дербес дұрыстық ” ( егернәтижешықса, ондаол дұрыс)
- Программаның дұрыстығын дәлелдеу өте қиын, көп және қымбат жұмыс. Программаның дұрыстығын дәлелдеуді программаны верификациялаудеп атайды.Жалпыжағдайда, кезкелген программаны верификациялауәдісіжоқ, оныңболуы дапмүмкін емес. Алайданақтыпрограммалар класына ( табына) арналған программаны верификациялау әідістерін жасауға көзделгенбірнешежолы бар.Программанысинтездеу проблемасы кейбір спецификацияларды қанағаттандыратын программаныңавтоматтытүрде құрылуынаәкеледі.
Кез-келген программаныпрограммалықбірліктеғрінекомпозиция операциясын қолдануқөмегіменқұрумүмкінекенібелгілі. Программалықбірліктерпрограмма жазылғантілдіңмооделінебайланысты. әдеттепрограммалықбірлікретінгдепрограммалау тілінің се мантикасыменанықталатынанықмәнгеиетілдіңсинтаксистік бірлігіалынады. Мұндайбірліктер мысалы, Pascal сияқты императивті( процерадуралық)тілдерді – операторлар Lisp сияқтыфункционалдықтілдерде – функциялар Refal сияқтыалмастырымдылық тіілдерде – алмастырымережелері, ал, Prolog сияқтылогикалық тілдерде – логикалықтұжырымдарболып табылады.
Яғни, қарастырылып отырғанР программасы р1,р2,..., рп программалық бірліктер композитциясынан тұрады. Бұлжағдайда, Р программасының орындалуы Р1, Р2,..., Рппрограммалық бірліктерініңтізбектеліпорындалуына әкеледі. Яғни, Р программасыР 1, орындалмастанбұрыншешілетінесептің барлықалғашқы деректерінің мәндері белгіліболатын бастапқыкүйінде болады, ал Рп орындалғаннан кейіносы есептің барлық нәтижесі анықталғансоңғыкүйіндеболуықажет.