Operaciona semantika

Operaciona semantika ili operativna semantika je kategorija formalne semantike programskog jezika u kojoj su određena željena svojstva programa, kao što su ispravnost, sigurnost ili sigurnost, verifikovana konstrukcijom dokaza iz logičkih izjava o njegovom izvršenju i procedurama, a ne povezivanjem matematičkih značenja sa njegovim uslovima (denotaciona semantika). Operativna semantika se klasificira u dve kategorije:

• strukturna operativna semantika (ili semantika u malom koraku) — formalno opisuje kako pojedinačni koraci računanja potiču u računarskom sistemu
• opoziciona prirodna semantika (ili semantika velikog stepena) — opisuje kako se dobijaju ukupni rezultati pogubljenja.

Drugi pristupi za pružanje formalne semantike programskih jezika uključuju aksiomatsku semantiku i denotacionu semantiku.

Operativna semantika za programski jezik opisuje kako se važeći program tumači kao sekvencu računskih koraka. Ove sekvence tada su značenje programa. U kontekstu funkcionalnih programa, poslednji korak u terminacijskoj sekvenci vraća vrijednost programa. (Uopšteno može biti mnogo povratnih vrednosti za jedan program, jer bi program mogao biti nedeterminističan; pa čak i za deterministički program može biti mnogo računskih sekvenci, jer semantika ne može precizno precizirati koji redosljed operacija stiže pri toj vrijednosti.)

Možda je prva formalna inkarnacija operativne semantike bila upotreba lambda računara za definisanje semantike LISP-a. Apstraktne mašine u tradiciji mašine SECD takođe su usko povezane.