Менің ойымша, интернеттің орыстілді секторында формальды тексеру тақырыбы жеткілікті түрде қамтылмаған, әсіресе қарапайым және түсінікті мысалдар жетіспейді.
Шетелдік деректен мысал келтіріп, өзеннің арғы бетіне қасқыр, ешкі, орамжапырақты кесіп өту туралы белгілі мәселеге өз шешімімді қосамын.
Бірақ алдымен мен ресми тексеру дегеніміз не және ол не үшін қажет екенін қысқаша сипаттаймын.
Ресми тексеру әдетте бір бағдарламаны немесе алгоритмді екіншісін пайдаланып тексеруді білдіреді.
Бұл бағдарламаның күтілгендей әрекет етуін қамтамасыз ету және оның қауіпсіздігін қамтамасыз ету үшін қажет.
Ресми тексеру осалдықтарды табудың және жоюдың ең қуатты құралы болып табылады: ол бағдарламадағы барлық бар тесіктер мен қателерді табуға немесе олардың жоқтығын дәлелдеуге мүмкіндік береді.
Айта кету керек, кейбір жағдайларда бұл мүмкін емес, мысалы, ені 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 биттен артық емес және көптеген басқа шектеулермен, өйткені фермер бір уақытта тек бір нысанды тасымалдай алады және барлығын бірге қалдыруға болмайды.
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