Απόδειξη Ορθότητας Μίας Υλοποίησης Του Αλγορίθμου Των Ford-fulkerson Για Την Εύρεση Της Ελάχιστης Τομής Γράφου Χωρίς Βάρη

Abstract

Σκοπός της εργασίας αυτής είναι η τυπική επαλήθευση της λύσης ενός προβλήματος παρόμοιου με τα προβλημάτα που εξετάζονται στην Ολυμπιάδα Πληροφορικής. Η τυπική επαλήθευση ενός προγράμματος αποτελεί τη διαδικασία απόδειξης ορθότητας του προγράμματος με βάση κάποια τυπικήπροδιαγραφή ή ιδιότητα, χρησιμοποιώντας ως εργαλεία τυπικές μεθόδους και μαθηματική λογική.Στην περίπτωσή μας υλοποιήσαμε μία λύση για το πρόβλημα με τίτλο damage2, που ήταν ένα από τα θέματα του διαγωνισμού πληροφορικής του Μαρτίου 2009 της USACO. Το πρόβλημα αυτόανάγεται εύκολα στο γνωστό από τη θεωρία γράφων πρόβλημα της εύρεσης ελάχιστης τομής (min cut) γράφου χωρίς βάρη, για τη λύση του οποίου μπορεί να χρησιμοποιηθεί ο αλγόριθμος των Ford-Fulkerson, Στη συνέχεια αποδείξαμε την ορθότητα της υλοποίησης αυτού του αλγορίθμου σε γλώσσαC, χρησιμοποιώντας τα εργαλεία Caduceus και Coq.