💻 computer science

Predicate Subtypes in VerCors

Este artículo presenta la integración de subtipos de predicado en el verificador de programas VerCors, una característica que permite generar especificaciones automáticas, combinar múltiples subtipos y realizar comprobaciones de desbordamiento mediante un modo estricto.

Autores originales: Tycho Dubbeling (University of Twente), Marieke Huisman (University of Twente), Ömer Şakar (University of Twente)

Publicado 2026-04-09

📖 4 min de lectura☕ Lectura para el café

CC BY 4.0

Autores originales: Tycho Dubbeling (University of Twente), Marieke Huisman (University of Twente), Ömer Şakar (University of Twente)

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

¡Hola! Imagina que estás construyendo una casa muy segura. Normalmente, cuando pides materiales de construcción, dices: "Necesito ladrillos". Pero, ¿qué pasa si necesitas ladrillos que sean rojos y de tamaño específico y que no estén rotos?

El papel que hemos leído habla de una herramienta llamada VerCors, que es como un inspector de obras digital muy inteligente. Su trabajo es revisar el código de los programas de computadora (especialmente los que hacen muchas cosas a la vez) para asegurarse de que no se rompan ni fallen.

Los autores, Tycho, Marieke y Ömer, han añadido una nueva función a este inspector: los Subtipos de Predicado. Suena complicado, pero es muy sencillo si lo imaginamos así:

1. ¿Qué son los "Subtipos de Predicado"?

Imagina que tienes una caja de herramientas.

Sin subtipos: Dices "Tengo un destornillador". El inspector solo sabe que es un destornillador. Podría ser pequeño, grande, oxidado o sin punta.
Con subtipos: Dices "Tengo un destornillador que tenga la punta en perfecto estado y mida exactamente 10 cm".

En el mundo de la programación, esto significa que puedes decirle al programa: "Esta variable es un número, pero solo si es mayor que cero" o "Esta lista es un array, pero solo si tiene exactamente 5 elementos".

El gran truco de este trabajo es que el inspector (VerCors) automáticamente entiende estas reglas. No tienes que escribir cientos de advertencias manuales en cada parte del código. Si dices "esto es un número no cero", el sistema pone un guardia invisible en esa variable para asegurarse de que nunca se convierta en cero.

2. La analogía del "Guardián Estricto" (Modo Strict)

Aquí viene la parte más interesante. A veces, no basta con que el resultado final sea correcto; ¡todo el proceso para llegar ahí también debe ser correcto!

Imagina que eres un chef y tienes una regla estricta: "Nunca toques un cuchillo si no tienes guantes".

Modo normal: Si al final del plato tienes guantes, el inspector dice "¡Bien hecho!". No le importa si te cortaste el dedo mientras pelabas la patata sin guantes, siempre que al final los pusieras.
Modo "Strict" (Estricto): El inspector dice: "¡Espera! Si en algún momento del proceso (incluso un segundo) no tenías guantes, el plato está arruinado".

En programación, esto sirve para evitar desbordamientos (overflows). Imagina que tienes un vaso que solo cabe hasta el borde (el límite de un número en una computadora).

Si llenas el vaso hasta el borde, está bien.
Pero si, al verter el agua, se derrama un poco por el camino (un cálculo intermedio que se sale del límite), en el modo estricto el inspector te gritará: "¡Cuidado! Se derramó agua, aunque al final el vaso esté lleno".

Esto es vital para evitar que los programas se rompan o se comporten de forma extraña cuando los números son demasiado grandes.

3. ¿Cómo funciona la magia?

Los autores explican que, en lugar de cambiar todo el motor del inspector (lo cual sería como reconstruir toda la casa), simplemente traducen estas reglas especiales a un lenguaje que el inspector ya entiende perfectamente.

Es como si tú le dijeras al inspector: "Quiero un ladrillo rojo". Y el inspector, automáticamente, escribe en su libreta: "Revisar que el ladrillo sea rojo, que no esté roto y que mida 10cm". Luego, el inspector hace su trabajo habitual revisando esas notas.

4. ¿Por qué es útil esto?

Seguridad: Evita errores tontos como dividir por cero o usar un índice que no existe en una lista.
Claridad: Hace que el código se lea mejor porque las reglas están pegadas a la variable misma, no escondidas en otro lado.
Flexibilidad: Puedes combinar reglas. Por ejemplo: "Un número que sea positivo O que sea cero, pero NO que sea negativo".

En resumen

Este paper presenta una mejora para el "Inspector de Código" VerCors. Ahora, los programadores pueden poner etiquetas de seguridad muy específicas en sus variables (como "solo números positivos" o "solo listas de 3 elementos").

El sistema traduce estas etiquetas en reglas automáticas que vigilan el código paso a paso. Además, tiene un "Modo Estricto" que vigila incluso los pasos intermedios de los cálculos para asegurar que no haya "derrames" de números (desbordamientos) que puedan romper el programa.

Es como pasar de tener un inspector que solo mira si la casa está de pie, a tener uno que revisa que cada ladrillo, cada mezcla de cemento y cada paso de construcción cumpla con las reglas de seguridad más estrictas.

Resumen Técnico: Predicados de Subtipos en VerCors

1. El Problema

En la verificación deductiva de programas, es fundamental especificar restricciones sobre los valores de las variables (por ejemplo, que un divisor no sea cero o que un índice de array esté dentro de los límites). Sin embargo, los sistemas de tipos tradicionales de lenguajes como Java o C a menudo son insuficientes para expresar estas restricciones de rango de manera concisa y segura.

Existen dos desafíos principales abordados en este trabajo:

