Cosette: SQL solver open source

Cosette è un SQL solver che si occupa di eseguire un controllo automatico delle equivalenze nelle query SQL. Tramite questo SQL solver gli sviluppatori e i DBA potranno verificare la correttezza delle regole di riscrittura SQL e scovare i possibili errori.

Il controllo sa parte di Cosette avviene in modo abbastanza semplice, ovvero: due query SQL vengono considerate semanticamente equivalenti se, una volta eseguite, entrambe producono il medesimo risultato.

L’idea base di Cosette è proprio quella di facilitare questo processo di verifica rendendolo del tutto automatico, i developer non saranno quindi obbligati a controllare manualmente le query prodotte dalla propria applicazione, procedura che potrebbe rivelarsi difficoltosa nel caso in cui le interrogazioni generate dovessero essere numerose.

Una volta che l’utilizzatore avrà inserito i dati da verificare Cosette eseguirà due operazioni:

• se le due query SQL sono semanticamente identiche, allora verrà impiegato un Proof Assistant (Coq) per ottenere una prova meccanica e convalidare definitivamente la loro equivalenza;
• se invece le due query SQL sono diverse, allora Cosette troverà un controesempio (cioè una dimostrazione dell’esatto contrario) per dimostrare che queste non sono equivalenti.

Ci sono però dei casi in cui Cosette non riesce a decidere se due query SQL sono equivalenti o meno, solo allora verrà richiesta l’assistenza dell’utente.

Cosette è disponibile su Github dove è possibile trovare anche dei link per poterlo testare online. Dentro il repository è disponibile anche un dockerfile con il quale costruire la propria immagine Docker per avviare Cosette ovunque senza problemi.

Via University of Washington Database Group