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

Конотати́вна (операці́йна) сема́нтика – це спосіб опису комп’ютерної системи за допомогою послідовностей кроків обчислення. Ці послідовності описують зміст системи.

Операційна семантика дуже тісно пов’язана з реалізацією системи мовою програмування, оскільки кроки обчислення описуються на мові деякого обчислювача.Такою мовою може виступати звичайна мова програмування.

Загальний спосіб строгого визначення операційної семантики був запропонований ^[en] у 1981 році у його статті «Структурний підхід до операційної семантики» . Він пропонував специфікувати мову обчислювача, на якій будуть записані послідовності кроків роботи системи, за допомогою (state transition system). Такий підхід дозволяв виконувати мови та опису системи.

Визначення операційної семантики системи зазвичай виконується за допомогою індуктивних визначень множин допустимих переходів. Такі визначення можна записати у вигляді правил виводу, що будуть визначати допустимі переходи системи з одного стану в інший.

Мінусом операційної семантики в порівнянні з денотаційною є те що з її допомогою дуже важко доводити якісь твердження про програму, бо для цього потрібно "запустити" її на якомусь ідеалізованому інтерпретаторі.

Див. також

• Денотаційна семантика
• Аксіоматична семантика

Джерела

1. (PDF). Архів оригіналу (PDF) за 19 вересня 2011. Процитовано 26 березня 2010.
2. Gordon D. Plotkin. A Structural Approach to Operational Semantics. Tech. Rep. DAIMI FN-19 - Computer Science Department, Aarhus University, Aarhus, Denmark – 1981 pdf
3. https://bartoszmilewski.com/2014/11/24/types-and-functions/