La semantica formale dei linguaggi di programmazione è di solito omessa nei manuali di riferimento per privilegiare le più semplici spiegazioni intuitive, sebbene sia indispensabile per chiunque voglia verificare proprietà di programmi o comprenderne il significato in modo rigoroso.

Questo libro offre un'introduzione completa alla descrizione della semantica operazionale dei linguaggi di programmazione secondo la quale un programma è inteso come la modifica che la sua esecuzione apporta ai dati da esso utilizzati.

Il testo copre gli aspetti principali di un linguaggio di programmazione ad alto livello come Pascal oppure C, spiegando chiaramente concetti quali variabile, dichiarazione, comando, procedura e ricorsione.

Oggetto di particolare enfasi è la verifica di proprietà dei programmi. Attraverso una serie di dimostrazioni il lettore è progressivamente introdotto ad ogni tecnica di prova di una teoria matematicamente rigorosa.

Pensato per un corso universitario, questo volume può sicuramente interessare tutti coloro che intendono addentrarsi per la prima volta nel campo dell'analisi e della verifica di programmi.

La presenza di esercizi alla fine di ogni capitolo, ordinati secondo una difficoltà crescente, consente di focalizzare gli aspetti più importanti ivi descritti e di apprendere le tecniche quotidianamente usate con successo degli esperti.

La prefazione è curata da Ugo Montanari, docente di Informatica Teorica dell'Università di Pisa.

Cosimo Laneve è ricercatore presso il Dipartimento di Scienze dell'Informazione dell'Università di Bologna, dove tiene i corsi di Programmazione e Laboratorio di Informatica 1.