Αυτό είναι ένα άρθρο μετάφρασης . Αλλά πριν από αυτό υπάρχει μια σύντομη εισαγωγή. Πώς σχηματίζονται τα ζόμπι; Όλοι έχουν βρεθεί σε μια κατάσταση όπου θέλουν να φέρουν έναν φίλο ή συνάδελφο στο επίπεδό τους, αλλά δεν τους βγαίνει. Επιπλέον, "δεν λειτουργεί" όχι τόσο για εσάς, όσο για εκείνον: στη μία πλευρά της κλίμακας υπάρχει ένας κανονικός μισθός, καθήκοντα και ούτω καθεξής, και από την άλλη είναι η ανάγκη να σκεφτείτε. Η σκέψη είναι δυσάρεστη και επώδυνη. Γρήγορα τα παρατάει και συνεχίζει να γράφει κώδικα χωρίς να χρησιμοποιεί καθόλου τον εγκέφαλό του. Συνειδητοποιείς πόση προσπάθεια χρειάζεται για να ξεπεράσεις το φράγμα της μαθημένης αδυναμίας και απλά δεν το κάνεις. Έτσι σχηματίζονται τα ζόμπι, τα οποία φαίνεται ότι είναι δυνατό να θεραπευτούν, αλλά φαίνεται ότι κανείς δεν θα το κάνει αυτό.
Όταν το είδα (ναι, ο ίδιος φίλος από τα σχολικά βιβλία) και δεν δίνει αναφορά, αλλά μια συνεδρία ερωτήσεων και απαντήσεων, ήμουν λίγο επιφυλακτικός. Για κάθε ενδεχόμενο, ο Leslie είναι ένας παγκοσμίου φήμης επιστήμονας, ο συγγραφέας σημαντικών εργασιών στον κατανεμημένο υπολογισμό, και ίσως τον γνωρίζετε επίσης με τα γράμματα La στο LaTeX - "Lamport TeX". Ο δεύτερος ανησυχητικός παράγοντας είναι η απαίτησή του: ο καθένας που έρχεται πρέπει (εντελώς δωρεάν) να ακούσει εκ των προτέρων μερικές από τις εκθέσεις του, να κάνει τουλάχιστον μια ερώτηση σχετικά με αυτές και μόνο τότε να έρθει. Αποφάσισα να δω τι μετέδιδε η Lamport εκεί - και είναι υπέροχο! Αυτό είναι ακριβώς αυτό το πράγμα, ένα μαγικό χάπι σύνδεσης για τη θεραπεία των ζόμπι. Σας προειδοποιώ: το κείμενο μπορεί να κάψει σοβαρά όσους αγαπούν τις εξαιρετικά ευέλικτες μεθοδολογίες και που δεν τους αρέσει να δοκιμάζουν αυτά που έχουν γράψει.
Μετά το habrokat ξεκινά ουσιαστικά η μετάφραση του σεμιναρίου. Απολαύστε την ανάγνωση!
Όποια και αν είναι η εργασία που αναλαμβάνετε, πρέπει πάντα να περνάτε από τρία βήματα:
- αποφασίστε ποιος στόχος θέλετε να επιτύχετε.
- αποφασίστε πώς ακριβώς θα πετύχετε τον στόχο σας.
- φτάσε τον στόχο σου.
Αυτό ισχύει και για τον προγραμματισμό. Όταν γράφουμε κώδικα, χρειαζόμαστε:
- Αποφασίστε τι ακριβώς πρέπει να κάνει το πρόγραμμα.
- να καθορίσει ακριβώς πώς θα πρέπει να εκτελέσει το έργο του.
- γράψτε τον κατάλληλο κωδικό.
Το τελευταίο βήμα, φυσικά, είναι πολύ σημαντικό, αλλά δεν θα μιλήσω γι' αυτό σήμερα. Αντίθετα, θα συζητήσουμε τα δύο πρώτα. Κάθε προγραμματιστής τις εκτελεί πριν ξεκινήσει να εργάζεται. Δεν κάθεσαι να γράψεις αν δεν έχεις αποφασίσει τι γράφεις: πρόγραμμα περιήγησης ή βάση δεδομένων. Πρέπει να υπάρχει μια συγκεκριμένη ιδέα του στόχου. Και σίγουρα σκέφτεστε τι ακριβώς θα κάνει το πρόγραμμα και μην το γράφετε τυχαία με την ελπίδα ότι ο ίδιος ο κώδικας θα μετατραπεί με κάποιο τρόπο σε πρόγραμμα περιήγησης.
Πώς ακριβώς συμβαίνει αυτή η εκ των προτέρων σκέψη του κώδικα; Πόση προσπάθεια πρέπει να καταβάλουμε σε αυτό; Όλα εξαρτώνται από το πόσο περίπλοκο είναι το πρόβλημα που επιλύουμε. Ας υποθέσουμε ότι θέλουμε να γράψουμε ένα κατανεμημένο σύστημα με ανοχή σφαλμάτων. Σε αυτήν την περίπτωση, θα πρέπει να σκεφτούμε προσεκτικά τα πράγματα πριν καθίσουμε να κωδικοποιήσουμε. Τι γίνεται αν χρειάζεται απλώς να αυξήσουμε μια ακέραια μεταβλητή κατά 1; Με την πρώτη ματιά, όλα εδώ είναι ασήμαντα και δεν χρειάζεται σκέψη, αλλά μετά θυμόμαστε ότι μπορεί να συμβεί υπερχείλιση. Επομένως, ακόμη και για να καταλάβετε εάν ένα πρόβλημα είναι απλό ή σύνθετο, πρέπει πρώτα να σκεφτείτε.
Εάν σκεφτείτε εκ των προτέρων πιθανές λύσεις σε ένα πρόβλημα, μπορείτε να αποφύγετε λάθη. Αλλά αυτό απαιτεί η σκέψη σας να είναι ξεκάθαρη. Για να το πετύχετε αυτό, πρέπει να γράψετε τις σκέψεις σας. Λατρεύω το απόφθεγμα του Ντικ Γκίντον: «Όταν γράφεις, η φύση σου δείχνει πόσο ατημέλητη είναι η σκέψη σου». Αν δεν γράφεις, μόνο νομίζεις ότι σκέφτεσαι. Και πρέπει να γράψετε τις σκέψεις σας με τη μορφή προδιαγραφών.
Οι προδιαγραφές εξυπηρετούν πολλές λειτουργίες, ειδικά σε μεγάλα έργα. Αλλά θα μιλήσω μόνο για ένα από αυτά: μας βοηθούν να σκεφτόμαστε καθαρά. Η καθαρή σκέψη είναι πολύ σημαντική και αρκετά δύσκολη, επομένως χρειαζόμαστε οποιαδήποτε βοήθεια εδώ. Σε ποια γλώσσα πρέπει να γράψουμε προδιαγραφές; Γενικά, αυτή είναι πάντα η πρώτη ερώτηση για τους προγραμματιστές: σε ποια γλώσσα θα γράφουμε; Δεν υπάρχει μία σωστή απάντηση: τα προβλήματα που επιλύουμε είναι πολύ διαφορετικά. Για μερικούς ανθρώπους, η TLA+ είναι μια γλώσσα προδιαγραφών που ανέπτυξα. Για άλλους, είναι πιο βολικό να χρησιμοποιούν κινέζικα. Όλα εξαρτώνται από την κατάσταση.
Το πιο σημαντικό ερώτημα είναι: πώς μπορούμε να επιτύχουμε πιο καθαρή σκέψη; Απάντηση: Πρέπει να σκεφτόμαστε σαν επιστήμονες. Αυτός είναι ένας τρόπος σκέψης που έχει λειτουργήσει καλά τα τελευταία 500 χρόνια. Στην επιστήμη χτίζουμε μαθηματικά μοντέλα πραγματικότητας. Η αστρονομία ήταν ίσως η πρώτη επιστήμη με τη στενή έννοια του όρου. Στο μαθηματικό μοντέλο που χρησιμοποιείται στην αστρονομία, τα ουράνια σώματα εμφανίζονται ως σημεία με μάζα, θέση και ορμή, αν και στην πραγματικότητα είναι εξαιρετικά πολύπλοκα αντικείμενα με βουνά και ωκεανούς, άμπωτες και ροές. Αυτό το μοντέλο, όπως και κάθε άλλο, δημιουργήθηκε για να λύσει ορισμένα προβλήματα. Είναι εξαιρετικό για να προσδιορίσετε πού να στρίψετε ένα τηλεσκόπιο εάν θέλετε να βρείτε έναν πλανήτη. Αλλά αν θέλετε να προβλέψετε τον καιρό σε αυτόν τον πλανήτη, αυτό το μοντέλο δεν θα λειτουργήσει.
Τα μαθηματικά μας επιτρέπουν να προσδιορίσουμε τις ιδιότητες ενός μοντέλου. Και η επιστήμη δείχνει πώς αυτές οι ιδιότητες σχετίζονται με την πραγματικότητα. Ας μιλήσουμε για την επιστήμη μας, την επιστήμη των υπολογιστών. Η πραγματικότητα με την οποία εργαζόμαστε είναι υπολογιστικά συστήματα πολλών διαφορετικών τύπων: επεξεργαστές, κονσόλες παιχνιδιών, υπολογιστές που εκτελούν προγράμματα κ.λπ. Θα μιλήσω για την εκτέλεση ενός προγράμματος σε έναν υπολογιστή, αλλά, σε γενικές γραμμές, όλα αυτά τα συμπεράσματα ισχύουν για οποιοδήποτε υπολογιστικό σύστημα. Στην επιστήμη μας χρησιμοποιούμε πολλά διαφορετικά μοντέλα: τη μηχανή Turing, μερικώς διατεταγμένα σετ γεγονότων και πολλά άλλα.
Ποιο είναι το πρόγραμμα; Αυτός είναι οποιοσδήποτε κωδικός που μπορεί να ληφθεί υπόψη από μόνος του. Ας πούμε ότι πρέπει να γράψουμε ένα πρόγραμμα περιήγησης. Εκτελούμε τρεις εργασίες: σχεδιάζουμε την παρουσίαση του προγράμματος από τον χρήστη, μετά γράφουμε το διάγραμμα υψηλού επιπέδου του προγράμματος και τέλος γράφουμε τον κώδικα. Καθώς γράφουμε τον κώδικα, συνειδητοποιούμε ότι πρέπει να γράψουμε έναν μορφοποιητή κειμένου. Εδώ πάλι πρέπει να λύσουμε τρία προβλήματα: να καθορίσουμε ποιο κείμενο θα επιστρέψει αυτό το εργαλείο. επιλέξτε έναν αλγόριθμο για μορφοποίηση. γράψτε κώδικα. Αυτή η εργασία έχει τη δική της δευτερεύουσα εργασία: εισαγωγή παύλων σε λέξεις σωστά. Επιλύουμε επίσης αυτήν την δευτερεύουσα εργασία σε τρία βήματα - όπως βλέπουμε, επαναλαμβάνονται σε πολλά επίπεδα.
Ας ρίξουμε μια πιο προσεκτική ματιά στο πρώτο βήμα: ποιο πρόβλημα επιλύει το πρόγραμμα. Εδώ μοντελοποιούμε συχνότερα ένα πρόγραμμα ως συνάρτηση που παίρνει κάποια είσοδο και δίνει κάποια έξοδο. Στα μαθηματικά, μια συνάρτηση συνήθως περιγράφεται ως ένα διατεταγμένο σύνολο ζευγών. Για παράδειγμα, η συνάρτηση τετραγωνισμού για φυσικούς αριθμούς περιγράφεται ως το σύνολο {<0,0>, <1,1>, <2,4>, <3,9>, …}. Το πεδίο ορισμού μιας τέτοιας συνάρτησης είναι το σύνολο των πρώτων στοιχείων κάθε ζεύγους, δηλαδή των φυσικών αριθμών. Για να ορίσουμε μια συνάρτηση, πρέπει να καθορίσουμε τον τομέα και τον τύπο της.
Αλλά οι συναρτήσεις στα μαθηματικά δεν είναι ίδιες με τις συναρτήσεις στις γλώσσες προγραμματισμού. Τα μαθηματικά είναι πολύ πιο απλά. Επειδή δεν έχω χρόνο για πολύπλοκα παραδείγματα, ας εξετάσουμε ένα απλό: μια συνάρτηση στο C ή μια στατική μέθοδο στην Java που επιστρέφει τον μεγαλύτερο κοινό διαιρέτη δύο ακεραίων. Στην προδιαγραφή αυτής της μεθόδου θα γράψουμε: υπολογίζει GCD(M,N) για επιχειρήματα M и NΌπου GCD(M,N) - μια συνάρτηση της οποίας ο τομέας είναι ένα σύνολο ζευγών ακεραίων αριθμών και η τιμή επιστροφής είναι ο μεγαλύτερος ακέραιος που διαιρείται με M и N. Πώς συγκρίνεται η πραγματικότητα με αυτό το μοντέλο; Το μοντέλο λειτουργεί με ακέραιους αριθμούς και σε C ή Java έχουμε 32-bit int. Αυτό το μοντέλο μας επιτρέπει να αποφασίσουμε εάν ο αλγόριθμος είναι σωστός GCD, αλλά δεν θα αποτρέψει σφάλματα υπερχείλισης. Αυτό θα απαιτούσε ένα πιο περίπλοκο μοντέλο, για το οποίο δεν υπάρχει χρόνος.
Ας μιλήσουμε για τους περιορισμούς της λειτουργίας ως μοντέλου. Ορισμένα προγράμματα (όπως τα λειτουργικά συστήματα) δεν επιστρέφουν απλώς μια συγκεκριμένη τιμή για ορισμένα ορίσματα, αλλά μπορούν να εκτελούνται συνεχώς. Επιπλέον, η λειτουργία ως μοντέλο δεν είναι κατάλληλη για το δεύτερο βήμα: τον σχεδιασμό του τρόπου επίλυσης του προβλήματος. Η γρήγορη ταξινόμηση και η ταξινόμηση με φυσαλίδες υπολογίζουν την ίδια συνάρτηση, αλλά είναι εντελώς διαφορετικοί αλγόριθμοι. Επομένως, για να περιγράψω τον τρόπο επίτευξης του στόχου του προγράμματος, χρησιμοποιώ ένα άλλο μοντέλο, ας το ονομάσουμε τυπικό μοντέλο συμπεριφοράς. Το πρόγραμμα αναπαρίσταται σε αυτό ως ένα σύνολο από όλες τις έγκυρες συμπεριφορές, καθεμία από τις οποίες, με τη σειρά της, είναι μια ακολουθία καταστάσεων και μια κατάσταση είναι η εκχώρηση τιμών σε μεταβλητές.
Ας δούμε πώς θα ήταν το δεύτερο βήμα για τον ευκλείδειο αλγόριθμο. Πρέπει να υπολογίσουμε GCD(M, N). Αρχικοποιούμε M как xΚαι N как y, στη συνέχεια αφαιρέστε επανειλημμένα τη μικρότερη από αυτές τις μεταβλητές από τη μεγαλύτερη μέχρι να εξισωθούν. Για παράδειγμα, εάν M = 12Και N = 18, μπορούμε να περιγράψουμε την ακόλουθη συμπεριφορά:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
Και αν M = 0 и N = 0? Το μηδέν διαιρείται με όλους τους αριθμούς, επομένως δεν υπάρχει μεγαλύτερος διαιρέτης σε αυτή την περίπτωση. Σε αυτήν την περίπτωση, πρέπει να επιστρέψουμε στο πρώτο βήμα και να ρωτήσουμε: χρειάζεται πραγματικά να υπολογίσουμε το GCD για μη θετικούς αριθμούς; Εάν αυτό δεν είναι απαραίτητο, τότε απλά πρέπει να αλλάξετε τις προδιαγραφές.
Εδώ χρειάζεται μια σύντομη παρέκβαση σχετικά με την παραγωγικότητα. Συχνά μετριέται στον αριθμό των γραμμών κώδικα που γράφονται ανά ημέρα. Αλλά η δουλειά σας είναι πολύ πιο χρήσιμη εάν απαλλαγείτε από έναν ορισμένο αριθμό γραμμών, επειδή έχετε λιγότερο χώρο για σφάλματα. Και ο ευκολότερος τρόπος για να απαλλαγείτε από τον κώδικα είναι στο πρώτο βήμα. Είναι πιθανό ότι απλά δεν χρειάζεστε όλες τις καμπάνες και σφυρίχτρες που προσπαθείτε να εφαρμόσετε. Ο πιο γρήγορος τρόπος για να απλοποιήσετε ένα πρόγραμμα και να εξοικονομήσετε χρόνο είναι να μην κάνετε πράγματα που δεν πρέπει να γίνουν. Το δεύτερο βήμα έχει τη δεύτερη μεγαλύτερη δυνατότητα εξοικονόμησης χρόνου. Εάν μετράτε την παραγωγικότητα με βάση τις γραμμές που γράφετε, τότε θα σας κάνει να σκεφτείτε πώς να ολοκληρώσετε μια εργασία λιγότερο παραγωγική, γιατί μπορείτε να λύσετε το ίδιο πρόβλημα με λιγότερο κώδικα. Δεν μπορώ να δώσω ακριβή στατιστικά εδώ, γιατί δεν έχω τρόπο να μετρήσω τον αριθμό των γραμμών που δεν έγραψα λόγω του χρόνου που αφιέρωσα στην προδιαγραφή, δηλαδή στο πρώτο και το δεύτερο βήμα. Και δεν μπορούμε να κάνουμε ένα πείραμα ούτε εδώ, γιατί σε ένα πείραμα δεν έχουμε το δικαίωμα να ολοκληρώσουμε το πρώτο βήμα· η εργασία καθορίζεται εκ των προτέρων.
Είναι εύκολο να παραβλεφθούν πολλές δυσκολίες στις ανεπίσημες προδιαγραφές. Δεν υπάρχει τίποτα δύσκολο στη σύνταξη αυστηρών προδιαγραφών για λειτουργίες· δεν θα το συζητήσω αυτό. Αντίθετα, θα μιλήσουμε για τη σύνταξη ισχυρών προδιαγραφών για τυπικές συμπεριφορές. Υπάρχει ένα θεώρημα που δηλώνει ότι οποιοδήποτε σύνολο συμπεριφορών μπορεί να περιγραφεί χρησιμοποιώντας την ιδιότητα ασφαλείας (ασφάλεια) και ιδιότητες επιβίωσης (ζωντάνια). Ασφάλεια σημαίνει ότι δεν θα συμβεί τίποτα κακό, το πρόγραμμα δεν θα δώσει λάθος απάντηση. Επιβίωση σημαίνει ότι αργά ή γρήγορα κάτι καλό θα συμβεί, δηλαδή το πρόγραμμα αργά ή γρήγορα θα δώσει τη σωστή απάντηση. Κατά κανόνα, η ασφάλεια είναι ένας πιο σημαντικός δείκτης· τα σφάλματα εμφανίζονται συχνότερα εδώ. Ως εκ τούτου, για να εξοικονομήσω χρόνο, δεν θα μιλήσω για επιβίωση, αν και, φυσικά, είναι επίσης σημαντικό.
Επιτυγχάνουμε ασφάλεια καθορίζοντας πρώτα ένα σύνολο πιθανών αρχικών καταστάσεων. Και δεύτερον, σχέσεις με όλες τις πιθανές επόμενες καταστάσεις για κάθε κατάσταση. Ας συμπεριφερόμαστε σαν επιστήμονες και ας ορίζουμε τις καταστάσεις μαθηματικά. Το σύνολο των αρχικών καταστάσεων περιγράφεται από τον τύπο, για παράδειγμα, στην περίπτωση του Ευκλείδειου αλγόριθμου: (x = M) ∧ (y = N). Για ορισμένες αξίες M и N υπάρχει μόνο μία αρχική κατάσταση. Η σχέση με την επόμενη κατάσταση περιγράφεται από έναν τύπο στον οποίο οι μεταβλητές της επόμενης κατάστασης γράφονται με πρώτο και οι μεταβλητές της τρέχουσας κατάστασης χωρίς πρώτο. Στην περίπτωση του Ευκλείδειου αλγόριθμου, θα έχουμε να κάνουμε με τον διαχωρισμό δύο τύπων, σε έναν από τους οποίους x είναι η μεγαλύτερη τιμή, και στη δεύτερη - y:
Στην πρώτη περίπτωση, η νέα τιμή του y είναι ίση με την προηγούμενη τιμή του y, και παίρνουμε τη νέα τιμή του x αφαιρώντας τη μικρότερη μεταβλητή από τη μεγαλύτερη. Στη δεύτερη περίπτωση, κάνουμε το αντίθετο.
Ας επιστρέψουμε στον ευκλείδειο αλγόριθμο. Άσε που πάλι αυτό M = 12, N = 18. Αυτό ορίζει μια ενιαία αρχική κατάσταση, (x = 12) ∧ (y = 18). Στη συνέχεια, συνδέουμε αυτές τις τιμές στον παραπάνω τύπο και παίρνουμε:
Εδώ είναι η μόνη δυνατή λύση: x' = 18 - 12 ∧ y' = 12, και παίρνουμε τη συμπεριφορά: [x = 12, y = 18]. Με τον ίδιο τρόπο, μπορούμε να περιγράψουμε όλες τις καταστάσεις στη συμπεριφορά μας: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
Σε τελευταία κατάσταση [x = 6, y = 6] και τα δύο μέρη της έκφρασης θα είναι ψευδή, επομένως δεν έχει επόμενη κατάσταση. Έτσι, έχουμε μια πλήρη προδιαγραφή του δεύτερου βήματος - όπως βλέπουμε, αυτά είναι αρκετά συνηθισμένα μαθηματικά, όπως αυτά των μηχανικών και των επιστημόνων, και όχι περίεργα, όπως στην επιστήμη των υπολογιστών.
Αυτοί οι δύο τύποι μπορούν να συνδυαστούν σε έναν τύπο χρονικής λογικής. Είναι κομψό και εύκολο να εξηγηθεί, αλλά δεν υπάρχει χρόνος για αυτό τώρα. Μπορεί να χρειαζόμαστε χρονική λογική μόνο για την ιδιότητα της ζωντάνιας· για την ασφάλεια δεν χρειάζεται. Δεν μου αρέσει η χρονική λογική ως τέτοια, δεν είναι αρκετά συνηθισμένα μαθηματικά, αλλά στην περίπτωση της ζωντάνιας είναι αναγκαίο κακό.
Στον Ευκλείδειο αλγόριθμο για κάθε τιμή x и y υπάρχουν μοναδικές αξίες x' и y', που κάνουν αληθινή τη σχέση με την επόμενη κατάσταση. Με άλλα λόγια, ο ευκλείδειος αλγόριθμος είναι ντετερμινιστικός. Για να μοντελοποιηθεί ένας μη ντετερμινιστικός αλγόριθμος, η τρέχουσα κατάσταση πρέπει να έχει πολλαπλές πιθανές μελλοντικές καταστάσεις και κάθε τιμή της μεταβλητής χωρίς εκκίνηση πρέπει να έχει πολλαπλές τιμές της αρχικής μεταβλητής έτσι ώστε η σχέση με την επόμενη κατάσταση να είναι αληθής. Αυτό δεν είναι δύσκολο να γίνει, αλλά δεν θα δώσω παραδείγματα τώρα.
Για να φτιάξετε ένα εργαλείο εργασίας, χρειάζεστε επίσημα μαθηματικά. Πώς να κάνετε μια τυπική προδιαγραφή; Για να γίνει αυτό θα χρειαστούμε μια επίσημη γλώσσα, π.χ. . Η προδιαγραφή του Ευκλείδειου αλγόριθμου σε αυτή τη γλώσσα θα μοιάζει με αυτό:
Το σύμβολο του ίσου με ένα τρίγωνο σημαίνει ότι η τιμή στα αριστερά του σημείου καθορίζεται να είναι ίση με την τιμή στα δεξιά του σημείου. Στην ουσία, μια προδιαγραφή είναι ένας ορισμός, στην περίπτωσή μας δύο ορισμοί. Στις προδιαγραφές στο TLA+ πρέπει να προσθέσετε δηλώσεις και κάποια σύνταξη, όπως στην παραπάνω διαφάνεια. Στο ASCII θα μοιάζει με αυτό:
Όπως μπορείτε να δείτε, τίποτα περίπλοκο. Η προδιαγραφή στο TLA+ μπορεί να επαληθευτεί, δηλ. είναι δυνατή η παράκαμψη όλων των πιθανών συμπεριφορών σε ένα μικρό μοντέλο. Στην περίπτωσή μας, αυτό το μοντέλο θα έχει ορισμένες τιμές M и N. Αυτή είναι μια πολύ αποτελεσματική και απλή μέθοδος επαλήθευσης που είναι εντελώς αυτόματη. Επιπλέον, είναι δυνατό να γράψετε επίσημες αποδείξεις αλήθειας και να τις ελέγξετε μηχανικά, αλλά αυτό απαιτεί πολύ χρόνο, επομένως σχεδόν κανείς δεν το κάνει αυτό.
Το κύριο μειονέκτημα του TLA+ είναι ότι είναι μαθηματικά και οι προγραμματιστές και οι επιστήμονες υπολογιστών φοβούνται τα μαθηματικά. Με την πρώτη ματιά ακούγεται σαν αστείο, αλλά, δυστυχώς, το λέω με κάθε σοβαρότητα. Ένας συνάδελφός μου μόλις μου έλεγε πώς προσπάθησε να εξηγήσει το TLA+ σε αρκετούς προγραμματιστές. Μόλις εμφανίστηκαν οι φόρμουλες στην οθόνη, τα μάτια τους έγιναν αμέσως γυάλινα. Έτσι, αν το TLA+ είναι τρομακτικό, μπορείτε να το χρησιμοποιήσετε , είναι ένα είδος γλώσσας προγραμματισμού παιχνιδιών. Μια έκφραση στο PlusCal μπορεί να είναι οποιαδήποτε έκφραση TLA+, δηλαδή βασικά οποιαδήποτε μαθηματική έκφραση. Επιπλέον, το PlusCal έχει σύνταξη για μη ντετερμινιστικούς αλγόριθμους. Επειδή η PlusCal μπορεί να γράψει οποιαδήποτε έκφραση TLA+, είναι σημαντικά πιο εκφραστική από οποιαδήποτε πραγματική γλώσσα προγραμματισμού. Στη συνέχεια, το PlusCal συγκεντρώνεται σε μια ευανάγνωστη προδιαγραφή TLA+. Αυτό δεν σημαίνει, φυσικά, ότι η σύνθετη προδιαγραφή PlusCal θα μετατραπεί σε απλή στο TLA+ - απλώς η αντιστοιχία μεταξύ τους είναι προφανής, δεν θα εμφανιστεί επιπλέον πολυπλοκότητα. Τέλος, αυτή η προδιαγραφή μπορεί να επαληθευτεί χρησιμοποιώντας εργαλεία TLA+. Γενικά, το PlusCal μπορεί να βοηθήσει να ξεπεραστεί μια φοβία για τα μαθηματικά· είναι εύκολο να το κατανοήσουν ακόμη και οι προγραμματιστές και οι επιστήμονες υπολογιστών. Δημοσίευσα αλγόριθμους για κάποιο διάστημα (περίπου 10 χρόνια) στο παρελθόν.
Ίσως κάποιος να αντιταχθεί ότι το TLA+ και το PlusCal είναι μαθηματικά και ότι τα μαθηματικά λειτουργούν μόνο με κατασκευασμένα παραδείγματα. Στην πράξη, χρειάζεστε μια πραγματική γλώσσα με τύπους, διαδικασίες, αντικείμενα κ.λπ. Αυτό είναι λάθος. Δείτε τι γράφει ο Chris Newcomb, ο οποίος εργαζόταν στην Amazon: «Χρησιμοποιήσαμε το TLA+ σε δέκα μεγάλα έργα και σε κάθε περίπτωση η χρήση του έκανε σημαντική διαφορά στην ανάπτυξη γιατί μπορέσαμε να συλλάβουμε επικίνδυνα σφάλματα προτού φτάσουν στην παραγωγή και επειδή μας έδωσε τη διορατικότητα και την αυτοπεποίθηση που χρειαζόμασταν για να κάνουμε επιθετικές βελτιστοποιήσεις απόδοσης χωρίς να επηρεάζουν την αλήθεια του προγράμματος". Μπορείτε συχνά να ακούσετε ότι όταν χρησιμοποιούμε επίσημες μεθόδους παίρνουμε αναποτελεσματικό κώδικα - στην πράξη, όλα είναι ακριβώς το αντίθετο. Επιπλέον, υπάρχει η αντίληψη ότι οι μάνατζερ δεν μπορούν να πειστούν για την ανάγκη για επίσημες μεθόδους, ακόμα κι αν οι προγραμματιστές είναι πεπεισμένοι για τη χρησιμότητά τους. Και ο Newcomb γράφει: «Οι διευθυντές πιέζουν τώρα με κάθε δυνατό τρόπο να γράψουν προδιαγραφές στο TLA+ και διαθέτουν ειδικά χρόνο για αυτό». Έτσι, όταν οι διαχειριστές βλέπουν ότι το TLA+ λειτουργεί, το ενστερνίζονται. Ο Chris Newcomb το έγραψε πριν από περίπου έξι μήνες (Οκτώβριος 2014), αλλά τώρα, από όσο ξέρω, το TLA+ χρησιμοποιείται σε 14 έργα, όχι σε 10. Ένα άλλο παράδειγμα σχετίζεται με τη σχεδίαση του XBox 360. Ένας ασκούμενος ήρθε στον Charles Thacker και έγραψε προδιαγραφές για το σύστημα μνήμης. Χάρη σε αυτήν την προδιαγραφή, εντοπίστηκε ένα σφάλμα που διαφορετικά δεν θα είχε εντοπιστεί και θα προκαλούσε τη συντριβή κάθε XBox 360 μετά από τέσσερις ώρες χρήσης. Οι μηχανικοί της IBM επιβεβαίωσαν ότι οι δοκιμές τους δεν θα είχαν εντοπίσει αυτό το σφάλμα.
Μπορείτε να διαβάσετε περισσότερα για το TLA+ στο Διαδίκτυο, αλλά τώρα ας μιλήσουμε για ανεπίσημες προδιαγραφές. Σπάνια χρειάζεται να γράψουμε προγράμματα που υπολογίζουν τον λιγότερο κοινό διαιρέτη και παρόμοια. Πολύ πιο συχνά γράφουμε προγράμματα όπως το εργαλείο όμορφου εκτυπωτή που έγραψα για το TLA+. Μετά την απλούστερη επεξεργασία, ο κωδικός TLA+ θα μοιάζει με αυτό:
Αλλά στο παραπάνω παράδειγμα, ο χρήστης πιθανότατα ήθελε να ευθυγραμμιστούν τα σύμβολα σύνδεσης και ίσου. Έτσι, η σωστή μορφοποίηση θα μοιάζει περισσότερο με αυτό:
Ας δούμε ένα άλλο παράδειγμα:
Εδώ, αντίθετα, η ευθυγράμμιση των ίσων, της πρόσθεσης και του πολλαπλασιασμού στην πηγή ήταν τυχαία, οπότε η απλούστερη επεξεργασία είναι αρκετά αρκετή. Γενικά, δεν υπάρχει ακριβής μαθηματικός ορισμός της σωστής μορφοποίησης, γιατί το "σωστό" σε αυτή την περίπτωση σημαίνει "αυτό που θέλει ο χρήστης" και αυτό δεν μπορεί να προσδιοριστεί μαθηματικά.
Φαίνεται ότι αν δεν έχουμε ορισμό της αλήθειας, τότε η προδιαγραφή είναι άχρηστη. Αλλά αυτό δεν είναι αλήθεια. Ακριβώς επειδή δεν ξέρουμε τι πρέπει να κάνει ένα πρόγραμμα δεν σημαίνει ότι δεν χρειάζεται να σκεφτόμαστε πώς πρέπει να λειτουργεί - αντίθετα, θα πρέπει να ξοδέψουμε ακόμη περισσότερη προσπάθεια σε αυτό. Η προδιαγραφή είναι ιδιαίτερα σημαντική εδώ. Είναι αδύνατο να προσδιορίσουμε το βέλτιστο πρόγραμμα για δομημένη εκτύπωση, αλλά αυτό δεν σημαίνει ότι δεν πρέπει να το αναλάβουμε καθόλου, και η σύνταξη κώδικα ως ροή συνείδησης δεν ισχύει. Κατέληξα να γράψω μια προδιαγραφή έξι κανόνων με ορισμούς με τη μορφή σχολίων σε αρχείο Java. Ακολουθεί ένα παράδειγμα ενός από τους κανόνες: a left-comment token is LeftComment aligned with its covering token. Αυτός ο κανόνας είναι γραμμένος, ας πούμε, στα μαθηματικά αγγλικά: LeftComment aligned, left-comment и covering token — όροι με ορισμούς. Έτσι περιγράφουν οι μαθηματικοί τα μαθηματικά: γράφουν ορισμούς όρων και, βάσει αυτών, δημιουργούν κανόνες. Το πλεονέκτημα αυτής της προδιαγραφής είναι ότι έξι κανόνες είναι πολύ πιο εύκολο να κατανοηθούν και να εντοπιστούν σφάλματα από 850 γραμμές κώδικα. Πρέπει να πω ότι η συγγραφή αυτών των κανόνων δεν ήταν εύκολη· χρειάστηκε πολύς χρόνος για να τους διορθώσετε. Έγραψα κώδικα ειδικά για αυτό το σκοπό που μου έλεγε ποιος κανόνας χρησιμοποιήθηκε. Επειδή δοκίμασα αυτούς τους έξι κανόνες με μερικά παραδείγματα, δεν χρειάστηκε να διορθώσω 850 γραμμές κώδικα και τα σφάλματα ήταν αρκετά εύκολο να βρεθούν. Η Java έχει εξαιρετικά εργαλεία για αυτό. Αν είχα μόλις γράψει τον κώδικα, θα μου έπαιρνε πολύ περισσότερο χρόνο και η μορφοποίηση θα ήταν πιο κακής ποιότητας.
Γιατί δεν μπορούσε να χρησιμοποιηθεί μια επίσημη προδιαγραφή; Από τη μία πλευρά, η σωστή εκτέλεση δεν είναι πολύ σημαντική εδώ. Μια δομημένη εκτύπωση είναι βέβαιο ότι δεν θα είναι ικανοποιητική για κάποιους, επομένως δεν χρειάστηκε να την κάνω να λειτουργεί σωστά σε όλες τις ασυνήθιστες καταστάσεις. Ακόμη πιο σημαντικό είναι το γεγονός ότι δεν είχα επαρκή εργαλεία. Ο έλεγχος μοντέλων TLA+ είναι άχρηστος εδώ, οπότε θα έπρεπε να γράψω τα παραδείγματα με το χέρι.
Η δεδομένη προδιαγραφή έχει χαρακτηριστικά κοινά σε όλες τις προδιαγραφές. Είναι υψηλότερο επίπεδο από τον κώδικα. Μπορεί να εφαρμοστεί σε οποιαδήποτε γλώσσα. Δεν υπάρχουν εργαλεία ή μέθοδοι για να το γράψετε. Κανένα μάθημα προγραμματισμού δεν θα σας βοηθήσει να γράψετε αυτήν την προδιαγραφή. Και δεν υπάρχουν εργαλεία που θα μπορούσαν να καταστήσουν περιττή αυτή την προδιαγραφή, εκτός εάν φυσικά γράφετε μια γλώσσα ειδικά για τη σύνταξη προγραμμάτων δομημένης εκτύπωσης στο TLA+. Τέλος, αυτή η προδιαγραφή δεν λέει τίποτα για το πώς ακριβώς θα γράψουμε τον κώδικα, απλώς δηλώνει τι κάνει ο κωδικός. Γράφουμε μια προδιαγραφή για να μας βοηθήσει να σκεφτούμε το πρόβλημα πριν αρχίσουμε να σκεφτόμαστε τον κώδικα.
Αλλά αυτή η προδιαγραφή έχει επίσης χαρακτηριστικά που τη διακρίνουν από άλλες προδιαγραφές. Το 95% των άλλων προδιαγραφών είναι πολύ πιο σύντομες και απλούστερες:
Επιπλέον, αυτή η προδιαγραφή είναι ένα σύνολο κανόνων. Αυτό είναι συνήθως σημάδι κακών προδιαγραφών. Η κατανόηση των συνεπειών ενός συνόλου κανόνων είναι αρκετά δύσκολη, γι' αυτό χρειάστηκε να αφιερώσω πολύ χρόνο για να τους διορθώσω. Ωστόσο, σε αυτή την περίπτωση δεν μπορούσα να βρω καλύτερο τρόπο.
Αξίζει να πούμε λίγα λόγια για προγράμματα που τρέχουν συνεχώς. Συνήθως λειτουργούν παράλληλα, όπως λειτουργικά συστήματα ή κατανεμημένα συστήματα. Πολύ λίγοι άνθρωποι μπορούν να τους καταλάβουν στο μυαλό τους ή στα χαρτιά, και δεν είμαι ένας από αυτούς, αν και κάποτε μπόρεσα να το κάνω. Επομένως, χρειαζόμαστε εργαλεία που θα ελέγχουν την εργασία μας - για παράδειγμα, TLA+ ή PlusCal.
Γιατί χρειάστηκε να γράψω μια προδιαγραφή, αν ήξερα ήδη τι πρέπει να κάνει ο κωδικός; Στην πραγματικότητα, νόμιζα μόνο ότι το ήξερα. Επιπλέον, με μια προδιαγραφή σε ισχύ, ένας ξένος δεν χρειάζεται πλέον να εξετάζει τον κώδικα για να καταλάβει τι ακριβώς κάνει. Έχω έναν κανόνα: δεν πρέπει να υπάρχουν γενικοί κανόνες. Υπάρχει μια εξαίρεση σε αυτόν τον κανόνα φυσικά, αυτός είναι ο μόνος γενικός κανόνας που ακολουθώ: η προδιαγραφή του τι κάνει ο κώδικας πρέπει να λέει στους ανθρώπους όλα όσα πρέπει να γνωρίζουν όταν χρησιμοποιούν αυτόν τον κώδικα.
Τι ακριβώς πρέπει να γνωρίζουν λοιπόν οι προγραμματιστές για τη σκέψη; Αρχικά, το ίδιο όπως για όλους: αν δεν γράφεις, τότε μόνο σου φαίνεται ότι σκέφτεσαι. Επίσης, πρέπει να σκεφτείτε πριν κωδικοποιήσετε, πράγμα που σημαίνει ότι πρέπει να γράψετε πριν κωδικοποιήσετε. Προδιαγραφή είναι αυτό που γράφουμε πριν ξεκινήσουμε την κωδικοποίηση. Απαιτείται μια προδιαγραφή για κάθε κωδικό που μπορεί να χρησιμοποιηθεί ή να αλλάξει από οποιονδήποτε. Και αυτός ο «κάποιος» μπορεί να αποδειχθεί ο συγγραφέας του κώδικα ένα μήνα μετά τη συγγραφή του. Απαιτείται μια προδιαγραφή για μεγάλα προγράμματα και συστήματα, για κλάσεις, για μεθόδους και μερικές φορές ακόμη και για πολύπλοκα τμήματα μιας μεμονωμένης μεθόδου. Τι ακριβώς πρέπει να γράψετε για τον κώδικα; Πρέπει να περιγράψετε τι κάνει, δηλαδή κάτι που μπορεί να είναι χρήσιμο σε οποιονδήποτε χρησιμοποιεί αυτόν τον κώδικα. Μερικές φορές μπορεί επίσης να είναι απαραίτητο να προσδιορίσετε πώς ακριβώς ο κώδικας επιτυγχάνει τον στόχο του. Αν περάσαμε από αυτή τη μέθοδο στο μάθημα αλγόριθμοι, τότε την ονομάζουμε αλγόριθμο. Αν είναι κάτι πιο εξειδικευμένο και νέο, τότε το λέμε design υψηλού επιπέδου. Δεν υπάρχει επίσημη διαφορά εδώ: και τα δύο είναι αφηρημένα μοντέλα του προγράμματος.
Πώς ακριβώς πρέπει να γράψετε μια προδιαγραφή κώδικα; Το κύριο πράγμα: θα πρέπει να είναι ένα επίπεδο υψηλότερο από τον ίδιο τον κώδικα. Πρέπει να περιγράφει καταστάσεις και συμπεριφορές. Θα πρέπει να είναι τόσο αυστηρό όσο απαιτεί η εργασία. Εάν γράφετε μια προδιαγραφή για τον τρόπο υλοποίησης μιας εργασίας, τότε μπορεί να γραφτεί σε ψευδοκώδικα ή χρησιμοποιώντας PlusCal. Πρέπει να μάθετε να γράφετε προδιαγραφές χρησιμοποιώντας επίσημες προδιαγραφές. Αυτό θα σας δώσει τις απαραίτητες δεξιότητες που θα βοηθήσουν και με τις άτυπες. Πώς μπορείτε να μάθετε να γράφετε επίσημες προδιαγραφές; Όταν μάθαμε να προγραμματίζουμε, γράφαμε προγράμματα και μετά τα διορθώσαμε. Το ίδιο πράγμα εδώ: πρέπει να γράψετε μια προδιαγραφή, να την ελέγξετε με έναν ελεγκτή μοντέλων και να διορθώσετε τα σφάλματα. Το TLA+ μπορεί να μην είναι η καλύτερη γλώσσα για μια επίσημη προδιαγραφή και μια άλλη γλώσσα θα ήταν πιθανότατα πιο κατάλληλη για τις συγκεκριμένες ανάγκες σας. Το υπέροχο με το TLA+ είναι ότι κάνει εξαιρετική δουλειά στη διδασκαλία της μαθηματικής σκέψης.
Πώς να συνδέσετε τις προδιαγραφές και τον κώδικα; Χρήση σχολίων που συνδέουν μαθηματικές έννοιες και την εφαρμογή τους. Εάν εργάζεστε με γραφήματα, τότε σε επίπεδο προγράμματος θα έχετε πίνακες κόμβων και πίνακες συνδέσμων. Πρέπει λοιπόν να γράψετε πώς ακριβώς υλοποιείται το γράφημα από αυτές τις δομές προγραμματισμού.
Θα πρέπει να σημειωθεί ότι τίποτα από τα παραπάνω δεν ισχύει για την ίδια τη διαδικασία σύνταξης κώδικα. Όταν γράφετε κώδικα, δηλαδή εκτελείτε το τρίτο βήμα, πρέπει επίσης να σκεφτείτε και να σκεφτείτε μέσα από το πρόγραμμα. Εάν μια δευτερεύουσα εργασία αποδειχθεί πολύπλοκη ή μη προφανής, πρέπει να γράψετε μια προδιαγραφή για αυτήν. Αλλά δεν μιλάω για τον ίδιο τον κώδικα εδώ. Μπορείτε να χρησιμοποιήσετε οποιαδήποτε γλώσσα προγραμματισμού, οποιαδήποτε μεθοδολογία, δεν πρόκειται για αυτούς. Επίσης, κανένα από τα παραπάνω δεν εξαλείφει την ανάγκη δοκιμής και εντοπισμού σφαλμάτων του κώδικά σας. Ακόμα κι αν το αφηρημένο μοντέλο είναι γραμμένο σωστά, μπορεί να υπάρχουν σφάλματα στην υλοποίησή του.
Η σύνταξη προδιαγραφών είναι ένα επιπλέον βήμα στη διαδικασία κωδικοποίησης. Χάρη σε αυτό, πολλά σφάλματα μπορούν να εντοπιστούν με λιγότερη προσπάθεια - το γνωρίζουμε από την εμπειρία των προγραμματιστών από την Amazon. Με τις προδιαγραφές, η ποιότητα των προγραμμάτων γίνεται υψηλότερη. Γιατί λοιπόν πάμε τόσο συχνά χωρίς αυτά; Γιατί το γράψιμο είναι δύσκολο. Αλλά το γράψιμο είναι δύσκολο, γιατί για αυτό πρέπει να σκεφτείς, και η σκέψη είναι επίσης δύσκολη. Είναι πάντα πιο εύκολο να προσποιηθείς ότι σκέφτεσαι. Εδώ μπορεί να γίνει μια αναλογία με το τρέξιμο - όσο λιγότερο τρέχεις, τόσο πιο αργά τρέχεις. Πρέπει να εκπαιδεύσετε τους μυς σας και να εξασκηθείτε στη γραφή. Χρειάζεται εξάσκηση.
Η προδιαγραφή μπορεί να είναι λανθασμένη. Μπορεί να έχετε κάνει κάπου λάθος ή να έχουν αλλάξει οι απαιτήσεις ή να χρειάζεται να γίνει κάποια βελτίωση. Οποιοσδήποτε κωδικός χρησιμοποιεί οποιοσδήποτε πρέπει να αλλάξει, οπότε αργά ή γρήγορα η προδιαγραφή δεν θα ταιριάζει πλέον με το πρόγραμμα. Στην ιδανική περίπτωση, σε αυτήν την περίπτωση, πρέπει να γράψετε μια νέα προδιαγραφή και να ξαναγράψετε εντελώς τον κώδικα. Ξέρουμε πολύ καλά ότι κανείς δεν το κάνει αυτό. Στην πράξη, επιδιορθώνουμε τον κώδικα και ίσως ενημερώνουμε τις προδιαγραφές. Εάν αυτό είναι βέβαιο ότι θα συμβεί αργά ή γρήγορα, τότε γιατί να γράψετε καθόλου προδιαγραφές; Πρώτον, για το άτομο που θα επεξεργαστεί τον κωδικό σας, κάθε επιπλέον λέξη στις προδιαγραφές θα αξίζει το βάρος της σε χρυσό και αυτό το άτομο μπορεί κάλλιστα να είστε εσείς. Συχνά κλωτσάω τον εαυτό μου επειδή δεν είμαι αρκετά συγκεκριμένος όταν επεξεργάζομαι τον κώδικά μου. Και γράφω περισσότερες προδιαγραφές παρά κώδικα. Επομένως, όταν επεξεργάζεστε τον κώδικα, η προδιαγραφή πρέπει πάντα να ενημερώνεται. Δεύτερον, με κάθε επεξεργασία ο κώδικας γίνεται χειρότερος, γίνεται πιο δύσκολο να διαβαστεί και να διατηρηθεί. Πρόκειται για αύξηση της εντροπίας. Αλλά αν δεν ξεκινήσετε με μια προδιαγραφή, τότε κάθε γραμμή που θα γράψετε θα είναι μια επεξεργασία και ο κώδικας θα είναι ογκώδης και δυσανάγνωστος από την αρχή.
Όπως είπε , καμία μάχη δεν κερδήθηκε σύμφωνα με ένα σχέδιο, και καμία μάχη δεν κερδήθηκε χωρίς σχέδιο. Και κάτι ήξερε για τις μάχες. Υπάρχει η άποψη ότι η σύνταξη προδιαγραφών είναι χάσιμο χρόνου. Μερικές φορές αυτό είναι αλήθεια και το έργο είναι τόσο απλό που δεν έχει νόημα να το σκεφτείς καλά. Αλλά θα πρέπει πάντα να θυμάστε ότι όταν σας συμβουλεύουν να μην γράφετε προδιαγραφές, σημαίνει ότι σας συμβουλεύουν να μην σκέφτεστε. Και αυτό πρέπει να το σκέφτεσαι κάθε φορά. Η σκέψη μέσα από μια εργασία δεν εγγυάται ότι δεν θα κάνετε λάθη. Όπως γνωρίζουμε, κανείς δεν εφηύρε ένα μαγικό ραβδί και ο προγραμματισμός είναι μια δύσκολη υπόθεση. Αλλά αν δεν σκεφτείς καλά την εργασία, είναι σίγουρο ότι θα κάνεις λάθη.
Μπορείτε να διαβάσετε περισσότερα για το TLA+ και το PlusCal σε έναν ειδικό ιστότοπο, μπορείτε να μεταβείτε εκεί από την αρχική μου σελίδα . Αυτό είναι όλο για μένα, ευχαριστώ για την προσοχή σας.
Να θυμάστε ότι πρόκειται για μετάφραση. Όταν γράφετε σχόλια, να θυμάστε ότι ο συγγραφέας δεν θα τα διαβάσει. Αν θέλετε πραγματικά να συνομιλήσετε με τον συγγραφέα, θα είναι στο συνέδριο Hydra 2019, που θα πραγματοποιηθεί στις 11-12 Ιουλίου 2019 στην Αγία Πετρούπολη. Μπορείτε να αγοράσετε εισιτήρια .
Πηγή: www.habr.com