Αγκαλιάζοντας τη δύναμη των τυπικών μεθόδων στο Ταξίδι κωδικοποίησης μου: Πώς έγινα Dafny Evangelist

blog 1ΕιδήσειςΑναπτυσσόμενοιΕξέτασηΕπεξήγηση BlockchainΕκδηλώσεις και ΣυνέδριαΠατήστεΕνημερωτικά δελτία

Εγγραφείτε στο newsletter μας.

Διεύθυνση ηλεκτρονικού ταχυδρομείου

Σεβόμαστε το απόρρητό σας

HomeBlogΠρογραμματιστές

Αγκαλιάζοντας τη δύναμη των τυπικών μεθόδων στο Ταξίδι κωδικοποίησης μου: Πώς έγινα Dafny Evangelist

από ConsenSys 22 Δεκεμβρίου 2020 Δημοσιεύτηκε στις 22 Δεκεμβρίου 2020

Στιγμιότυπο 2020 12 15 στις 6 46 32 μ.μ. 1


Από τη Joanne Fuller

Θέλω να ξεκινήσω λέγοντας ότι γράφω αυτήν την ανάρτηση ιστολογίου με την ελπίδα ότι άλλοι θα βιώσουν τη στιγμή των Θεοφάνων που είχα κατά τη μάθηση Ντάφνι ως μέρος της εξερεύνησής μου στο τυπικές μεθόδους. Επιπλέον, ελπίζω ότι αυτή η ανάρτηση θα λειτουργήσει ως καταλύτης για τους άλλους να θεωρήσουν τις επίσημες μεθόδους ως μια κρίσιμη και απαραίτητη ικανότητα στο οπλοστάσιο όσων γράφουν κώδικα. Ως μέρος του Ομάδα αυτόματης επαλήθευσης εντός R&D στο ConsenSys, Χρησιμοποιώ το Dafny στην επίσημη επαλήθευση των προδιαγραφών Ethereum 2 Phase 0 και θέλω να μοιραστώ γιατί το βρίσκω χρήσιμο.

Το φόντο μου

Πρέπει να καταστήσω σαφές ότι δεν είμαι προγραμματιστής λογισμικού, αλλά μάλλον θεωρώ τον εαυτό μου μαθηματικό προγραμματιστή με κάποια γνώση της ανάπτυξης λογισμικού. Πρώτα έμαθα να γράφω προγράμματα ως μέρος της τάξης των μαθηματικών κατά τη διάρκεια του τελευταίου έτους του γυμνασίου και μάλλον θα έπρεπε να αναφέρω ότι παρόλο που μου άρεσε πολύ να χρησιμοποιώ υπολογιστές εκείνη την εποχή, η προοπτική της μάθησης πώς να προγραμματίζω με φοβόταν στο σημείο που σχεδόν έριξε τη συγκεκριμένη τάξη μαθηματικών. Αφού αποφάσισα να αντιμετωπίσω τον φόβο της αποτυχίας μου (σε σχέση με την εκμάθηση του προγράμματος και την πιθανή καταστροφή του αποτελέσματός μου σε αυτήν την τάξη), συνέχισα να βιώνω την πρώτη μου επιφατική στιγμή στο πλαίσιο του προγραμματισμού. Μπορώ ακόμα να θυμηθώ ότι κάθομαι στην τάξη και έχοντας συνειδητοποιήσει ότι η σύνταξη ενός προγράμματος για την επίλυση ενός μαθηματικού προβλήματος δεν ήταν κάποια μαγική και μυστηριώδης διαδικασία, ήταν σχεδόν σαν να γράφω πώς θα έκανα ένα πρόβλημα στο μυαλό μου. Δεν υπήρχε καμία αναδρομή μετά από αυτό! 

Ο προγραμματισμός ήταν μια σημαντική πτυχή όλων όσων έχω κάνει από τότε. Το διδακτορικό μου στην κρυπτογραφία βασίστηκε σε μεγάλο βαθμό στην ικανότητα ανάπτυξης αλγορίθμων και στη συνέχεια στον προγραμματισμό βέλτιστων εφαρμογών. Τα προγράμματά μου γράφτηκαν για πειραματισμό και, παρόλο που δεν ανέλαβα αυτό που θα λέγαμε τώρα ως επίσημη δοκιμή, θα έλεγχα ανεπίσημα τα όρια και θα δοκιμάσω περιπτώσεις χρησιμοποιώντας λογική συλλογιστική σχετικά με την επιδιωκόμενη έξοδο. Εργάστηκα επίσης για πολλά χρόνια ως ακαδημαϊκή επιχείρηση έρευνας στον τομέα των οικονομικών και των οικονομικών. Και πάλι αυτό περιλάμβανε προγράμματα γραφής, και πάλι χρησιμοποίησα τις δικές μου τεχνικές για να ελέγξω ανεπίσημα και να αιτιολογήσω την ορθότητά τους. 