Falta de expresividad en el sistema de tipos: Es difícil comunicar información semántica (como "no nulo" o "longitud específica") a través del sistema de tipos del lenguaje de programación sin recurrir a anotaciones manuales repetitivas o lógica de contratos compleja.
Desbordamientos de enteros (Overflows): En VerCors, los tipos numéricos (como int o byte) se codifican inicialmente como enteros matemáticos abstractos. Esto ignora los desbordamientos (overflows) que ocurren en la aritmética real de la máquina. Como consecuencia, el verificador podría pasar por alto comportamientos indefinidos o fallos de ejecución, especialmente en expresiones intermedias que, aunque el resultado final sea válido, violan los límites del tipo durante el cálculo.

2. Metodología

Los autores proponen extender el lenguaje de especificación de VerCors (un verificador deductivo para programas concurrentes) con subtipos predicados. La metodología se basa en los siguientes pilares:

Definición de Subtipos: Un subtipo predicado se define como un conjunto de elementos de un tipo base $X$ que satisfacen un predicado $P$ . Formalmente: $\{x:X \mid P(x)\}$ .
Codificación Automática: Dado que la verificación de tipos con predicados es indecidible, el enfoque no modifica el sistema de tipos estático del lenguaje, sino que genera automáticamente especificaciones estándar (precondiciones, postcondiciones y aserciones intermedias) en el lenguaje de especificación de VerCors (PVL).
- Parámetros de entrada: Se generan precondiciones que aseguran que los argumentos cumplen el predicado.
- Retornos: Se generan postcondiciones que aseguran que el valor de retorno cumple el predicado.
- Asignaciones: Se insertan aserciones después de cada asignación a una variable subtipada para verificar que el nuevo valor satisface el predicado.
Modo Estricto (Strict Mode): Para abordar el problema de los desbordamientos, se introduce un modo estricto (strict). En este modo, todas las subexpresiones deben permanecer dentro de los límites del subtipo, no solo el resultado final. Esto permite detectar desbordamientos en operaciones intermedias (ej. x - 2 dentro de un rango positivo).
Combinación de Predicados: Se permite combinar múltiples subtipos mediante operadores lógicos: conjunción (implícita), disyunción (|), implicación (==>), y negación (!).

3. Contribuciones Clave

El artículo presenta las siguientes contribuciones técnicas:

Implementación de Subtipos Predicados en VerCors: Se ha integrado soporte para definir y utilizar subtipos en las especificaciones de VerCors para Java y PVL.
Generación Automática de Especificaciones: El sistema traduce automáticamente las anotaciones de subtipos en contratos estándar (requires, ensures, assert), eliminando la necesidad de que el usuario escriba manualmente las condiciones de rango para cada variable.
Mecanismo de Verificación de Desbordamientos (Strict Arithmetic):
- Se introduce una bandera de opción (--strict-arithmetic) que convierte automáticamente el tipo int de Java en un subtipo estricto con límites de 32 bits ( $-2^{31}$ a $2^{31}-1$ ).
- Esto fuerza al verificador a comprobar que cada operación aritmética intermedia no exceda estos límites, detectando desbordamientos que el modelo de enteros matemáticos ignoraría.
Soporte para Subtipos Parametrizados y Anidados: El sistema soporta predicados con parámetros (ej. Index(length)) y la anidación de subtipos (subtipos de subtipos), resolviendo las dependencias mediante la conjunción de los cuerpos de los predicados.
Estrategia de Inline (Inlining): Para evitar la complejidad de la expansión de predicados y mantener la carga de prueba razonable, los autores decidieron "inlinear" (expandir) los predicados de subtipo directamente en las especificaciones generadas en lugar de mantener referencias a nombres de predicados que requerirían desdoblamiento explícito.

4. Resultados

Prototipo Funcional: Se ha desarrollado un prototipo integrado en el verificador VerCors que soporta la sintaxis de subtipos, la combinación lógica de predicados y la verificación de desbordamientos.
Validación de Casos de Uso: El sistema ha demostrado ser capaz de:
- Verificar automáticamente que un divisor no sea cero.
- Garantizar que los índices de arrays estén dentro de los límites.
- Detectar desbordamientos en expresiones intermedias bajo el modo estricto, incluso cuando el resultado final parece válido.
Comparación con Dafny: A diferencia de Dafny, que tiene subtipos más rígidos y no soporta subtipos parametrizados instanciados posteriormente de la misma manera flexible, la implementación en VerCors ofrece mayor flexibilidad en la expresión de restricciones y la combinación de predicados.

5. Significancia

Este trabajo es significativo por varias razones:

Seguridad en Programación Concurrente: Al integrar esta funcionalidad en VerCors, se mejora la capacidad de verificar programas concurrentes complejos donde los desbordamientos de enteros o las violaciones de invariantes de rango pueden llevar a comportamientos catastróficos difíciles de rastrear.
Abstracción vs. Realidad de Máquina: Proporciona un puente crucial entre la abstracción matemática (usada para la verificación lógica) y la realidad de la aritmética de máquina (con límites fijos y desbordamientos), permitiendo a los desarrolladores elegir cuándo verificar desbordamientos mediante una bandera de configuración.
Reducción de Carga Cognitiva: Al automatizar la generación de aserciones de rango a partir de anotaciones de tipo, reduce la carga de trabajo del desarrollador y minimiza errores humanos al especificar contratos manuales.
Base para Futuras Extensiones: Establece una base sólida para futuras mejoras, como la extensión a otros lenguajes (C), la creación de bibliotecas estándar de subtipos y la integración automática con anotaciones de nullabilidad (@NonNull).

En conclusión, el artículo demuestra que la adición de subtipos predicados a un verificador de programas existente es viable y altamente efectiva para mejorar la precisión de la verificación, especialmente en la detección de errores de rango y desbordamientos, manteniendo la automatización del proceso de generación de pruebas.