Aksiomatska semantika

U računarstvu, aksiomatska semantika je jedan od formalizama specificiranja semantike programskih jezika. Značenje računalnog programa nije uopće eksplicitno dano, već su definirana svojstva jezičnih konstrukata preko aksioma i pravila inferencije iz simboličke logike. Svojstvo programa je deducirano iz njih da bi se konstruirao formalan dokaz svojstva.

Ključna ideja jest da se ne definira ponašanje programa (kao npr. operacijskom ili denotacijskom semantikom) i izvođenjem iz tih definicija, već se uzimaju sami zakoni kao definicija jezika. Značenje termina je ono što može biti dokazano o njemu. Ljepota aksiomatskih metoda jest što fokusiraju na proces zaključivanja o programima, postupak koji je u računarstvu doveo do moćnih ideja poput invarijanti.

Jednostavni sustavi mogu npr. samo dozvoljavati dokaze da je jedan program ekvivalentan drugom, kojegod značenje imali. Složeniji sustavi mogu mogu dozvoljavati dokaze o ulazno/izlaznim svojstvima programa. Aksiomatske definicije su apstraktnije od denotacijskih i operacijskih, i svojstva dokazana o programu možda ne budu dovoljna da u potpunosti odrede značenje programa. Ovaj format je najbolji za preliminarne specifikacije jezika kao i da korisnicima da dokumentaciju o zanimljivim svojstvima jezika.

Nedovršeni članak Aksiomatska semantika koji govori o računarstvu treba dopuniti. Dopunite ga prema pravilima uređivanja Hrvatske internetske enciklopedije.