Αναφορές Και Ανάθεση Στον Προγραμματισμό Με Αποδείξεις

Abstract

Σκοπός της εργασίας είναι η μελέτη της δυνατότηταςεισαγωγής αναφορών (references) και ανάθεσης(destructive update) στο μοντέλο του προγραμματισμού μεαποδείξεις. Η ανάγκη για την παραγωγή αξιόπιστου και πιστοποιημένου κώδικα είναι ακόμαμεγαλύτερη σήμερα από το παρελθόν. Σε πολλές περιπτώσεις, ζητήματαασφάλειας και συμβατότητας λογισμικού έθεσαν σε κίνδυνο τη λειτουργίαμεγάλων συστημάτων. Τα τελευταία χρόνια η επικρατέστερη μέθοδος παραγωγήςπιστοποιημένου κώδικα είναι η χρήση γλωσσών με ισχυρά συστήματα τύπων πουενσωματώνουν διάφορα συστήματα λογικής, μέσω των οποίων εκφράζονται καιαποδεικνύονται ιδιότητες που πρέπει να πληρεί το λογισμικό ώστε να είναιασφαλές. Οι προσπάθειες για τον ορισμό γλωσσώνπρογραμματισμού με ισχυρά συστήματα τύπων που υποστηρίζουν αποδείξεις επικεντρώθηκαν σε γλώσσες με αμιγώςσυναρτησιακά χαρακτηριστικά. Οι συναρτησιακές, όμως, γλώσσες δενυποστηρίζουν λειτουργίες όπως η ανάθεση ή οντότητες όπως οι αναφορές. Ταπροστακτικά αυτά στοιχεία είναι πολύ χρήσιμα εργαλεία για τονπρογραμματιστή γιατί του δίνουν τη δυνατότητα της άμεσης διαμόρφωσης τηςμνήμης και τη δυνατότητα της ροής των δεδομένων ανάμεσα στα διάφορα τμήματαενός προγράμματος μέσω της μνήμης.Η εισαγωγή τέτοιων χαρακτηριστικών σε συναρτησιακές γλώσσες δεν είναιυλοποιήσιμη με τετριμμένο τρόπο. Τα παραδοσιακά συστήματα δεν μπορούννα δώσουν πληροφορίες για τα περιεχόμενα της μνήμης και δεν μπορούν ναπροσφέρουν μία βάση πάνω στην οποία να διατυπωθούν και να αποδειχθούνλογικές προτάσεις που να περιγράφουν ιδιότητες της μνήμης.Τα linear συστήματα τύπων προσφέρουν μια βάση που επιτρέπει την καταγραφήπληροφοριών για την κατάσταση της μνήμης και τις μεταβολές της. Τίθενται, λοιπόν, τα θεμέλια για να περιγραφούν με λογικέςπροτάσεις οι ιδιότητες της μνήμης μέσα από το σύστημα τύπων μία γλώσσαςπρογραμματισμού. Στο πλαίσιο της παρούσας εργασίας, κατ' αρχήν σχεδιάστηκε, ορίστηκε η σημασιολογία και διατυπώθηκε η μεταθεωρία για μία γλώσσα προγραμματισμού, το σύστημα τύπων της οποίας υποστηρίζει linear και unrestrictedτύπους και ελεγχόμενη μετατροπή μεταξύ αυτών. Στη συνέχειασχεδιάστηκε ένα σύστημα προγραμματισμού με αποδείξεις πουυποστηρίζει αναφορές και ανάθεση, το σύστημα τύπων του οποίουβασίζεται σε μία παραλλαγή της προηγούμενης γλώσσας.