Μηχανική Επαλήθευση Προστακτικών Προγραμμάτων

Abstract

Σκοπός της διπλωματικής είναι ο ορισμός μιας γλώσσας προγραμματισμού που επιτρέπει την επαλήθευση προγραμμάτων και η υλοποίηση ενός εργαλείου επαλήθευσης. Το σύστημα επαλήθευσης βασίζεται στο εργαλείο υποστήριξης αποδείξεων (proof assistant) Coq.Τα προγράμματα που δέχεται ως είσοδο το σύστημά μας είναι γραμμένα σε μια απλή γλώσσα προστακτικού προγραμματισμού, την Tony. Λόγω του προστακτικού της ύφους η Tony είναι οικεία στους περισσότερους προγραμματιστές, παρέχει όμως και χαρακτηριστικά αναγκαία για την επαλήθευση προγραμμάτων. Οι προδιαγραφές που πρέπει να ικανοποιούν τα προγράμματα ορίζονται με τη μορφή προσυνθηκών (preconditions) και μετασυνθηκών (postconditions), τις οποίες ο προγραμματιστής συμπεριλαμβάνει στο πρόγραμμα ως επισημειώσεις (annotations). Στόχος ήταν να παρέχουμε μια εκφραστική γλώσσα για τη διατύπωση των συνθηκών αυτών. Επιλέξαμε ως εκ τούτου να γράφονται απ' ευθείας στη γλώσσα προδιαγραφών του Coq (Gallina). Ο κώδικας των προγραμμάτων περιλαμβάνει και άλλα στοιχεία που μπορούν να βοηθήσουν στη διαδικασία απόδειξης της ορθότητας, όπως θεωρήματα και ορισμούς που θα χρειαστούν και αναλλοίωτες βρόχου (loop invariants).Το εργαλείο επαλήθευσης διαβάζει ένα πρόγραμμα σε Tony και παράγει ένα θεώρημα του Coq, το οποίο αποτελεί διατύπωση της μερικής ορθότητας κατά Hoare. Στη συνέχεια εφαρμόζει αυτοματοποιημένες τακτικές για να κατασκευάσει μια απόδειξη του εν λόγω θεωρήματος. Σε περίπτωση που αποτύχει, ενημερώνει τον προγραμματιστή ποια θεωρήματα πρέπει να αποδείξει για να ολοκληρωθεί η διαδικασία επαλήθευσης, με τη μορφή ενός προτύπου (template) με κώδικα Coq που πρέπει να συμπληρωθεί.