Sémantika v programování je disciplína , která studuje formalizaci významů konstruktů programovacího jazyka budováním jejich formálních matematických modelů . Různé nástroje mohou být použity jako nástroje pro vytváření takových modelů, například matematická logika , λ-počet , teorie množin , teorie kategorií , teorie modelů , univerzální algebra . Formalizaci sémantiky programovacího jazyka lze použít jak k popisu jazyka, k určení vlastností jazyka, tak k formálnímu ověření .programy v tomto programovacím jazyce.
Sémantika jazyka je sémantický význam slov. V programování, počáteční sémantický význam operátorů , základní jazykové konstrukce atd.
Příklad:
První kód: i=0; while(i<5){i++;} Druhý kód: i=0; do{i++;} while(i<=4);Logicky tyto dva fragmenty kódu dělají totéž, výsledky jejich práce jsou totožné. Sémanticky se přitom jedná o dva různé cykly . Také značky:
<i></i> <em></em>budou na stránce vypadat úplně stejně, to znamená, že budou ve skutečnosti představovat totéž a sémanticky je první značka kurzíva a druhá logický výběr (prohlížeče se zobrazují kurzívou).
Operační sémantika se používá pro syntaktické pojmy jazyka . Zachází s funkcemi jako s textovými dobře zpracovanými definicemi, které poskytují aplikaci na argument, a nikoli jako s funkcemi v matematickém smyslu tohoto termínu.
Existuje klasifikace různých typů operační sémantiky:
Axiomatická sémantika – Sémantiku každého syntaktického konstruktu v jazyce lze definovat jako soubor axiomů nebo inferenčních pravidel, které lze použít k vyvození výsledků tohoto konstruktu. Abychom pochopili smysl celého programu, měly by být tyto axiomy a pravidla vyvozování použity stejným způsobem jako při dokazování běžných matematických vět. Za předpokladu, že hodnoty vstupních proměnných splňují některá omezení, lze axiomy a pravidla odvození použít k získání omezení hodnot jiných proměnných po provedení každého příkazu programu. Když je program spuštěn, získáme důkaz, že vypočítané výsledky splňují nezbytná omezení jejich hodnot vzhledem ke vstupním hodnotám. To znamená, že je prokázáno, že výstup představuje hodnoty odpovídající funkce vypočítané z hodnot vstupu.
Denotační sémantika uvádí skutečné matematické objekty do korespondence s výrazy v programu , tedy výrazy označují ( anglicky označují – odkud „denotační“) jejich hodnoty [1] . Nejvýznamnější, včetně průkopnických výsledků v konstrukci denotační sémantiky byly získány v pracích D. Scotta (Dana Scott) a K. Stracheyho (Christopher Strachey) koncem 60. a začátkem 70. let na Oxfordské univerzitě [2] . Scott jako první postavil model λ-kalkulu založený na konceptu kompletní částečně uspořádané množiny. K tomu používal funkce, které jsou na takové množině spojité.
Interpretační sémantika je popis operační sémantiky konstruktů z hlediska nízkoúrovňových programovacích jazyků ( jazyk assembler , strojový kód ). Tato metoda umožňuje identifikovat pomalu se spouštějící části programu a často se používá v odpovídajících fragmentech programovacích systémů za účelem optimalizace programového kódu .
Translační sémantika je popis operační sémantiky konstruktů z hlediska vysokoúrovňových programovacích jazyků . Pomocí této metody se můžete naučit jazyk podobný tomu, který již programátor zná.
Transformační sémantika je popisem operační sémantiky jazykových konstruktů z hlediska stejného jazyka. Základem metaprogramování je transformační sémantika .
Předmětem neustálého zájmu a zkoumání je konstrukce systémů pro dokazování správnosti, respektive správnosti programů. Jako nejrozvinutější se ukázaly důkazní systémy pro případ správnosti funkčních programů, které sahají až k LCF systému Robina Milnera a systému R. Boyera (R. Boyer) a J. Moora (J. Moore) .
Současný výzkum se zaměřuje na budování systémů založených na konstruktivní logice a na vytvoření analogie mezi programy a důkazy. Je důležité, že jak programy, tak důkazy jsou považovány za ponořené do λ-počtu s typy, což je formální systém vyšších řádů. To zajišťuje, že lze sestavit pouze programy, které se ukončí. Jedním z takových systémů je systém Coq .