Εθνικό Μετσόβιο Πολυτεχνείο
Σχολή Ηλεκτρολόγων Μηχ. & Μηχ. Υπολογιστών
Τομέας Τεχνολογίας Πληροφορικής & Υπολογιστών
Εργαστήριο
Λογισμικού
http://www.softlab.ntua.gr/
|
|
Εθνικό Μετσόβιο Πολυτεχνείο Εργαστήριο
Λογισμικού |
Αν ενδιαφέρεστε να εκπονήσετε διπλωματική εργασία σε ένα από τα παρακάτω θέματα ή σε άλλο θέμα της αρεσκείας σας στην ευρύτερη περιοχή της θεωρίας και υλοποίησης γλωσσών προγραμματισμού, επικοινωνήστε μαζί μου.
Νίκος Παπασπύρου, Λέκτορας Ε.Μ.Π.
E-mail:
Τηλ.: 210-772-3393, 210-772-2486
Το παρόν κείμενο είναι διαθέσιμο και σε εκτυπώσιμη μορφή (PDF, 208ΚΒ).
Στην εποχή της κοινωνίας της πληροφορίας και της γνώσης, το ζήτημα της αξιοπιστίας του εκτελέσιμου κώδικα έχει μεγάλη βαρύτητα. Οι προδιαγραφές των μελλοντικών συστημάτων λογισμικού θα πρέπει να εγγυώνται ιδιότητες ιδιαίτερης ευαισθησίας για τους χρήστες τους, όπως η ασφάλεια, η ακεραιότητα, η εμπιστευτικότητα, το απόρρητο των πληροφοριών, καθώς και ιδιότητες εξέχουσας σημασίας από την πλευρά της τεχνολογίας λογισμικού, όπως η μερική ορθότητα, ο τερματισμός, η χρονική και χωρική πολυπλοκότητα.
Οι υπάρχοντες μεταγλωττιστές που παράγουν πιστοποιημένο κώδικα, όπως π.χ. οι μεταγλωττιστές της Java και της πλατφόρμας .NET της Microsoft, επικεντρώνονται σε σχετικά απλές και όχι τυπικά ορισμένες ιδιότητες ασφάλειας των προγραμμάτων που αστυνομεύονται από ένα περίπλοκο σύστημα σε χρόνο εκτέλεσης (συνήθως μια νοητή μηχανή). Κατά τα άλλα, η ασφάλεια εκτέλεσης του κώδικα σήμερα στηρίζεται στην πιστοποίηση της ταυτότητας του κατασκευαστή του και απαιτεί συνήθως τη συνεργασία εξωτερικών πηγών που θεωρούνται έμπιστες.
Πρόσφατες ερευνητικές εργασίες ενισχύουν την άποψη ότι, αν και φιλόδοξο σχέδιο, είναι δυνατή η σχεδίαση και υλοποίηση ενός γενικού πλαισίου για τη ρητή αναπαράσταση πολύπλοκων προτάσεων και των αποδείξεών τους σε γλώσσες χαμηλού επιπέδου (ενδιάμεσες ή συμβολικές) με ισχυρά συστήματα τύπων. Σε μια τέτοια γλώσσα, ένα αρχείο πιστοποιημένου κώδικα (certified binary) είναι απλά ένα πρόγραμμα ο τύπος του οποίου παρέχει μια συλλογή από ιδιότητες που το πρόγραμμα ικανοποιεί. Ο ελεγκτής τύπων της γλώσσας μπορεί στατικά και σχετικά εύκολα να αποφαίνεται αν ένα αρχείο πιστοποιημένου κώδικα είναι συνεπές και, στην περίπτωση που είναι, μπορεί εν συνεχεία να εκτελεστεί χωρίς επιπλέον επιβάρυνση στην απόδοση.
Στο Εργαστηρίου Λογισμικού (βασισμένη σε συνεργασία με μέλη της ερευνητικής ομάδας FLINT του τμήματος Επιστήμης των Υπολογιστών του Πανεπιστημίου Yale) έχει αναπτυχθεί η NFlint, μια συναρτησιακή (functional) ενδιάμεση γλώσσα που υποστηρίζει τον προγραμματισμό με αποδείξεις. Η σύνταξη και η σημασιολογία της NFlint περιγράφεται με λεπτομέρεια σε εργασίες μελών του εργαστηρίου και η υλοποίησή της έχει τη μορφή ενός στατικού ελεγκτή τύπων (type checker) και ενός διερμηνέα (interpreter).
Σχετική ύλη προς ανάγνωση: nflint.zip (603KB), lambda.zip (524KB), pcc.zip (1.651KB)
Η εργασία αυτή αποσκοπεί αφενός στη σχεδίαση μιας αρχικής γλώσσας υψηλού επιπέδου που να υποστηρίζει τον προγραμματισμό με αποδείξεις, αφετέρου στην υλοποίηση ενός μεταγλωττιστή για αυτήν που να παράγει πιστοποιημένο κώδικα στη γλώσσα NFlint. Στην αρχική γλώσσα θα πρέπει να μπορούν να διατυπωθούν ενδιαφέρουσες ιδιότητες των προγραμμάτων, η απόδειξη των οποίων θα καθοδηγείται από τον προγραμματιστή με την ενσωμάτωση υποδείξεων (proof hints) ως επισημειώσεων (annotations) μέσα στα προγράμματα. Οι παρεμβάσεις του προγραμματιστή όμως θα πρέπει να περιορίζονται στο ελάχιστο δυνατό. Η εργασία αυτή μπορεί να βασιστεί σε προηγούμενη σχετική διπλωματική εργασία και, στην περίπτωση αυτή, να ασχοληθεί με τον εμπλουτισμό της αντίστοιχης γλώσσας.
Σχετική ύλη προς ανάγνωση: διπλωματική εργασία Α. Σταμπούλη (659KB)
Η εργασία αυτή αποσκοπεί στη σχεδίαση και υλοποίηση μιας νοητής μηχανής (virtual machine) που να υλοποιεί τη γλώσσα NFlint, ώστε να είναι δυνατή η μεταφορά πιστοποιημένου κώδικα μέσω του διαδικτύου και η εκτέλεσή του μέσα σε έναν περιηγητή (web browser). Η νοητή μηχανή θα λειτουργεί κατά το πρότυπο των αντιστοίχων μηχανών της Java ή της πλατφόρμας Microsoft .NET και μπορεί να βασιστεί σε μια προσαρμογή της υπάρχουσας υλοποίησης της NFlint. Η σχεδίαση θα συμπεριλαμβάνει μια κατάλληλη μορφή αναπαράστασης των προγραμμάτων της ενδιάμεσης γλώσσας με δυαδικά αρχεία (binary format) που να ελαχιστοποιεί το μέγεθός τους και να διευκολύνει τον έλεγχο των αποδείξεων. Η υλοποίηση θα γίνει με τη μορφή ενός πρόσθετου τμήματος (plugin) σε κάποιον περιηγητή.
Η εργασία αυτή αποσκοπεί στην οργάνωση ενός συνόλου θεωριών χρήσιμων για την απόδειξη ιδιοτήτων των προγραμμάτων και στην κωδικοποίησή τους στη γλώσσα NFlint. Οι θεωρίες αυτές θα βασίζονται στη βιβλιοθήκη του εργαλείου υποστήριξης αποδείξεων Coq και θα συμπεριλαμβάνουν την αριθμητική των φυσικών και ακέραιων αριθμών, την άλγεβρα Boole, τον προτασιακό και τον κατηγορηματικό λογισμό.
Σχετική ύλη προς ανάγνωση: βιβλιοθήκη θεωριών του Coq
Οι γλώσσες που υποστηρίζουν προγραμματισμό με αποδείξεις συνήθως ακολουθούν το συναρτησιακό μοντέλο προγραμματισμού. Σε αυτές τις γλώσσες η υποστήριξη του κλασσικού προστακτικού μοντέλου προγραμματισμού, που χρησιμοποιεί μεταβλητές και ανάθεση, δεν είναι προφανής. Ιδιαίτερα όμως δύσκολη στο πλαίσιο του προγραμματισμού με αποδείξεις είναι η απόδειξη ιδιοτήτων των προγραμμάτων που χρησιμοποιούν προστακτικά χαρακτηριστικά.
Για το σκοπό αυτό, στο Εργαστήριο Λογισμικού έχει σχεδιαστεί η LinFlint, μια επέκταση της γλώσσας NFlint με γραμμικό σύστημα τύπων (linear type system). Η εργασία αυτή αποσκοπεί στην υλοποίηση ενός ελεγκτή τύπων και ενός διερμηνέα για τη γλώσσα LinFlint.
Σχετική ύλη προς ανάγνωση: linrgn.zip (680KB), διπλωματική εργασία Χ. Δημουλά (647KB)
Ιδιαίτερα ενδιαφέρουσες ιδιότητες του εκτελέσιμου κώδικα είναι ο τερματισμός (κατά πόσον δηλαδή η εκτέλεση του κώδικα τερματίζει για δοθείσα είσοδο) και η χρονική και χωρική πολυπλοκότητα (δηλαδή για πόσο χρόνο διαρκεί η εκτέλεση και πόσο χώρο χρειάζεται στη μνήμη, ως συνάρτηση του μεγέθους της εισόδου). Οι ιδιότητες αυτές συνήθως μελετώνται στο χαρτί σε μεταθεωρητικό επίπεδο, όμως στο πλαίσιο του προγραμματισμού με αποδείξεις είναι δυνατή η διατύπωση και η απόδειξή τους μέσω του συστήματος τύπων της γλώσσας προγραμματισμού.
Η εργασία αυτή αποσκοπεί αφενός στη βιβλιογραφική μελέτη και στην καταγραφή των ερευνητικών προσπαθειών που έχουν προταθεί, αφετέρου στη διερεύνηση της δυνατότητας προσαρμογής αυτών των προσπαθειών στη γλώσσα NFlint.
Σχετική ύλη προς ανάγνωση: termcmpl.zip (1.682KB)
Οι κβαντικοί υπολογισμοί (quantum computing) έγιναν σχετικά πρόσφατα αντικείμενο ερευνητικής μελέτης. Από το 1982, όταν οι Benio και Feynman απέδειξαν ότι ένα κβαντομηχανικό σύστημα μπορεί να χρησιμοποιηθεί για τη διενέργεια υπολογισμών, η ανακάλυψη αποδοτικών κβαντικών αλγορίθμων έστρεψε την προσοχή πολλών ερευνητών σε αυτή την περιοχή. Το γνωστότερο ίσως παράδειγμα είναι ο (πιθανοτικός) κβαντικός αλγόριθμος του Shor για την παραγοντοποίηση αριθμών σε πολυωνυμικό χρόνο: δεν υπάρχει κλασσικός (πιθανοτικός) αλγόριθμος που να επιλύει το ίδιο πρόβλημα σε πολυωνυμικό χρόνο. Σήμερα, παρά την έλλειψη κβαντικών υπολογιστών, υπάρχει έντονο ενδιαφέρον για τον ορισμό και τη μελέτη γλωσσών προγραμματισμού που υποστηρίζουν κβαντικούς υπολογισμούς.
Στο Εργαστήριο Λογισμικού έχει αναπτυχθεί η γλώσσα nQML, μια γλώσσα κβαντικού προγραμματισμού βασισμένη στην QML των Altenkirch και Grattage. Η nQML έχει υλοποιηθεί με τη μορφή ενός προσομοιωτή του κβαντικού υπολογιστικού μοντέλου σε κλασσικό υπολογιστή, βασισμένου στη δηλωτική σημασιολογία (denotational semantics) της γλώσσας πάνω σε πίνακες πυκνότητας (density matrices).
Σχετική ύλη προς ανάγνωση: quantum.zip (1.844KB), διπλωματική εργασία Μ. Λαμπή (428KB)
Η εργασία αυτή αποσκοπεί στην υλοποίηση του αλγορίθμου του Shor στη γλώσσα nQML. Επιμέρους στόχοι είναι η κατανόηση του κβαντικού μοντέλου προγραμματισμού, η βιβλιογραφική μελέτη του προβλήματος της παραγοντοποίησης αριθμών και των μεθόδων που έχουν προταθεί για τη λύση του, καθώς και η κατανόηση και αναλυτική παρουσίαση του αλγορίθμου του Shor.
Σχετική ύλη προς ανάγνωση: Shor's algorithm (wikipedia)
Η εργασία αυτή αποσκοπεί στην υλοποίηση της γλώσσας nQML με απεικόνιση σε κβαντικά κυκλώματα, κατ' αντιστοιχία της υλοποίησης της QML των Altenkirch και Grattage. Επιμέρους στόχοι είναι η κατανόηση του κβαντικού μοντέλου προγραμματισμού και των κβαντικών κυκλωμάτων, ο φορμαλισμός των κβαντικών κυκλωμάτων, η μετάφραση των προγραμμάτων της nQML σε κβαντικά κυκλώματα και η υλοποίηση αυτών με προσομοίωση σε κλασσικό υπολογιστή (που μπορεί να βασιστεί σε υπάρχουσα υλοποίηση του Grattage).
Σχετική υλοποίηση: μεταγλωττιστής QML του Jonathan Grattage, και παλαιότερη έκδοση
Η μηχανική απόδειξη θεωρημάτων (mechanized theorem proving) ασχολείται με τη διατύπωση και απόδειξη θεωρημάτων με τυπικό τρόπο και με την υποστήριξη ειδικών εργαλείων λογισμικού (proof assistants). Η χρήση της λέξης «μηχανική» αντί της λέξης «αυτόματη» δεν είναι τυχαία: τα εργαλεία αυτά συνήθως υποστηρίζουν την αυτόματη απόδειξη θεωρημάτων, αν φυσικά αυτή είναι δυνατή (το πρόβλημα της απόδειξης θεωρημάτων σε οποιαδήποτε μη τετριμμένη λογική είναι μη αποκρίσιμο). Στις περιπτώσεις που δεν είναι, τα εργαλεία υποστηρίζουν ημι-αυτόματη ή και πλήρως χειροκίνητη απόδειξη, με την καθοδήγηση του χρήστη.
Στο Εργαστήριο Λογισμικού έχουν εγκατασταθεί και χρησιμοποιούνται τρία τέτοια εργαλεία:
Ως περιοχή εφαρμογών, η ερευνητική ομάδα του Εργαστηρίου Λογισμικού ενδιαφέρεται για την απόδειξη της μεταθεωρίας (metatheory) γλωσσών προγραμματισμού (π.χ. ασφάλεια τύπων). Τα εργαλεία όμως αυτά μπορούν να χρησιμοποιηθούν και για τελείως διαφορετικές περιοχές εφαρμογών (π.χ. μαθηματικά, θεωρητική πληροφορική, λειτουργικά συστήματα, ασφάλεια πρωτοκόλλων, model checking, κ.λπ.).
Στα παρακάτω θέματα εργασιών, σκοπός δεν είναι η εύρεση της απόδειξης κάποιου θεωρήματος, η οποία θεωρείται δεδομένη. Σκοπός είναι η διατύπωση του θεωρήματος και της απόδειξής του σε κάποιο proof assistant. Η κατάλογος θεμάτων που ακολουθεί είναι ενδεικτικός αλλά όχι περιοριστικός.
Σχετική ύλη προς ανάγνωση: coq.zip (860KB), isabelle.zip (2.790KB), twelf.zip (1.544KB)
Αντικείμενο αυτής της εργασίας είναι η μηχανική απόδειξη της ασφάλειας τύπων (type safety) του λ-λογισμού με απλούς τύπους και αναφορές (references). Η ασφάλεια τύπων σημαίνει ότι, αν ένα πρόγραμμα περνά από τον ελεγκτή τύπων, τότε δεν μπορεί να προκαλέσει σφάλμα κατά την εκτέλεσή του. Σε γλώσσες που ορίζονται με λειτουργική σημασιολογία (operational semantics), η ασφάλεια τύπων αποδεικνύεται συνήθως με δύο θεωρήματα: το θεώρημα προόδου (progress) και το θεώρημα διατήρησης (preservation).
|
Σχετική ύλη προς ανάγνωση: κεφ. 13 του βιβλίου του B. Pierce (109KB) |
Ο νοηματικός προγραμματισμός (intensional programming) είναι ένα εναλλακτικό μοντέλο προγραμματισμού που υποστηρίζει πολυδιάστατες τιμές μεταβλητών και εκφράσεων. Δηλαδή, οι μεταβλητές και οι εκφράσεις δεν έχουν μία μοναδική τιμή, αλλά μία τιμή σε κάθε σημείο ενός διακριτού χώρου διαστάσεων. Πρόσφατες ερευνητικές εργασίες δείχνουν ότι ένα συναρτησιακό πρόγραμμα υψηλής τάξης μπορεί να μετασχηματιστεί σε ένα ισοδύναμο νοηματικό πρόγραμμα μηδενικής τάξης (δηλαδή χωρίς συναρτήσεις), το οποίο στη συνέχεια μπορεί να υλοποιηθεί με τεχνικές εντελώς διαφορετικές από αυτές που χρησιμοποιούνται παραδοσιακά από τους μεταγλωττιστές των συναρτησιακών γλωσσών. Ο μετασχηματισμός αυτός ονομάζεται μετασχηματισμός διακλαδιζόμενων διαστάσεων (branching dimensions transformation). Σκοπός αυτής της εργασίας είναι η μηχανική απόδειξη της ορθότητας του μετασχηματισμού διακλαδιζόμενων διαστάσεων.
|
Σχετική ύλη προς ανάγνωση: εργασία Π. Ροντογιάννη (350KB) |
Ο αλγόριθμος του Dijkstra είναι ένας άπληστος (greedy) αλγόριθμος που λύνει το πρόβλημα της εύρεσης ελαχίστων μονοπατιών από συγκεκριμένη κορυφή (αφετηρία) σε κατευθυνόμενους γράφους με μη αρνητικά βάρη ακμών. Σκοπός αυτής της εργασίας είναι η διατύπωση και μελέτη του αλγορίθμου με τη βοήθεια ενός proof assistant, που θα περιλαμβάνει τις αποδείξεις τερματισμού και ορθότητας και (προαιρετικά) την απόδειξη πολυπλοκότητας.
Σχετική ύλη προς ανάγνωση: Dijkstra's algorithm (wikipedia)
Οι παραμετρικές γραμματικές χωρίς συμφραζόμενα (parametric context-free grammars, PCFG) είναι μια απλή και φυσική επέκταση των κοινών γραμματικών χωρίς συμφραζόμενα (CFG), στην οποία τα μη τερματικά σύμβολα φέρουν έναν αριθμό παραμέτρων. Ο φορμαλισμός PCFG συνδυάζει την απλότητα των CFG με την εκφραστική ικανότητα που συναντάται σε αρκετά πιο πολύπλοκα τυπικά μοντέλα. Αποδεικνύεται ότι οι PCFG είναι περισσότερο εκφραστικές από τις CFG και μπορούν να χρησιμοποιηθούν για την περιγραφή γλωσσών με εξάρτηση από τα συμφραζόμενα. Βρίσκουν εφαρμογές στην περιγραφή της σύνταξης γλωσσών προγραμματισμού, γλωσσών διαπροσωπείας χρήστη και φυσικών γλωσσών.
Σκοπός αυτής της εργασίας είναι η περαιτέρω διερεύνηση των PCFG με στόχο αφενός τη μελέτη της κατασκευής αποδοτικών συντακτικών αναλυτών για PCFG, αφετέρου την αξιολόγηση των PCFG για ένα τουλάχιστον από τα προαναφερθέντα πεδία εφαρμογών, μέσω κατάλληλων παραδειγμάτων.
Σχετική ύλη προς ανάγνωση: pbnf.pdf (241KB)
Ο έλεγχος με τη μέθοδο του μαύρου κουτιού (black box testing) είναι αδιαμφισβήτητα χρήσιμος στην ανάπτυξη συστημάτων λογισμικού, η εφαρμογή του όμως στην πράξη είναι δύσκολο έργο. Λίγες συμπαγείς μέθοδοι έχουν προταθεί για αυτό το σκοπό, οι περισσότερες από τις οποίες βασίζονται στις αρχές της ισοδύναμης διαμέρισης (equivalence partitioning) και της ανάλυσης οριακών τιμών (boundary value analysis). Η μέθοδος Poirot2 είναι μια τέτοια μέθοδος που βασίζεται στη συνθήκη εγκυρότητας για τα δεδομένα εισόδου και στη συνθήκη ισοδύναμης ταξινόμησης που προκύπτει από τις προδιαγραφές των δεδομένων εξόδου. Τα βήματα της διαδικασίας, που τελικά ορίζει τις απαιτούμενες περιπτώσεις ελέγχου, απαιτούν τη συμβολική επεξεργασία τύπων που παριστάνουν τις παραπάνω συνθήκες, εκφρασμένων σε μια κατάλληλη τυπική λογική.
Αυτή η εργασία αποσκοπεί στη σχεδίαση και υλοποίηση ενός εργαλείου που να υποστηρίζει τη μέθοδο Poirot2 για την κατασκευή περιπτώσεων ελέγχου βασισμένων στην τυπική λογική.
Σχετική ύλη προς ανάγνωση: poirot2.zip (2.082ΚΒ)
Happiness is not a state to arrive at, but a manner of travelling.
-- Margaret Lee Runbeck.
Τελευταία ενημέρωση: October 31, 2006 3:35