Кіріспе

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

Шолу

Анықтама тілдері әдетте тікелей орындалмайды. Олар не істеу керектігін, қалай істеу керектігін емес, сипаттау үшін арналған. Егер талаптардың сипаттамасы қажетсіз орындалу егжей-тегжейімен толтырылса, ол қате саналады. Көптеген сипаттама тәсілдерінің негізгі болжамы – бағдарламалар дерек мәндері жиынтығын және осы жиынтықтардағы функцияларды қамтитын алгебралық немесе модельдік-теориялық құрылымдар ретінде модельденеді. Бұл абстракция деңгейі бағдарламаның кіріс/шығыс мінез-құлқының дұрыстығы оның барлық басқа қасиеттерінен басым екендігі көзқарасына сәйкес келеді. Қасиетке бағытталған сипаттама тәсілінде (мысалы, CASL-де) бағдарламалардың сипаттамалары негізінен логикалық аксиомалардан тұрады, әдетте теңдік маңызды рөл атқаратын логикалық жүйеде, функциялардың қанағаттандыруы тиіс қасиеттерін сипаттайды – көбінесе олардың өзара байланысы арқылы. Бұл VDM және Z сияқты құрылымдардағы модельге бағытталған сипаттамадан өзгеше, ол қажетті мінез-құлықтың қарапайым іске асырылуынан тұрады. Сипаттамалар нақты іске асырылудан бұрын жетілдіру процесіне (орындалу егжей-тегжейін толтыру) ұшырауы керек. Мұндай жетілдіру процесінің нәтижесі – орындалатын алгоритм, ол бағдарламалау тілінде немесе қолдағы сипаттама тілінің орындалатын кіші жиынтығында құрастырылады. Мысалы, дұрыс қолданылған Хардтманн құбырлары тікелей орындалатын дерек ағыны сипаттамасы ретінде қарастырылуы мүмкін. Тағы бір мысал – актерлік модель, ол нақты қолданба мазмұнына ие емес және орындалуы үшін мамандануы керек. Сипаттама тілдерінің маңызды қолданылуы – бағдарламаның дұрыстығын дәлелдеуге мүмкіндік беру (теореманы дәлелдеушіге қараңыз).