ScratchLens: Lens-Parametric Behavioral Equivalence for Scratch Programs

Sintesi Tecnica: ScratchLens: Equivalenza Comportamentale Parametrica rispetto alla Lente per Programmi Scratch

Problema
Scratch, un ambiente di programmazione visiva a blocchi utilizzato da oltre 140 milioni di bambini, presenta una sfida unica per il confronto automatico dei programmi. Due programmi Scratch possono essere sintatticamente distanti a causa del rinomina di variabili, della suddivisione degli script, dell'estrazione di blocchi personalizzati o del riordinamento dell'inizializzazione, pur rimanendo comportamentalmente equivalenti. Al contrario, una singola modifica a un blocco (ad esempio, sostituire un broadcast bloccante con uno asincrono) può introdurre divergenze che si manifestano solo sotto specifiche pianificazioni, input casuali o condizioni temporali.

I metodi di confronto esistenti falliscono in questo contesto:

• Il differenziamento ad albero (Tree differencing) è troppo rigido, segnalando cambiamenti sintattici (come i confini degli script) che non alterano la semantica.
• Il confronto dinamico a singola esecuzione è insicuro per comportamenti concorrenti, casuali e dipendenti dal tempo, poiché campiona un solo schema e un singolo tracciato di input.
• La falsa equivalenza è particolarmente costosa in contesti educativi, poiché può convalidare erroneamente un programma difettoso dello studente, interrompendo prematuramente un episodio di debugging.

La difficoltà fondamentale è che l'equivalenza comportamentale in Scratch non è assoluta ma parametrica rispetto a una lente di osservazione. Un "glide" (scivolamento) e un "jump" (salto) possono concordare sullo stato finale ma dissentire sui tracciati visivi fotogramma per fotogramma; due script possono concordare sotto uno schema ma divergere sotto un altro.

Metodologia
Gli autori propongono ScratchLens, un controllore di equivalenza strutturato attorno a una tassonomia della divergenza comportamentale e a un modello di osservazione parametrico rispetto alla lente.

1. Tassonomia della Divergenza:
   Il sistema organizza la divergenza comportamentale lungo due assi:

   • Lenti di Osservazione (Observation Lenses): Proiezioni dai tracciati di esecuzione concreti a osservazioni specifiche (ad esempio, stato finale, istantanee ai confini dei fotogrammi, effetti sullo stadio, valori dei monitor, causalità degli eventi, o tracce di debug).
   • Fenomeni Causali: Otto famiglie di vettori (Stato, Causalità degli Eventi, Sensibilità alla Pianificazione, Casualità, Tempo/Fotogrammi, Ciclo di Vita dei Cloni, Code di Interazione, Output Persistente) che mappano verso cause radici tipizzate (ad esempio, MISSINGJOINEDGE, UninitializedRead).

2. Rappresentazione Intermedia Causale (CSIR):
   I progetti Scratch vengono compilati in CSIR, una rappresentazione tipizzata di risorse (variabili, liste, sprite, broadcast, ecc.) e transazioni.

   • Impronte (Footprints): Ogni transazione registra impronte tipizzate (letture, scritture, consumi, spawn, join, kill).
   • Canonicalizzazione: Il sistema esegue una canonicalizzazione invariante rispetto all'alpha-renaming utilizzando profili di utilizzo e raffinamento Weisfeiler–Leman. Le procedure vengono confrontate tramite digest di contenuto su primitive normalizzate.
   • Forme Normali dei Tracciati: Per gestire la concorrenza, ScratchLens applica una forma normale di traccia di Mazurkiewicz su una relazione di indipendenza conservativa. Separa l'ordine del programma dalle condizioni di race, permettendo a script commutativi di essere trattati come equivalenti pur preservando gli impegni dello scheduler (ad esempio, i bordi di join).

