Sémantika programovacích jazyků: Porovnání verzí

Smazaný obsah Přidaný obsah
→‎Statická sémantika: Oprava 'tipované' na 'typované'
opraveny odkaz Hoarova logika na Hoareova logika, momentalne funguje
Řádek 42:
*'''[[Denotační sémantika]]''', kde je každá fráze jazyka interpretována jako [[denotace]]. Tyto denotace často bývají matematickými objekty, ovšem není to podmínkou. V praxi je nezbytné, aby byly denotace popsány nějakou formou matematického zápisu, která může být formalizována jako denotační [[metajazyk]]. Například denotační sémantika funkčního jazyka často překládá jazyk do [[teorie domén]]. Popis denotační sémantikou může také sloužit pro překlady z programovacího jazyka do denotačního metajazyka a být použit jako základ pro návrh [[Překladač|překladače]].
*'''[[Operační sémantika]]''', kde je provádění jazyka popsáno přímo (nikoliv při překladu). Operační sémantika volně odpovídá [[Interpretovaný jazyk|interpretaci]], kdy je použitý jazyk [[Interpret (software)|interpretu]] obecně matematicky formální. Operační sémantika může definována pomocí abstraktního stroje, který dává frázím význam pomocí přechodu stavů stroje. Alternativně může být operační sémantika definována pomocí syntaktických transformací na fráze samotného jazyka.
*'''[[Axiomatická sémantika]]''', kde je frázím přiřazován význam popisem [[Logika|logických]] [[Axiom|axiomů]], vztahujícím se k nim. Axiomatická sémantika nerozlišuje mezi logickými formulemi, které ji popisují. Jejich význam je přesně to co lze dokázat pomocí nějaké logiky. Příklad axiomatické sémantiky je [[HoarovaHoareova logika]].
 
Rozdíly mezi těmito třemi přístupy mohou být vágní. Ale všechny známé přístupy k formální sémantice používají tyto výše zmíněné tři techniky, nebo jejich kombinace.