Liquid Haskell

Οι ελλείψεις στον κώδικα και τα σφάλματα αποτελούν αναπόφευκτο μέρος των λογισμικών συστημάτων. Σε συστήματα κρίσιμα για την ασφάλεια, όπως αυτά των αεροσκαφών ή του ιατρικού εξοπλισμού, ακόμα και ένα μόνο σφάλμα μπορεί να οδηγήσει σε καταστροφικές συνέπειες, όπως τραυματισμούς ή θάνατο. Η τυπική επαλήθευση μπορεί να χρησιμοποιηθεί για τον στατικό εντοπισμό ελλείψεων στον κώδικα, αποδεικνύοντας ή διαψεύδοντας ιδιότητες ορθότητας ενός συστήματος. Ωστόσο, στην παρούσα της μορφή, η τυπική επαλήθευση είναι μια περίπλοκη διαδικασία που σπάνια χρησιμοποιείται από προγραμματιστές του ευρύτερου χώρου, κυρίως επειδή αφορά γλώσσες που δεν είναι γενικού σκοπού (π.χ. Coq, Agda, Dafny). Παρουσιάζουμε το LIQUID HASKELL, έναν πρακτικό επαληθευτή προγραμμάτων που στοχεύει στην καθιέρωση της τυπικής επαλήθευσης ως αναπόσπαστο μέρος της διαδικασίας ανάπτυξης λογισμικού. Το LIQUID HASKELL ενσωματώνει φυσικά τον καθορισμό ιδιοτήτων ορθότητας ως λογικές εξειδικεύσεις στους τύπους της Haskell. Επιπλέον, χρησιμοποιεί το πλαίσιο αφηρημένης ερμηνείας των “liquid types” ώστε να ελέγχει αυτόματα την ορθότητα των προδιαγραφών μέσω επιλυτών SMT (Satisfiability Modulo Theories), χωρίς να απαιτούνται ρητές αποδείξεις ή περίπλοκες επισημάνσεις. Τέλος, η γλώσσα προδιαγραφής είναι αυθαίρετα εκφραστική, επιτρέποντας στον χρήστη να γράφει γενικές ιδιότητες ορθότητας για τον κώδικά του, μετατρέποντας έτσι τη Haskell σε αποδεικτικό εργαλείο θεωρημάτων. Η μετατροπή μιας ώριμης γλώσσας — με βελτιστοποιημένες βιβλιοθήκες και ιδιαίτερα αποδοτική παραλληλοποίηση — σε αποδεικτικό εργαλείο, μας επιτρέπει να επαληθεύσουμε ευρύ φάσμα ιδιοτήτων σε εφαρμογές πραγματικού κόσμου. Χρησιμοποιήσαμε το LIQUID HASKELL για να επαληθεύσουμε ρηχές ακεραιότητες σε υπάρχοντα Haskell προγράμματα, π.χ. την ασφάλεια μνήμης της βελτιστοποιημένης βιβλιοθήκης επεξεργασίας συμβολοσειρών ByteString. Επιπλέον, ελέγξαμε βαθιές και σύνθετες ιδιότητες παραλληλισμένου Haskell κώδικα, π.χ. την ισοδυναμία ενός απλού αλγορίθμου εύρεσης συμβολοσειράς και της παραλληλοποιημένης εκδοχής του. Έχοντας επαληθεύσει περίπου 20.000 γραμμές Haskell κώδικα, παρουσιάζουμε πώς το LIQUID HASKELL λειτουργεί ως ένας πρωτότυπος επαληθευτής σε ένα μέλλον όπου οι τυπικές τεχνικές θα διευκολύνουν — αντί να εμποδίζουν — την ανάπτυξη λογισμικού.