Sipas mendimit tim, në sektorin në gjuhën ruse të internetit, tema e verifikimit zyrtar nuk është e mbuluar sa duhet, dhe veçanërisht ka mungesë të shembujve të thjeshtë dhe të qartë.
Do të jap një shembull nga një burim i huaj dhe do t'i shtoj zgjidhjen time problemit të njohur të kalimit të një ujku, një dhie dhe një lakre në anën tjetër të lumit.
Por së pari, unë do të përshkruaj shkurtimisht se çfarë është verifikimi zyrtar dhe pse është i nevojshëm.
Verifikimi formal zakonisht nënkupton kontrollimin e një programi ose algoritmi duke përdorur një tjetër.
Kjo është e nevojshme për të siguruar që programi të sillet siç pritet dhe gjithashtu për të garantuar sigurinë e tij.
Verifikimi formal është mjeti më i fuqishëm për gjetjen dhe eliminimin e dobësive: ju lejon të gjeni të gjitha vrimat dhe gabimet ekzistuese në një program, ose të provoni se ato nuk ekzistojnë.
Vlen të përmendet se në disa raste kjo është e pamundur, si për shembull në problemin e 8 mbretëreshave me një gjerësi dërrase prej 1000 katrore: gjithçka varet nga kompleksiteti algoritmik ose problemi i ndalimit.
Sidoqoftë, në çdo rast, do të merret një nga tre përgjigjet: programi është i saktë, i pasaktë ose nuk ishte e mundur të llogaritet përgjigja.
Nëse është e pamundur të gjesh një përgjigje, shpesh është e mundur të ripunohen pjesë të paqarta të programit, duke zvogëluar kompleksitetin e tyre algoritmik, për të marrë një përgjigje specifike po ose jo.
Dhe verifikimi zyrtar përdoret, për shembull, në kernelin Windows dhe sistemet operative të dronëve Darpa, për të siguruar nivelin maksimal të mbrojtjes.
Ne do të përdorim Z3Prover, një mjet shumë i fuqishëm për vërtetimin e automatizuar të teoremës dhe zgjidhjen e ekuacioneve.
Për më tepër, Z3 zgjidh ekuacione dhe nuk zgjedh vlerat e tyre duke përdorur forcën brutale.
Kjo do të thotë se është në gjendje të gjejë përgjigjen, edhe në rastet kur ka 10^100 kombinime të opsioneve të hyrjes.
Por kjo është vetëm rreth një duzinë argumente hyrëse të tipit Integer, dhe kjo shpesh haset në praktikë.
Problemi rreth 8 mbretëreshave (Marrë nga anglishtja ).
# 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 ekzekutuar Z3, marrim zgjidhjen:
[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ëreshës është i krahasueshëm me një program që merr si hyrje koordinatat e 8 mbretëreshave dhe jep përgjigjen nëse mbretëreshat munden njëra-tjetrën.
Nëse do të zgjidhnim një program të tillë duke përdorur verifikimin zyrtar, atëherë krahasuar me problemin, thjesht do të duhej të bënim një hap më shumë në formën e konvertimit të kodit të programit në një ekuacion: do të rezultonte në thelb identik me tonin ( sigurisht, nëse programi është shkruar saktë).
Pothuajse e njëjta gjë do të ndodhë në rastin e kërkimit të dobësive: ne thjesht vendosim kushtet e daljes që na duhen, për shembull, fjalëkalimin e administratorit, transformojmë burimin ose kodin e dekompiluar në ekuacione të përputhshme me verifikimin dhe më pas marrim një përgjigje se çfarë të dhënat duhet të jepen si input për të arritur qëllimin.
Për mendimin tim, problemi me ujkun, dhinë dhe lakrën është edhe më interesant, pasi tashmë duhen shumë (7) hapa për ta zgjidhur atë.
Nëse problemi i mbretëreshës është i krahasueshëm me rastin kur mund të depërtoni në një server duke përdorur një kërkesë të vetme GET ose POST, atëherë ujku, dhia dhe lakra demonstrojnë një shembull nga një kategori shumë më komplekse dhe më e përhapur, në të cilën qëllimi mund të arrihet vetëm nga disa kërkesa.
Kjo është e krahasueshme, për shembull, me një skenar ku ju duhet të gjeni një injeksion SQL, të shkruani një skedar përmes tij, pastaj të ngrini të drejtat tuaja dhe vetëm atëherë të merrni një fjalëkalim.
Kushtet e problemit dhe zgjidhja e tijFermeri duhet të transportojë një ujk, një dhi dhe lakër përtej lumit. Fermeri ka një varkë që mund të strehojë vetëm një objekt, përveç vetë fermerit. Ujku do të hajë dhinë dhe dhia do të hajë lakrën nëse fermeri i lë pa mbikëqyrje.
Zgjidhja është se në hapin 4 fermeri do të duhet të marrë dhinë.
Tani le të fillojmë ta zgjidhim atë në mënyrë programore.
Le të shënojmë fermerin, ujkun, dhinë dhe lakrën si 4 variabla që marrin vlerën vetëm 0 ose 1. Zero do të thotë se janë në bregun e majtë dhe një do të thotë se 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) ]
# 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
Numri është numri i hapave që kërkohen për të zgjidhur. Çdo hap përfaqëson gjendjen e lumit, varkës dhe të gjitha entiteteve.
Tani për tani, le ta zgjedhim atë në mënyrë të rastësishme dhe me një diferencë, marrim 10.
Çdo entitet përfaqësohet në 10 kopje - kjo është vlera e tij në secilin nga 10 hapat.
Tani le 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 vendosim kushtet ku ujku ha dhinë, ose dhia ha lakër, si kufizime në ekuacion.
(Në prani të një fermeri, 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ë fundi, ne do të përcaktojmë të gjitha veprimet e mundshme të fermerit kur kalon atje ose mbrapa.
Ai ose mund të marrë një ujk, një dhi ose një lakër me vete, ose të mos marrë askënd, ose të mos lundrojë askund.
Sigurisht, askush nuk mund të kalojë pa një fermer.
Kjo do të shprehet me faktin se çdo gjendje pasuese e lumit, varkës dhe entiteteve mund të ndryshojë nga ajo e mëparshme vetëm në një mënyrë rreptësisht të kufizuar.
Jo më shumë se 2 bit, dhe me shumë kufizime të tjera, pasi fermeri mund të transportojë vetëm një entitet në të njëjtën 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])) for i in range(Num-1) ]
Le të ekzekutojmë zgjidhjen.
solve(Side + Start + Finish + Safe + Travel)
Dhe ne e marrim përgjigjen!
Z3 gjeti një grup të qëndrueshëm gjendjesh që plotëson të gjitha kushtet.
Një lloj kasti katërdimensional i hapësirë-kohës.
Le të kuptojmë se çfarë ndodhi.
Shohim që në fund të gjithë kaluan, vetëm në fillim fermeri ynë vendosi të pushojë dhe në 2 hapat e parë nuk noton askund.
Human_2 = 0
Human_3 = 0
Kjo sugjeron që numri i shteteve që kemi zgjedhur është i tepërt dhe 8 do të jenë mjaft të mjaftueshme.
Në rastin tonë, fermeri e bëri këtë: filloni, pushoni, pushoni, kaloni dhinë, kaloni mbrapa, kaloni lakrën, kthehuni me dhinë, kaloni ujkun, kthehuni vetëm, ri-dorzoni dhinë.
Por në fund problemi u zgjidh.
#Старт.
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ë përpiqemi të ndryshojmë kushtet dhe të vërtetojmë se nuk ka zgjidhje.
Për ta bërë këtë, ne do t'i japim ujkut tonë barishtore, dhe ai do të dëshirojë të hajë lakër.
Kjo mund të krahasohet me rastin në të cilin qëllimi ynë është të sigurojmë aplikacionin dhe duhet të sigurohemi që të mos ketë boshllëqe.
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 na dha përgjigjen e mëposhtme:
no solution
Do të thotë se realisht nuk ka zgjidhje.
Kështu, në mënyrë programore vërtetuam pamundësinë e kalimit me një ujk gjithëngrënës pa humbje për fermerin.
Nëse audienca e sheh këtë temë interesante, atëherë në artikujt e ardhshëm do t'ju tregoj se si ta shndërroni një program ose funksion të zakonshëm në një ekuacion të pajtueshëm me metodat formale dhe ta zgjidhni atë, duke zbuluar kështu të gjithë skenarët legjitimë dhe dobësitë. Së pari, në të njëjtën detyrë, por të paraqitur në formën e një programi, dhe më pas duke e komplikuar gradualisht dhe duke kaluar në shembujt aktualë nga bota e zhvillimit të softuerit.
Artikulli tjetër është tashmë gati:
Në të kaloj nga verifikimi zyrtar i problemeve në programe dhe përshkruaj
si mund të shndërrohen automatikisht në sisteme të rregullave formale.
Burimi: www.habr.com