Please use this identifier to cite or link to this item: http://artemis.cslab.ece.ntua.gr:8080/jspui/handle/123456789/14849
Title: Αναδρομικοί Τύποι Στον Προγραμματισμό Με Αποδείξεις
Authors: Χρήστος Στεργίου
Παπασπύρου Νικόλαος
Keywords: συστήματα τύπων
αναδρομικοί τύποι
αλγεβρικοί τύποι δεδομένων
λογισμός των επαγωγικών κατασκευών
προγραμματισμός με αποδείξεις
ασφάλεια εκτελέσιμου κώδικα
Issue Date: 27-Jul-2007
Abstract: Σκοπός της εργασίας είναι η μελέτη των αναδρομικών τύπων στο λάμβδα λογισμό και η εισαγωγή τους στο μοντέλο του προγραμματισμού με αποδείξεις.Μία από τις μεγαλύτερες προκλήσεις στην ανάπτυξη συστημάτων λογισμικού σήμερα είναι η πιστοποίηση της ασφάλειας των διαφορετικών ψηφίδων. Το πρόβλημα εντείνεται από την όλο και μεγαλύτερη ανάγκη χρήσης στοιχείων λογισμικού των οποίων η προέλευση είναι άγνωστη ή εκ των πραγμάτων μη έμπιστη όπως στην περίπτωση χρήσης απομακρυσμένου κώδικα ή επεκτάσεων σε πυρήνες λειτουργικών και συστημάτων βάσεων δεδομένων από χρήστες. Τα τελευταία χρόνια η επικρατέστερη μέθοδος παραγωγής πιστοποιημένου κώδικα είναι η χρήση πλαισίων που ενσωματώνουν διάφορα συστήματα λογικής, μέσω των οποίων εκφράζονται και αποδεικνύονται ιδιότητες που πρέπει να πληρεί το λογισμικό ώστε να είναιασφαλές.Τα συστήματα που έχουν προταθεί για την ανάπτυξη κώδικα με αποδείξεις είναι ενδιάμεσου επιπέδου οπότε ηδιαδικασία προγραμματισμού σε αυτά είναι ιδιαίτερα πολύπλοκη. Οι γλώσσες υψηλού επιπέδου που παράγουν κώδικα για χαμηλού επιπέδου συστήματα προγραμματισμού με αποδείξεις ενώ είναι ιδιαίτερα εκφραστικές, παραμένουν δύσκολες στον προγραμματισμό. Επομένως, η σχεδίαση μίας απλούστερης γλώσσας υψηλού επιπέδου, που θα διευκολύνει το χρήστη της τόσο στην κατασκευή των αποδείξεων αλλά και παρέχοντας δυνατοτήτα ορισμού ενδιαφέροντων δομών δεδομένων, προς την επίτευξη της οποίας κινείται η παρούσα εργασία, θα επέτρεπε ευρύτερη εξάπλωση του συγκεκριμένου ιδιώματος προγραμματισμού.Πιστεύουμε ότι η υλοποίηση αναδρομικών τύπων σε ένα σύστημα προγραμματισμού με αποδείξεις θα βοηθήσει στην παραγωγή πιο φιλικών προς το χρήστη γλωσσών προγραμματισμού ανώτερου επιπέδου. Για παράδειγμα παρέχουν άμεσα τη δυνατότητα χρήσης αλγεβρικών τύπων δεδομένων, δηλαδή μιας τεχνικής ορισμού ενδιαφέροντων και πολύ χρήσιμων δομών δεδομένων.
URI: http://artemis-new.cslab.ece.ntua.gr:8080/jspui/handle/123456789/14849
Appears in Collections:Διπλωματικές Εργασίες - Theses

Files in This Item:
File SizeFormat 
DT2007-0090.pdf685.44 kBAdobe PDFView/Open


Items in Artemis are protected by copyright, with all rights reserved, unless otherwise indicated.