Introduction au langage de spécification formelle Z qui fait largement appel aux notations des mathématiques discrètes. Les mathématiques de Z sont expliquées et accompagnées d'un exemple de spécification. ©Electre 2025

Les problèmes qui surgissent dans les systèmes informatiques découlent souvent d'erreurs et d'insuffisances dans leurs spécifications de départ. Leurs effets s'insinuant dans chaque phase du processus de développement, de tels problèmes sont particulièrement difficiles et coûteux à rectifier. L'avènement, durant ces dernières années, de techniques de spécifications formelles qui rendent les spécifications plus claires, plus courtes et plus précises, contribue à l'amélioration des spécifications et devrait donc offrir de substantiels bénéfices aux développeurs de systèmes informatiques.

C'est en utilisant des notations s'appuyant sur des éléments aussi simples des mathématiques discrètes que la théorie des ensembles et la logique, que la spécification formelle évite les ambiguïtés et l'imprécision inhérente à la prose. Que cela soit pour spécifier de nouveaux systèmes que pour spécifier rétrospectivement des systèmes existants, son usage va croissant car elle permet une meilleure compréhension de leur comportement attendu et réel.

La notation pour la spécification formelle appelée Z a été développée au Groupe de Recherche de Programmation (PRG) de l'université d'Oxford, à la suite des travaux du français Jean-Raymond Abrial. Elle est devenue «leader» dans ce domaine.

Ce livre est tout d'abord destiné au non-mathématicien. Très didactique, il introduit les idées en construisant chaque nouveau concept sur ceux qui ont été précédemment présentés et chaque chapitre est suivi par un ensemble d'exercices, pour lesquels des exemples de solutions sont fournis en annexe. Chaque symbole Z est présenté lorsque le besoin s'en fait sentir. L'auteur illustre son propos de nombreux exemples tirés de l'expérience quotidienne et un exemple plus vaste est développé tout au long du livre.

Cette traduction française a corrigé un certain nombre d'erreurs de l'édition anglaise. De plus, elle comprend un lexique français/anglais et une bibliographie d'ouvrages en français.