Semantica programelor

Specificarea limbajelor de programare:

Sintaxa (structura (forma) programelor)

Specificare neformalizată (limbaj natural)

Specificare formalizată (gramatici generative Chomsky independente de context în notaţia Backus-Naur Form)

Semantica (semnificaţia programelor)

Specificare neformalizată (limbaj natural):

explicare intuitivă a semnificaţiei programelor

predispusă la ambiguitate, inconsistenţă şi incompletitudine

Nu oferă suport riguros pentru:

Implementarea limbajelor de programare (automatizarea procesului de scriere a compilatoarelor)

Raţionamente despre proprietăţile programelor şi ale limbajelor

Specificare formalizată (definiţii matematice): însoţeşte, dar nu inlocuieşte prezentarea neformalizată

Semantică operaţională

Semantică denotaţională

Semantică axiomatică (propoziţională)

etc.

Sintaxa (notaţie BNF) S ::== skip | V:= E | S;S| if B then S else S fi | while B do S od

Abreviere: if B then S fi ≡ if B then S else skip fi

Observaţie: Sintaxa nu este ambiguă (problema dangling else este eliminată prin prezenţa cuvântului cheie fi): if b1 then if b2 then S1 fi else S2 fi sau if b1 then if b2 then S1 else S2 fi fi

Hennessy şi Plotkin, 1979

Limbajul expresiilor şi al aserţiunilor

Tipuri

Tipuri de bază: integer, (nume de tip, nu mulţime concretă!) Boolean, mulţimea {true, false}; elementele mulţimii nu au (încă) o semnificaţie.

Tipuri de ordin superior: (T1 x...Tn → T), unde Ti ,T sunt tipuri de bază: Ti tipuri de argumente iar T tipul valorilor.

Alfabet

Var, mulţimea variabilelor Fiecare variabilă are asociat un tip (poate lua valori numai din tipul asociat)

Simple (tipul asociat este tip de bază)

Tablouri (tipul asociat este un tip de ordin superior): valoarea unui tablou este o funcţie.

Constante (un tip asociat şi o valoare fixată)

de tip de bază: constante întregi ( 0, -1,1,-2,2...) sau logice (true, false)

de tip superior (au ca valoare o funcţie fixată)

Simboluri relaţionale: codomeniul este Boolean =,<: W x W→ Boolean, unde W este tip de bază divide:integer x integer → Boolean ⋀,∨, →,↔:Boolean x Boolean → Boolean (conectori logici) ⌉ : Boolean → Boolean

Simboluri de funcţii (codomeniul integer) +,-,min,max,div,mod: integer x integer → integer

Parantezele (,),[,]

Semne de punctuaţie (punct, două puncte, virgula)