💻 computer science

Predicate Subtypes in VerCors

Este artigo descreve a implementação de subtipos predicativos no verificador de programas VerCors, apresentando uma abordagem que gera automaticamente especificações a partir de declarações de subtipos, permite a combinação de múltiplos subtipos e introduz um modo estrito para verificação de estouro de limites.

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

Publicado 2026-04-09

📖 5 min de leitura🧠 Leitura aprofundada

CC BY 4.0

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

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você é um chef de cozinha extremamente rigoroso. Você tem uma receita (o programa de computador) e quer garantir que, se alguém seguir as instruções, o prato final sairá perfeito, sem queimar a comida ou usar ingredientes proibidos.

O VerCors é como um "inspetor de receitas" superinteligente que lê o código do seu programa e tenta provar matematicamente que ele não vai dar errado. Mas, até agora, esse inspetor tinha uma limitação: ele aceitava ingredientes genéricos. Se a receita dizia "adicione um número", o inspetor aceitava qualquer número, desde que fosse um número. Ele não conseguia garantir, por exemplo, que você não fosse adicionar "zero" quando a receita exigia um divisor (o que faria a conta explodir) ou que o sal não passasse de uma pitada.

É aqui que entra o trabalho de Tycho Dubbeling, Marieke Huisman e Ömer Şakar. Eles criaram uma nova ferramenta para o VerCors chamada Subtipos de Predicado.

O Que São Subtipos de Predicado? (A Analogia do "Filtro Mágico")

Pense nos tipos de dados normais (como inteiro ou texto) como grandes caixas de armazenamento.

A caixa "Inteiro" guarda todos os números possíveis.
O problema é que, dentro dessa caixa gigante, podem haver números que estragam sua receita (como dividir por zero).

Os Subtipos de Predicado são como filtros mágicos que você coloca na boca da caixa.

Em vez de apenas dizer "coloque um número aqui", você diz: "coloque um número aqui, mas apenas se ele for diferente de zero".
Ou: "coloque um número aqui, mas apenas se ele estiver entre 0 e 127" (como um byte de memória).

O papel descreve como eles ensinaram o VerCors a criar esses filtros automaticamente. Quando você escreve no código:
int divisor = 5; (com um filtro de "não zero")
O VerCors não apenas aceita o 5. Ele gera automaticamente uma "nota de segurança" que diz: "Ei, antes de usar esse número, verifique se ele não é zero. E se alguém tentar mudar esse número para zero mais tarde, o sistema vai gritar 'ALERTA!'."

O Grande Truque: O "Modo Estrito" (O Guarda-Costas Rigoroso)

A parte mais legal e inovadora do artigo é a ideia do Modo Estrito (Strict Mode).

Imagine que você está dirigindo um carro em uma estrada com limite de velocidade de 100 km/h.

Modo Normal: O inspetor olha apenas para o velocímetro no final da viagem. Se você chegou a 90 km/h, está tudo bem. Ele não se importa se, no meio do caminho, você acelerou para 200 km/h e depois freou bruscamente.
Modo Estrito: O inspetor coloca um guarda-costas em cada curva, em cada aceleração e em cada freio. Ele exige que cada pequeno movimento do carro respeite o limite de 100 km/h.

No mundo dos computadores, isso é crucial para evitar estouro de memória (overflow).
Imagine que você tem um copo que cabe até 100ml de água.

Você coloca 90ml.
Adiciona 20ml. (Agora são 110ml! O copo transbordou, mesmo que você tire 20ml depois e deixe com 90ml).
No Modo Normal, o VerCors olharia apenas para o final (90ml) e diria "Tudo certo".
No Modo Estrito, o VerCors gritaria no passo 2: "Espere! Você tentou colocar 110ml num copo de 100ml! Isso é perigoso!"

Os autores criaram uma opção no sistema (--strict-arithmetic) que ativa esse guarda-costas rigoroso para todos os cálculos matemáticos, garantindo que nenhum número intermediário "vaze" do copo.

