Իմ կարծիքով ինտերնետի ռուսալեզու հատվածում ֆորմալ ստուգման թեման բավականաչափ լուսաբանված չէ, և հատկապես պարզ ու հստակ օրինակների պակաս կա։
Օտար աղբյուրից օրինակ բերեմ, իսկ հայտնի խնդրին՝ գայլի, այծի ու կաղամբի գետից այն կողմ անցնելու իմ լուծումը կավելացնեմ։
Բայց նախ, ես հակիրճ նկարագրելու եմ, թե ինչ է պաշտոնական ստուգումը և ինչու է դա անհրաժեշտ:
Պաշտոնական ստուգումը սովորաբար նշանակում է մեկ ծրագրի կամ ալգորիթմի ստուգում՝ օգտագործելով մյուսը:
Սա անհրաժեշտ է ապահովելու, որ ծրագիրը վարվի այնպես, ինչպես ակնկալվում է, ինչպես նաև ապահովելու նրա անվտանգությունը:
Պաշտոնական ստուգումը խոցելիությունները գտնելու և վերացնելու ամենահզոր միջոցն է. այն թույլ է տալիս գտնել ծրագրում առկա բոլոր անցքերը և սխալները կամ ապացուցել, որ դրանք գոյություն չունեն:
Հարկ է նշել, որ որոշ դեպքերում դա անհնար է, օրինակ՝ 8 քառակուսի տախտակի լայնությամբ 1000 թագուհու խնդրի դեպքում. ամեն ինչ հանգում է ալգորիթմական բարդությանը կամ կանգառի խնդրին:
Սակայն ամեն դեպքում ստացվելու է երեք պատասխաններից մեկը՝ ծրագիրը ճիշտ է, սխալ, կամ հնարավոր չի եղել հաշվել պատասխանը։
Եթե պատասխան գտնելն անհնար է, հաճախ հնարավոր է լինում վերամշակել ծրագրի անհասկանալի մասերը՝ նվազեցնելով դրանց ալգորիթմական բարդությունը՝ կոնկրետ այո կամ ոչ պատասխան ստանալու համար:
Իսկ պաշտոնական ստուգումն օգտագործվում է, օրինակ, Windows kernel և Darpa անօդաչու օպերացիոն համակարգերում՝ առավելագույն պաշտպանվածության մակարդակ ապահովելու համար։
Մենք կօգտագործենք 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
Դա նշանակում է, որ լուծումներ իսկապես չկան։
Այսպիսով, մենք ծրագրային կերպով ապացուցեցինք գյուղացու համար ամենակեր գայլի հետ առանց կորուստների անցնելու անհնարինությունը։
Եթե հանդիսատեսին այս թեման հետաքրքիր է, ապա հետագա հոդվածներում ես ձեզ կասեմ, թե ինչպես սովորական ծրագիրը կամ գործառույթը վերածել ֆորմալ մեթոդների հետ համատեղելի հավասարման և լուծել այն՝ դրանով իսկ բացահայտելով բոլոր օրինական սցենարները և խոցելիությունները: Նախ՝ նույն առաջադրանքով, բայց ներկայացված ծրագրի տեսքով, իսկ հետո աստիճանաբար բարդացնելով այն ու անցնելով ծրագրային ապահովման մշակման աշխարհի արդի օրինակներին։
Հաջորդ հոդվածն արդեն պատրաստ է.
Դրանում ես խնդիրների պաշտոնական ստուգումից անցնում եմ ծրագրերի և նկարագրում
ինչպես կարող են դրանք ավտոմատ կերպով վերածվել պաշտոնական կանոնների համակարգերի:
Source: www.habr.com