Παρακαλώ χρησιμοποιήστε αυτό το αναγνωριστικό για να παραπέμψετε ή να δημιουργήσετε σύνδεσμο προς αυτό το τεκμήριο:
http://artemis.cslab.ece.ntua.gr:8080/jspui/handle/123456789/15470
Τίτλος: | Απόδειξη Ορθότητας Μίας Υλοποίησης Του Αλγορίθμου Των Ford-fulkerson Για Την Εύρεση Της Ελάχιστης Τομής Γράφου Χωρίς Βάρη |
Συγγραφείς: | Μιχαήλ Γιακκούπης Παπασπύρου Νικόλαος |
Λέξεις κλειδιά: | αλγόριθμος ford-fulkerson πρόβλημα μέγιστης ροής/ ελάχιστης τομής απόδειξη ορθότητας πρόβλημα damage2 από usaco coq. |
Ημερομηνία έκδοσης: | 23-Ιου-2009 |
Περίληψη: | Σκοπός της εργασίας αυτής είναι η τυπική επαλήθευση της λύσης ενός προβλήματος παρόμοιου με τα προβλημάτα που εξετάζονται στην Ολυμπιάδα Πληροφορικής. Η τυπική επαλήθευση ενός προγράμματος αποτελεί τη διαδικασία απόδειξης ορθότητας του προγράμματος με βάση κάποια τυπικήπροδιαγραφή ή ιδιότητα, χρησιμοποιώντας ως εργαλεία τυπικές μεθόδους και μαθηματική λογική.Στην περίπτωσή μας υλοποιήσαμε μία λύση για το πρόβλημα με τίτλο damage2, που ήταν ένα από τα θέματα του διαγωνισμού πληροφορικής του Μαρτίου 2009 της USACO. Το πρόβλημα αυτόανάγεται εύκολα στο γνωστό από τη θεωρία γράφων πρόβλημα της εύρεσης ελάχιστης τομής (min cut) γράφου χωρίς βάρη, για τη λύση του οποίου μπορεί να χρησιμοποιηθεί ο αλγόριθμος των Ford-Fulkerson, Στη συνέχεια αποδείξαμε την ορθότητα της υλοποίησης αυτού του αλγορίθμου σε γλώσσαC, χρησιμοποιώντας τα εργαλεία Caduceus και Coq. |
URI: | http://artemis-new.cslab.ece.ntua.gr:8080/jspui/handle/123456789/15470 |
Εμφανίζεται στις συλλογές: | Διπλωματικές Εργασίες - Theses |
Αρχεία σε αυτό το τεκμήριο:
Αρχείο | Μέγεθος | Μορφότυπος | |
---|---|---|---|
DT2009-0207.pdf | 1.46 MB | Adobe PDF | Εμφάνιση/Άνοιγμα |
Όλα τα τεκμήρια του δικτυακού τόπου προστατεύονται από πνευματικά δικαιώματα.