Hardened Golo : Donnez de la confiance en votre code Golo

Raphael Laurent (1)

1 CITI - CITI Centre of Innovation in Telecommunications and Integration of services

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.

Mots clés: Golo; analyse statique; preuve de programme; Why3

Domaines: Génie logiciel [cs.SE]

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