ScratchLens: Lens-Parametric Behavioral Equivalence for Scratch Programs

Resumen Técnico: ScratchLens: Equivalencia de Comportamiento Paramétrica por Lentes para Programas de Scratch

Planteamiento del Problema
Scratch, un entorno de programación visual basado en bloques utilizado por más de 140 millones de niños, presenta un desafío único para la comparación automatizada de programas. Dos programas de Scratch pueden ser sintácticamente distantes debido al renombrado de variables, la división de scripts, la extracción de bloques personalizados o el reordenamiento de la inicialización, y aun así ser comportamentalmente equivalentes. Por el contrario, una edición de un solo bloque (por ejemplo, reemplazar un broadcast bloqueante por uno asíncrono) puede introducir divergencias que solo se manifiestan bajo condiciones específicas de programación, entradas aleatorias o tiempos.

Los métodos de comparación existentes fallan en este contexto:

• La diferenciación de árboles es demasiado estricta, señalando cambios sintácticos (como los límites de los scripts) que no alteran la semántica.
• La comparación dinámica de ejecución única es unsound (no es sólida) para comportamientos concurrentes, aleatorios y dependientes del tiempo, ya que solo muestrea un esquema y un rastro de entrada.
• La falsa equivalencia es particularmente costosa en entornos educativos, ya que puede validar incorrectamente un programa de estudiante defectuoso, terminando prematuramente un episodio de depuración.

La dificultad central es que la equivalencia de comportamiento en Scratch no es absoluta, sino paramétrica en un lente de observación. Un "glide" (deslizar) y un "jump" (saltar) pueden coincidir en el estado final, pero discrepar en los rastros visuales fotograma a fotograma; dos scripts pueden coincidir bajo un esquema pero divergir bajo otro.

Metodología
Los autores proponen ScratchLens, un verificador de equivalencia estructurado en torno a una taxonomía de divergencia de comportamiento y un modelo de observación paramétrico por lentes.

1. Taxonomía de la Divergencia:
   El sistema organiza la divergencia de comportamiento a lo largo de dos ejes:

   • Lentes de Observación: Proyecciones desde rastros de ejecución concretos hacia observaciones específicas (por ejemplo, estado final, instantáneas en los límites de fotogramas, efectos de la etapa, valores de monitores, causalidad de eventos o rastros de depuración).
   • Fenómenos Causales: Ocho familias de portadores (Estado, Causalidad de Eventos, Sensibilidad al Esquema, Aleatoriedad, Tiempo/Fotogramas, Ciclo de Vida de Clones, Colas de Interacción, Salida Persistente) que se mapean a causas raíz tipadas (por ejemplo, MISSINGJOINEDGE, UninitializedRead).

2. Representación Intermedia Causal (CSIR):
   Los proyectos de Scratch se compilan en CSIR, una representación tipada de recursos (variables, listas, sprites, broadcasts, etc.) y transacciones.

   • Footprints (Huellas): Cada transacción registra huellas tipadas (lecturas, escritas, consumos, spawns, joins, kills).
   • Canonicidad: El sistema realiza una canonicidad invariante de renombramiento alfa mediante perfiles de uso y refinamiento de Weisfeiler–Leman. Los procedimientos se comparan mediante digests de contenido sobre primitivas normalizadas.
   • Formas Normales de Rastro: Para manejar la concurrencia, ScratchLens aplica una forma normal de rastro de Mazurkiewicz sobre una relación de independencia conservadora. Separa el orden del programa de las condiciones de carrera, permitiendo que los scripts conmutativos sean tratados como equivalentes mientras se preservan los compromisos del programador (por ejemplo, los bordes de unión/join edges).

