Στατική Ανάλυση Για Έλεγχο Λαθών Στη Γλώσσα Ruby

Abstract

Ο προγραμματισμός ηλεκτρονικών υπολογιστών είναι μία επιστήμη που έχει γνωρίσει ραγδαία ανάπτυξη τις τελευταίες δεκαετίες. Τη σημερινή μέρα είναι εύκολο για τον οποιονδήποτε να γράψει κάποιο πρόγραμμα σε κάποια γλώσσα προγραμματισμού. Αντίθετα, οι τεχνικές απόδειξης οτι ένα πρόγραμμα όντως κάνει αυτό που θέλει ο προγραμματιστής δεν είναι εξίσου ανεπτυγμένες. Η πιο απλή μορφή απόδειξης για τη σωστή λειτουργία ενός προγράμματος είναι ο έλεγχος ορθότητας από ένα σύστημα τύπων. Σε αυτή τη διπλωματική κατασκευάζουμε ένα στατικό σύστημα τύπων που να εντοπίζει σφάλματα τύπου σε αντικειμενοστρεφείς γλώσσες προγραμματισμού με δυναμικό σύστημα τύπων. Στη συνέχεια, υλοποιούμε αυτό το σύστημα τύπων για ένα υποσύνολο της γλώσσας προγραμματισμού Ruby, το οποίο εν συνεχεία επεκτείνουμε ώστε να καλύψει μεγαλύτερο μέρος της γλώσσας Ruby.Το σύστημα τύπων που κατασκευάζουμε είναι βασισμένο στα Success Typings, τη θεωρία πίσω από το εργαλείο Dialyzer που βρίσκει σφάλματα τύπου σε προγράμματα της γλώσσας Erlang. Η βασική του ιδιότητα είναι οτι δεν υπάρχει περίπτωση να εντοπίσει σφάλμα σε πρόγραμμα το οποίο δεν έχει σφάλμα. Δηλαδή, εντοπίζει μόνο υπαρκτά σφάλματα. Το εργαλείο που εντοπίζει τα σφάλματα στο υποσύνολο της γλώσσας Ruby είναι εύκολο στη χρήση του, καθώς δεν χρειάζεται καμία υποσημείωση τύπων για να λειτουργήσει σωστά.Τέλος, παρουσιάζουμε μία βήμα προς βήμα σύγκριση με τον κύριο ανταγωνιστή στον εντοπισμό σφαλμάτων τύπου στη γλώσσα Ruby, Diamondback Ruby, σχολιάζοντας τις εξόδους των δύο εργαλείων.