Операциона семантика

Операциона семантика или оперативна семантика је категорија формалне семантике програмског језика у којој су одређена жељена својства програма, као што су исправност, сигурност или сигурност, верификована конструкцијом доказа из логичких изјава о његовом извршењу и процедурама, а не повезивањем математичких значења са његовим условима (денотациона семантика). Оперативна семантика се класифицира у две категорије:

структурна оперативна семантика (или семантика у малом кораку) — формално описује како појединачни кораци рачунања потичу у рачунарском систему
опозициона природна семантика (или семантика великог степена) — описује како се добијају укупни резултати погубљења.

Други приступи за пружање формалне семантике програмских језика укључују аксиоматску семантику и денотациону семантику.

Оперативна семантика за програмски језик описује како се важећи програм тумачи као секвенцу рачунских корака. Ове секвенце тада су значење програма. У контексту функционалних програма, последњи корак у терминацијској секвенци враћа вриједност програма. (Уопштено може бити много повратних вредности за један програм, јер би програм могао бити недетерминистичан; па чак и за детерминистички програм може бити много рачунских секвенци, јер семантика не може прецизно прецизирати који редосљед операција стиже при тој вриједности.)

Можда је прва формална инкарнација оперативне семантике била употреба ламбда рачунара за дефинисање семантике LISP-а.^[1] Апстрактне машине у традицији машине SECD такође су уско повезане.