Les annotations, dans le langage de programmation Java, sont un moyen d'embarquer des méta-données dans le code source d'un programme. Elles peuvent être utilisées pour étendre le langage Java avec des concepts spécifiques à un domaine. Utilisées de cette manière, les annotations offrent un moyen de réduire le fossé sémantique entre les concepts du domaine et les concepts fournis par le langage de programmation. Pour l'utilisateur de ce cadre d'annotations (c.-à-d., le développeur d'applications), il est important de comprendre comment les différentes annotations se relient entre elles afin de les utiliser correctement et de détecter des erreurs d'utilisation au plus tôt. Des cadres d'annotation ont déjà été adoptés par l'industrie. Cependant, leur développe- ment demeure complexe et est fait, en grande partie, de façon ad-hoc. En développant un cadre d'annotations, le développeur doit s'assurer que le programme qui emploie les annotations est conforme aux contraintes définies pour elles. Telles contraintes sont souvent reléguées à la documentation du cadre logiciel, puisque les processeurs d'annotation existants ne fournissent pas une façon de les spécifier et vérifier. En plus de ceci, les processeurs d'annotations existants offrent comme entité de manipulation juste l'arbre de syntaxe abstraite (AST) du programme. Ceci force le développeur à réifier les annotations elles-mêmes s'il veut des éléments d'abstraction d'un plus haut niveau. Pour aider le réalisateur de cadre d'annotations, nous proposons deux cadres d'annotations. Le premier, appelé AVal, fournit un nombre de contraintes réutilisables, déclaratives et extensibles pour spécifier un cadre d'annotation. Les applications annotées peuvent ainsi être interprétées afin de les valider. Le deuxième cadre, appelé ModelAn, permet au réalisateur de cadre d'annotations de décrire un modèle qui correspond aux annotations définies dans cadre d'annotations. Par ce moyen, le réalisateur peut exprimer les contraintes en termes du modèle. Des programmes annotés sont alors représentés comme instances du modèle (d'annotation), et les contraintes sont vérifiées sur cette même instance. A partir de ce modèle d'annotations, les classes Java qui réifient les annotations sont pro duites. Les annotations réifiéess peuvent alors servir de point de départ à l'interprétation du programme annoté. Pour valider notre approche, nous avons construit le modèle d'annotation et décrit leurs contraintes à l'aide d'AVal et d'expressions OCL pour trois cadres d'annotation industriels: Fraclet, un cadre d'annotation pour le modèle composant de Fractal, JWS pour le développement de services Web dans Java, et l'API de persistance Java, une partie de la spécification Java de EJB3.

Le calcul massivement parallèle a connu durant ces deux dernières décennies un fort développement. Les efforts dans ce domaine ont d'abord surtout été orientés vers les machines, plutôt qu'à la définition de langages adaptés au parallélisme massif. Par la suite, deux principaux modèles de programmation ont émergé : le parallélisme de contrôle et le parallélisme de données. Le premier a connu un vif succès. Dans ce modèle cependant, les applications massivement parallèles s'avèrent difficiles à concevoir et peu fiables, compte tenu du grand nombre de processus envisagés. En revanche, le parallélisme de données paraît aujourd'hui être un bon compromis entre les besoins des utilisateurs et les contraintes imposées par les architectures parallèles. Dans cette thèse, nous nous sommes intéressé à la validation formelle des langages à parallélisme de données. L'idée est de tirer parti de la relative simplicité de ce modèle de programmation pour développer des méthodes semblables à celles déjà éprouvées dans le cadre des langages scalaires classiques. La première partie du travail effectué concerne un langage data-parallèle simple, de type impératif. Nous avons montré qu'il était possible de définir un système de preuve complet pour ce langage, inpiré de la logique de Hoare. L'étude théorique nous a permis en outre de définir une méthodologie pratique de preuve par annotations, semblable à celle utilisée pour les langages scalaires. Nous nous sommes ensuite tourné vers le langage d'équations récurrentes Alpha. Il s'avérait nécessaire de définir pour ce langage un cadre formel de validation, plus riche que le système de transformations existant ne permettant que des preuves par équivalence. Nous avons défini un modèle d'exécution par l'intermédiaire d'une sémantique opérationnelle, et une méthodologie de preuve. Celle-ci utilise des invariants qui sont raffinés à partir d'une traduction du programme dans un langage logique jusqu'à l'obtention de la propriété voulue.