🥇शुरुआत से एक औपचारिक सत्यापन प्रणाली बनाना। भाग 1: PHP और पायथन में कैरेक्टर वर्चुअल मशीन

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

यह सबसे शक्तिशाली तरीकों में से एक है जो आपको किसी प्रोग्राम में सभी कमजोरियों को खोजने या यह साबित करने की अनुमति देता है कि वे मौजूद नहीं हैं।

औपचारिक सत्यापन का अधिक विस्तृत विवरण समस्या के समाधान के उदाहरण में देखा जा सकता है भेड़िया, बकरी, और गोभी मेरे पिछले लेख में.

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

ऐसा करने के लिए, मैंने प्रतीकात्मक सिद्धांतों का उपयोग करते हुए एक वर्चुअल मशीन का अपना एनालॉग लिखा।

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

चूँकि प्रतीकात्मक गणनाओं के बारे में जानकारी इंटरनेट पर खंडित रूप से प्रस्तुत की जाती है,
मैं संक्षेप में बताऊंगा कि यह क्या है।

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

उदाहरण के लिए, हम इनपुट स्थितियाँ निर्धारित कर सकते हैं जहाँ पहला तर्क कोई भी सकारात्मक मान ले सकता है, दूसरा नकारात्मक, तीसरा शून्य और आउटपुट तर्क, उदाहरण के लिए, 42।

एक बार में प्रतीकात्मक गणना हमें यह उत्तर देगी कि क्या हमारे लिए वांछित परिणाम प्राप्त करना और ऐसे इनपुट मापदंडों के एक सेट का उदाहरण प्राप्त करना संभव है। या सबूत है कि ऐसे कोई पैरामीटर नहीं हैं।

इसके अलावा, हम इनपुट तर्कों को सभी संभावित तर्कों पर सेट कर सकते हैं, और केवल आउटपुट तर्कों का चयन कर सकते हैं, उदाहरण के लिए, व्यवस्थापक पासवर्ड।

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

यह ध्यान दिया जा सकता है कि विशिष्ट इनपुट डेटा के साथ किसी प्रोग्राम का शास्त्रीय निष्पादन प्रतीकात्मक निष्पादन का एक विशेष मामला है।

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

पिछले लेख की टिप्पणियों में इसकी कमजोरियों की चर्चा के साथ औपचारिक सत्यापन की निष्पक्ष आलोचना पाई जा सकती है।

मुख्य समस्याएँ हैं:

संयुक्त विस्फोट, चूँकि औपचारिक सत्यापन अंततः P=NP पर आ जाता है
फ़ाइल सिस्टम, नेटवर्क और अन्य बाह्य संग्रहण पर कॉल संसाधित करना सत्यापित करना अधिक कठिन है
विनिर्देश में बग, जब ग्राहक या प्रोग्रामर एक चीज़ का इरादा रखते थे, लेकिन तकनीकी विनिर्देश में इसका पर्याप्त सटीक वर्णन नहीं करते थे।

परिणामस्वरूप, प्रोग्राम सत्यापित हो जाएगा और विनिर्देशों का अनुपालन करेगा, लेकिन यह रचनाकारों की अपेक्षा से बिल्कुल अलग कुछ करेगा।

चूंकि इस लेख में मैं मुख्य रूप से व्यवहार में औपचारिक सत्यापन के उपयोग पर विचार कर रहा हूं, मैं अभी दीवार के खिलाफ अपना सिर नहीं फोड़ूंगा, और एक ऐसी प्रणाली चुनूंगा जहां एल्गोरिदम जटिलता और बाहरी कॉल की संख्या न्यूनतम हो।

चूंकि स्मार्ट कॉन्ट्रैक्ट इन आवश्यकताओं के लिए सबसे उपयुक्त हैं, इसलिए विकल्प वेव्स प्लेटफ़ॉर्म से RIDE कॉन्ट्रैक्ट्स पर गिर गया: वे ट्यूरिंग पूर्ण नहीं हैं, और उनकी अधिकतम जटिलता कृत्रिम रूप से सीमित है।

