Semantica formale

Nel campo dell'informatica teorica, il termine semantica formale riguarda i modelli matematici che definiscono formalmente i linguaggi di programmazione o, più generalmente, la computazione stessa.

Esistono molteplici approcci allo studio di queste semantiche; i quali ricadono in 3 categorie principali:

La semantica denotazionale; che si preoccupa di formalizzare l'esecuzione delle istruzioni di un linguaggio di programmazione utilizzando degli oggetti matematici, chiamati denotazioni, che ne descrivono il significato e quindi l'esecuzione. In genere questa semantica dev'essere composizionale: la denotazione di una parte del programma dev'essere costruita partendo da sue sotto istruzioni.
La semantica operazionale; che descrive l'esecuzione di un programma attraverso transizioni definite direttamente sul linguaggio del programma. Questo tipo di formalismo è concettualmente simile all'interpretazione vera e propria in cui abbiamo una macchina astratta e le istruzioni applicano transizioni di stato in questa macchina. Abbiamo dunque una sequenza di passi computazionali definita per ogni programma (che può essere non deterministica) e che viene generata solitamente con l'applicazione di un insieme di regole di inferenza sull'insieme delle istruzioni stesso.
La semantica assiomatica; che come la precedente si basa sul contraddistinguere lo stato della computazione ma utilizza dei predicati logici per definire lo stato attuale. Questo tipo di semantica non distingue la verità implicata da una parte di codice ed il significato dello stesso: sono esattamente la stessa cosa. In genere si utilizza per cercare di verificare la correttezza dei programmi ed il suo esempio più lampante e classico è la logica di Hoare^[1]