Sipas mendimit tim, tema e verifikimit formal në sektorin rusisht-folës të internetit është përcjellë në mënyrë të pamjaftueshme, sidomos janë të munguar shembujt e thjeshtë dhe të qartë.
Do të jap një shembull nga një burim ndërkombëtar dhe do ta plotësoj me një zgjidhje të njohur për problemin e kalimit të ujkut, dhe të ziegrit dhe të lakrës në anën tjetër të lumit.
Por përpara se të filloj, do të përshkruaj shkurtimisht se çfarë përfaqëson verifikimi formal dhe pse është i nevojshëm.
Verifikimi formal zakonisht kuptohet si kontrolli i një programi ose algoritmi me anë të një tjetri.
Kjo është e nevojshme për të siguruar se sjellja e programit është në përputhje me atë që pritet, si dhe për të garantuar sigurinë e tij.
Verifikimi formal është mjeti më i fuqishëm për gjetjen dhe eliminimin e dobësive: ai lejon të gjejmë të gjitha të metat dhe gabimet ekzistuese në program, ose të dëshmojmë se ato nuk ekzistojnë.
Duhet të theksohet se në disa raste kjo është e pamundur, si për shembull në problemin e 8 mbretëreshave me një tabelë 1000 katrorë: gjithçka varet nga kompleksiteti algoritmik ose problemi i ndalimit.
Megjithatë, në çdo rast do të merret një nga tri përgjigjet: programi është korrekte, jo korekt, ose nuk arriti të llogarisë përgjigjen.
Në rastin e pamundësisë për të gjetur një përgjigje, shpesh është e mundur të përpunohen vendet e paqarta të programit, duke e reduktuar kompleksitetin e tyre algoritmik, për të marrë një përgjigje të qartë po ose jo.
Verifikimi formal përdoret, për shembull, në bërthamën e Windows dhe në sistemet operative të dronëve Darpa, për të siguruar një nivel maksimal mbrojtjeje.
Ne do të përdorim Z3Prover, një mjet shumë të fuqishëm për provimin automatizuar të teoremave dhe zgjidhjen e ekuacioneve.
Dhe Z3 pikërisht zgjidh ekuacionet, e jo i gjen vlerat e tyre përmes forcës brutale.
Kjo do të thotë se ai është në gjendje të gjejë përgjigjen, madje edhe në rastet kur kombinimet e mundshme të hyrjeve janë 10^100.
Dhe kjo është vetëm rreth një duzine argumentesh hyrëse të tipit Integer, dhe diçka e tillë shpesh ndodh në praktikë.
Problemi i 8 mbretëreshave (Marrë nga një burim në anglisht ).
# 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)
Duke e nisur Z3, ne marrim një zgjidhje:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
Problemi i mbretëreshave është krahasues me një program që merr si input koordinatat e 8 mbretëreshave dhe në përfundim tregon nëse mbretëreshat godasin njëra-tjetrën.
Nëse do të zgjidhnim një program të tillë me anë të verifikimit formal, krahasuar me problemin, do të na nevojitej thjesht të bënim një hap tjetër në formën e transformimit të kodit të programit në ekuacion: ai do të rezultonte esencialisht identik me tonin tonë (sigurisht, nëse programi është shkruar pa gabime).
Në mënyrë praktike, e njëjta gjë do të ndodhte në rastin e kërkimit të dobësive: ne thjesht do të caktuam kushtet e duhura të rezultatit, për shembull fjalëkalimin e administratorit, do ta transformonim kodin origjinal ose të dekompiluara në ekuacione të përputhshme për verifikim, dhe më pas do të merrnim përgjigjen, çfarë të dhënash duhet të jepnim si input për të arritur qëllimin.
Sipras mendimit tim, problemi i ujkut, dhe te ziegrit dhe lakrës është edhe më interesant, pasi për zgjidhjen e tij ne do të na duhen më shumë (7) hapa.
Nëse problemi i mbretëreshave është krahasues me një variant, kur mund të hyjmë në server përmes një GET ose POST kërkese, ujku, koza dhe lakra demonstrojnë një shembull nga një kategori shumë më komplekse dhe të zakonshme, në të cilën qëllimet mund të arrihen vetëm përmes disa kërkesave.
Kjo tregon, për shembull, një skenar, ku duhet të gjej një injeksion SQL, të shkruaj një skedar përmes tij, të rris nivelin tim të privilegjeve dhe vetëm atëherë të marr fjalëkalimin.
Kushtet e problemit dhe zgjidhja e tijFermieri duhet të kalojë në anën tjetër të lumit ujkun, kozen dhe lakrën. Fermieri ka një barkë, në të cilën ka vend për të, përveç vetë fshatarit, vetëm një objekt. Ujku do të hajë kozen, dhe koza do të hajë lakrën, nëse fshatari i lë ata pa mbikëqyrje.
Zgjidhja është se në hapin e 4-të, fshatari duhet të kthente kozen përsëri.
Tani le të kalojmë në zgjidhjen me program.
Le të shënojmë fshatarin, ujkun, kozen dhe lakrën si 4 variabla, të cilët japin vetëm vlerat 0 ose 1. Zero tregon që ata janë në bregun e majtë, ndërsa një - që janë në të djathtë.
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) ]
# Secili krijesë mund të jetë vetëm në anën e majtë (0) ose të djathtë (1) në çdo gjendje
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 është numri i hapave të nevojshëm për zgjidhjen. Çdo hap paraqet një gjendje të lumit, barkës dhe të gjitha entiteteve.
Për tani të zgjedhim atë rastësisht dhe me rezerve, le të marrim 10.
Çdo entitet paraqitet në 10 kopje — ky është kuptimi i saj në çdo një nga 10 hapat.
Tani do të vendosim kushtet për fillimin dhe përfundimin.
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 ]
Më pas do të vendosim kushtet, ku kjo ujq i hanë dhentë, ose dhenta kapustën, si kufizime në barazim.
(Në prani të fermerit agresioni është i pamundur)
# 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) ]
Dhe së fundmi, do të vendosim të gjitha veprimet e mundshme të fermerit gjatë kalimit atje ose këtu.
Ai mund të marrë me vete ujqin, dhentë ose kapustën, ose të mos marrë askënd, ose madje të mos udhëtojë fare.
Natyrisht, pa fermerin askush nuk mund të kalojë.
Kjo do të shprehet në mënyrën se si çdo gjendje e mëpasshme e lumit, anijes dhe entiteteve mund të ndryshojë nga e mëparshmja vetëm në një mënyrë strikte të kufizuar.
Jo më shumë se 2 bita, dhe me shumë kufizime të tjera, pasi fermeri mund të transportojë vetëm një entitet në një kohë dhe jo të gjithë mund të lihen së bashku.
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])) për i në range(Num-1) ]
Të fillojmë zgjidhjen.
solve(Side + Start + Finish + Safe + Travel)
Dhe ne marrim përgjigjen!
Z3 gjeti një grup gjendjesh që nuk është në kontradiktë dhe që plotëson të gjitha kushtet.
Një lloj gjurme katër-dimensionale e hapësirë-kohës.
Le të kuptojmë se çfarë ka ndodhur.
Shohim se në fund të gjithë kaluan, por fillimisht fermeri vendosi të pushojë dhe nuk udhëton askund në 2 hapat e parë.
Human_2 = 0
Human_3 = 0
Kjo tregon se numri i gjendjeve e kemi zgjedhur më shumë se sa të nevojshme, dhe 8 do të ishte mjaft e mjaftueshme.
Në rastin tonë, fermeri veproi kështu: fillim, pushim, pushim, kalimi i dhentës, kthimi, kalimi i kapustës, kthimi me dhentën, kalimi i ujqit, kthimi vetëm, përsëritja e dërgesës së dhentës.
Por në fund, detyra është zgjidhur.
#Старт.
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
Tani le të provojmë të ndryshojmë kushtet dhe të provojmë se nuk ka zgjidhje.
Për këtë, ne do ta pajisim ujqin tonë me herbivorizëm dhe ai do të dëshirojë të hajë kapustën.
Kjo mund të krahasohet me rastin kur qëllimi ynë është mbrojtja e aplikacionit dhe ne duhet të sigurohemi që nuk ka evazion.
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])) për i në range(Num) ]
Z3 na dha përgjigjen e mëposhtme:
no solution
Kjo do të thotë se në të vërtetë nuk ka zgjidhje.
Kështu, ne provuam në mënyrë programore pamundësinë e kalimit me ujqin mishngrënës, pa humbje për fermerin.
Nëse audienca e konsideron këtë temë interesante, atëherë në artikujt e ardhshëm do të tregoj se si të kthejmë një program ose funksion të zakonshëm në një ekuacion të përputhshëm me metodat formale, dhe ta zgjidhim atë, duke zbuluar kështu si skenarët legjitimë ashtu edhe dobësitë. Fillimisht për këtë detyrë, por e paraqitur tashmë si program, dhe pastaj gradualisht duke u ndërlikuar dhe duke kaluar në raste aktuale nga bota e zhvillimit të softuerit.
Artikulli tjetër është gati:
Atje po kaloj nga verifikimi formale i detyrave në programe, dhe përshkruaj,
se si mund t'i konvertojmë ato automatikisht në sisteme rregullash formale.
Burimi: habr.com