लेकिन हम उन पर विशेष रूप से तकनीकी पक्ष से विचार करेंगे।

सब कुछ के अलावा, औपचारिक सत्यापन विशेष रूप से किसी भी अनुबंध की मांग में होगा: लॉन्च होने के बाद अनुबंध त्रुटि को ठीक करना आमतौर पर असंभव है।
और ऐसी त्रुटियों की लागत बहुत अधिक हो सकती है, क्योंकि स्मार्ट अनुबंधों पर अक्सर बड़ी मात्रा में धनराशि संग्रहीत की जाती है।

मेरी प्रतीकात्मक वर्चुअल मशीन PHP और Python में लिखी गई है, और परिणामी SMT फ़ार्मुलों को हल करने के लिए Microsoft रिसर्च से Z3Prover का उपयोग करती है।

इसके मूल में एक शक्तिशाली बहु-लेन-देन संबंधी खोज है, जो
आपको समाधान या कमजोरियाँ ढूंढने की अनुमति देता है, भले ही इसके लिए कई लेन-देन की आवश्यकता हो।
और भी मिथकएथेरियम की कमजोरियों को खोजने के लिए सबसे शक्तिशाली प्रतीकात्मक रूपरेखाओं में से एक, इस क्षमता को कुछ महीने पहले ही जोड़ा गया था।

लेकिन यह ध्यान देने योग्य है कि ईथर अनुबंध अधिक जटिल और ट्यूरिंग पूर्ण हैं।

PHP RIDE स्मार्ट कॉन्ट्रैक्ट के स्रोत कोड को एक पायथन स्क्रिप्ट में अनुवादित करता है, जिसमें प्रोग्राम को अनुबंध राज्यों और उनके संक्रमणों के लिए Z3 SMT-संगत प्रणाली के रूप में प्रस्तुत किया जाता है:

अब मैं विस्तार से बताऊंगा कि अंदर क्या हो रहा है।

लेकिन पहले, RIDE स्मार्ट कॉन्ट्रैक्ट भाषा के बारे में कुछ शब्द।

यह एक कार्यात्मक और अभिव्यक्ति-आधारित प्रोग्रामिंग भाषा है जो डिजाइन में आलसी है।
RIDE ब्लॉकचेन के भीतर अलगाव में चलता है और उपयोगकर्ता के वॉलेट से जुड़े स्टोरेज से जानकारी प्राप्त और लिख सकता है।

आप प्रत्येक वॉलेट में एक RIDE अनुबंध संलग्न कर सकते हैं, और निष्पादन का परिणाम केवल TRUE या FALSE होगा।

सत्य का अर्थ है कि स्मार्ट अनुबंध लेनदेन की अनुमति देता है, और गलत का अर्थ है कि यह इसे प्रतिबंधित करता है।
एक सरल उदाहरण: यदि वॉलेट बैलेंस 100 से कम है तो एक स्क्रिप्ट स्थानांतरण पर रोक लगा सकती है।

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

उपयोगकर्ता उस वॉलेट से पैसे नहीं निकाल पाएगा जिस पर अनुबंध तैनात है जब तक कि वह सभी को दूसरी तरफ नहीं भेज देता।

#Извлекаем положение всех объектов из блокчейна
let contract = tx.sender
let human= extract(getInteger(contract,"human"))
let wolf= extract(getInteger(contract,"wolf"))
let goat= extract(getInteger(contract,"goat"))
let cabbage= extract(getInteger(contract,"cabbage"))

