4 La semantica dei linguaggi di programmazione

Dopo aver esaminato la sintassi dei linguaggi di programmazione, ci concentriamo ora sulla semantica, l’altra componente fondamentale di un linguaggio di programmazione. Mentre la sintassi si occupa della forma e della struttura del codice, la semantica riguarda il significato delle istruzioni e come queste vengono interpretate ed eseguite dal computer.

La semantica di un linguaggio di programmazione definisce come le istruzioni sintatticamente corrette devono essere interpretate e quale effetto producono quando vengono eseguite. È il ponte tra la struttura formale del codice e il suo comportamento effettivo durante l’esecuzione.

L’importanza della comprensione della semantica è simile alla comprensione del significato delle parole e delle frasi in un linguaggio naturale:

Correttezza del programma: Una buona comprensione della semantica permette di scrivere programmi che non solo sono sintatticamente corretti, ma che producono anche i risultati desiderati.
Debugging efficace: Conoscere la semantica aiuta a identificare e correggere errori logici nel codice, che possono essere più sottili e difficili da individuare rispetto agli errori sintattici.
Ottimizzazione del codice: Una comprensione approfondita della semantica consente di scrivere codice più efficiente, sfruttando al meglio le caratteristiche del linguaggio.
Portabilità del codice: Conoscere le sfumature semantiche di diversi linguaggi aiuta a scrivere codice che si comporta in modo coerente su piattaforme diverse.
Comunicazione tra programmatori: Una chiara comprensione della semantica facilita la collaborazione tra sviluppatori, permettendo di discutere e ragionare sul comportamento del codice in modo preciso.

4.1 Tipi di semantica

Esistono diversi tipi di semantica nel contesto dei linguaggi di programmazione. Ciascun tipo di semantica ha un ruolo specifico e può essere particolarmente rilevante a seconda del linguaggio di programmazione o del paradigma di programmazione adottato.

4.1.1 Semantica statica

La semantica statica riguarda le regole che possono essere verificate durante la compilazione, senza eseguire il programma. Include il controllo dei tipi, la verifica della dichiarazione delle variabili prima del loro uso e altre regole che non dipendono dall’esecuzione del programma.

Esempio in Java:

int x = 10;
String y = "Hello";

1y = x;

1: Il compilatore segnala un errore su questa riga perché non è possibile assegnare un valore intero a una variabile di tipo stringa.

4.1.2 Semantica dinamica

La semantica dinamica si riferisce al comportamento del programma durante l’esecuzione. Descrive come le istruzioni vengono eseguite e come il programma si evolve nel tempo.

Esempio in Python:

1def divide(a, b):
2  return a / b

3print(divide(10, 2))
4print(divide(10, 0))

1: Definizione della funzione divide che accetta due parametri a e b.
2: La funzione divide ritorna il risultato della divisione di a per b.
3: print(divide(10, 2)) stampa 5.0.
4: print(divide(10, 0)) causa un errore a runtime per la divisione per zero.

4.1.3 Semantica operazionale

La semantica operazionale spiega come un programma esegue le sue istruzioni passo dopo passo. Immaginiamo di seguire una ricetta di cucina: la semantica operazionale ci direbbe esattamente cosa fare in ogni passo, come prendere un ingrediente, mescolarlo, cuocerlo, ecc.

In termini di programmazione, la semantica operazionale descrive come ogni istruzione del programma modifica lo stato del computer, come i valori delle variabili o il flusso di esecuzione. Questo tipo di semantica è spesso utilizzato per definire formalmente come dovrebbe comportarsi un linguaggio di programmazione, fornendo una guida precisa su come il codice dovrebbe essere eseguito dal computer.

Esempio in C++:

for (int i = 0; i < 5; i++) {  /* <1> */
  if (i % 2 == 0) {  /* <2> */
    continue;  /* <3> */
  }

  std::cout << i << std::endl;  /* <4> */
}

Ciclo for che itera da 0 a 4.
Controllo condizionale per verificare se i è pari.
continue salta le iterazioni pari.
Stampa solo i valori dispari di i.

4.1.4 Semantica denotazionale

La semantica denotazionale è un approccio formale per definire il significato di un programma associando ogni costrutto del linguaggio a una denotazione matematica, tipicamente una funzione. Questo metodo consente di ragionare in modo rigoroso e preciso sul comportamento dei programmi.

In altre parole, ogni parte di un programma è mappata a un valore o a una funzione matematica. Questa mappatura permette di comprendere e prevedere il comportamento del programma in termini matematici, indipendentemente dall’implementazione concreta.