Είναι δίκαιο να πω ότι παρόλο που είχα μια εκτίμηση για το γεγονός ότι οι δοκιμές θα ήταν πάντα ελλιπείς με την έννοια ότι ήταν αδύνατο να δοκιμάσω κάθε περίπτωση. ότι ήμουν αρκετά σίγουρος ότι ο μαθηματικός τρόπος σκέψης μου ήταν πολύ καλός όταν έπρεπε να κάνω άτυπες δοκιμές με αυστηρό τρόπο. Ως εκ τούτου, σίγουρα δεν είχα πλήρη εκτίμηση της διαφοράς μεταξύ δοκιμής και απόδειξης ορθότητας, ούτε τις συνέπειες αυτού του είδους! Κατά τη διάρκεια της καριέρας μου πριν από την ένταξή μου στο ConsenSys ήμουν ικανοποιημένος να βασίζομαι στις δικές μου άτυπες τεχνικές για να προσδιορίσω τι νόμιζα ότι ήταν ορθότητα μέσω δοκιμών. 

Το ιστορικό μου είναι λοιπόν μέρος της ιστορίας, καθώς είμαι ο ίδιος κάπως έκπληκτος που δεν ανακάλυψα επίσημες μεθόδους νωρίτερα. Θεωρώ τον εαυτό μου μαθηματικό. Μου αρέσουν τα μαθηματικά, οι αλγόριθμοι και η λογική. Φαίνεται τώρα τρελό να βασίζεσαι απλώς σε ελλιπείς δοκιμές, αλλά επίσης φαίνεται τρελός για όποιον προγραμματίζει να μην έχει τουλάχιστον κάποια εκτίμηση για το τι μπορούν να προσφέρουν οι επίσημες μέθοδοι και τις πιθανές συνέπειες της απώλειας ενός σφάλματος, δεδομένου του πολλού τρόπου με τον οποίο τα προγράμματα υπολογιστών ενσωματωμένο στη ζωή μας. Οι επίσημες μέθοδοι μας επιτρέπουν να προχωρήσουμε πέρα ​​από τις δοκιμές, για να αποδείξουμε ότι ένα πρόγραμμα είναι σωστό έναντι μιας προδιαγραφής που περιλαμβάνει προϋποθέσεις πριν και μετά. 

Ένα πρώτο παράδειγμα Dafny

Ως απλό παράδειγμα, εξετάστε τον ακέραιο διαχωρισμό ενός μη αρνητικού μερίσματος n από έναν θετικό διαιρέτη d. 

η / η

Φαίνεται παρακάτω:

Αν και σε μια πληκτρολογημένη γλώσσα προγραμματισμού μπορούμε κάπως να περιορίσουμε τις παραμέτρους εισαγωγής, δεν είναι πάντα αρκετή. Σε αυτό το παράδειγμα, ο προσδιορισμός των n και d ως φυσικών αριθμών σημαίνει ότι και οι δύο είσοδοι πρέπει να είναι μη αρνητικοί ακέραιοι, αλλά δεν προβλέπει τον περιορισμό του d ως θετικού ακέραιου. Η χρήση μιας προϋπόθεσης μέσω της δήλωσης απαιτήσεων προβλέπει έναν τέτοιο περιορισμό και σημαίνει ότι αυτή η μέθοδος μπορεί να κληθεί μόνο εάν d > 0. Ως εκ τούτου, εάν οποιοδήποτε άλλο μέρος του προγράμματος θα προκαλούσε κλήση div χωρίς να πληρούται μια τέτοια προϋπόθεση, τότε το πρόγραμμα δεν θα επαληθεύσει. Η δήλωση εξασφαλίζει στη συνέχεια την κατάσταση μετά και παρέχει μια επίσημη περιγραφή του τι πρέπει να ικανοποιεί η έξοδος της μεθόδου.

