Semantica formala

În domeniul informaticii teoretice , termenul semantică formală se referă la modelele matematice care definesc formal limbajele de programare sau, mai general, la calculul în sine.

Există mai multe abordări ale studiului acestor semantici; care se încadrează în 3 categorii principale:

Semantica denotațională ; care se ocupă cu formalizarea executării instrucțiunilor unui limbaj de programare folosind obiecte matematice, numite denotații , care descriu semnificația lor și deci execuția lor. În general, această semantică trebuie să fie compozițională : denotarea unei părți a programului trebuie să fie construită pornind de la subinstrucțiunile sale.
Semantica operațională ; care descrie executarea unui program prin tranziții definite direct pe limbajul programului. Acest tip de formalism este similar din punct de vedere conceptual cu interpretarea efectivă în care avem o mașină abstractă și instrucțiunile aplică tranziții de stare în această mașină. Prin urmare, avem o secvență de pași de calcul definiți pentru fiecare program (care poate fi nedeterminist) și care este de obicei generată cu aplicarea unui set de reguli de inferență asupra setului de instrucțiuni.
Semantica axiomatică ; care, ca și precedentul, se bazează pe identificarea stării de calcul, dar folosește predicate logice pentru a defini starea curentă. Acest tip de semantică nu distinge adevărul implicat de o bucată de cod și semnificația acestuia: sunt exact același lucru. Este folosit în general pentru a încerca să verifice corectitudinea programelor, iar exemplul său cel mai izbitor și clasic este logica lui Hoare ^[1]

Notă