Consideriamo un esempio di codice in Python che filtra, ordina e somma elementi di una lista:

1def filtra_pari(lista):
2  return [x for x in lista if x % 2 == 0]

3def ordina(lista):
4  return sorted(lista)

5def somma_primi_tre(lista):
6  return sum(lista[:3])

7lista = [5, 3, 8, 6, 2, 9, 1, 4, 7]

8lista_pari = filtra_pari(lista)

9lista_ordinata = ordina(lista_pari)

10risultato = somma_primi_tre(lista_ordinata)

11print(risultato)

1: Definizione della funzione filtra_pari che accetta una lista.
2: La funzione filtra_pari restituisce una nuova lista contenente solo i numeri pari.
3: Definizione della funzione ordina che accetta una lista.
4: La funzione ordina restituisce la lista ordinata.
5: Definizione della funzione somma_primi_tre che accetta una lista.
6: La funzione somma_primi_tre restituisce la somma dei primi tre elementi della lista.
7: Definizione della lista lista contenente numeri interi.
8: Applicazione della funzione filtra_pari alla lista lista, memorizzando il risultato in lista_pari.
9: Applicazione della funzione ordina alla lista lista_pari, memorizzando il risultato in lista_ordinata.
10: Applicazione della funzione somma_primi_tre alla lista lista_ordinata, memorizzando il risultato in risultato.
11: Stampa del valore di risultato.

La relativa mappatura denotazionale diviene:

filtra_pari(lista) corrisponde a una funzione \(F\) che mappa una lista \(L\) a una lista contenente solo gli elementi pari di \(L\).
ordina(lista) corrisponde a una funzione \(S\) che mappa una lista \(L\) alla lista ordinata.
somma_primi_tre(lista) corrisponde a una funzione \(T\) che mappa una lista \(L\) alla somma dei suoi primi tre elementi.

Quindi, il programma può essere rappresentato come la composizione delle funzioni matematiche:

\[ T(S(F(L))) \]

dove \(L\) è la lista iniziale, \(F\) è filtra_pari, \(S\) è ordina, e \(T\) è somma_primi_tre.

La semantica denotazionale è utilizzata per garantire la correttezza dei programmi e per la verifica formale del loro comportamento. È un approccio potente per verificare che un programma rispetti specifiche formali e per dimostrare proprietà dei programmi in modo matematico. Operativamente, lo sviluppatore definisce le mappature denotazionali per i costrutti del programma, esprimendoli come funzioni matematiche. Strumenti come Coq e Isabelle/HOL aiutano a verificare formalmente queste mappature, dimostrando che il programma soddisfa specifiche precise e comportandosi come atteso in ogni possibile scenario.

4.1.5 Semantica assiomatica

La semantica assiomatica è un approccio formale per definire il significato dei programmi basato su precondizioni e postcondizioni logiche. Questo metodo, sviluppato da Tony Hoare (Hoare 1969), utilizza asserzioni logiche per descrivere lo stato del programma prima e dopo l’esecuzione delle istruzioni, permettendo di dimostrare formalmente la correttezza dei programmi.

HOARE, Charles A. R., 1969. An Axiomatic Basis for Computer Programming. Communications of the ACM. 1969. Vol. 12, n° 10, pp. 576–580. DOI 10.1145/363235.363259.

In altre parole, la semantica assiomatica stabilisce regole per verificare che un programma rispetti determinate specifiche formali. Questo è particolarmente utile per garantire che il programma funzioni correttamente in tutte le condizioni previste.

Consideriamo un semplice esempio in Python che calcola la somma di due numeri:

1def somma(a, b):
2  return a + b

3print(somma(3, 4))

1: Definizione della funzione somma che accetta due parametri a e b.
2: La funzione somma restituisce la somma di a e b.
3: Chiamata della funzione somma con argomenti 3 e 4, stampa 7.

Per verificare formalmente questo codice in Coq¹:

¹ Coq è scaricabile da Coq Official Website.

(* Importazione della libreria standard di Coq *)
Require Import Coq.Arith.Arith.
Require Import Coq.Init.Nat.

(* Definizione della funzione somma in Coq *)
Definition somma (a b : nat) : nat := a + b.

(* Affermazione del teorema che verifica la correttezza della funzione somma *)
Theorem somma_corretto : forall a b : nat,
    somma a b = a + b.
Proof.
  intros a b.
  unfold somma.
  reflexivity.
Qed.

(* Verifica di un caso specifico: somma 3 4 = 7 *)
Example test_somma : somma 3 4 = 7.
Proof.
  simpl.
  reflexivity.
