Sipas mendimit tim, në sektorin e internetit në gjuhën ruse, tematika e verifikimit formal është e mbuluar mjaft dobët, dhe sidomos mungojnë shembujt e thjeshtë dhe të qartë.
Do t'i jap një shembull nga një burim të huaj dhe do ta plotësoj me zgjidhjen time të njohur për problemin e kalimit të ujkut, dhisë dhe kapitalit në anën tjetër të lumit.
Por në fillim do të përshkruaj shkurtimisht se çfarë përfaqëson verifikimi formal dhe pse është i nevojshëm.
Verifikimi formal zakonisht kuptohet si kontrolle e një programi ose algoritmi me anë të një tjetri.
Kjo është e nevojshme për të siguruar që sjellja e programit përputhet 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 gjetjen e të gjitha vrimave dhe defekteve në program, ose prova që ato nuk ekzistojnë.
Duhet të theksohet se në disa raste kjo është e pamundur, siç është në problemin e 8 mbretërve me gjerësi të tabelës 1000 kutish: gjithçka varet nga kompleksiteti algoritmik ose problemi i ndalimit.
Megjithatë, në çdo rast do të merret një nga tri përgjigjet: programi është korrekt, jo korrekt, ose — nuk ishte e mundur të llogaritet përgjigja.
Në rastin e pamundësisë për të gjetur një përgjigje, shpesh herë mund të rishikojmë vendet e paqarta të programit, duke ulur kompleksitetin e tyre algoritmik, për të marrë një përgjigje specifike po ose jo.
Verifikimi formal aplikohet, për shembull, në kernelin e Windows dhe sistemet operative të dronëve Darpa, për të siguruar nivelin më të lartë të mbrojtjes.
Ne do të përdorim Z3Prover, një instrument shumë të fuqishëm për provimin automatizuar të teoremave dhe zgjidhjen e ekuacioneve.
Dhe Z3 në fakt zgjidh ekuacione, dhe jo vetëm që kërkon vlerat e tyre në mënyrë brute.
Kjo do të thotë se ai është në gjendje të gjejë përgjigjen, madje edhe në rastet kur kombinimet e mundshme të inputeve janë 10^100.
Megjithatë, kjo është vetëm rreth një duzinë argumentesh hyrëse të tipit Integer, dhe diçka e tillë ndodh shpesh në praktikë.
Problemi i 8 mbretërve (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 nisur 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ërve është i krahasueshëm me një program që merr si input koordinatat e 8 mbretërve dhe jep përgjigjen nëse mbretërit godasin ose jo.
Nëse do të zgjidhnim një program të tillë duke përdorur verifikimin formal, krahasuar me problemin, ne thjesht do të na nevojitej të bënim një hap tjetër në formën e konvertimit të kodit të programit në një ekuacion: ai do të rezultonte esencialisht identik me të tonin (sigurisht, nëse programi është shkruar pa gabime).
Praktikisht, e njëjta do të ndodhte edhe në rastin e kërkimit të dobësive: ne thjesht i japim kushtet e daljes që na duhen, për shembull fjalëkalimin e administratorit, e më pas e konvertojmë kodin burimor ose të dekompiluara në ekuacione të përputhshme me verifikimin, dhe pastaj merrni përgjigjen se cilat të dhëna duhet të dorëzohen si input për të arritur qëllimin.
Sipas mendimit tim, problemi i ujku, kapra dhe kungulli është edhe më interesant, pasi për zgjidhjen e tij nevojiten tashmë shumë (7) hapa.
Nëse problemi i mbretëreshës është i krahasueshëm me variantin kur është e mundshme të hysh në server me një kërkesë GET ose POST, ujku, kapra dhe kungulli demonstrojnë një shembull nga një kategori shumë më të komplikuar dhe të përhapur, në të cilën qëllimet mund të arrihen vetëm me disa kërkesa.
Kjo është e krahasueshme, për shembull, me një skenar ku nevojitet të gjeni një injeksion SQL, të shkruani një skedar përmes tij, pastaj të rrisni të drejtat tuaj dhe vetëm atëherë të merrni fjalëkalimin.
Kushtet e problemit dhe zgjidhja e tijFermieri duhet të transportojë nëpër lumë ujkun, kaprën dhe kungullin. Fermieri ka një barkë, në të cilën mund të vendoset, përveç vetë fermerit, vetëm një objekt. Ujku do të hajë kaprën, ndërsa kapra do të hajë kungullin, nëse fermeri i lë ata pa mbikëqyrje.
Zgjidhja është se në hapin e katërt fermeri duhet ta cojë kaprën prapa.
Tani le të kalojmë në zgjidhjen nëpërmjet programimit.
Le të caktuar fermerin, ujkun, kaprën dhe kungullin si 4 variabla, të cilat marrin vetëm vlerat 0 ose 1. Zero do të thotë që ata janë në bregun e majtë, ndërsa 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) ]
# Secila krijesë mund të jetë vetëm në të 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 përfaqëson një gjendje të lumit, barkës dhe të gjitha entiteteve.
Për momentin, do ta zgjedhim atë të rastësishëm dhe me kapacitet, do të marim 10.
Çdo entitet paraqitet në 10 kopje — kjo është vlera e tij në çdo nga 10 hapat.
Tani do të vendosim kushtet për fillimin dhe mbarimin.
Fillimi = [ Human[0] == 0, Wolf[0] == 0, Goat[0] == 0, Cabbage[0] == 0 ]
Mbarimi = [ Human[9] == 1, Wolf[9] == 1, Goat[9] == 1, Cabbage[9] == 1 ]
Pastaj do të vendosim kushtet, ku tërmeti ha kaprën, ose kapra ha kulturën, si kufizime në ekuacion.
(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 përfundimisht, do të vendosim të gjitha veprimet e mundshme të fermerit gjatë kalimit lart apo poshtë.
Ai mund të marrë me vete ujkun, kaprën, ose kulturën, ose të mos marrë askënd, ose të mos lëvizë fare.
Sigurisht, pa fermerin, askush nuk mund të kalojë.
Kjo do të shprehet në mënyrën se çdo gjendje e ardhshme e lumit, anijes dhe entiteteve mund të ndryshojë nga e mëparshmja vetëm në një mënyrë 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.
Udhëtimi = [ Ose(
Dhe(Human[i] == Human[i+1] + 1, Wolf[i] == Wolf[i+1] + 1, Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1]),
Dhe(Human[i] == Human[i+1] + 1, Goat[i] == Goat[i+1] + 1, Wolf[i] == Wolf[i+1], Cabbage[i] == Cabbage[i+1]),
Dhe(Human[i] == Human[i+1] + 1, Cabbage[i] == Cabbage[i+1] + 1, Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1]),
Dhe(Human[i] == Human[i+1] - 1, Wolf[i] == Wolf[i+1] - 1, Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1]),
Dhe(Human[i] == Human[i+1] - 1, Goat[i] == Goat[i+1] - 1, Wolf[i] == Wolf[i+1], Cabbage[i] == Cabbage[i+1]),
Dhe(Human[i] == Human[i+1] - 1, Cabbage[i] == Cabbage[i+1] - 1, Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1]),
Dhe(Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1])) për i në gamën e Num-1 ]
Të fillojmë zgjidhjen.
zgjidh(Side + Start + Finish + Safe + Travel)
Dhe ne marrim përgjigjen!
Z3 gjeti një grup gjendjesh që është i paqëndrueshëm dhe plotëson të gjitha kushtet.
Një lloj katër dimensional i gjurmës së hapësirës-kohe.
Le të kuptojmë se çfarë ndodhi.
Ne shohim se në fund të gjitha kaluan, vetëm se në fillim fermeri vendosi të pushojë dhe nuk lëvizte fare në 2 hapat e parë.
Human_2 = 0
Human_3 = 0
Kjo tregon se ne kemi zgjedhur një numër gjendjesh të tepruar, dhe 8 do të ishin mjaft.
Në rastin tonë, fermeri veproi si vijon: fillimi, pushimi, pushimi, kalimi i kaprës, kthimi mbrapa, kalimi i kulturës, kthimi me kaprën, kalimi i ujkut, kthimi mbrapa vetëm, dërgesa e përsëritur e kaprës.
Por përfundimisht, problemi ë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ë dëmshohemi se nuk ka zgjidhje.
Për këtë, ne do ta pajisim ujkun me vegjetarianizëm, dhe ai do të dëshirojë të hajë kulturën.
Kjo mund të krahasohet me një rast ku synimi ynë është mbrojtja e aplikacionit dhe ne duhet të sigurohemi që nuk ka të meta.
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 këtë përgjigje:
nuk ka zgjidhje
Kjo do të thotë se në të vërtetë nuk ka zgjidhje.
Në këtë mënyrë, ne provuam në mënyrë programore pamundësinë e kalimit me një ujk gjithjoshës, pa humbje për fermerin.
Nëse publiku e konsideron këtë temë interesante, atëherë në artikujt e ardhshëm do të flas për mënyrat e kthimit të një programi ose funksioni të zakonshëm në një ekuacion të përputhshëm me metodat formale dhe për ta zgjidhur atë, duke zbuluar kështu si skenaret legjitime ashtu edhe dobësitë. Fillimisht do të merrem me këtë problem, por i paraqitur tashmë si një program, dhe më pas gradualisht do ta komplikohem dhe do kalojmë në shembuj aktualë nga bota e zhvillimit të softuerit.
Artikulli i ardhshëm është gati:
Në të, unë kaloj nga verifikimi formal i problemeve, në programe, dhe përshkruaj,
se si është e mundur t'i konvertojmë ato në sisteme rregullash formale automatikisht.
Burimi: habr.com
