Logique, volume 2 : méthodes formelles pour l'étude des programmes

La première partie est consacrée à la théorie des
ensembles. Le chapitre 1 donne une introduction
philosophique et historique, les aspects techniques
étant exposés au chapitre 2. La théorie des ensembles
constitue à la fois une application essentielle de la
logique du premier ordre, étudiée dans le premier
volume, et la base théorique des méthodes formelles
en programmation. La seconde partie est consacrée
à ces méthodes et à leur illustration. Le chapitre 3
présente la logique de Hoare classique, permettant
l'étude formelle des programmes séquentiels ; cette
logique est adaptée à la programmation parallèle au
chapitre 4. Le chapitre 5 examine la théorie du point
fixe, qui permet l'étude systématique des programmes
et langages de programmation de tous types,
y compris des langages fonctionnels et logiques.
Cet ouvrage constitue donc une présentation claire
et raisonnée des liens qui associent en profondeur
logique et étude des propriétés des programmes.