#Это так называемая дата-транзакция, в которой пользователь присылает новые 4 переменные.
#Контракт разрешит её только в случае если все объекты останутся в сохранности.
match tx {
case t:DataTransaction =>
   #Извлекаем будущее положение всех объектов из транзакции
   let newHuman= extract(getInteger(t.data,"human")) 
   let newWolf= extract(getInteger(t.data,"wolf"))
   let newGoat= extract(getInteger(t.data,"goat"))
   let newCabbage= extract(getInteger(t.data,"cabbage"))
   
   #0 обозначает, что объект на левом берегу, а 1 что на правом
   let humanSide= human == 0 || human == 1
   let wolfSide= wolf == 0 || wolf == 1
   let goatSide= goat == 0 || goat == 1
   let cabbageSide= cabbage == 0 || cabbage == 1
   let side= humanSide && wolfSide && goatSide && cabbageSide

   #Будут разрешены только те транзакции, где с козой никого нет в отсутствии фермера.
   let safeAlone= newGoat != newWolf && newGoat != newCabbage
   let safe= safeAlone || newGoat == newHuman
   let humanTravel= human != newHuman 

   #Способы путешествия фермера туда и обратно, с кем-то либо в одиночку.
   let t1= humanTravel && newWolf == wolf + 1 && newGoat == goat && newCabbage == cabbage 
   let t2= humanTravel && newWolf == wolf && newGoat == goat + 1 && newCabbage == cabbage
   let t3= humanTravel && newWolf == wolf && newGoat == goat && newCabbage == cabbage + 1
   let t4= humanTravel && newWolf == wolf - 1 && newGoat == goat && newCabbage == cabbage
   let t5= humanTravel && newWolf == wolf && newGoat == goat - 1 && newCabbage == cabbage
   let t6= humanTravel && newWolf == wolf && newGoat == goat && newCabbage == cabbage - 1
   let t7= humanTravel && newWolf == wolf && newGoat == goat && newCabbage == cabbage
   let objectTravel = t1 || t2 || t3 || t4 || t5 || t6 || t7
   
   #Последняя строка в разделе транзакции описывает разрешающее транзакцию условие.
   #Переменные транзакции должны иметь значения 1 или 0, все объекты должны
   #быть в безопасности, а фермер должен переплывать реку в одиночку 
   #или с кем-то на каждом шагу
   side && safe && humanTravel && objectTravel
case s:TransferTransaction =>
   #Транзакция вывода средств разрешена только в случае если все переплыли на другой берег
   human == 1 && wolf == 1 && goat == 1 && cabbage == 1

#Все прочие типы транзакций запрещены
case _ => false

}

PHP पहले स्मार्ट कॉन्ट्रैक्ट से सभी वेरिएबल्स को उनकी कुंजियों और संबंधित बूलियन एक्सप्रेशन वेरिएबल के रूप में निकालता है।

cabbage: extract ( getInteger ( contract , "cabbage" ) )
goat: extract ( getInteger ( contract , "goat" ) )
human: extract ( getInteger ( contract , "human" ) )
wolf: extract ( getInteger ( contract , "wolf" ) )
fState: human== 1 && wolf== 1 && goat== 1 && cabbage== 1
fState: 
wolf: 
goat: 
cabbage: 
cabbageSide: cabbage== 0 || cabbage== 1
human: extract ( getInteger ( contract , "human" ) )
newGoat: extract ( getInteger ( t.data , "goat" ) )
newHuman: extract ( getInteger ( t.data , "human" ) )
goatSide: goat== 0 || goat== 1
humanSide: human== 0 || human== 1
t7: humanTravel && newWolf== wolf && newGoat== goat && newCabbage== cabbage
t3: humanTravel && newWolf== wolf && newGoat== goat && newCabbage== cabbage + 1
t6: humanTravel && newWolf== wolf && newGoat== goat && newCabbage== cabbage - 1
t2: humanTravel && newWolf== wolf && newGoat== goat + 1 && newCabbage== cabbage
t5: humanTravel && newWolf== wolf && newGoat== goat - 1 && newCabbage== cabbage
t1: humanTravel && newWolf== wolf + 1 && newGoat== goat && newCabbage== cabbage
t4: humanTravel && newWolf== wolf - 1 && newGoat== goat && newCabbage== cabbage
safeAlone: newGoat != newWolf && newGoat != newCabbage
wolfSide: wolf== 0 || wolf== 1
humanTravel: human != newHuman
side: humanSide && wolfSide && goatSide && cabbageSide
safe: safeAlone || newGoat== newHuman
objectTravel: t1 || t2 || t3 || t4 || t5 || t6 || t7

