Κατά τη γνώμη μου, στον ρωσόφωνο τομέα του Διαδικτύου, το θέμα της επίσημης επαλήθευσης δεν καλύπτεται επαρκώς και υπάρχει ιδιαίτερα έλλειψη απλών και σαφών παραδειγμάτων.
Θα δώσω ένα παράδειγμα από μια ξένη πηγή, και θα προσθέσω τη δική μου λύση στο γνωστό πρόβλημα της διέλευσης ενός λύκου, μιας κατσίκας και ενός λάχανου στην άλλη άκρη του ποταμού.
Αλλά πρώτα, θα περιγράψω εν συντομία τι είναι η επίσημη επαλήθευση και γιατί χρειάζεται.
Η επίσημη επαλήθευση συνήθως σημαίνει τον έλεγχο ενός προγράμματος ή ενός αλγορίθμου χρησιμοποιώντας ένα άλλο.
Αυτό είναι απαραίτητο για να διασφαλιστεί ότι το πρόγραμμα συμπεριφέρεται όπως αναμένεται και επίσης να διασφαλιστεί η ασφάλειά του.
Η επίσημη επαλήθευση είναι το πιο ισχυρό μέσο εύρεσης και εξάλειψης τρωτών σημείων: σας επιτρέπει να βρείτε όλες τις υπάρχουσες τρύπες και σφάλματα σε ένα πρόγραμμα ή να αποδείξετε ότι δεν υπάρχουν.
Αξίζει να σημειωθεί ότι σε ορισμένες περιπτώσεις αυτό είναι αδύνατο, όπως στο πρόβλημα των 8 βασιλισσών με πλάτος σανίδας 1000 τετραγώνων: όλα καταλήγουν στην αλγοριθμική πολυπλοκότητα ή στο πρόβλημα διακοπής.
Ωστόσο, σε κάθε περίπτωση, θα ληφθεί μία από τις τρεις απαντήσεις: το πρόγραμμα είναι σωστό, λάθος ή δεν ήταν δυνατός ο υπολογισμός της απάντησης.
Εάν είναι αδύνατο να βρεθεί μια απάντηση, είναι συχνά δυνατό να ξαναδουλέψουμε ασαφή μέρη του προγράμματος, μειώνοντας την αλγοριθμική τους πολυπλοκότητα, προκειμένου να λάβουμε μια συγκεκριμένη απάντηση ναι ή όχι.
Και η επίσημη επαλήθευση χρησιμοποιείται, για παράδειγμα, στα λειτουργικά συστήματα πυρήνα Windows και Darpa drone, για να διασφαλιστεί το μέγιστο επίπεδο προστασίας.
Θα χρησιμοποιήσουμε το Z3Prover, ένα πολύ ισχυρό εργαλείο για αυτοματοποιημένη απόδειξη θεωρημάτων και επίλυση εξισώσεων.
Επιπλέον, το Z3 λύνει εξισώσεις και δεν επιλέγει τις τιμές τους χρησιμοποιώντας ωμή δύναμη.
Αυτό σημαίνει ότι μπορεί να βρει την απάντηση, ακόμη και σε περιπτώσεις που υπάρχουν 10^100 συνδυασμοί επιλογών εισαγωγής.
Αλλά αυτό είναι μόνο μια ντουζίνα ορίσματα εισόδου τύπου Integer, και αυτό συναντάται συχνά στην πράξη.
Πρόβλημα σχετικά με 8 βασίλισσες (Λήψη από τα αγγλικά ).
# We know each queen must be in a different row.
# So, we represent each queen by a single integer: the column position
Q = [ Int('Q_%i' % (i + 1)) for i in range(8) ]
# Each queen is in a column {1, ... 8 }
val_c = [ And(1 <= Q[i], Q[i] <= 8) for i in range(8) ]
# At most one queen per column
col_c = [ Distinct(Q) ]
# Diagonal constraint
diag_c = [ If(i == j,
True,
And(Q[i] - Q[j] != i - j, Q[i] - Q[j] != j - i))
for i in range(8) for j in range(i) ]
solve(val_c + col_c + diag_c)
Τρέχοντας το Z3, έχουμε τη λύση:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
Το πρόβλημα της βασίλισσας είναι συγκρίσιμο με ένα πρόγραμμα που παίρνει ως είσοδο τις συντεταγμένες 8 βασίλισσες και δίνει την απάντηση εάν οι βασίλισσες νικούν η μία την άλλη.
Εάν επρόκειτο να λύσουμε ένα τέτοιο πρόγραμμα χρησιμοποιώντας επίσημη επαλήθευση, τότε σε σύγκριση με το πρόβλημα, θα έπρεπε απλώς να κάνουμε ένα ακόμη βήμα με τη μορφή της μετατροπής του κώδικα προγράμματος σε εξίσωση: θα αποδεικνυόταν ότι είναι ουσιαστικά πανομοιότυπο με το δικό μας ( φυσικά, αν το πρόγραμμα ήταν γραμμένο σωστά).
Σχεδόν το ίδιο θα συμβεί και στην περίπτωση της αναζήτησης ευπαθειών: απλώς ορίζουμε τις συνθήκες εξόδου που χρειαζόμαστε, για παράδειγμα, τον κωδικό πρόσβασης διαχειριστή, μετατρέπουμε τον πηγαίο κώδικα ή τον απομεταγλωττισμένο κώδικα σε εξισώσεις συμβατές με την επαλήθευση και, στη συνέχεια, λαμβάνουμε μια απάντηση για το τι Τα δεδομένα πρέπει να παρέχονται ως δεδομένα για την επίτευξη του στόχου.
Κατά τη γνώμη μου, το πρόβλημα με τον λύκο, την κατσίκα και το λάχανο είναι ακόμα πιο ενδιαφέρον, αφού η επίλυσή του απαιτεί ήδη πολλά (7) βήματα.
Εάν το πρόβλημα της βασίλισσας είναι συγκρίσιμο με την περίπτωση όπου μπορείτε να διεισδύσετε σε έναν διακομιστή χρησιμοποιώντας ένα μόνο αίτημα GET ή POST, τότε ο λύκος, η κατσίκα και το λάχανο παρουσιάζουν ένα παράδειγμα από μια πολύ πιο περίπλοκη και διαδεδομένη κατηγορία, στην οποία ο στόχος μπορεί να επιτευχθεί μόνο από διάφορα αιτήματα.
Αυτό είναι συγκρίσιμο, για παράδειγμα, με ένα σενάριο όπου πρέπει να βρείτε μια ένεση SQL, να γράψετε ένα αρχείο μέσω αυτής, στη συνέχεια να αυξήσετε τα δικαιώματά σας και μόνο στη συνέχεια να λάβετε έναν κωδικό πρόσβασης.
Οι συνθήκες του προβλήματος και η επίλυσή τουΟ αγρότης πρέπει να μεταφέρει έναν λύκο, μια κατσίκα και λάχανο πέρα από το ποτάμι. Ο αγρότης έχει ένα σκάφος που μπορεί να φιλοξενήσει μόνο ένα αντικείμενο, εκτός από τον ίδιο τον αγρότη. Ο λύκος θα φάει το κατσίκι και η κατσίκα θα φάει το λάχανο αν ο αγρότης τα αφήσει χωρίς επίβλεψη.
Η λύση είναι ότι στο βήμα 4 ο αγρότης θα χρειαστεί να πάρει την κατσίκα πίσω.
Τώρα ας αρχίσουμε να το λύνουμε μέσω προγραμματισμού.
Ας υποδηλώσουμε τον αγρότη, τον λύκο, την κατσίκα και το λάχανο ως 4 μεταβλητές που παίρνουν την τιμή μόνο 0 ή 1. Το μηδέν σημαίνει ότι βρίσκονται στην αριστερή όχθη και το ένα σημαίνει ότι βρίσκονται στη δεξιά.
import json
from z3 import *
s = Solver()
Num= 8
Human = [ Int('Human_%i' % (i + 1)) for i in range(Num) ]
Wolf = [ Int('Wolf_%i' % (i + 1)) for i in range(Num) ]
Goat = [ Int('Goat_%i' % (i + 1)) for i in range(Num) ]
Cabbage = [ Int('Cabbage_%i' % (i + 1)) for i in range(Num) ]
# Each creature can be only on left (0) or right side (1) on every state
HumanSide = [ Or(Human[i] == 0, Human[i] == 1) for i in range(Num) ]
WolfSide = [ Or(Wolf[i] == 0, Wolf[i] == 1) for i in range(Num) ]
GoatSide = [ Or(Goat[i] == 0, Goat[i] == 1) for i in range(Num) ]
CabbageSide = [ Or(Cabbage[i] == 0, Cabbage[i] == 1) for i in range(Num) ]
Side = HumanSide+WolfSide+GoatSide+CabbageSide
Ο αριθμός είναι ο αριθμός των βημάτων που απαιτούνται για την επίλυση. Κάθε βήμα αντιπροσωπεύει την κατάσταση του ποταμού, του σκάφους και όλων των οντοτήτων.
Προς το παρόν, ας το επιλέξουμε τυχαία και με ένα περιθώριο, πάρουμε 10.
Κάθε οντότητα αντιπροσωπεύεται σε 10 αντίγραφα - αυτή είναι η αξία της σε καθένα από τα 10 βήματα.
Τώρα ας θέσουμε τις προϋποθέσεις για την έναρξη και τον τερματισμό.
Start = [ Human[0] == 0, Wolf[0] == 0, Goat[0] == 0, Cabbage[0] == 0 ]
Finish = [ Human[9] == 1, Wolf[9] == 1, Goat[9] == 1, Cabbage[9] == 1 ]
Στη συνέχεια ορίζουμε τις συνθήκες όπου ο λύκος τρώει την κατσίκα ή η κατσίκα το λάχανο, ως περιορισμούς στην εξίσωση.
(Με την παρουσία ενός αγρότη, η επιθετικότητα είναι αδύνατη)
# Wolf cant stand with goat, and goat with cabbage without human. Not 2, not 0 which means that they are one the same side
Safe = [ And( Or(Wolf[i] != Goat[i], Wolf[i] == Human[i]), Or(Goat[i] != Cabbage[i], Goat[i] == Human[i])) for i in range(Num) ]
Και τέλος, θα ορίσουμε όλες τις πιθανές ενέργειες του αγρότη κατά τη διέλευση από εκεί ή πίσω.
Μπορεί είτε να πάρει μαζί του έναν λύκο, μια κατσίκα ή ένα λάχανο, είτε να μην πάρει κανέναν, είτε να μην πλεύσει πουθενά.
Φυσικά, κανείς δεν μπορεί να περάσει χωρίς αγρότη.
Αυτό θα εκφραστεί από το γεγονός ότι κάθε επόμενη κατάσταση του ποταμού, του σκάφους και των οντοτήτων μπορεί να διαφέρει από την προηγούμενη μόνο με αυστηρά περιορισμένο τρόπο.
Όχι περισσότερα από 2 bit, και με πολλά άλλα όρια, αφού ο αγρότης μπορεί να μεταφέρει μόνο μία οντότητα τη φορά και δεν μπορούν να μείνουν όλες μαζί.
Travel = [ Or(
And(Human[i] == Human[i+1] + 1, Wolf[i] == Wolf[i+1] + 1, Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1]),
And(Human[i] == Human[i+1] + 1, Goat[i] == Goat[i+1] + 1, Wolf[i] == Wolf[i+1], Cabbage[i] == Cabbage[i+1]),
And(Human[i] == Human[i+1] + 1, Cabbage[i] == Cabbage[i+1] + 1, Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1]),
And(Human[i] == Human[i+1] - 1, Wolf[i] == Wolf[i+1] - 1, Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1]),
And(Human[i] == Human[i+1] - 1, Goat[i] == Goat[i+1] - 1, Wolf[i] == Wolf[i+1], Cabbage[i] == Cabbage[i+1]),
And(Human[i] == Human[i+1] - 1, Cabbage[i] == Cabbage[i+1] - 1, Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1]),
And(Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1])) for i in range(Num-1) ]
Ας τρέξουμε τη λύση.
solve(Side + Start + Finish + Safe + Travel)
Και παίρνουμε την απάντηση!
Ο Z3 βρήκε ένα συνεπές σύνολο καταστάσεων που ικανοποιεί όλες τις προϋποθέσεις.
Ένα είδος τετραδιάστατου καστ του χωροχρόνου.
Ας καταλάβουμε τι έγινε.
Βλέπουμε ότι στο τέλος όλοι πέρασαν, μόνο που στην αρχή ο αγρότης μας αποφάσισε να ξεκουραστεί, και στα πρώτα 2 βήματα δεν κολυμπάει πουθενά.
Human_2 = 0
Human_3 = 0
Αυτό υποδηλώνει ότι ο αριθμός των πολιτειών που επιλέξαμε είναι υπερβολικός και 8 θα είναι αρκετά επαρκείς.
Στην περίπτωσή μας, ο αγρότης έκανε αυτό: ξεκινήστε, ξεκουραστείτε, ξεκουραστείτε, σταύρωσε τη γίδα, σταύρωσε πίσω, σταύρωσε το λάχανο, επέστρεψε με την κατσίκα, σταύρωσε τον λύκο, επέστρεφε πίσω μόνος, ξαναπαράδωσε την κατσίκα.
Αλλά τελικά το πρόβλημα λύθηκε.
#Старт.
Human_1 = 0
Wolf_1 = 0
Goat_1 = 0
Cabbage_1 = 0
#Фермер отдыхает.
Human_2 = 0
Wolf_2 = 0
Goat_2 = 0
Cabbage_2 = 0
#Фермер отдыхает.
Human_3 = 0
Wolf_3 = 0
Goat_3 = 0
Cabbage_3 = 0
#Фермер отвозит козу на нужный берег.
Human_4 = 1
Wolf_4 = 0
Goat_4 = 1
Cabbage_4 = 0
#Фермер возвращается.
Human_5 = 0
Wolf_5 = 0
Goat_5 = 1
Cabbage_5 = 0
#Фермер отвозит капусту на нужный берег.
Human_6 = 1
Wolf_6 = 0
Cabbage_6 = 1
Goat_6 = 1
#Ключевая часть операции: фермер возвращает козу обратно.
Human_7 = 0
Wolf_7 = 0
Goat_7 = 0
Cabbage_7 = 1
#Фермер отвозит волка на другой берег, где он теперь находится вместе с капустой.
Human_8 = 1
Wolf_8 = 1
Goat_8 = 0
Cabbage_8 = 1
#Фермер возвращается за козой.
Human_9 = 0
Wolf_9 = 1
Goat_9 = 0
Cabbage_9 = 1
#Фермер повторно доставляет козу на нужный берег и завершают переправу.
Human_10 = 1
Wolf_10 = 1
Goat_10 = 1
Cabbage_10 = 1
Τώρα ας προσπαθήσουμε να αλλάξουμε τις συνθήκες και να αποδείξουμε ότι δεν υπάρχουν λύσεις.
Για να γίνει αυτό, θα δώσουμε στον λύκο μας φυτοφάρμακο και θα θέλει να φάει λάχανο.
Αυτό μπορεί να συγκριθεί με την περίπτωση που στόχος μας είναι να εξασφαλίσουμε την εφαρμογή και πρέπει να βεβαιωθούμε ότι δεν υπάρχουν κενά.
Safe = [ And( Or(Wolf[i] != Goat[i], Wolf[i] == Human[i]), Or(Goat[i] != Cabbage[i], Goat[i] == Human[i]), Or(Wolf[i] != Cabbage[i], Goat[i] == Human[i])) for i in range(Num) ]
Το Z3 μας έδωσε την εξής απάντηση:
no solution
Σημαίνει ότι πραγματικά δεν υπάρχουν λύσεις.
Έτσι αποδείξαμε προγραμματικά την αδυναμία διασταύρωσης με παμφάγο λύκο χωρίς απώλειες για τον αγρότη.
Εάν το κοινό βρίσκει ενδιαφέρον αυτό το θέμα, τότε σε μελλοντικά άρθρα θα σας πω πώς να μετατρέψετε ένα συνηθισμένο πρόγραμμα ή λειτουργία σε εξίσωση συμβατή με επίσημες μεθόδους και να το λύσετε, αποκαλύπτοντας έτσι όλα τα νόμιμα σενάρια και τα τρωτά σημεία. Πρώτα, στην ίδια εργασία, αλλά παρουσιάζεται με τη μορφή προγράμματος, και στη συνέχεια περιπλέκεται σταδιακά και προχωρά σε τρέχοντα παραδείγματα από τον κόσμο της ανάπτυξης λογισμικού.
Το επόμενο άρθρο είναι ήδη έτοιμο:
Σε αυτό μετακινούμαι από την επίσημη επαλήθευση προβλημάτων στα προγράμματα και περιγράφω
πώς μπορούν να μετατραπούν αυτόματα σε επίσημα συστήματα κανόνων.
Πηγή: www.habr.com