Contrats publics et privés pour ACSL

Frama-C est une plateforme collaborative de l'analyse de programmes écrits en C. Cette plateforme comprend un langage de spécification nommé ACSL basé sur la notion de contrat. Ces contrats, fournis via des annotations dans le code, permettent de spécifier ce que l'on attend des différentes fonctions d'un programme. Il est ensuite possible de vérifier que le programme est conforme aux différents contrats à l'aide des analyseurs de la plateforme. Une limitation actuelle des contrats vis-à-vis du langage C est qu'ils ne permettent pas facilement de spécifier des contrats différents (interne/privé, externe/public) pour des modules d'un système lorsque ceux-ci cachent les détails d'implémentation aux modules utilisateurs. Pour cela, une différenciation entre contrat public et contrat privé est nécessaire, mais également les moyens de faire le lien entre les deux pour assurer la cohérence globale de la spécification et de l'analyse.