વરુ, બકરી અને કોબી સમસ્યાના ઉદાહરણનો ઉપયોગ કરીને ઔપચારિક ચકાસણી

મારા મતે, ઇન્ટરનેટના રશિયન-ભાષાના ક્ષેત્રમાં, ઔપચારિક ચકાસણીનો વિષય પર્યાપ્ત રીતે આવરી લેવામાં આવ્યો નથી, અને ખાસ કરીને સરળ અને સ્પષ્ટ ઉદાહરણોનો અભાવ છે.

હું વિદેશી સ્ત્રોતમાંથી એક ઉદાહરણ આપીશ, અને નદીની બીજી બાજુ વરુ, બકરી અને કોબીને પાર કરવાની જાણીતી સમસ્યા માટે મારો પોતાનો ઉકેલ ઉમેરીશ.

પરંતુ પ્રથમ, હું ટૂંકમાં વર્ણન કરીશ કે ઔપચારિક ચકાસણી શું છે અને શા માટે તેની જરૂર છે.

સામાન્ય રીતે ઔપચારિક ચકાસણીનો અર્થ થાય છે એક પ્રોગ્રામ અથવા બીજાનો ઉપયોગ કરીને અલ્ગોરિધમ તપાસવું.

પ્રોગ્રામ અપેક્ષા મુજબ વર્તે તેની ખાતરી કરવા માટે અને તેની સુરક્ષાની ખાતરી કરવા માટે આ જરૂરી છે.

ઔપચારિક ચકાસણી એ નબળાઈઓ શોધવા અને દૂર કરવા માટેનું સૌથી શક્તિશાળી માધ્યમ છે: તે તમને પ્રોગ્રામમાં અસ્તિત્વમાં રહેલા તમામ છિદ્રો અને બગ્સ શોધવા અથવા સાબિત કરવા દે છે કે તેઓ અસ્તિત્વમાં નથી.
તે નોંધવું યોગ્ય છે કે કેટલાક કિસ્સાઓમાં આ અશક્ય છે, જેમ કે 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 વિનંતીનો ઉપયોગ કરીને સર્વરને ઘૂસી શકો છો, તો વરુ, બકરી અને કોબી વધુ જટિલ અને વ્યાપક શ્રેણીમાંથી એક ઉદાહરણ દર્શાવે છે, જેમાં ફક્ત લક્ષ્ય પ્રાપ્ત કરી શકાય છે. અનેક વિનંતીઓ દ્વારા.

આ તુલનાત્મક છે, ઉદાહરણ તરીકે, એવી પરિસ્થિતિ સાથે જ્યાં તમારે 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

Num એ ઉકેલવા માટે જરૂરી પગલાંઓની સંખ્યા છે. દરેક પગલું નદી, હોડી અને તમામ સંસ્થાઓની સ્થિતિનું પ્રતિનિધિત્વ કરે છે.

હમણાં માટે, ચાલો તેને રેન્ડમ અને માર્જિન સાથે પસંદ કરીએ, 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 અને Python માં પ્રતીકાત્મક VM લખવું

તેમાં હું સમસ્યાઓની ઔપચારિક ચકાસણીથી કાર્યક્રમો તરફ આગળ વધું છું અને તેનું વર્ણન કરું છું
તેઓને ઔપચારિક નિયમ પ્રણાલીમાં આપમેળે કેવી રીતે રૂપાંતરિત કરી શકાય છે.

સોર્સ: www.habr.com