PHP फिर उन्हें Python में Z3Prover SMT-संगत सिस्टम विवरण में परिवर्तित करता है।
डेटा को एक लूप में लपेटा जाता है, जहां स्टोरेज वैरिएबल इंडेक्स i, ट्रांजैक्शन वैरिएबल इंडेक्स i + 1 प्राप्त करते हैं, और एक्सप्रेशन वाले वेरिएबल पिछली स्थिति से अगली स्थिति में संक्रमण के लिए नियम निर्धारित करते हैं।

यह हमारी वर्चुअल मशीन का हृदय है, जो एक बहु-लेनदेन खोज तंत्र प्रदान करता है।

fState:  And( And( And( human[Steps]  ==  1 , wolf[Steps]  ==  1 )  , goat[Steps]  ==  1 )  , cabbage[Steps]  ==  1 )  
final:  fState[Steps] 
fState:   
wolf:   
goat:   
cabbage:   
cabbageSide:  Or( cabbage[i]  ==  0 , cabbage[i]  ==  1 )  
goatSide:  Or( goat[i]  ==  0 , goat[i]  ==  1 )  
humanSide:  Or( human[i]  ==  0 , human[i]  ==  1 )  
t7:  And( And( And( humanTravel[i] , wolf  ==  wolf[i] )  , goat[i+1]  ==  goat[i] )  , cabbage  ==  cabbage[i] )  
t3:  And( And( And( humanTravel[i] , wolf  ==  wolf[i] )  , goat[i+1]  ==  goat[i] )  , cabbage  ==  cabbage[i] + 1 )  
t6:  And( And( And( humanTravel[i] , wolf  ==  wolf[i] )  , goat[i+1]  ==  goat[i] )  , cabbage  ==  cabbage[i] - 1 )  
t2:  And( And( And( humanTravel[i] , wolf  ==  wolf[i] )  , goat[i+1]  ==  goat[i] + 1 )  , cabbage  ==  cabbage[i] )  
t5:  And( And( And( humanTravel[i] , wolf  ==  wolf[i] )  , goat[i+1]  ==  goat[i] - 1 )  , cabbage  ==  cabbage[i] )  
t1:  And( And( And( humanTravel[i] , wolf  ==  wolf[i] + 1 )  , goat[i+1]  ==  goat[i] )  , cabbage  ==  cabbage[i] )  
t4:  And( And( And( humanTravel[i] , wolf  ==  wolf[i] - 1 )  , goat[i+1]  ==  goat[i] )  , cabbage  ==  cabbage[i] )  
safeAlone:  And( goat[i+1] != wolf , goat[i+1] != cabbage )  
wolfSide:  Or( wolf[i]  ==  0 , wolf[i]  ==  1 )  
humanTravel:  human[i] != human[i+1] 
side:  And( And( And( humanSide[i] , wolfSide[i] )  , goatSide[i] )  , cabbageSide[i] )  
safe:  Or( safeAlone[i] , goat[i+1]  ==  human[i+1] )  
objectTravel:  Or( Or( Or( Or( Or( Or( t1[i] , t2[i] )  , t3[i] )  , t4[i] )  , t5[i] )  , t6[i] )  , t7[i] )  
data:  And( And( And( side[i] , safe[i] )  , humanTravel[i] )  , objectTravel[i] )

शर्तों को क्रमबद्ध किया जाता है और पायथन में एसएमटी प्रणाली का वर्णन करने के लिए डिज़ाइन किए गए स्क्रिप्ट टेम्पलेट में डाला जाता है।

रिक्त टेम्पलेट


import json

from z3 import *

s = Solver()

  
  
    
Steps=7
Num= Steps+1

$code$



#template, only start rest
s.add(data + start)

#template
s.add(final)




ind = 0

f = open("/var/www/html/all/bin/python/log.txt", "a")



while s.check() == sat:
  ind = ind +1
  

  print ind
  m = s.model()
  print m

  print "traversing model..." 
  #for d in m.decls():
	#print "%s = %s" % (d.name(), m[d])

  
 
  f.write(str(m))
  f.write("nn")
  exit()
  #s.add(Or(goat[0] != s.model()[data[0]] )) # prevent next model from using the same assignment as a previous model