3. Algoritmo di Confronto:
   L'algoritmo procede attraverso una gerarchia di controlli:

   • Equivalenza Statica: Confronta multisetti di caratteristiche canonicalizzate. Se uguali e le condizioni laterali sono chiuse, restituisce l'equivalenza con una bijezione esplicita e un quoziente di traccia.
   • Ricerca di Bijezione Limitata: Se i profili iniziali sono uguali, cerca una bijezione a discesa di coordinate per minimizzare il delta di spiegazione.
   • Trasferimento Astratto: Per le lenti Lfinal (stato finale), verifica se un trasferimento astratto su domini numerici, stringhe e liste dimostri l'equivalenza nonostante le differenze strutturali.
   • Classificazione e Obblighi: I disallineamenti sono classificati in cause radici tipizzate. Le differenze condizionali (ad esempio, la fattibilità delle guardie) diventano obblighi.
   • CEGAR con VM Strumentata: Le frontiere irrisolte attivano un processo di Raffinamento dell'Astrazione Guidato da Controesempi (CEGAR). Il sistema sintetizza scenari mirati (ad esempio, token casuali specifici o esecuzioni sotto stress del ricevitore) eseguiti su una VM Scratch strumentata per confermare o confutare la divergenza.

4. Verdetto:
   Ogni verdetto conclusivo porta prove esplicite:

   • Equivalenza: Dimostrata da una bijezione e un quoziente di traccia (o trasferimento astratto).
   • Differenza: Dimostrata da un testimone tipizzato (ad esempio, un bordo di join mancante) o da un controesempio concreto della VM.
   • Sconosciuto (Unknown): Riportato esplicitamente per le frontiere irrisolte, impedendo rivendicazioni di falsa equivalenza.

Contributi Chiave

• Una Tassonomia a Due Assi: Un framework formale che collega meccanismi causali, lenti di osservazione e cause radici tipizzate per i programmi Scratch.
• Equivalenza Parametrica rispetto alla Lente: Una definizione di equivalenza che tiene esplicitamente conto dell'osservatore, consentendo verdetti diversi per la stessa coppia sotto diverse lenti (ad esempio, equivalente sotto Lfinal ma differente sotto Lframe).
• CSIR e Algoritmo di Confronto: Una rappresentazione intermedia causale e un kernel di confronto che combina la canonicalizzazione invariante rispetto al rinomina, forme normali di traccia e raffinamento supportato da SMT/VM.
• Metodologia di Valutazione Riproducibile: Un corpus di mutanti costruito da veri progetti Scratch, completamente automatizzato e testimoniato dalla VM. Include etichette di verità fondamentale (ground-truth) per ogni lente e uno strato di "composizione profonda" che nasconde i difetti sotto pile di refactoring che preservano l'equivalenza.

Risultati
Il sistema è stato valutato su un corpus di 444 coppie validate (incluse 158 differenze testimoniate dalla VM) e 88 mutanti ambigui.

• Accuratezza: ScratchLens ha raggiunto un'accuratezza di 1.000 sul corpus validato con 0 rivendicazioni di falsa equivalenza sulle 158 coppie etichettate come differenti.
• Diagnosi: Ha recuperato sia il verdetto che la causa radice iniettata per il 98,7% delle coppie differenti.
• Baseline: I baseline strutturali, di astrazione degli opcode e puramente dinamici sono falliti significativamente su classi specifiche previste dalla tassonomia (ad esempio, il testing dinamico ha prodotto 28 false equivalenze; i modelli linguistici LLM ne hanno prodotte tra 8 e 15).
• Ablazioni: Rimuovere la Riduzione dell'Ordine Parziale (POR) ha aumentato le false differenze; limitarsi solo a Lfinal ha causato un drastico calo del richiamo (0.215), poiché le divergenze di eventi e fotogrammi diventavano invisibili.
• Scenari Mirati: Sugli 88 mutanti ambigui (irrisolti dal testing casuale), gli scenari mirati generati da ScratchLens hanno esposto 14 divergenze concrete che il testing casuale aveva mancato.

Significatività
Il saggio sostiene che l'equivalenza comportamentale per i programmi visivi guidati da eventi deve essere parametrica rispetto alla lente. Un singolo verdetto binario è insufficiente; l'osservatore (stato finale vs tracciato dei fotogrammi vs causalità degli eventi) deve essere esplicito. ScratchLens dimostra che combinando l'analisi causale statica con il raffinamento dinamico mirato, è possibile ottenere un controllo di equivalenza ad alta precisione che evita i falsi allarmi del differenziamento ad albero e l'insicurezza del testing a singola esecuzione. Il lavoro stabilisce una metodologia per il "punteggio rigoroso" dove l'astensione (UNKNOWN) è preferita rispetto alla falsa equivalenza, un requisito critico per i sistemi di feedback e valutazione automatizzata in ambito educativo. L'artefatto rilasciato fornisce un benchmark per il controllo dell'equivalenza semantica che separa il ragionamento semantico dal rilevamento delle differenze testuali.