Кіріспе

Бағдарламалау тілдерінің мағынасын математикалық зерттеу

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

Тарих

1967 жылы Роберт В. Флойд «Программаларға мағына тағайындау» деген мақаласын жариялады; оның басты мақсаты – «компьютерлік бағдарламалар туралы дәлелдер үшін қатаң стандарт, соның ішінде дұрыстығын, эквиваленттігін және тоқтауын дәлелдеу» болды. Флойд одан әрі былай деп жазды: Біздің тәсілімізде бағдарламалау тілінің семантикалық анықтамасы синтаксистік анықтамаға негізделген. Ол синтаксистік тұрғыдан дұрыс бағдарламадағы тіркестердің қайсысы командаларды көрсететінін және әрбір команданың айналасындағы интерпретацияға қандай шарттар қойылуы керектігін нақты көрсетуі керек. 1969 жылы Тони Хоар Флойдтың идеяларынан бастау алған Хоар логикасы туралы мақала жариялады, бұл қазірде аксиоматикалық семантика деп аталады. 1970 жылдары операциялық семантика және денотациялық семантика терминдері пайда болды.

Қарым-қатынасты сипаттау

Әр түрлі себептерге байланысты, формальды семантиканың әртүрлі арақатынастарын сипаттау қажет болуы мүмкін. Мысалы:
Тіл үшін белгілі бір операциялық семантика, сол тілге арналған аксиоматикалық семантиканың логикалық формулаларын қанағаттандыратынын дәлелдеу. Мұндай дәлелдеу, белгілі бір (операциялық) түсіндіру стратегиясы туралы ойлау, белгілі бір (аксиоматикалық) дәлелдеу жүйесін қолдану арқылы "дұрыс" екенін көрсетеді. Жоғары деңгейдегі машинаның операциялық семантикасы, төмен деңгейдегі машинаның семантикасымен симуляция арқылы байланысты екенін дәлелдеу, мұнда төмен деңгейдегі абстрактілі машинада, берілген тілдің жоғары деңгейдегі абстрактілі машина анықтамасына қарағанда қарапайым операциялар көп болады. Мұндай дәлелдеу төмен деңгейдегі машинаның жоғары деңгейдегі машинаны "адал түрде іске асыратынын" көрсетеді. Абстрактілі түсіндіру теориясы арқылы абстракциялар көмегімен бірнеше семантиканы байланыстыру да мүмкін.