Como Eles Fizeram Isso? (A Máquina de Tradução)

O VerCors não entende nativamente esses "filtros mágicos" na linguagem de programação original. Então, os autores construíram uma máquina de tradução automática.

Leitura: O sistema lê o código com os filtros (ex: "inteiro não nulo").
Tradução: Ele transforma esses filtros em regras de segurança comuns que o VerCors já sabe ler (chamadas de "pré-condições" e "pós-condições"). É como se o sistema dissesse: "Ok, você pediu um 'inteiro não nulo'. Vou transformar isso em uma regra que diz: 'Antes de usar, verifique se não é zero'."
Verificação: O VerCors então prova matematicamente que essas regras nunca serão quebradas.

Por Que Isso é Importante?

Segurança: Evita que programas travem ou se comportem de forma estranha quando números ficam muito grandes ou quando se divide por zero.
Facilidade: O programador não precisa escrever centenas de verificações manuais. Ele apenas define o "filtro" uma vez na declaração da variável, e o sistema cuida de todo o resto.
Flexibilidade: Você pode combinar filtros. Por exemplo: "Um número que é maior que zero E menor que 100 OU é exatamente 200". O sistema entende essa lógica complexa e a transforma em regras de segurança.

Conclusão

Em resumo, esse artigo apresenta uma maneira inteligente de ensinar o VerCors a ser um "guardião de limites" mais esperto. Em vez de apenas olhar para o tipo de dado (ex: "é um número"), ele agora olha para o que esse número pode ou não fazer (ex: "é um número que não pode ser zero").

Eles adicionaram um "modo estrito" que vigia cada passo do cálculo, garantindo que não haja vazamentos de memória ou erros de cálculo ocultos. É como passar de um inspetor que só olha o resultado final para um inspetor que vigia cada ingrediente e cada passo da receita, garantindo que o prato final seja seguro e perfeito.

Título: Predicados de Subtipos no VerCors

Autores: Tycho Dubbeling, Marieke Huisman e Ömer Şakar (Universidade de Twente, Holanda)
Contexto: 17º Workshop Internacional sobre Abordagens de Linguagens de Programação para Concorrência e Software Centrado em Comunicação (PLACES 2026).

1. O Problema

Ao raciocinar sobre o comportamento de programas, é frequentemente necessário especificar restrições sobre os valores das variáveis (ex: um divisor não pode ser zero, um índice deve estar dentro dos limites de um array).

Limitação das Linguagens Atuais: A maioria das linguagens de programação possui sistemas de tipos limitados que não conseguem expressar essas restrições de valor de forma nativa e concisa.
Desafio na Verificação: Embora subtipos predicados (definidos como $\{x : X \mid P(x)\}$ ) sejam uma solução teórica atraente, a verificação de tipos com predicados é indecidível. Isso exige que as verificações sejam feitas fora do sistema de verificação de tipos tradicional, gerando verificações explícitas.
Problema de Overflow: Em verificadores como o VerCors, os tipos numéricos (como int ou byte) são frequentemente abstraídos para inteiros matemáticos. Isso ignora o comportamento de overflow (estouro de limite) das máquinas reais, podendo levar a falsos positivos na verificação ou falha em detectar comportamentos indefinidos e crashes.

2. Metodologia

Os autores propõem uma extensão ao VerCors (um verificador dedutivo para programas concorrentes em Java e C) que adiciona suporte a subtipos predicados através de uma abordagem de geração automática de especificações.

Mecanismo de Codificação:
- O sistema permite que usuários definam predicados booleanos que atuam como modificadores de tipo.
- Tradução Automática: Em vez de alterar o núcleo do verificador, as declarações de subtipos são traduzidas para especificações padrão do VerCors (contratos requires, ensures e assert).
- Geração de Asserções:
  - Parâmetros de Entrada: Geram pré-condições (requires) que afirmam que o parâmetro satisfaz o predicado.
  - Retorno de Métodos: Geram pós-condições (ensures) que afirmam que o valor retornado satisfaz o predicado.
  - Atribuições: Geram asserções (assert) após cada atribuição a uma variável subtipada para garantir que o novo valor ainda esteja dentro do subtipo.
