ScratchLens: Lens-Parametric Behavioral Equivalence for Scratch Programs

Resumo Técnico: ScratchLens: Equivalência Comportamental Paramétrica por Lentes para Programas Scratch

Problema
O Scratch, um ambiente de programação visual baseado em blocos utilizado por mais de 140 milhões de crianças, apresenta um desafio único para a comparação automatizada de programas. Dois programas Scratch podem ser sintaticamente distantes devido à renomeação de variáveis, divisão de scripts, extração de blocos personalizados ou reordenação de inicialização, mas permanecer comportamentalmente equivalentes. Inversamente, uma única edição de um bloco (por exemplo, substituir um broadcast bloqueante por um assíncrono) pode introduzir divergências que só se manifestam sob condições específicas de escalonamento, entradas aleatórias ou temporização.

Os métodos de comparação existentes falham neste contexto:

• Diferenciação de árvore (Tree differencing) é estrita demais, sinalizando mudanças sintáticas (como limites de scripts) que não alteram a semântica.
• Comparação dinâmica de execução única (Single-run dynamic comparison) é insustentável para comportamentos concorrentes, aleatórios e dependentes de tempo, pois amostra apenas um escalonamento e um rastro de entrada.
• Falsa equivalência é particularmente custosa em contextos educacionais, pois pode validar incorretamente um programa de aluno defeituoso, encerrando prematuramente um episódio de depuração.

A dificuldade central é que a equivalência comportamental no Scratch não é absoluta, mas paramétrica em uma lente de observação. Um "deslizar" (glide) e um "pular" (jump) podem concordar no estado final, mas discordar nos rastros visuais quadro a quadro; dois scripts podem concordar sob um escalonamento, mas divergir sob outro.

Metodologia
Os autores propõem o ScratchLens, um verificador de equivalência estruturado em torno de uma taxonomia de divergência comportamental e um modelo de observação paramétrico por lentes.

1. Taxonomia da Divergência:
   O sistema organiza a divergência comportamental ao longo de dois eixos:

   • Lentes de Observação: Projeções de rastros de execução concretos para observações específicas (ex: estado final, instantâneos de fronteira de quadro, efeitos de palco, valores de monitores, causalidade de eventos, ou rastros de depuração).
   • Fenômenos Causais: Oito famílias de transportadores (carrier families) (Estado, Causalidade de Eventos, Sensibilidade de Escalonamento, Aleatoriedade, Tempo/Quadros, Ciclo de Vida de Clones, Filas de Interação, Saída Persistente) que mapeiam para causas raiz tipadas (ex: MISSINGJOINEDGE, UninitializedRead).

2. Representação Intermediária Causal (CSIR):
   Os projetos Scratch são compilados em CSIR, uma representação tipada de recursos (variáveis, listas, sprites, broadcasts, etc.) e transações.

   • Pegadas (Footprints): Cada transação registra pegadas tipadas (leituras, escritas, consumo, criação, junção, morte).
   • Canonicização: O sistema realiza uma canonicização invariante de renomeação alfa usando perfis de uso e refinamento de Weisfeiler–Leman. Procedimentos são comparados via digests de conteúdo sobre primitivas normalizadas.
   • Formas Normais de Rastro: Para lidar com concorrência, o ScratchLens aplica uma forma normal de rastro de Mazurkiewicz sobre uma relação de independência conservadora. Ele separa a ordem do programa das condições de corrida, permitindo que scripts comutativos sejam tratados como equivalentes enquanto preserva compromissos de escalonamento (ex: arestas de junção).

