Please use this identifier to cite or link to this item:
http://artemis.cslab.ece.ntua.gr:8080/jspui/handle/123456789/15431
Title: | Μηχανική Επαλήθευση Προστακτικών Προγραμμάτων |
Authors: | Βασίλειος Παπαβασιλείου Παπασπύρου Νικόλαος |
Keywords: | αξιωματική σημασιολογία λογική hoare επαλήθευση προγραμμάτων μερική ορθότητα coq |
Issue Date: | 21-Jul-2009 |
Abstract: | Σκοπός της διπλωματικής είναι ο ορισμός μιας γλώσσας προγραμματισμού που επιτρέπει την επαλήθευση προγραμμάτων και η υλοποίηση ενός εργαλείου επαλήθευσης. Το σύστημα επαλήθευσης βασίζεται στο εργαλείο υποστήριξης αποδείξεων (proof assistant) Coq.Τα προγράμματα που δέχεται ως είσοδο το σύστημά μας είναι γραμμένα σε μια απλή γλώσσα προστακτικού προγραμματισμού, την Tony. Λόγω του προστακτικού της ύφους η Tony είναι οικεία στους περισσότερους προγραμματιστές, παρέχει όμως και χαρακτηριστικά αναγκαία για την επαλήθευση προγραμμάτων. Οι προδιαγραφές που πρέπει να ικανοποιούν τα προγράμματα ορίζονται με τη μορφή προσυνθηκών (preconditions) και μετασυνθηκών (postconditions), τις οποίες ο προγραμματιστής συμπεριλαμβάνει στο πρόγραμμα ως επισημειώσεις (annotations). Στόχος ήταν να παρέχουμε μια εκφραστική γλώσσα για τη διατύπωση των συνθηκών αυτών. Επιλέξαμε ως εκ τούτου να γράφονται απ' ευθείας στη γλώσσα προδιαγραφών του Coq (Gallina). Ο κώδικας των προγραμμάτων περιλαμβάνει και άλλα στοιχεία που μπορούν να βοηθήσουν στη διαδικασία απόδειξης της ορθότητας, όπως θεωρήματα και ορισμούς που θα χρειαστούν και αναλλοίωτες βρόχου (loop invariants).Το εργαλείο επαλήθευσης διαβάζει ένα πρόγραμμα σε Tony και παράγει ένα θεώρημα του Coq, το οποίο αποτελεί διατύπωση της μερικής ορθότητας κατά Hoare. Στη συνέχεια εφαρμόζει αυτοματοποιημένες τακτικές για να κατασκευάσει μια απόδειξη του εν λόγω θεωρήματος. Σε περίπτωση που αποτύχει, ενημερώνει τον προγραμματιστή ποια θεωρήματα πρέπει να αποδείξει για να ολοκληρωθεί η διαδικασία επαλήθευσης, με τη μορφή ενός προτύπου (template) με κώδικα Coq που πρέπει να συμπληρωθεί. |
URI: | http://artemis-new.cslab.ece.ntua.gr:8080/jspui/handle/123456789/15431 |
Appears in Collections: | Διπλωματικές Εργασίες - Theses |
Files in This Item:
File | Size | Format | |
---|---|---|---|
DT2009-0168.pdf | 375.2 kB | Adobe PDF | View/Open |
Items in Artemis are protected by copyright, with all rights reserved, unless otherwise indicated.