Ce manuel vise à initier le lecteur aux méthodes formelles de modélisation et de spécification et à leur rôle dans le développement de logiciels. Entre autres, il vise à familiariser le lecteur avec le mode descriptif de spécification (quoi ?) plutôt qu'avec le mode algorithmique traditionnel (comment ?).La principale notation utilisée dans ce manuel est la notation Spec. Ce langage de spécification formelle, tout commeVDMou Z, est basé sur la technique de modélisation abstraite. Toutefois, contrairement à ces langages, Spec s'inspire fortement des langages de programmation modernes : syntaxe textuelle plutôt que symboles mathématiques, langage fortement typé, mécanismes de modularisation et d'encapsulation, généricité et héritage, traitements d'exceptions, etc. En plus de la notation Spec, d'autres méthodes de spécifications sont aussi introduites - VDM, Z, Larch, sans oublier la notation OCL d'UML, ce qui permet de bien comparer ces diverses approches.Bien qu'une partie de ce manuel porte sur l'utilisation d'une méthode rigou reuse de développement (à la VDM), sa principale caractéristique est l'accent mis sur les techniques de description et de spécification de composants et de systèmes logiciels : fonctions, machines, types abstraits ou classes d'objets. De simples connaissances de base en mathématiques discrètes (théorie des ensembles et logique) et la connaissance d'un langage de programmation sont donc les seuls prérequis suggérés.Cette édition a été mise à jour et augmentée du chapitre 15 sur la conception et la programmation par contrats et l'utilisation d'assertions.