IST Project -- Hardened Golo : Giving some confidence into your Golo code

Advisors

• Nicolas Stouls (nicolas.stouls@insa-lyon.fr)
• Oscar Carrillo (oscar.carrillo@insa-lyon.fr)

Number of students

Context

Golo is a simple, dynamic, weakly-typed language for the JVM created in 2012 as part of the research activities of the DynaMid group of the Centre of Innovation in Telecommunications and Integration of service aka CITI Laboratory.

This language adds the dynamicity into the objects. It means that objects themselves can evolve during time, by adding new methods, new attributs, ... It's also possible to dynamically modify classes provided by the standard API. By instance by adding new method into String. Its called the augmentation.

HardenedGolo is a project aiming in statically verify some Golo code. The static verification could be only the verification of the language semantic (a division is not made by 0) or the verification of the respect of a specification. We are then currently adding the possibility to describe a specification into a Golo program in a JML-like manner, with the syntax of WhyML. This IST project is in the context of this new feature.

Objectives

In this project, many aspects could be developped, according to the preferences of the students, among them:

• Test and complete parser for First Order Logic specification, with the associate intermediate representation
• Integration into Gradle whith non-regression tests
• Add type information into intermediate representation (IR)
• Add type propagation / induction into IR
• Extend the JGolo specification language with some new primitives expressing that a method/an attribute exists or does not exist into an object.
• Considere specific WhyML functions into JGolo specification (i.e. to_int, of_int, ...)
• Propose a new name for the specification language (or found an explanation for "Why JGolo ?")

References