3. Algoritmo de Comparación:
   El algoritmo procede a través de una jerarquía de comprobaciones:

   • Equivalencia Estática: Compara multiconjuntos de características canónicas. Si son iguales y las condiciones laterales están cerradas, devuelve equivalencia con una biyección explícita y un cociente de rastro.
   • Búsqueda de Biyectiva Acotada: Si los perfiles iniciales empatan, busca una biyección de descenso de coordenadas para minimizar el delta de explicación.
   • Transferencia Abstracta: Para los lentes de Lfinal (estado final), verifica si una transferencia abstracta sobre dominios numéricos, de cadenas y de listas demuestra la equivalencia a pesar de las diferencias estructurales.
   • Clasificación y Obligaciones: Los desajustes se clasifican en causas raíz tipadas. Las diferencias condicionales (por ejemplo, la viabilidad de una guarda) se convierten en obligaciones.
   • CEGAR con VM Instrumentada: Los frentes no resueltos activan un Refinamiento de Abstracción Guiado por Contraejemplos (CEGAR). El sistema sintetiza escenarios dirigidos (por ejemplo, tokens aleatorios específicos o ejecuciones de estrés de receptor) ejecutados en una VM de Scratch instrumentada para confirmar o refutar la divergencia.

4. Veredictos:
   Cada veredicto conclusivo conlleva evidencia explícita:

   • Equivalencia: Probada por una biyección y un cociente de rastro (o transferencia abstracta).
   • Diferencia: Probada por un testigo tipado (por ejemplo, un borde de unión faltante) o un contraejemplo concreto de la VM.
   • Desconocido: Se reporta explícitamente para frentes no resueltos, evitando afirmaciones de falsa equivalencia.

Contribuciones Clave

• Una Taxonomía de Dos Ejes: Un marco formal que vincula mecanismos causales, lentes de observación y causas raíz tipadas para programas de Scratch.
• Equivalencia Paramétrica por Lentes: Una definición de equivalencia que considera explícitamente al observador, permitiendo diferentes veredictos para el mismo par bajo diferentes lentes (por ejemplo, equivalente bajo Lfinal pero diferente bajo Lframe).
• CSIR y Algoritmo de Comparación: Una representación intermedia causal y un núcleo de comparación que combina canonicidad invariante de renombramiento, formas normales de rastro y refinamiento respaldado por SMT/VM.
• Metodología de Evaluación Reproducible: Un corpus de mutaciones construido a partir de proyectos reales de Scratch, totalmente automatizado y con testigos de VM. Incluye etiquetas de verdad fundamental por lente y un estrato de "composición profunda" que oculta defectos bajo pilas de refactorizaciones que preservan la equivalencia.

Resultos
El sistema fue evaluado en un corpus de 444 pares validados (incluyendo 158 diferencias con testigos de VM) y 88 mutantes ambiguos.

• Precisión: ScratchLens logró una precisión de 1.000 en el corpus validado con 0 afirmaciones de falsa equivalencia en los 158 pares etiquetados como diferentes.
• Diagnóstico: Recuperó tanto el veredicto como la causa raíz inyectada para el 98.7% de los pares diferentes.
• Líneas Base: Las líneas base estructural, de abstracción de opcodes y de solo dinámica fallaron significativamente en clases específicas predichas por la taxonomía (por ejemplo, las pruebas dinámicas produjeron 28 falsas equivalencias; los LLM produjeron entre 8 y 15).
• Ablaciones: Eliminar la Reducción de Orden Parcial (POR) aumentó las falsas diferencias; restringir el análisis solo a Lfinal causó una caída masiva en la recuperación (0.215), ya que las divergencias de eventos y fotogramas se volvieron invisibles.
• Escenarios Dirigidos: En los 88 mutantes ambiguos (no resueltos por pruebas aleatorias), los escenarios dirigidos generados por ScratchLens expusieron 14 divergencias concretas que las pruebas aleatorias pasaron por alto.

Significado
El artículo argumenta que la equivalencia de comportamiento para programas visuales impulsados por eventos debe ser paramétrica por lentes. Un único veredicto binario es insuficiente; el observador (estado final vs. rastro de fotogramas vs. causalidad de eventos) debe ser explícito. ScratchLens demuestra que, combinando el análisis causal estático con el refinamiento dinámico dirigido, es posible lograr una verificación de equivalencia de alta precisión que evita las falsas alarmas del diferenciamiento de árboles y la falta de solidez de las pruebas de ejecución única. Este trabajo establece una metodología para la "calificación estricta" donde la abstención (UNKNOWN) es preferible a la falsa equivalencia, un requisito crítico para los sistemas de retroalimentación y calificación automatizados en la educación. El artefacto liberado proporciona un benchmark para la verificación de equivalencia semántica que separa el razonamiento semántico de la detección de diferencias textuales.