Abstract FR:

Java est un langage à objets concurrent. Ces deux facettes, déjà complexes prises isolément, deviennent très difficiles à appréhender quand elles sont réunies. Une sémantique formelle de Java est alors quasiment indispensable afin de pouvoir définir de façon formelle chaque caractéristique du langage étudié. Cette spécification devient alors une référence à laquelle le programmeur peut se reporter en cas de problème lors de la mise au point de programmes. Elle constitue aussi une base formelle au développement de preuves de propriétés. Nous avons fait le choix de définir une sémantique dynamique qui spécifie l’exécution de programme Java (par opposition à une sémantique dynamique qui spécifie l’exécution de programme Java (par opposition à une sémantique statique qui spécifierait les aspects typage du langage). L’utilisation du formalisme Typol disponible au sein du système Centaur pour exprimer cette sémantique nous a permis de la rendre directement exécutable, ce qui nous a amené à développer un environnement de visualisation de l’exécution de programmes Java mettant graphiquement en évidence les mécanismes liés à l’orientation objet, à la concurrence et à la synchronisation. Dans un dernier temps, nous avons examiné des propriétés du langage Java portant sur la concurrence et la synchronisation et nous avons étudié leur expression et leur vérification u sein de notre sémantique.