भेड़िया, बकरी और गोभी की समस्या के उदाहरण पर औपचारिक सत्यापन

मेरी राय में, इंटरनेट के रूसी भाषी क्षेत्र में, औपचारिक सत्यापन का विषय पर्याप्त रूप से कवर नहीं किया गया है, और विशेष रूप से सरल और स्पष्ट उदाहरणों की कमी है।

मैं एक विदेशी स्रोत से इस तरह का एक उदाहरण दूंगा, और अपने स्वयं के समाधान को एक भेड़िये, बकरी और गोभी को नदी के दूसरी ओर ले जाने की अच्छी तरह से ज्ञात समस्या का पूरक बनूंगा।

लेकिन पहले, मैं संक्षेप में बताऊंगा कि औपचारिक सत्यापन क्या है और इसकी आवश्यकता क्यों है।

औपचारिक सत्यापन का अर्थ आमतौर पर एक प्रोग्राम या एल्गोरिथ्म को दूसरे का उपयोग करके जांचना होता है।

यह सुनिश्चित करने के लिए आवश्यक है कि कार्यक्रम का व्यवहार अपेक्षा के अनुरूप हो, और इसकी सुरक्षा भी सुनिश्चित हो।

औपचारिक सत्यापन कमजोरियों को खोजने और समाप्त करने का सबसे शक्तिशाली साधन है: यह आपको कार्यक्रम में सभी मौजूदा छेद और बग्स को खोजने या यह साबित करने की अनुमति देता है कि वे वहां नहीं हैं।
यह ध्यान देने योग्य है कि कुछ मामलों में यह असंभव है, जैसे कि 1000 कोशिकाओं की बोर्ड चौड़ाई के साथ 8 रानियों की समस्या में: सब कुछ एल्गोरिथम जटिलता या रुकने की समस्या पर निर्भर करता है।

हालांकि, किसी भी मामले में, तीन में से एक उत्तर प्राप्त होगा: कार्यक्रम सही है, गलत है, या उत्तर की गणना नहीं की जा सकती है।

यदि कोई उत्तर खोजना असंभव है, तो कार्यक्रम में अस्पष्ट स्थानों को फिर से बनाना संभव है, एक विशिष्ट उत्तर प्राप्त करने के लिए उनकी एल्गोरिथ्म जटिलता को कम करने के लिए, हां या नहीं।

और औपचारिक सत्यापन का उपयोग किया जाता है, उदाहरण के लिए, विंडोज कर्नेल और डारपा ड्रोन ऑपरेटिंग सिस्टम में, अधिकतम स्तर की सुरक्षा प्रदान करने के लिए।

हम Z3Prover का उपयोग करेंगे, प्रमेयों के स्वचालित प्रमाण और समीकरणों को हल करने के लिए एक बहुत शक्तिशाली उपकरण।

इसके अलावा, जेड 3 बिल्कुल समीकरणों को हल करता है, और जानवर बल के साथ उनके मूल्यों का चयन नहीं करता है।
इसका मतलब है कि वह उन जवाबों को खोजने में सक्षम है, यहां तक ​​कि उन मामलों में भी जहां इनपुट विकल्प और 10 ^ 100 के संयोजन।

लेकिन यह केवल एक दर्जन इनपुट प्रकार के पूर्णांक के बारे में है, और यह अक्सर व्यवहार में पाया जाता है।

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) कदम पहले से ही आवश्यक हैं।

यदि आप एक जीईटी या पीओटीएस अनुरोध का उपयोग करके सर्वर में प्रवेश कर सकते हैं तो रानियों के कार्य की तुलना तुलनीय है, तो भेड़िया, बकरी और गोभी एक बहुत अधिक जटिल और व्यापक श्रेणी से एक उदाहरण प्रदर्शित करते हैं जिसमें केवल कुछ अनुरोधों तक पहुंचा जा सकता है।

यह तुलनीय है, उदाहरण के लिए, उस परिदृश्य के साथ जहां आपको एसक्यूएल इंजेक्शन खोजने की आवश्यकता है, इसके माध्यम से एक फ़ाइल लिखें, फिर अपने अधिकारों को बढ़ाएं और उसके बाद ही पासवर्ड प्राप्त करें।


अब समाधान को प्रोग्रामेटिक रूप से शुरू करते हैं।

हम किसान, भेड़िया, बकरी और गोभी को 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 बिट्स से अधिक नहीं, और कई अन्य सीमाओं के साथ, क्योंकि किसान केवल एक समय में एक इकाई का परिवहन कर सकता है और सभी को एक साथ नहीं छोड़ा जा सकता है।

 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 

इसका मतलब है कि वास्तव में कोई समाधान नहीं हैं।

इस प्रकार, हमने प्रोग्रामर को किसान के लिए नुकसान के बिना, एक सर्वाहारी भेड़िया के साथ पार करने की असंभवता साबित कर दी है।

यदि दर्शकों को यह विषय दिलचस्प लगता है, तो भविष्य के लेखों में मैं आपको बताऊंगा कि कैसे एक साधारण कार्यक्रम या फ़ंक्शन को औपचारिक तरीकों के साथ संगत समीकरण में बदल दें और इसे हल करें, जिससे सभी वैध परिदृश्य और कमजोरियां दोनों का पता चलता है। सबसे पहले, एक ही कार्य पर, लेकिन पहले से ही एक कार्यक्रम के रूप में प्रस्तुत किया गया, और फिर धीरे-धीरे जटिल हो गया और सॉफ्टवेयर विकास की दुनिया से प्रासंगिक उदाहरणों पर आगे बढ़ रहा है।

निम्नलिखित लेख तैयार है:
खरोंच से एक औपचारिक सत्यापन प्रणाली बनाना: हम PHP और पायथन में एक चरित्र वीएम लिखते हैं

इसमें, मैं कार्यों के औपचारिक सत्यापन से कार्यक्रमों तक जाता हूं, और वर्णन करता हूं
स्वचालित रूप से उन्हें औपचारिक नियम प्रणालियों में कैसे परिवर्तित किया जाए।