Hardened Golo : Donnez de la confiance en votre code Golo

Résumé : Golo est un langage dynamique construit autour de l’instruction "invokedynamic" de la machine virtuelle Java. Originellement développé au laboratoire CITI de l’INSA de Lyon par le groupe Dynamid, Golo est open-source et dédié à la réalisation d’applications dynamiques. L’objectif de ce stage est de pouvoir augmenter la confiance que l’on peut avoir en un programme Golo. L’approche retenue est d’utiliser l’outil Why3 développé par l’équipe Toccata de l’INRIA/LRI/CNRS, originellement conçu pour la vérification de programmes en C, Java et Ada. En s’appuyant sur le travail fait par le plugin Krakatoa pour analyser du code Java avec cet outil, une traduction du code Golo vers du code WhyML exécutable a été implémentée dans le compilateur Golo. Cette implémentation vise à poser une base pour pouvoir analyser statiquement du code Golo avec Why3, ainsi que pour faire des vérifications statiques lors de la traduction. La spécification dans le code Golo devait originellement se faire dans un langage inspiré de JML, cependant l’approche implémentée permet au programmeur de spécifier le code Golo dans le langage de spécification de Why3 directement. Le détail de la mé- thode d’implémentation, des fonctionnalités supportées ainsi que des limitations sera abordé dans une partie ultérieure.
Type de document :
Mémoires d'étudiants -- Hal-inria+
Génie logiciel [cs.SE]. 2016
Liste complète des métadonnées

Littérature citée [10 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01354836
Contributeur : <>
Soumis le : vendredi 19 août 2016 - 16:11:35
Dernière modification le : mardi 23 août 2016 - 01:02:51

Identifiants

  • HAL Id : hal-01354836, version 1
  • Mot de passe : y&nanfh

Collections

Citation

Raphael Laurent. Hardened Golo : Donnez de la confiance en votre code Golo. Génie logiciel [cs.SE]. 2016. 〈hal-01354836〉

Partager

Métriques

Consultations de la notice

272

Téléchargements de fichiers

50