Αυτό το παράδειγμα γράφεται χρησιμοποιώντας το Dafny: «Μια γλώσσα και πρόγραμμα επαλήθευσης για λειτουργική ορθότητα» και με φέρνει στο επόμενο σημείο, δηλαδή, γιατί είμαι τόσο θαυμαστής του Dafny. Νομίζω ότι είναι δίκαιο να πούμε ότι για πολλούς προγραμματιστές, η σκέψη της χρήσης «τυπικών μεθόδων» για την επαλήθευση της ορθότητας του προγράμματος είναι κάπως τρομακτική και συχνά θεωρείται ότι είναι «πολύ» σκληρή. Είτε αυτό οφείλεται στην έλλειψη έκθεσης στις τεχνικές, στην έλλειψη εκτίμησης των οφελών, ή ακόμη και στην έλλειψη εκπαίδευσης σε αυτόν τον τομέα; Όποιοι και αν είναι οι λόγοι, πιστεύω ότι η Dafny έχει τη δυνατότητα να επιτρέπει σε οποιονδήποτε προγραμματιστή να επιτύχει γρήγορα την εφαρμογή επίσημων μεθόδων στο έργο του. Κοιτάζοντας το παραπάνω απόσπασμα κώδικα, θα περίμενα από οποιονδήποτε με κάποια γνώση προγραμματισμού να μπορεί να διαβάσει αυτόν τον κωδικό Dafny. Η Dafny είναι πολύ φιλική προς τον προγραμματιστή γλώσσα. Μόλις μάθετε λίγο Dafny, είναι πολύ εύκολο να ξεκινήσετε τον πειραματισμό και στη συνέχεια να μάθετε βασικά καθώς πηγαίνετε. Και αν σας ενδιαφέρει να μάθετε Dafny, ένα εξαιρετικό μέρος για να ξεκινήσετε είναι το σειρά μαθημάτων από τη Microsoft. Ο ιστότοπος περιλαμβάνει επίσης έναν διαδικτυακό επεξεργαστή, οπότε είναι πολύ εύκολο να δοκιμάσετε τα παραδείγματα του σεμιναρίου. ο Κανάλι γωνίας επαλήθευσης στο YouTube είναι μια άλλη πηγή χρήσιμων αναφορών.

Η επιφανειακή μου στιγμή

Τελικά ήθελα να μοιραστώ τη θεοφωνική μου στιγμή από όταν έμαθα τον Ντάφνι. Σίγουρα έχω ακούσει ιστορίες για σύντομα και απλά κομμάτια κώδικα, από μεγάλες αξιόπιστες εταιρείες, με σφάλματα που χάθηκαν και τελικά κόστισαν πολλά εκατομμύρια δολάρια. αλλά νομίζω ότι μόνο όταν συνειδητοποιείτε πόσο εύκολο θα ήταν να δημιουργήσετε ακούσια ένα σφάλμα σε μια απλή λειτουργία, όλα αυτά έχουν νόημα! Τη στιγμή που λες στον εαυτό σου “Ω, θα ήταν τόσο εύκολο να κάνεις αυτό το λάθος!”

Ήρθε η στιγμή μου βλέποντας ένα από τα Βίντεο γωνίας επαλήθευσης

Σε αυτό το σεμινάριο ο Rustan Leino ακολουθεί μια μέθοδο SumMax που παίρνει δύο ακέραιους αριθμούς, x και y, και επιστρέφει το άθροισμα και το μέγιστο, s και m, αντίστοιχα. Αυτό το παράδειγμα είναι σχετικά απλό και ο κωδικός Dafny φαίνεται παρακάτω.

Οι είσοδοι x και y καθορίζονται ως ακέραιοι αριθμοί μέσω της πληκτρολόγησης και δεν απαιτούνται άλλες προϋποθέσεις. Οι τρεις συνθήκες μετά παρέχουν ελέγχους ότι η έξοδος πληροί όντως τις προδιαγραφές, δηλαδή ότι είναι ίσο με x + y και ότι το m είναι ίσο με x ή y και ότι το m δεν υπερβαίνει τα x και y. Η μέθοδος SumMaxBackwards παρουσιάζεται στη συνέχεια ως άσκηση και εδώ γίνεται πιο ενδιαφέρουσα. Η προδιαγραφή είναι το αντίστροφο του SumMax, δηλαδή δεδομένου του αθροίσματος και της μέγιστης επιστροφής οι ακέραιοι αριθμοί x και y. Εντάξει, οπότε μια πρώτη προσπάθεια μπορεί να είναι με τις ίδιες προϋποθέσεις καθώς οι σχέσεις μεταξύ των εισόδων και των εξόδων εξακολουθούν να ισχύουν. Αν αφήσουμε το x να είναι το μέγιστο, τότε ένα γρήγορο άλγεβρα μας λέει ότι πρέπει να ισούται με το άθροισμα μείον το μέγιστο. Η τοποθέτηση αυτού στο διαδικτυακό πρόγραμμα επεξεργασίας δίνει τα εξής.

Screen Shot 2020 12 15 στις 6 38 37 μ.μ. 1 Στιγμιότυπο 2020 12 16 στις 5 35 22 μ.μ.

