💻 computer science

Predicate Subtypes in VerCors

Ce papier présente l'intégration des sous-types prédicats dans le vérificateur de programme VerCors, une fonctionnalité qui génère automatiquement des spécifications à partir des déclarations de sous-types, permet leur combinaison et introduit un mode strict pour la vérification des débordements.

Auteurs originaux : Tycho Dubbeling (University of Twente), Marieke Huisman (University of Twente), Ömer Şakar (University of Twente)

Publié 2026-04-09

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Tycho Dubbeling (University of Twente), Marieke Huisman (University of Twente), Ömer Şakar (University of Twente)

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

🍳 La Cuisine de la Vérification : VerCors et les Sous-Types

Imaginez que VerCors est un chef cuisinier très méticuleux (un vérificateur de programme) qui prépare des plats complexes (des logiciels) pour des clients exigeants. Son travail est de s'assurer que le plat final est sûr, sans poison (bugs) et qu'il respecte exactement la commande du client.

Le problème, c'est que les ingrédients de base (les types de données comme les nombres entiers) sont souvent trop génériques. Un "nourriture" peut être n'importe quoi : un poison, un diamant, ou une pomme. Le chef veut pouvoir dire : "Non, pour cette recette, j'ai besoin d'une pomme rouge et sans vers."

C'est là qu'interviennent les sous-types prédicats.

1. Qu'est-ce qu'un sous-type prédicat ? (Le Filtre Magique)

Normalement, en programmation, on dit : "C'est un nombre entier". C'est vague.
Avec les sous-types prédicats, on ajoute un filtre magique ou une étiquette de contrôle qualité.

Exemple simple : Au lieu de dire "Donne-moi un nombre", on dit "Donne-moi un nombre qui n'est pas zéro".
L'analogie : Imaginez que vous commandez une pizza.
- Sans sous-type : "Je veux une pizza." (Le chef pourrait vous donner une pizza brûlée ou sans fromage).
- Avec sous-type : "Je veux une pizza avec exactement 3 tranches de pepperoni."
- Le chef (VerCors) va maintenant vérifier à chaque étape : "Attends, cette pizza a-t-elle 3 tranches ? Si non, je ne la sers pas."

Dans le papier, les auteurs montrent comment ils ont ajouté ce système de filtres dans VerCors. Au lieu de juste écrire le code, on écrit des règles comme : "Ce nombre doit être non nul" ou "Ce tableau doit avoir exactement 2 éléments".

2. Comment ça marche ? (Le Chef qui vérifie tout)

Le chef VerCors ne se contente pas de regarder la fin du plat. Il vérifie chaque étape de la préparation.

Les ingrédients (Paramètres) : Si une fonction demande un "nombre non nul", le chef vérifie l'ingrédient avant même de commencer à cuisiner.
Le résultat (Retour) : Si la fonction promet de rendre un "tableau de 3 éléments", le chef vérifie le plat fini avant de le servir.
La préparation (Assignations) : C'est ici que c'est génial. À chaque fois qu'on change un ingrédient (par exemple, on remplit un verre), le chef vérifie immédiatement : "Est-ce que ce verre est toujours plein ? Est-ce qu'il n'a pas débordé ?"

Si vous essayez de mettre un nombre qui ne respecte pas la règle (par exemple, diviser par zéro), le chef crie : "STOP ! Ce plat est interdit !" avant même que le programme ne plante.

3. Le Mode "Strict" : La Sécurité Anti-Explosion 🚨

C'est la partie la plus intéressante du papier. Parfois, même si le résultat final est bon, le chemin pour y arriver peut être dangereux.

L'analogie du pont :
Imaginez que vous devez traverser un pont (le calcul) pour arriver de l'autre côté.

Mode normal : Le chef regarde seulement si vous arrivez sain et sauf de l'autre côté. Il ne regarde pas si vous avez failli tomber pendant le trajet.
Mode "Strict" (Strict Subtypes) : Le chef vous met un harnais de sécurité. Il vérifie chaque pas que vous faites. Si, au milieu du pont, vous faites un faux pas (une opération intermédiaire qui dépasse les limites, comme un débordement de nombre), le harnais se déclenche et vous arrête.