print "Total solution number: "
print ind  

f.close()

संपूर्ण श्रृंखला में अंतिम स्थिति के लिए, स्थानांतरण लेनदेन अनुभाग में निर्दिष्ट नियम लागू होते हैं।

इसका मतलब यह है कि Z3Prover शर्तों के सटीक सेट की तलाश करेगा जो अंततः अनुबंध से धन निकालने की अनुमति देगा।

परिणामस्वरूप, हमें स्वचालित रूप से हमारे अनुबंध का पूर्णतः कार्यात्मक एसएमटी मॉडल प्राप्त होता है।
आप देख सकते हैं कि यह मेरे पिछले लेख के मॉडल से काफी मिलता-जुलता है, जिसे मैंने मैन्युअल रूप से संकलित किया था।

पूर्ण टेम्पलेट


import json

from z3 import *

s = Solver()

  
  
    
Steps=7
Num= Steps+1

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) ]
nothing= [  And( human[i] == human[i+1], wolf[i] == wolf[i+1], goat[i] == goat[i+1], cabbage[i] == cabbage[i+1] )   for i in range(Num-1) ]


start= [ human[0] == 1, wolf[0] == 0, goat[0] == 1, cabbage[0] == 0 ]

safeAlone= [  And( goat[i+1] != wolf[i+1] , goat[i+1] != cabbage[i+1] )   for i in range(Num-1) ]
safe= [  Or( safeAlone[i] , goat[i+1]  ==  human[i+1] )   for i in range(Num-1) ]
humanTravel= [  human[i] != human[i+1]  for i in range(Num-1) ]
cabbageSide= [  Or( cabbage[i]  ==  0 , cabbage[i]  ==  1 )   for i in range(Num-1) ]
goatSide= [  Or( goat[i]  ==  0 , goat[i]  ==  1 )   for i in range(Num-1) ]
humanSide= [  Or( human[i]  ==  0 , human[i]  ==  1 )   for i in range(Num-1) ]
t7= [  And( And( And( humanTravel[i] , wolf[i+1]  ==  wolf[i] )  , goat[i+1]  ==  goat[i] )  , cabbage[i+1]  ==  cabbage[i] )   for i in range(Num-1) ]
t3= [  And( And( And( humanTravel[i] , wolf[i+1]  ==  wolf[i] )  , goat[i+1]  ==  goat[i] )  , cabbage[i+1]  ==  cabbage[i] + 1 )   for i in range(Num-1) ]
t6= [  And( And( And( humanTravel[i] , wolf[i+1]  ==  wolf[i] )  , goat[i+1]  ==  goat[i] )  , cabbage[i+1]  ==  cabbage[i] - 1 )   for i in range(Num-1) ]
t2= [  And( And( And( humanTravel[i] , wolf[i+1]  ==  wolf[i] )  , goat[i+1]  ==  goat[i] + 1 )  , cabbage[i+1]  ==  cabbage[i] )   for i in range(Num-1) ]
t5= [  And( And( And( humanTravel[i] , wolf[i+1]  ==  wolf[i] )  , goat[i+1]  ==  goat[i] - 1 )  , cabbage[i+1]  ==  cabbage[i] )   for i in range(Num-1) ]
t1= [  And( And( And( humanTravel[i] , wolf[i+1]  ==  wolf[i] + 1 )  , goat[i+1]  ==  goat[i] )  , cabbage[i+1]  ==  cabbage[i] )   for i in range(Num-1) ]
t4= [  And( And( And( humanTravel[i] , wolf[i+1]  ==  wolf[i] - 1 )  , goat[i+1]  ==  goat[i] )  , cabbage[i+1]  ==  cabbage[i] )   for i in range(Num-1) ]
wolfSide= [  Or( wolf[i]  ==  0 , wolf[i]  ==  1 )   for i in range(Num-1) ]
side= [  And( And( And( humanSide[i] , wolfSide[i] )  , goatSide[i] )  , cabbageSide[i] )   for i in range(Num-1) ]
objectTravel= [  Or( Or( Or( Or( Or( Or( t1[i] , t2[i] )  , t3[i] )  , t4[i] )  , t5[i] )  , t6[i] )  , t7[i] )   for i in range(Num-1) ]
data= [ Or(  And( And( And( side[i] , safe[i] )  , humanTravel[i] )  , objectTravel[i] )   , nothing[i]) for i in range(Num-1) ]


