Systerel publishes a new version of the HLL specification document (HLL LFD) and submits it to the next HLL Forum review in order to converge on the new definition of the language in collaboration with the other actors of the community.

These evolutions will facilitate modelling, improve the readability of models and allow users to build finer proof environments.

Thanks to these evolutions, the HLL is enriched with the following functionalities:

– syntax now allows the use of tuples in an assignment

– functions become a generalization of arrays

– a newSELECT quantifier allowing the user to query its model for the possible singleton defined by an expression

– nil generalization for models correct definition

– management of empty types

– quantification on types

– generalization of elementhood

– quantification on composite types

– POs can now be collections

The document is available in preview here, feel free to download it.

To know more about the HLL language Our formal verification offer Systerel Smart Solver around this language