W informatyce , semantyka operacyjnych jest jedną z metod, które służą do nadać sens programów komputerowych w sposób rygorystyczny, matematycznie mówiącej sposób (patrz Semantyka języków programowania ).
Semantyka operacyjna danego języka programowania opisuje, w jaki sposób każdy poprawny program tego języka ma być interpretowany w kategoriach sekwencji kolejnych stanów maszyny.
Ta kontynuacja jest znaczeniem programu.
W przypadku programu funkcyjnego stan końcowy sekwencji, która się kończy, daje wartość zwracaną przez program. W ogólnym przypadku może istnieć kilka sekwencji obliczeń i kilka wartości zwracanych dla jednego programu, ponieważ ten program może być niedeterministyczny .
Jednym z najpowszechniejszych sposobów rygorystycznego definiowania semantyki operacyjnej jest zapewnienie systemu przejść stanów, odzwierciedlającego oczekiwane zachowanie rozważanego programu. Taka definicja pozwala na formalną analizę języka, umożliwiając badanie relacji między programami. Spośród ważnych relacji, symulacji wstępne zamówienia i bisymulacje są bardzo przydatne w kontekście równoległości .
Definiowanie semantyki operacyjnej przez system przejść zwykle odbywa się poprzez podanie indukcyjnej definicji zbioru możliwych przejść. Zwykle przyjmuje to postać zestawu reguł wnioskowania definiujących prawidłowe przejścia w systemie.
Semantyka operacyjna jest powiązana z semantyką denotacyjną poprzez pojęcie abstrakcji .