Semantica în programare este o disciplină care studiază formalizarea semnificațiilor constructelor limbajului de programare prin construirea modelelor lor matematice formale . Diverse instrumente pot fi folosite ca instrumente pentru construirea unor astfel de modele, de exemplu, logica matematică , calculul λ , teoria mulțimilor , teoria categoriilor , teoria modelelor , algebra universală . Formalizarea semanticii unui limbaj de programare poate fi folosită atât pentru a descrie limbajul, pentru a determina proprietățile limbajului, cât și în scopul verificării formale .programe în acest limbaj de programare.
Semantica unei limbi este sensul semantic al cuvintelor. În programare, semnificația semantică inițială a operatorilor , constructele de bază ale limbajului etc.
Exemplu:
Primul cod: i=0; în timp ce(i<5){i++;} Al doilea cod: i=0; do{i++;} while(i<=4);În mod logic, aceste două fragmente de cod fac același lucru, rezultatele muncii lor sunt identice. În același timp, din punct de vedere semantic, acestea sunt două cicluri diferite . De asemenea, etichetă:
<i></i> <em></em>vor arăta exact la fel pe pagină, adică vor reprezenta de fapt același lucru, iar din punct de vedere semantic, prima etichetă este italic, iar a doua este selecția logică (browserele afișează în italic).
Semantica operațională este folosită pentru conceptele sintactice ale limbajului . Tratează funcțiile ca definiții textuale bine formate care oferă aplicare unui argument și nu ca funcții în sensul matematic al termenului.
Există o clasificare a diferitelor tipuri de semantică operațională:
Semantica axiomatică - Semantica fiecărui construct sintactic dintr-o limbă poate fi definită ca un set de axiome sau reguli de inferență care pot fi folosite pentru a deduce rezultatele acelui construct. Pentru a înțelege semnificația întregului program, aceste axiome și reguli de inferență ar trebui utilizate în același mod ca și în demonstrarea teoremelor matematice obișnuite. Presupunând că valorile variabilelor de intrare satisfac unele constrângeri, axiomele și regulile de inferență pot fi folosite pentru a obține constrângeri asupra valorilor altor variabile după execuția fiecărei instrucțiuni de program. Când programul este executat, obținem o dovadă că rezultatele calculate îndeplinesc restricțiile necesare asupra valorilor lor în raport cu valorile de intrare. Adică, se dovedește că ieșirea reprezintă valorile funcției corespunzătoare calculate din valorile intrării.
Semantica denotațională pune obiectele matematice reale în corespondență cu expresiile din program , adică expresiile denotă ( ing . a denota — de unde „denotațional”) valorile lor [1] . Cele mai importante rezultate, inclusiv de pionierat, în construcția semanticii denotaționale au fost obținute în lucrările lui D. Scott (Dana Scott) și K. Strachey (Christopher Strachey) la sfârșitul anilor 1960 și începutul anilor 1970 la Universitatea Oxford [2] . Scott a fost primul care a construit un model al calculului λ bazat pe conceptul de mulțime completă parțial ordonată. Pentru a face acest lucru, a folosit funcții care sunt continue pe un astfel de set.
Semantica interpretativă este o descriere a semanticii operaționale a constructelor în termeni de limbaje de programare de nivel scăzut ( limbaj de asamblare , cod de mașină ). Această metodă vă permite să identificați secțiunile programului cu executare lentă și este adesea folosită în fragmentele corespunzătoare ale sistemelor de programare pentru a optimiza codul programului .
Semantica translațională este o descriere a semanticii operaționale a constructelor în termeni de limbaje de programare de nivel înalt . Folosind această metodă, puteți învăța un limbaj similar cu cel deja cunoscut programatorului.
Semantica transformațională este o descriere a semanticii operaționale a constructelor de limbaj în termenii aceluiași limbaj. Semantica transformațională este baza metaprogramării .
Subiectul de interes și cercetare constantă este construcția de sisteme de demonstrare a corectitudinii, sau a corectitudinii programelor. Sistemele de probă pentru cazul corectitudinii programelor funcționale s-au dovedit a fi cele mai dezvoltate, care se întorc la sistemul LCF al lui Robin Milner și sistemul lui R. Boyer (R. Boyer) și J. Moore (J. Moore) .
Cercetările actuale se concentrează pe construirea de sisteme bazate pe logica constructivă și stabilirea unei analogii între programe și dovezi. Este semnificativ faptul că atât programele, cât și dovezile sunt considerate a fi scufundate într-un calcul λ cu tipuri, care este un sistem formal de ordine superioară. Acest lucru asigură că numai programele care se încheie pot fi construite. Un astfel de sistem este sistemul Coq .