Программа дисциплины для студентов

Сақталғыштық қасиеті – программа ақыр аяғында «жақсы» күйге келетіндігінде, яғни, барлық айнымалылардың керекті мәндерге ие болатын күйі.

Қауіпсіздік қасиеті – программа ешқашанда «нашар» күйге келмейтіндігіне (кейбір айнымалылар керек емес мәндерге ие болуы мүмкін).

Қауіпсіздік қасиетінің мысалы ретінде жартылай дәлдікті (дұрыстық) алуға болады.

Программа жартылай дәл (дұрыс), егер оның соңғы күйі дұрыс болса (программаның аяқталуының шарты). Егер программаның орындалуы аяқталмаса, ол ешуақытта дұрыс нәтиже бермейді, бірақ программа аяқталуының тарихы болмайды.

Аяқталушылық – сақталғыштық қасиетінің мысалы. Әрбір цикл немесе процедура шақылуы аяқталса программа аяқталады, яғни әрбір тарих ұзындығы шектелген.

Программаның толық дәлдігі – жартылай дәлдік пен аяқталушылықты біріктіретін қасиет: программа толық дәл, егер ол дұрыс нәтиже бере отырып әрқашан аяқталса.

Өзара шығарып тастау – параллель прграммадағы қауіпсіздік қасиетінің мысалы. Нашар күйде мұндай прграмманың екі процесі біруақытта әртүрлі сыныекцияларында әрекеттер орындайды. Ақыр аяғында сын секциясына кіру мүмкіндігі – параллель программадағы сақталғышьық қасиеті мысалы. Жақсы күйлерде әрбір процесс өз сын секциясында орындалады.

Әдістердің бірі тестілеу немесе жөндеу. Оны бір ғана «программаны жібер және нәтижесінде не болатынын қара» сөйлеммен сипаттауға болады. Бұл программаның кейбір мүмкін тарихын іріктеу және олардың тиімділігін тексеруге сәйкес. Мұндай тексерудің кемшілігі әрбір тест бір ғана орындалу тарихына қатысты, ал шектелген тестер саны нашар тарихтардың болмайтындығын демонстрациялауға қабілеттілігіне күмән келтіреді.

Екінші әдіс – «жағдайлардың толық анализі» деп атауға болатын операторлық пікірлерді қолдану. Ол үшін процесстердің бөлінбейтін әрекеттерінің ауысу әдістері анализденеді. Бірақ бөлінбейтін әрекеттерінің ауысу әдістері анализденеді. Бірақ параллель программада мүмкін тарихтар саны өте үлкен (сондықтан әдіс өте ұзақ). Прарллель программа n процесстен тұрады және олардың әрбіреуі m бөлінбейтін әрекет орындайдыдеп есептейік. Сонда программаның әртүрлі тарихы (n-m)!(m!). Әрбіреуі екі бөлінбейтін амалды орындайтын үш программадан тұратын процесстің әртүрлі 90 тарихы болады. Әрбір процесс амалдар тізбегін орындайтындықтан ол үшін m әрекеттен бір ғана рет болуы мүмкін: бөлімі реті дұрыс еместердің бәрін лақтырып тастайды. Бұл формула әрбір қолодада карталар реті сақталадыдеген шарт орындалғанда m картаы бар n колоданы ауыстыру сынының формуласын береді.

Үшінші әдіс – тұжырымдамалық пікірлерді қолдану, оны «абстракциялы анализ» деп атауға болады. Бұл әдісте предикаттар логикасының формулаларын тұжырымдамалар деп атайды және қалып-күй жиынтығын сипаттау үшін қолданылады – мысалы, х>0 болатын барлық қалып-күйлер. Бір предикатты қанағаттандыратын программаның қалып-күйі, басқасына қанағаттандыратын қалып-күйге өзгеретіндіктен бөлінбейтін әрекеттер предикаттық түрлендірулер ретінде қарастырылады. Бұл әдістің артықшылығы - қалып-күйлер және олардың түрлендірулерді ыңғайлы ғып өрнектеу. Бұл әдіс программаны құру және анализ жасау әдісіне алып келеді, соған сәйкес жұмыс көлемі программадағы бөлінбейтін әрекеттер санына тура пропационал.