Qed.

In questo codice:

Abbiamo definito la funzione somma in Coq per replicare il comportamento della funzione Python.
Abbiamo affermato e dimostrato formalmente che somma a b è uguale a a + b per tutti i numeri naturali a e b.
Abbiamo verificato un caso specifico (somma 3 4 = 7) per dimostrare che il nostro teorema e la nostra funzione sono corretti.

Salviamo il codice in un file somma.v e, in un terminale, navighiamo nella sua directory contenente. Quindi, eseguiamo il comando:

coqc somma.v

Questo comando compila il file somma.v e verifica i teoremi e gli esempi al suo interno. Se tutto è corretto, non verrà restituito alcun errore.

In contesti dove la correttezza del software è critica, come nei sistemi avionici, nei dispositivi medici e nei sistemi finanziari, la verifica formale basata sulla semantica assiomatica è fondamentale. Utilizzando strumenti come Coq, Isabelle/HOL, SPARK e altri prover interattivi, gli ingegneri del software possono formalizzare le specifiche del sistema e dimostrare che il codice implementato le soddisfa.²

² Per approfondire: (Chlipala 2022).

CHLIPALA, Adam, 2022. Certified Programming with Dependent Types [online]. MIT Press. ISBN 9780262545747. Disponibile all'indirizzo : http://adam.chlipala.net/cpdt/html/

Il libro "Certified Programming with Dependent Types" di Adam Chlipala offre un’introduzione dettagliata al software Coq per la scrittura e la verifica di dimostrazioni matematiche, con un forte focus pratico sull’ingegneria del software. La verifica formale dei programmi è un campo in crescita che trova applicazione sia nella matematica che nell’ingegneria, e questo libro si propone di rendere accessibili le tecniche per costruire, comprendere e mantenere sviluppi in Coq di grandi dimensioni. Una delle caratteristiche distintive del libro è la trattazione approfondita della programmazione con tipi dipendenti, un aspetto centrale del sistema Coq, e la costruzione di tattiche di prova specifiche per il dominio. Questi argomenti, raramente trattati altrove, sono essenziali per la verifica interattiva dei teoremi. Il libro utilizza uno stile unico di prova automatizzata e offre una libreria di tattiche progettate per essere utilizzate con gli esempi del testo, fornendo ai lettori le competenze necessarie per reimplementare queste tattiche in altri contesti.

4.2 Elementi semantici fondamentali

Dopo aver esplorato i vari tipi di semantica nei linguaggi di programmazione, è importante comprendere i componenti fondamentali che questi tipi di semantica descrivono e regolano. Gli elementi semantici fondamentali sono i mattoni con cui costruiamo e comprendiamo il comportamento dei programmi. Tra questi, alcuni concetti come variabili, tipi di dati, espressioni, controllo del flusso, gestione della memoria, funzioni e sistemi di tipi sono cruciali per ogni linguaggio di programmazione moderno, altri sono particolari di linguaggi specifici come la concorrenza e il supporto alla programmazione ad aspetti.

Di seguito, vediamo sinteticamente ciascuno degli elementi principali, per poi approfondire nei successivi capitoli.

4.2.1 La variabile e il tipo di dato

Una variabile in un linguaggio di programmazione è un nome simbolico associato a una locazione di memoria in cui è memorizzato un dato. Le variabili sono utilizzate all’interno di espressioni e istruzioni, per referenziare e manipolare dati durante l’esecuzione di un programma. Il valore associato alla variabile è memorizzato nella locazione di memoria a cui la variabile fa riferimento e il tipo di dato della variabile determina come quel valore viene interpretato e quali operazioni possono essere eseguite su di esso.

Dichiarazione: Introduce una variabile nel programma, specificando il suo nome e, in molti linguaggi, il suo tipo di dato.
Definizione: Oltre a dichiarare la variabile, le assegna anche uno spazio di memoria.
Inizializzazione: L’assegnazione del primo valore a una variabile.
Ambito (inglese: scope): Definisce la visibilità e l’accessibilità di una variabile all’interno del codice.
Durata: Il periodo durante il quale una variabile mantiene valido il legame con un dato presente in memoria.

Un tipo di dato definisce un dominio di valori e un insieme di operazioni ammissibili su tali valori. I tipi di dato sono fondamentali per la semantica dei linguaggi di programmazione, influenzando l’analisi statica, la gestione della memoria e l’esecuzione del programma. Si classificano in:

