Abstract FR:

Nous developpons de facon uniforme un point de vue local et un point de vue global sur les proprietes des programmes. Notre domaine de reference est l'ensemble des comportements infinis sur un alphabet particulier. L'intuition sous-jacente a une classe de proprietes s'exprime par une organisation interne des proprietes correspondantes, qui apparait de facon specifique dans la topologie produit associee au domaine semantique. Les travaux existants font apparaitre deux aspects fondamentaux et orthogonaux de l'etude des proprietes des programmes, qui conduisent a les structurer comme une partition ou comme une hierarchie. Ces caracterisations etant incompletes, notre premiere contribution a consiste a identifier les qualites topologiques pertinentes en procedant a une analyse topologique systematique des classes de proprietes qui supportent la methodologie de preuve de p&r-cousot. Nous proposons une extension de ces classes qui trouve son application dans l'etude de la logique de unity ainsi que dans celle de l'equite generalisee. Finalement nous indiquons les conditions generales d'emergence des qualites topologiques qui ont retenu notre attention. Notre seconde contribution introduit une notion abstraite de specification qui subsument tous les types de proprietes rencontres precedemment. Une notion raisonnable de propriete determine comme structure la tribu de borel du domaine semantique. Il est cependant possible de fonder une approche structurale coherente en utilisant une notion de propriete adaptee a des besoins specifiques. Nous donnons un exemple de construction d'une telle algebre en utilisant l'insensibilite au begaiement comme principe de selection d'une propriete. L'algebre obtenue est complete et distincte dans la majorite des cas de la tribu des boreliens. Nous nous interessons finalement a la mesure des proprietes dans le cas ou elles sont boreliennes