http://www.univ-tours.fr/discala/livres/basesinfo2.pdf1.5 Les langages de spécification
Les langages de spécification sont encore du domaine de la recherche. Leurs objectifs sont de
décrire le plus rigoureusement possible (les modèles principaux sont mathématiques) un
logiciel afin de pouvoir le valider et le vérifier.
Nous ne mentionnerons ici que le langage LPG de D.Bert(Grenoble) pour les spécifications
de types abstraits algébriques, Z de J.R. Abrial, le langage dont la notation est fondée sur la
théorie des ensembles (puis d’une amélioration de Z dénotée B par Abrial) et VDM langage
formel de spécification par pré-condition et post-condition. Ces langages ne peuvent être
utilisés d’une manière pratique que sous forme de notation, bien qu’ils soient implantés sur
des systèmes informatiques. Ils ne sont pas encore à la disposition du grand public comme les
langages des catégories précédentes, bien que certains soient utilisés dans des sites industriels.
Par la suite, nous utiliserons un langage de spécification pédagogique fondé sur les types
abstraits algébriques.