Tipi primitivi: Rappresentano valori atomici direttamente supportati dal linguaggio, come numeri interi, numeri in virgola mobile, caratteri e booleani.
Tipi composti: Costruiti a partire da altri tipi, permettono di rappresentare dati strutturati. Includono:
- Array: Collezioni indicizzate di elementi dello stesso tipo.
- Strutture (o record): Aggregati di campi eterogenei.
- Classi: In linguaggi orientati agli oggetti, definiscono sia dati che comportamenti.
- Tuple: Sequenze ordinate e immutabili di elementi potenzialmente di tipi diversi.
Tipi di riferimento: Permettono l’accesso indiretto ai dati:
- Puntatori: Contengono indirizzi di memoria.
- Riferimenti: Alias per altre variabili o oggetti.
Tipi astratti di dato (inglese: abstract data type, ADT): Definiti dall’utente, incapsulano una rappresentazione interna e forniscono un’interfaccia di operazioni.
Tipi generici (o parametrici): Consentono la definizione di strutture o algoritmi che operano su tipi non specificati, promuovendo il riuso del codice.
Tipi unione: Rappresentano valori che possono essere di uno tra diversi tipi specificati.
Tipi funzione: Descrivono le firme delle funzioni, includendo tipi dei parametri e del valore di ritorno.

4.2.2 Il controllo di flusso

La semantica del controllo di flusso definisce come l’esecuzione del programma procede attraverso le istruzioni, determinando l’ordine in cui le operazioni vengono eseguite. Questo aspetto fondamentale della semantica dei linguaggi di programmazione include vari costrutti che permettono di dirigere e modificare il flusso di esecuzione in modo deterministico o in risposta a condizioni specifiche. I principali meccanismi di controllo del flusso includono:

Strutture condizionali:
- if-else: Permette l’esecuzione selettiva di blocchi di codice basata su condizioni booleane.
- switch-case: Fornisce un meccanismo per la selezione multipla basata sul valore di un’espressione.
- Operatore ternario: Offre una forma compatta di decisione condizionale, spesso usata per assegnazioni.
Strutture iterative (cicli):
- for: Esegue un blocco di codice per un numero predefinito di iterazioni, spesso utilizzando un contatore.
- while: Ripete un blocco di codice fintanto che una condizione specificata rimane vera.
- do-while: Simile al while, ma garantisce almeno una esecuzione del blocco di codice.
- foreach (o for-in): Itera su elementi di collezioni o strutture dati enumerabili.
Istruzioni di salto:
- Break: Esce immediatamente da un ciclo o da uno switch.
- Continue: Salta il resto dell’iterazione corrente e procede con la successiva.
- Return: Termina l’esecuzione di una funzione, opzionalmente restituendo un valore.
- Goto: Trasferisce direttamente il controllo a un’etichetta specificata (sconsigliato in programmazione strutturata).
Gestione delle eccezioni:
- Try: Definisce un blocco di codice in cui potrebbero verificarsi eccezioni.
- Catch: Specifica come gestire specifici tipi di eccezioni.
- Finally: Definisce un blocco di codice che viene eseguito indipendentemente dal verificarsi di eccezioni.
- Throw: Solleva manualmente un’eccezione.
Chiamate di funzione e ricorsione:
- Le chiamate di funzione alterano il flusso trasferendo il controllo alla funzione chiamata.
- La ricorsione permette a una funzione di chiamare se stessa, creando un flusso di controllo potenzialmente complesso.
Coroutine e generatori:
- Permettono l’esecuzione cooperativa, consentendo la sospensione e la ripresa dell’esecuzione in punti specifici.
Parallelismo e concorrenza:
- Costrutti come fork-join, async-await, e primitive di sincronizzazione influenzano il flusso di esecuzione in contesti multi-thread o distribuiti.
Pattern matching (in linguaggi funzionali e alcuni moderni linguaggi OO):
- Permette il controllo del flusso basato sulla struttura e il contenuto dei dati.

La semantica del controllo di flusso definisce precisamente come questi costrutti influenzano l’ordine di esecuzione delle istruzioni, come vengono valutate le condizioni, come viene gestito il passaggio dei parametri nelle chiamate di funzione, e come vengono propagate le eccezioni. Inoltre, specifica le regole per la visibilità e la durata delle variabili (scope) in relazione a questi costrutti di controllo.

La comprensione e l’uso appropriato di questi meccanismi sono cruciali per la progettazione di algoritmi efficienti e per la gestione della complessità nei programmi. Inoltre, la scelta e l’implementazione di questi costrutti in un linguaggio di programmazione hanno un impatto significativo sulla sua espressività, leggibilità e manutenibilità.

4.2.3 5. Funzioni e procedure

