ΕΠΑΛΗΘΕΥΣΗ ΙΔΙΟΤΗΤΩΝ ΑΛΓΟΡΙΘΜΩΝ ΣΕ LIQUID HASKELL

Abstract

Στη Διπλωματική εργασία αυτή γίνεται μελέτη των τεχνικών που παρέχονται από τη Liquid Haskell για την απόδειξη θεωρημάτων και η χρησιμοποίησή τους για την επαλήθευση ιδιοτήτων διαφόρων αλγορίθμων. Η Liquid Haskell αποτελεί ένα σύστημα που μας δίνει τη δυνατότητα να εκφράζουμε ιδιότητες για προγράμματα γραμμένα σε Haskell με τη χρήση refinement types οι οποίες επαληθέυονται αυτόματα με τη χρήση SMT solver. Επιπλέον η Liquid Haskell με την εισαγωγή του reflection μας επιτρέπει την διατύπωση και απόδειξη θεωρημάτων εκφρασμένων ως συναρτήσεις σε Haskell, προσφέρωντας ειδικές βιβλιοθήκες που παρέχουν ένα πλήρες περιβάλλον για την ανάπτυξη αρκτεκά εξελιγμένων αποδείξεων χρησιμοποιώντας βασικά refinements και ορισμούς συναρτήσεων . Στο πλαίσιο της εργασίας , αρχικά γίνεται μια ανασκόπηση σχετικά με τις ένοιες που θα συναντήσουμε στη Liquid Haskell, όπως refinement types, την έννοια του reflection, μεθόδους αποδείξεων, ανάλυση της βιβλιοθήκης που μας δίνει τη δυνατότητα για συγγραφή αποδείξεων κλπ.. και στη συνέχεια προχωράμε στην ανάλυση ιδιοτήτων ορισμένων διαδέδομένων αλγορίθμων και δομών δεδομένων που αποτελεί και το βασικό μέρος της διπλωματικής. Οι αλγόριθμοι που αναλύουμε προέχρονται από το 3ο τόμο του βιβλίου Software Foundations που περιέχει διατυπώσεις θεωρημάτων και ιδιοτήτων σε γλώσσα Coq. Στη παρούσα διπλωματική θα αναδιατυπώσουμε τα θεωρήματα και ιδιότητες σε γλώσσα Haskell και θα τα επαληθευσουμε γράφωντας αποδείξεις σε Liquid Haskell παρουσιάζοντας έτσι το τρόπο με τον οποίο μπορούμε να διατυπώνουμε θεωρήματα και αναδεικνύωντας τη Liquid Haskell ως ένα πλήρες εργαλείο για απόδειξη θεωρημάτων.