Please use this identifier to cite or link to this item:
http://artemis.cslab.ece.ntua.gr:8080/jspui/handle/123456789/17036
Title: | ΕΠΑΛΗΘΕΥΣΗ ΙΔΙΟΤΗΤΩΝ ΑΛΓΟΡΙΘΜΩΝ ΣΕ LIQUID HASKELL |
Authors: | Πέτρου, Γεώργιος Παπασπύρου Νικόλαος |
Keywords: | Liquid Haskell refinement types απόδειξη θεωρημάτων επαλήθευση SMT solver reflection proof by logical evaluation |
Issue Date: | 16-Jul-2018 |
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 ως ένα πλήρες εργαλείο για απόδειξη θεωρημάτων. |
URI: | http://artemis.cslab.ece.ntua.gr:8080/jspui/handle/123456789/17036 |
Appears in Collections: | Διπλωματικές Εργασίες - Theses |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
theses.pdf | ΕΠΑΛΗΘΕΥΣΗ ΙΔΙΟΤΗΤΩΝ ΑΛΓΟΡΙΘΜΩΝ ΣΕ LIQUID HASKELL | 834.51 kB | Adobe PDF | View/Open |
Items in Artemis are protected by copyright, with all rights reserved, unless otherwise indicated.