Le funzioni sono blocchi di codice riutilizzabili che eseguono specifiche operazioni. Le procedure sono simili alle funzioni ma non restituiscono un valore.

Definizione e dichiarazione: Sintassi per creare funzioni
Parametri: Formali vs. attuali, passaggio per valore vs. riferimento
Valori di ritorno: Tipi di ritorno, multiple return values
Ricorsione: Funzioni che chiamano se stesse
Overloading: Definizione di più funzioni con lo stesso nome ma parametri diversi
Lambda e funzioni anonime: Funzioni senza nome, spesso usate come argomenti
Funzioni in prima classe: Le funzioni possono essere trattate come dati, passate come argomenti e restituite come valori.

4.2.4 6. Gestione della memoria

La gestione della memoria definisce come il programma alloca, utilizza e libera la memoria. Questo include il ciclo di vita delle variabili e la gestione della memoria dinamica.

Allocazione statica: Memoria allocata al momento della compilazione
Allocazione dinamica: Memoria allocata durante l’esecuzione
Garbage collection: Meccanismo automatico di liberazione della memoria
Gestione manuale della memoria: Allocazione e deallocazione esplicita (es. in C)
Memory leaks: Problemi dovuti a memoria non correttamente deallocata

4.2.5 7. Sistemi di tipi

Il sistema di tipi di un linguaggio definisce come i tipi vengono assegnati e controllati.

Tipizzazione statica vs dinamica: Quando avviene il controllo dei tipi
Tipizzazione forte vs debole: Rigidità nel controllo dei tipi
Inferenza di tipo: Il compilatore deduce automaticamente il tipo di una variabile (es. TypeScript, Haskell)
Polimorfismo: Capacità di un’entità di assumere più forme
Coercizione di tipo: Conversione automatica tra tipi diversi

4.2.6 8. Programmazione orientata agli oggetti

Paradigma di programmazione basato sul concetto di “oggetti” che contengono dati e codice.

Classi e oggetti: Modelli e istanze
Incapsulamento: Nascondere i dettagli implementativi
Ereditarietà: Meccanismo per creare nuove classi basate su classi esistenti
Polimorfismo: Capacità di oggetti di classi diverse di rispondere allo stesso messaggio
Interfacce e classi astratte: Definizione di contratti per le classi

4.2.7 9. Programmazione asincrona

Permette l’esecuzione di operazioni non bloccanti, migliorando l’efficienza e la reattività dei programmi.

Promise/Future: Rappresentano il risultato di un’operazione asincrona
async/await: Sintassi che semplifica la scrittura di codice asincrono
Callback: Funzioni chiamate al completamento di un’operazione asincrona
Event loop: Meccanismo per gestire operazioni asincrone

4.2.8 10. Modularità e organizzazione del codice

La suddivisione del codice in moduli migliora la manutenibilità, la riusabilità e l’incapsulamento.

Namespace: Meccanismo per evitare conflitti di nomi
Moduli e pacchetti: Organizzazione del codice in unità logiche
Import/Export: Meccanismi per condividere codice tra moduli
Visibilità e accesso: public, private, protected

4.2.9 11. Metaprogrammazione

Tecniche per scrivere programmi che manipolano o generano altri programmi.

Reflection: Capacità di un programma di esaminare, introspezione e modificare la propria struttura e comportamento
Generazione di codice: Creazione automatica di codice sorgente
Macro: Istruzioni che vengono espanse in tempo di compilazione

4.2.10 12. Concorrenza e parallelismo

Meccanismi per eseguire più task simultaneamente o apparentemente simultaneamente.

Thread e processi: Unità di esecuzione concorrente
Sincronizzazione: Meccanismi per coordinare l’esecuzione di thread (mutex, semafori)
Parallellismo: Esecuzione simultanea su hardware multi-core

4.2.11 13. Programmazione orientata agli aspetti

Un paradigma di programmazione che permette di separare le preoccupazioni trasversali dal codice principale.

Aspetti: Moduli che incapsulano comportamenti trasversali
Pointcut: Punti nel programma dove viene applicato un aspetto
Advice: Codice che viene eseguito quando viene raggiunto un pointcut
Weaving: Processo di applicazione degli aspetti al codice principale

Questa panoramica estesa fornisce una base solida per comprendere gli elementi semantici fondamentali dei linguaggi di programmazione moderni. Ogni concetto merita un approfondimento dettagliato, che verrà fornito nei capitoli successivi, offrendo una comprensione più approfondita e pratica di come questi elementi interagiscono per creare sistemi software complessi e potenti.