Μηχανική κατασκευή συνεπαγωγικών (coinductive) αποδείξεων στη Liquid Haskell

Abstract

Η ορθότητα είναι μια επιθυμητή αλλά όχι τετριμμένη ιδιότητα του λογισμικού. Ένας πολύ αξιόπιστος τρόπος για να διασφαλιστεί η ορθότητα είναι η επαλήθευση λογισμικού. H Liquid Haskell είναι ένας επαγωγικός επαληθευτής που βασίζεται σε έναν επιλύτη SMT και επεκτείνει το σύστημα τύπων της Haskell χρησιμοποιώντας λογικά κατηγορήματα. Χρησιμοποιώντας τη Liquid Haskell, είναι δυνατό να αποδειχθούν πολλές επιθυμητές ιδιότητες για κώδικα γραμμένο σε Haskell. Η Haskell, λόγω της οκνηρής αποτίμησης, μας επιτρέπει να ορίσουμε αντικείμενα που έχουν πιθανώς άπειρα στοιχεία, όπως άπειρες λίστες. Ωστόσο, η Liquid Haskell δεν είναι σε θέση να επαληθεύσει τέτοιους ορισμούς λόγω έλλειψη τερματισμού τους. Επίσης, για παρόμοιους λόγους, δεν μπορεί να επιχειρηματολογήσει για ιδιότητες τέτοιων ορισμών.

Αυτή η εργασία έχει στόχο να αντιμετωπίσει αυτό το χάσμα μεταξύ των δυνατοτήτων της Haskell και της εκφραστικότητας της Liquid Haskell. Παρουσιάζουμε μια τεχνική που μας βοηθά να επαληθεύσουμε την παραγωγικότητα των συναναδρομικών ορισμών, ακολουθώντας παρόμοια δουλειά σε άλλες γλώσσες. Παρουσιάζουμε επίσης δύο εναλλακτικές προσεγγίσεις, δηλαδή τις συνεπαγωγικές αποδείξεις με τη χρήση δεικτών και τις εποικοδομητικές συνεπαγωγικές αποδείξεις, οι οποίες κωδικοποιούν με συνέπεια συνεπαγωγικές αποδείξεις στη Liquid Haskell. Χρησιμοποιούμε αυτές τις κωδικοποιήσεις για να ελέγξουμε αυτόματα διάφορους ορισμούς και αποδείξεις, επιδεικνύοντας πώς μπορεί να χρησιμοποιηθεί ένας επαγωγικός επαληθευτής για να ελέγχθούν οι συνεπαγωγικές ιδιότητες και η παραγωγικότητα κώδικα Haskell.