Δεν επαληθεύει. Λοιπόν, τι πήγε στραβά; Μας λένε ότι μια μετα-κατάσταση δεν κράτησε και συγκεκριμένα η μετα-κατάσταση στη γραμμή 3 (εξασφαλίζει x<= μ && γ <= m) δεν μπορεί να κρατήσει. Κοιτώντας πιο προσεκτικά βλέπουμε ότι αυτή η συνθήκη ανάρτησης καθορίζει ότι x <= m και y <= μ. Λοιπόν, γνωρίζουμε ότι το x είναι μικρότερο ή ίσο με το m καθώς ορίζουμε το x ίσο με το m, έτσι αυτό σημαίνει ότι το y <= m μέρος δεν επαληθεύει. Πώς μπορεί να συμβεί αυτό; Η άλγεβρα μας μας είπε ότι y: = s – m. Ας υποθέσουμε ότι το s είναι 5 και το m είναι 3, τότε y = 5 – 3 = 2 που εξασφαλίζει y <= μ; αλλά ας πούμε ότι ονομάζουμε αυτήν τη μέθοδο με s ίσο με 5 και m ίσο με 1. Τίποτα δεν θα μας εμποδίσει να καλέσουμε τη μέθοδο με αυτές τις παραμέτρους εισόδου, αλλά κάτι τέτοιο θα προκαλέσει πρόβλημα όπως y = 5 – 1 = 4 και μετά y > Μ. Βασικά αυτό που βλέπουμε εδώ είναι ότι παρόλο που η παράμετρος εισαγωγής προορίζεται να είναι το μέγιστο των δύο ακεραίων που δημιουργεί το άθροισμα, δεν υπάρχει τίποτα που να μας εμποδίζει να καλέσουμε τη μέθοδο με μια είσοδο που δεν είναι έγκυρη. Εάν δεν περιλαμβάνεται μια προϋπόθεση για τον περιορισμό των εισόδων των s και m σε έγκυρους ακέραιους αριθμούς που θα οδηγήσουν σε έξοδοι x και y που πληρούν τις προδιαγραφές, τότε η μέθοδος μας μπορεί να παράγει λανθασμένα αποτελέσματα. Τι σχέση χρειαζόμαστε μεταξύ s και m για να παρέχουμε έγκυρες εισόδους; Λίγο περισσότερη άλγεβρα μας δείχνει ότι <= m * 2 για να υπάρχει μια έγκυρη λύση των x και y. Εάν το προσθέσουμε ως προϋπόθεση, η Dafny μπορεί πλέον να επαληθεύσει τον κωδικό όπως φαίνεται παρακάτω. 

Στιγμιότυπο 2020 12 15 στις 6 46 32 μ.μ. 1 Screen Shot 2020 12 16 στις 5 37 39 μ.μ.

Αυτό ήταν το παράδειγμα όπου μπορούσα να δω πόσο εύκολο είναι να εισαγάγω ένα σφάλμα στον κώδικα. Ακριβώς επειδή ονομάζουμε τις παραμέτρους εισαγωγής «για άθροισμα και« m »για μέγιστο, δεν σημαίνει ότι η μέθοδος θα καλείται κατάλληλα και ως τέτοιο μέρος κάποιου μεγαλύτερου προγράμματος, θα μπορούσαν να υπάρχουν πολλές ακούσιες συνέπειες που προκύπτουν από αυτό τύπος σφάλματος. Ελπίζω να είναι χρήσιμο για οποιονδήποτε άλλον να μαθαίνει για το Dafny ή τις τυπικές μεθόδους γενικότερα.

Τι δουλεύω τώρα

Λοιπόν αυτό με φέρνει στο τέλος της ανάρτησής μου. Αν θέλετε να δείτε τι δουλεύω αυτήν τη στιγμή με την Dafny, ρίξτε μια ματιά σε αυτό Repo GitHub. Είμαι μέλος της αυτοματοποιημένης ομάδας επαλήθευσης εντός του R&D στο ConsenSys και χρησιμοποιούμε το Dafny στην επίσημη επαλήθευση της προδιαγραφής Ethereum 2 Phase 0. Η χρήση τυπικών μεθόδων στο χώρο του blockchain είναι ένας συναρπαστικός νέος τομέας έρευνας που έχει αγκαλιάσει η ConsenSys και θα ενθαρρύνω όσους ενδιαφέρονται να μάθουν περισσότερα για το Eth 2.0 για να δουν τους διαθέσιμους πόρους στο repo του έργου μας.

Εγγραφείτε στο ενημερωτικό δελτίο μας για τις τελευταίες ειδήσεις Ethereum, εταιρικές λύσεις, πόρους προγραμματιστών και πολλά άλλα. Διεύθυνση ηλεκτρονικού ταχυδρομείου

Mike Owergreen Administrator
Sorry! The Author has not filled his profile.
follow me