- Combinação de Subtipos: O sistema suporta operadores lógicos para combinar múltiplos subtipos em uma única declaração: disjunção (|), implicação (==>), conjunção (concatenação) e negação (!).
Modo Estrito (Strict Mode) para Overflow:
- Para lidar com overflows, foi introduzido um modo "estrito" (strict).
- Neste modo, não apenas o valor final da variável, mas todas as subexpressões intermediárias devem permanecer dentro dos limites do subtipo.
- Um flag --strict-arithmetic converte automaticamente tipos int em subtipos estritos definidos pelos limites do inteiro de 32 bits (ex: $-2^{31}$ a $2^{31}-1$ ), verificando overflows em cada operação aritmética.

3. Contribuições Principais

Implementação de Subtipos Predicados no VerCors: Uma extensão funcional que permite anotações de tipo personalizadas (ex: NonZero, NonNull, Index) diretamente na sintaxe do código.
Geração Automática de Especificações: O sistema traduz automaticamente as anotações de subtipos em contratos formais (pré/pós-condições) e asserções intermediárias, eliminando a necessidade de o usuário escrever manualmente todas as verificações de domínio.
Flexibilidade na Combinação de Predicados: Suporte para combinar subtipos de forma complexa (ex: um array que é null OU tem tamanho 10 OU tem tamanho 3), algo que sistemas de tipos rígidos não permitem facilmente.
Verificação de Overflow via Subtipos Estritos: Uma abordagem inovadora para detectar overflows de inteiros verificando se expressões intermediárias violam os limites do tipo, superando a abstração para inteiros matemáticos.
Protótipo Integrado: A implementação foi integrada ao VerCors, suportando a análise de programas Java e PVL (Prototypal Verification Language).

4. Resultados

Funcionalidade: O protótipo demonstrou sucesso na tradução de anotações de subtipos para especificações Viper (backend do VerCors).
Cobertura: Suporta tipos definidos pelo usuário, subtipos parametrizados (ex: Index(length)) e aninhamento de subtipos.
Detecção de Erros: O modo estrito conseguiu identificar falhas de overflow em expressões intermediárias que seriam ignoradas em uma verificação padrão baseada em inteiros matemáticos.
Comparação: O trabalho oferece mais flexibilidade na expressão de predicados em comparação com o suporte a subtipos no Dafny, embora compartilhe conceitos similares com os "newtypes" e "subset types" do Dafny.

5. Significado e Impacto

Segurança de Programas Concorrentes: Ao permitir a especificação precisa de restrições de valores (como divisores não nulos ou índices válidos) diretamente no sistema de tipos, o VerCors torna a verificação de programas concorrentes mais robusta e menos propensa a erros de lógica.
Abordagem Prática para Overflow: A introdução do modo estrito oferece uma solução prática para o problema de verificação de overflows, permitindo que os desenvolvedores alternem entre uma verificação abstrata (inteiros matemáticos) e uma verificação concreta (inteiros de máquina) conforme necessário.
Redução de Esforço Manual: A automação da geração de asserções reduz significativamente a carga cognitiva sobre o programador, que não precisa escrever manualmente as verificações de domínio para cada variável.
Futuro: O trabalho abre caminho para bibliotecas padrão de subtipos, suporte a outras linguagens (como C) e melhorias na qualidade das mensagens de erro, tornando a verificação formal mais acessível e intuitiva.

Em resumo, o artigo apresenta uma evolução significativa na capacidade do VerCors de especificar e verificar restrições de domínio de variáveis, utilizando subtipos predicados para preencher a lacuna entre a abstração matemática e o comportamento real de execução de programas, especialmente em cenários críticos como concorrência e gerenciamento de memória.