Modélisation et spécification formelles des logiciels

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, tour comme VDM ou Z, est basé sur la technique de modélisation abstraite. Toutefois, contraitement à 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 introduites – VDM, Z, Larch, sans oublier la notation OCL d’UML, ce qui permet de bien comparer ces diverses approches.