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

CommentaDi' la tua

Il tuo indirizzo email non sarà mostrato pubblicamente. I campi obbligatori sono contrassegnati da *