Pourquoi est-ce important ?
En informatique, les nombres ont des limites (comme un compteur de voiture qui ne peut pas afficher plus de 999 999). Si vous faites un calcul intermédiaire qui dépasse cette limite, ça crée un "débordement" (overflow), comme un tuyau d'arrosage qui éclate.
Le mode strict de VerCors permet de dire : "Non seulement le résultat final doit être correct, mais aucune étape intermédiaire ne doit exploser le compteur."

4. La Cuisine en Équipe (Combinaison de règles)

Les auteurs montrent aussi qu'on peut mélanger ces filtres, comme des épices.

On peut dire : "Ce nombre doit être positif ET inférieur à 100." (Conjonction).
Ou : "Ce nombre doit être positif OU égal à zéro." (Disjonction).
C'est comme si le chef disait : "J'accepte soit une pomme rouge, soit une pomme verte, mais pas une poire."

En Résumé : Pourquoi c'est génial ?

Automatique : Le chef VerCors fait tout le travail de vérification tout seul. Vous n'avez pas besoin d'écrire des centaines de lignes de code pour vérifier que "A n'est pas nul". Vous écrivez juste "A est non nul" dans la définition, et le chef s'occupe du reste.
Sécurité maximale : Grâce au mode strict, on peut détecter des explosions de calculs (overflows) qui seraient restées invisibles autrement.
Flexibilité : On peut créer des règles sur mesure pour n'importe quel type de donnée, même celles que le langage de base ne comprend pas bien.

L'idée finale :
Ce papier explique comment transformer un vérificateur de code un peu "naïf" en un chef d'orchestre ultra-sécuritaire qui ne laisse passer aucun ingrédient douteux, ni aucune étape de cuisson risquée, garantissant ainsi que le logiciel final est solide, sûr et conforme à la commande.

Titre de l'article

Predicate Subtypes in VerCors (Sous-types prédicats dans VerCors)
Auteurs : Tycho Dubbeling, Marieke Huisman, Ömer Şakar (Université de Twente, Pays-Bas)
Conférence : PLACES 2026 (EPTCS 444)

1. Problématique

La vérification formelle de programmes, en particulier concurrents, nécessite souvent de spécifier des contraintes strictes sur les valeurs des variables au-delà de leur type de base (par exemple, un diviseur ne doit pas être nul, un tableau doit avoir une longueur spécifique, ou un entier doit rester dans une plage donnée).

Les défis principaux identifiés sont :

Spécification manuelle : Sans sous-types prédicats, les développeurs doivent écrire manuellement des préconditions, postconditions et des assertions à chaque point d'utilisation, ce qui est fastidieux et sujet aux erreurs.
Gestion des débordements (Overflows) : Dans des langages comme Java ou C, les types entiers sont abstraits en entiers mathématiques par les vérificateurs pour faciliter la preuve. Cependant, cette abstraction masque les débordements d'entiers (overflows) qui peuvent survenir lors d'opérations intermédiaires, conduisant à des comportements indéfinis ou des plantages non détectés.
Flexibilité des types : Les systèmes de types classiques ne permettent pas toujours d'encoder des contraintes complexes (ex: "un tableau non nul de longueur 2") directement dans la déclaration de la variable.

2. Méthodologie

Les auteurs proposent une extension du vérificateur de programme VerCors (qui utilise la logique de séparation basée sur les permissions et le langage intermédiaire Viper) pour supporter les sous-types prédicats.

L'approche repose sur les principes suivants :

