Sémantika programovacích jazyků

V teoretické informatice je formální sémantika ( programovacích jazyků ) studium významu počítačových programů vnímaných jako matematické objekty .

Spojení s lingvistikou

Stejně jako v lingvistice , sémantika aplikovaná na programovací jazyky označuje spojení mezi signifikátorem , programem a významným matematickým objektem. Matematický objekt závisí na vlastnostech, které program zná.

Sémantika je také spojovacím článkem mezi:

značící jazyk: programovací jazyk
označený jazyk: logika Hoare , automaty ...

Běžná sémantika programovacího jazyka

Nejběžnější sémantika používaná k pochopení programovacího jazyka je:

Provozní sémantika

V operační sémantice je významem programu posloupnost stavů stroje, který program provádí. Jinými slovy, program je považován za popis systému přechodu stavu .

V této sémantice programy:

a=1; b=0

jsou ekvivalentní, protože mají stejný význam.

Na druhou stranu program:

b=0; a=1

není s nimi ekvivalentní. Dokonce i když je konečný výsledek stejný, akce přiřazení hodnot k proměnným a a b neprobíhají ve stejném pořadí.

Tuto sémantiku je možné abstrahovat pozorováním pouze části paměti stroje, například:

interakce programu s vnějším světem
stopa programu.

Denotační sémantika

Denotační sémantika, kterou iniciovali Christopher Strachey a Dana Scott , je přístup, při kterém je ke každému programu přidružena matematická funkce zvaná denotace a svým způsobem představuje jeho účinek, jeho význam. Tato funkce přebírá například stav paměti před provedením a má za následek stav po provedení.

V této sémantice jsou všechny výše uvedené příklady operační sémantiky ekvivalentní, ale program:

a=1; b=1;

není s nimi ekvivalentní.

Existuje několik variant denotační sémantiky, jednou z nejznámějších je denotační sémantika pokračováním, která místo přidružení programu k funkci, která transformuje paměť, spojuje ji s funkcí, která transformuje pokračování (budoucnost) stroje po provádění programu a pokračování před provedením programu. Jinými slovy, denotační sémantika pokračováním funguje obráceně od programu, zvažuje, co se stane po instrukci, aby z ní odvodila, co se musí stát před touto instrukcí.

Jedním z důležitých aspektů denotační sémantiky je vlastnost kompozičnosti : denotace programu se získá kombinací denotací jeho složek.

Axiomatická sémantika

V axiomatické sémantice není program nic jiného než transformátor logických vlastností stavu paměti: pokud máme před provedením p true, pak máme q true po. Už nás nezajímá přesný stav paměti, pokud víme, zda vlastnost platí.

Pokud vlastnost, o kterou se zajímáme, je vědět, zda a a b jsou po provedení programu kladné, pak jsou všechny předchozí příklady ekvivalentní v tom smyslu, že bez ohledu na stav stroje před provedením programu platí en en. Co si všimneme v logice Hoare :

\ {{{\ text {true}}} \}

a = 1; b = 0

{\ displaystyle \ {a \ geq 0 \ land b \ geq 0 \}}

Vztah mezi různými sémantiky

Tyto tři sémantiky, jak naznačují příklady, nejsou navzájem zcela nezávislé:

dva syntakticky ekvivalentní programy jsou provozně ekvivalentní;
dva provozně rovnocenné programy jsou denotačně rovnocenné;
a dva denotačně ekvivalentní programy jsou axiomaticky ekvivalentní.

Ale obrácení je špatné.

Můžeme tedy hierarchizovat sémantiku tím, že řekneme, že jedna sémantika je abstrakcí jiné právě tehdy, když dva ekvivalentní programy v posledním jsou také ekvivalentní v prvním. Tyto vztahy byly formalizovány teorií abstraktního výkladu .

Tuto hierarchii ( částečné pořadí ) můžeme dokončit na sémantických ekvivalencích tím, že umístíme identitu na začátek (dva programy jsou identické právě tehdy, pokud mají stejnou posloupnost znaků) a dole nejhrubší, která se nazývá chaos , kdy je jakýkoli program ekvivalentní jakémukoli jinému programu.

Dodatky

Související články

Reference

ROGERAPERY, „ Povaha matematických objektů “ , na /www.numdam.org ,1985
(in) Peter Landin, " příštích 700 programovacích jazyků " , CACM , n o Vol 9, číslo 31966, s. 157 - 166.
(in) Joseph E. Stoy, „ denotační sémantika: Scott-Stracheyův přístup k teorii programovacího jazyka. " , MIT Stiskněte. ,1977( ISBN 0-262-19147-4 ).
Tuto myšlenku reverzní sémantiky zvažoval také Dijkstra ve svých predikátových transformátorech
(in) Tony Hoare, „ Základ pro matematickou teorii výpočtu “ , Počítačové programování a formální systémy, Severní Holandsko ,1963.