fState=  And( And( And( human[Steps]  ==  1 , wolf[Steps]  ==  1 )  , goat[Steps]  ==  1 )  , cabbage[Steps]  ==  1 )  
final=  fState 




#template, only start rest
s.add(data + start)

#template
s.add(final)




ind = 0

f = open("/var/www/html/all/bin/python/log.txt", "a")



while s.check() == sat:
  ind = ind +1
  

  print ind
  m = s.model()
  print m

  print "traversing model..." 
  #for d in m.decls():
	#print "%s = %s" % (d.name(), m[d])

  
 
  f.write(str(m))
  f.write("nn")
  exit()
  #s.add(Or(goat[0] != s.model()[data[0]] )) # prevent next model from using the same assignment as a previous model



print "Total solution number: "
print ind  

f.close()

लॉन्च के बाद, Z3Pover स्मार्ट अनुबंध को हल करता है और हमें लेनदेन की एक श्रृंखला प्रदान करता है जो हमें धन निकालने की अनुमति देगा:

Winning transaction chain found:
Data transaction: human= 0, wolf= 0, goat= 1, cabbage= 0
Data transaction: human= 1, wolf= 0, goat= 1, cabbage= 1
Data transaction: human= 0, wolf= 0, goat= 0, cabbage= 1
Data transaction: human= 1, wolf= 1, goat= 0, cabbage= 1
Data transaction: human= 0, wolf= 1, goat= 0, cabbage= 1
Data transaction: human= 1, wolf= 1, goat= 1, cabbage= 1
Data transaction: human= 1, wolf= 1, goat= 1, cabbage= 1
Transfer transaction

नौका अनुबंध के अलावा, आप अपने स्वयं के अनुबंधों के साथ प्रयोग कर सकते हैं या इस सरल उदाहरण को आज़मा सकते हैं, जो 2 लेनदेन में हल हो जाता है।

let contract = tx.sender
let a= extract(getInteger(contract,"a"))
let b= extract(getInteger(contract,"b"))
let c= extract(getInteger(contract,"c"))
let d= extract(getInteger(contract,"d"))

match tx {
case t:DataTransaction =>
let na= extract(getInteger(t.data,"a")) 
let nb= extract(getInteger(t.data,"b"))
let nc= extract(getInteger(t.data,"c"))
let nd= extract(getInteger(t.data,"d"))
   
   nd == 0 || a == 100 - 5
case s:TransferTransaction =>
   ( a + b - c ) * d == 12

case _ => true

}

चूँकि यह पहला संस्करण है, सिंटैक्स बहुत सीमित है और इसमें बग भी हो सकते हैं।
निम्नलिखित लेखों में, मैं वीएम के आगे के विकास को कवर करने की योजना बना रहा हूं, और यह दिखाऊंगा कि आप इसकी मदद से औपचारिक रूप से सत्यापित स्मार्ट अनुबंध कैसे बना सकते हैं, न कि केवल उन्हें हल कर सकते हैं।

कैरेक्टर वर्चुअल मशीन यहां उपलब्ध है http://2.59.42.98/hyperbox/
प्रतीकात्मक वीएम के स्रोत कोड को क्रम में रखने और वहां टिप्पणियां जोड़ने के बाद, मैं इसे मुफ्त पहुंच के लिए GitHub पर डालने की योजना बना रहा हूं।

स्रोत: www.habr.com

शुरुआत से एक औपचारिक सत्यापन प्रणाली बनाना। भाग 1: PHP और पायथन में कैरेक्टर वर्चुअल मशीन

एक टिप्पणी जोड़ें उत्तर रद्द