Systerel publie une nouvelle version du document de spécification du langage HLL (HLL LFD) et le soumet à la prochaine revue du HLL Forum de manière à converger sur la nouvelle définition du langage en collaboration avec les autres acteurs de la communauté.

Ces évolutions permettent notamment de faciliter les modélisations, améliorer la lisibilité des modèles et  permettre aux utilisateurs de construire des environnements de preuve plus fins.

Grâce à ces évolutions, le HLL s’enrichit des fonctionnalités suivantes :

  • la syntaxe s’enrichit pour permettre d’utiliser des n-uplets dans une affectation
  • les fonctions deviennent une généralisation des tableaux
  • apparition du quantificateur SELECT qui permet à l’utilisateur de requêter son modèle à la recherche de l’éventuel singleton défini par une expression
  • la généralisation du nil pour la bonne définition des modèles
  • la gestion des types vides
  • la quantification sur les types
  • la généralisation de l’appartenance
  • la quantification sur les types composites
  • les POs peuvent désormais être des collections

Le document est disponible en avant-première ici, n’hésitez pas à le télécharger.

Pour en savoir plus sur le langage HLL

x

Notre offre de vérification formelle Systerel Smart Solver autour de ce langage