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

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

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

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

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

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

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

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

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

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

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

इसके अलावा, Z3 समीकरणों को हल करता है, और क्रूर बल का उपयोग करके उनके मूल्यों का चयन नहीं करता है।
इसका मतलब यह है कि यह उत्तर ढूंढने में सक्षम है, यहां तक ​​कि उन मामलों में भी जहां इनपुट विकल्पों के 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) चरणों की आवश्यकता होती है।

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

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

समस्या की स्थितियाँ एवं उसका समाधानकिसान को एक भेड़िया, एक बकरी और गोभी को नदी के पार ले जाना है। किसान के पास एक नाव है जिसमें किसान के अलावा केवल एक ही वस्तु को रखा जा सकता है। यदि किसान उन्हें लावारिस छोड़ देगा तो भेड़िया बकरी को खा जाएगा और बकरी गोभी को खा जाएगी।

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

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 और पायथन में एक प्रतीकात्मक वीएम लिखना

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

स्रोत: www.habr.com