3. Algoritmo de Comparação:
   O algoritmo procede através de uma hierarquia de verificações:

   • Equivalência Estática: Compara multiconjuntos de características canônicas. Se forem iguais e as condições laterais estiverem fechadas, retorna equivalência com uma bijeção explícita e um quociente de rastro.
   • Busca de Bijeção Limitada: Se os perfis iniciais empatarem, o sistema busca uma bijeção de descida de coordenadas para minimizar o delta de explicação.
   • Transferência Abstrata: Para lentes Lfinal (estado final), verifica se uma transferência abstrata sobre domínios numéricos, de strings e de listas prova a equivalência apesar das diferenças estruturais.
   • Classificação & Obrigações: Incompatibilidades são classificadas em causas raiz tipadas. Diferenças condicionais (ex: viabilidade de guarda) tornam-se obrigações.
   • CEGAR com VM Instrumentada: Fronteiras não resolvidas disparam Refinamento de Abstração Guiado por Contraexemplo (CEGAR). O sistema sintetiza cenários direcionados (ex: tokens aleatórios específicos ou execuções de estresse de receptor) executados em uma VM Scratch instrumentada para confirmar ou refutar a divergência.

4. Vereditos:
   Cada veredito conclusivo carrega evidência explícita:

   • Equivalência: Provada por uma bijeção e um quociente de rastro (ou transferência abstrata).
   • Diferença: Provada por uma testemunha tipada (ex: uma aresta de junção ausente) ou um contraexemplo concreto de VM.
   • Desconhecido: Reportado explicitamente para fronteiras não resolvidas, evitando alegações de falsa equivalência.

Principais Contribuições

• Uma Taxonomia de Dois Eixos: Um framework formal ligando mecanismos causais, lentes de observação e causas raiz tipadas para programas Scratch.
• Equivalência Paramétrica por Lentes: Uma definição de equivalência que considera explicitamente o observador, permitindo diferentes vereditos para o mesmo par sob diferentes lentes (ex: equivalente sob Lfinal mas diferente sob Lframe).
• CSIR e Algoritmo de Comparação: Uma representação intermediária causal e um núcleo de comparação combinando canonicização invariante de renomeação, formas normais de rastro e refinamento baseado em SMT/VM.
• Metodologia de Avaliação Reproduzível: Um corpus de mutação construído a partir de projetos Scratch reais, totalmente automatizado e testemunhado por VM. Inclui rótulos de verdade fundamental (ground-truth) por lente e um estrato de "composição profunda" que esconde defeitos sob pilhas de refatorações que preservam a equivalência.

Resultos
O sistema foi avaliado em um corpus de 444 pares validados (incluindo 158 diferenças testemunhadas por VM) e 88 mutantes ambíguos.

• Acurácia: O ScratchLens alcançou 1.000 de acurácia no corpus validado com 0 alegações de falsa equivalência nos 158 pares rotulados como diferentes.
• Diagnóstico: Recuperou tanto o veredito quanto a causa raiz injetada para 98,7% dos pares diferentes.
• Linhas de Base (Baselines): As linhas de base estrutural, de abstração de opcode e puramente dinâmica falharam significativamente em classes específicas previstas pela taxonomia (ex: testes dinâmicos produziram 28 falsas equivalências; LLMs produziram de 8 a 15).
• Ablações: Remover a Redução de Ordem Parcial (POR) aumentou as falsas diferenças; restringir apenas para a lente Lfinal causou uma queda massiva no recall (0,215), pois divergências de evento e de quadro tornaram-se invisíveis.
• Cenários Direcionados: Nos 88 mutantes ambíguos (não resolvidos por testes aleatórios), os cenários direcionados gerados pelo ScratchLens expuseram 14 divergências concretas que os testes aleatórios perderam.

Significância
O artigo argumenta que a equivalência comportamental para programas visuais orientados a eventos deve ser paramétrica por lentes. Um único veredito binário é insuficiente; o observador (estado final vs. rastro de quadros vs. causalidade de eventos) deve ser explícito. O ScratchLens demonstra que, ao combinar análise causal estática com refinamento dinâmico direcionado, é possível alcançar uma verificação de equivalência de alta precisão que evita os alarmes falsos da diferenciação de árvore e a falta de consistência (unsoundness) de testes de execução única. O trabalho estabelece uma metodologia para "pontuação estrita" onde a abstenção (UNKNOWN) é preferível à falsa equivalência, um requisito crítico para sistemas de feedback automatizado e avaliação em educação. O artefato liberado fornece um benchmark para verificação de equivalência semântica que separa o raciocínio semântico da detecção de diferenças textuais.