Définition des sous-types : Un sous-type prédicat est défini comme un ensemble d'éléments d'un type de base satisfaisant un prédicat booléen $P$ (notation : $\{x : X \mid P(x)\}$ ). Les utilisateurs peuvent définir ces prédicats (ex: NonZero, Byte, Index).
Génération automatique de spécifications : Au lieu de modifier le système de typage (ce qui rendrait la vérification indécidable), le compilateur de VerCors traduit automatiquement les annotations de sous-types en spécifications standard (préconditions requires, postconditions ensures, et assertions assert).
- Les paramètres de méthode annotés génèrent des préconditions.
- Les types de retour génèrent des postconditions.
- Les affectations de variables génèrent des assertions après l'opération pour vérifier que la nouvelle valeur respecte le sous-type.
Combinaison de prédicats : Le système permet de combiner plusieurs sous-types pour une même variable via des opérateurs logiques : conjonction (implicite ou explicite), disjonction (|), implication (==>), et négation (!).
Mode Strict pour la vérification des débordements : Pour adresser le problème des débordements, les auteurs introduisent un mode strict. Dans ce mode, non seulement la valeur finale d'une expression doit respecter le sous-type, mais chaque sous-expression intermédiaire doit également rester dans les limites du sous-type.
- Un drapeau --strict-arithmetic est implémenté. Il convertit automatiquement tous les types int en un sous-type strict (strictIntGenerated) défini par les bornes de l'entier Java 32 bits ( $-2^{31}$ à $2^{31}-1$ ).

3. Contributions Clés

Implémentation dans VerCors : Intégration d'un prototype supportant les sous-types prédicats pour les langages Java et PVL (Prototypal Verification Language).
Traduction Automatisée : Développement d'une phase de réécriture (rewriting) qui transforme les annotations de sous-types en conditions de vérification standard (FOL - First Order Logic) compatibles avec le backend Viper.
Support des Sous-types Paramétrés : Capacité à définir des prédicats prenant des arguments (ex: Index(int x, int length)), permettant une réutilisation flexible des contraintes.
Détection d'Overflows par Sous-types Strict : Introduction d'une approche novatrice où la vérification des débordements est traitée comme une contrainte de sous-type stricte sur les expressions intermédiaires, offrant une granularité de contrôle supérieure aux approches classiques.
Opérateurs Logiques Avancés : Support natif pour la combinaison de sous-types (disjonction, implication, etc.), permettant des spécifications complexes comme « nul OU longueur 10 OU longueur 3 ».

4. Résultats et Fonctionnement Technique

Architecture : L'implémentation s'insère dans le pipeline de compilation de VerCors (Parsing -> AST -> Résolution -> Réécriture -> Viper). Les annotations de sous-types sont interprétées comme des expressions booléennes stockées dans des nœuds de type TSubtype.
Inlining des Prédicats : Pour éviter une explosion des obligations de preuve et simplifier la gestion des prédicats, les auteurs choisissent d'inliner (développer) les prédicats de sous-types directement dans les spécifications générées, plutôt que de les laisser sous forme de noms de fonctions à déplier.
Exemple de débordement : Le système détecte correctement qu'une expression comme (x - 2) + 2 échoue si x est dans un sous-type strict [0, 128], car l'intermédiaire x - 2 sort de cette plage, même si le résultat final y revient.
Comparaison avec Dafny : Contrairement à Dafny qui gère les sous-types de manière similaire mais avec moins de flexibilité sur les types paramétrés et les combinaisons logiques complexes, VerCors offre une plus grande flexibilité dans l'expression des contraintes via ses opérateurs logiques personnalisés.

5. Signification et Impact

Ce travail est significatif pour plusieurs raisons :

Réduction de la charge cognitive : Il automatise la génération de preuves de sécurité (comme la non-nullité ou les bornes de tableaux), permettant aux développeurs de se concentrer sur la logique métier.
Sécurité accrue : La capacité de détecter les débordements d'entiers via le mode strict offre une alternative puissante aux vérifications manuelles ou aux plugins externes, en intégrant cette vérification directement dans le système de types logique.
Extensibilité : L'approche est conçue pour être générique et peut être étendue à d'autres langages (comme C, mentionné comme travail futur) et à d'autres types de contraintes.
Équilibre Performance/Précision : En permettant de basculer entre une vérification sur les entiers mathématiques (rapide, sans overflow) et une vérification stricte (précise, avec overflow), les utilisateurs peuvent adapter le niveau de rigueur de la vérification à leurs besoins.

En conclusion, cet article présente une avancée pratique dans l'adoption des sous-types prédicats pour la vérification de programmes concurrents, en résolvant le compromis entre expressivité des spécifications et automatisation de la génération de preuves, tout en apportant une solution robuste à la problématique des débordements d'entiers.