Uthibitishaji rasmi kwa kutumia mfano wa tatizo la mbwa mwitu, mbuzi na kabichi

Kwa maoni yangu, katika sekta ya lugha ya Kirusi ya mtandao, mada ya uthibitishaji rasmi haipatikani vya kutosha, na kuna ukosefu wa mifano rahisi na wazi.

Nitatoa mfano kutoka kwa chanzo cha kigeni, na kuongeza suluhisho langu kwa shida inayojulikana ya kuvuka mbwa mwitu, mbuzi na kabichi hadi ng'ambo ya mto.

Lakini kwanza, nitaelezea kwa ufupi uthibitishaji rasmi ni nini na kwa nini unahitajika.

Uthibitishaji rasmi kwa kawaida humaanisha kuangalia programu moja au algoriti kwa kutumia nyingine.

Hii ni muhimu ili kuhakikisha kuwa programu inatenda kama inavyotarajiwa na pia kuhakikisha usalama wake.

Uthibitishaji rasmi ndiyo njia yenye nguvu zaidi ya kutafuta na kuondoa udhaifu: hukuruhusu kupata mashimo na hitilafu zote zilizopo kwenye programu, au kuthibitisha kwamba hazipo.
Inafaa kumbuka kuwa katika hali zingine hii haiwezekani, kama vile katika shida ya malkia 8 na upana wa bodi ya mraba 1000: yote inakuja kwa ugumu wa algorithmic au shida ya kuacha.

Hata hivyo, kwa hali yoyote, moja ya majibu matatu yatapokelewa: programu ni sahihi, si sahihi, au haikuwezekana kuhesabu jibu.

Ikiwa haiwezekani kupata jibu, mara nyingi inawezekana kufanya upya sehemu zisizo wazi za programu, kupunguza utata wao wa algorithmic, ili kupata jibu maalum la ndiyo au hapana.

Na uthibitishaji rasmi hutumiwa, kwa mfano, katika mifumo ya uendeshaji ya Windows kernel na Darpa drone, ili kuhakikisha kiwango cha juu cha ulinzi.

Tutatumia Z3Prover, zana yenye nguvu sana ya uthibitishaji wa nadharia ya kiotomatiki na utatuzi wa milinganyo.

Kwa kuongezea, Z3 hutatua hesabu, na haichagui maadili yao kwa kutumia nguvu ya kikatili.
Hii inamaanisha kuwa inaweza kupata jibu, hata katika hali ambapo kuna mchanganyiko 10 ^ 100 wa chaguzi za kuingiza.

Lakini hii ni kuhusu hoja kadhaa za pembejeo za aina ya Integer, na hii mara nyingi hukutana katika mazoezi.

Tatizo kuhusu malkia 8 (Imechukuliwa kutoka kwa Kiingereza mwongozo).

# 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)

Kuendesha Z3, tunapata suluhisho:

[Q_5 = 1,
 Q_8 = 7,
 Q_3 = 8,
 Q_2 = 2,
 Q_6 = 3,
 Q_4 = 6,
 Q_7 = 5,
 Q_1 = 4]

Tatizo la malkia linalinganishwa na programu inayochukua kama pembejeo ya viwianishi vya malkia 8 na kutoa jibu ikiwa malkia walishindana.

Ikiwa tungesuluhisha programu kama hiyo kwa kutumia uthibitishaji rasmi, kisha ikilinganishwa na shida, tungehitaji kuchukua hatua moja zaidi katika mfumo wa kubadilisha nambari ya programu kuwa equation: ingegeuka kuwa sawa na yetu ( Bila shaka, ikiwa mpango uliandikwa kwa usahihi).

Karibu sawa itatokea katika kesi ya kutafuta udhaifu: tunaweka tu hali ya matokeo tunayohitaji, kwa mfano, nenosiri la msimamizi, kubadilisha chanzo au msimbo ulioharibika kuwa hesabu zinazoendana na uthibitishaji, na kisha kupata jibu la data gani. inahitaji kutolewa kama pembejeo ili kufikia lengo.

Kwa maoni yangu, shida kuhusu mbwa mwitu, mbuzi na kabichi ni ya kuvutia zaidi, kwani kutatua tayari kunahitaji hatua nyingi (7).

Ikiwa shida ya malkia inalinganishwa na kesi ambapo unaweza kupenya seva kwa kutumia ombi moja la GET au POST, basi mbwa mwitu, mbuzi na kabichi huonyesha mfano kutoka kwa jamii ngumu zaidi na iliyoenea, ambayo lengo linaweza kupatikana tu. kwa maombi kadhaa.

Hii inalinganishwa, kwa mfano, na hali ambapo unahitaji kupata sindano ya SQL, andika faili kupitia hiyo, kisha uinulie haki zako na kisha tu kupata nenosiri.

Masharti ya shida na suluhisho lakeMkulima anahitaji kusafirisha mbwa mwitu, mbuzi na kabichi kuvuka mto. Mkulima ana mashua ambayo inaweza kubeba kitu kimoja tu, badala ya mkulima mwenyewe. Mbwa mwitu atakula mbuzi na mbuzi atakula kabichi ikiwa mkulima atawaacha bila kutunzwa.

Suluhisho ni kwamba katika hatua ya 4 mkulima atahitaji kumrudisha mbuzi.
Sasa hebu tuanze kuisuluhisha kwa utaratibu.

Wacha tuonyeshe mkulima, mbwa mwitu, mbuzi na kabichi kama vigeu 4 ambavyo huchukua thamani 0 au 1 tu. Sifuri inamaanisha kuwa ziko kwenye ukingo wa kushoto, na moja inamaanisha kuwa ziko upande wa kulia.

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 ni idadi ya hatua zinazohitajika kutatua. Kila hatua inawakilisha hali ya mto, mashua na vyombo vyote.

Kwa sasa, wacha tuichague bila mpangilio na kwa ukingo, chukua 10.

Kila huluki inawakilishwa katika nakala 10 - hii ni thamani yake katika kila moja ya hatua 10.

Sasa hebu tuweke masharti ya kuanza na kumaliza.

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 ]

Kisha tunaweka masharti ambapo mbwa mwitu hula mbuzi, au mbuzi hula kabichi, kama vikwazo katika equation.
(Mbele ya mkulima, uchokozi hauwezekani)

# 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) ]

Na hatimaye, tutafafanua vitendo vyote vinavyowezekana vya mkulima wakati wa kuvuka huko au nyuma.
Anaweza kuchukua mbwa mwitu, mbuzi au kabichi pamoja naye, au asichukue mtu yeyote, au asisafiri popote.

Bila shaka, hakuna mtu anayeweza kuvuka bila mkulima.

Hii itaonyeshwa na ukweli kwamba kila hali inayofuata ya mto, mashua na vyombo vinaweza kutofautiana na ile ya awali kwa njia ndogo tu.

Sio zaidi ya bits 2, na kwa mipaka mingine mingi, kwa kuwa mkulima anaweza tu kusafirisha chombo kimoja kwa wakati mmoja na sio wote wanaweza kushoto pamoja.

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) ]

Wacha tuendeshe suluhisho.

solve(Side + Start + Finish + Safe + Travel)

Na tunapata jibu!

Z3 ilipata seti thabiti ya majimbo ambayo inakidhi masharti yote.
Aina ya waigizo wa pande nne wa muda wa nafasi.

Hebu tujue kilichotokea.

Tunaona kwamba mwishowe kila mtu alivuka, tu mwanzoni mkulima wetu aliamua kupumzika, na katika hatua 2 za kwanza haogelei popote.

Human_2 = 0
Human_3 = 0

Hii inaonyesha kwamba idadi ya majimbo tuliyochagua ni nyingi, na 8 itatosha kabisa.

Kwa upande wetu, mkulima alifanya hivi: kuanza, kupumzika, kupumzika, kuvuka mbuzi, kuvuka nyuma, kuvuka kabichi, kurudi na mbuzi, kuvuka mbwa mwitu, kurudi nyuma peke yake, kutoa tena mbuzi.

Lakini hatimaye tatizo lilitatuliwa.

#Старт.
 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

Sasa hebu tujaribu kubadilisha hali na kuthibitisha kwamba hakuna ufumbuzi.

Ili kufanya hivyo, tutampa mbwa mwitu mimea yetu, na atataka kula kabichi.
Hii inaweza kulinganishwa na hali ambayo lengo letu ni kupata maombi na tunahitaji kuhakikisha kuwa hakuna mianya.

 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 ilitupa jibu lifuatalo:

 no solution

Ina maana kwamba kwa kweli hakuna ufumbuzi.

Kwa hivyo, tulithibitisha kwa utaratibu kuwa haiwezekani kuvuka na mbwa mwitu wa omnivorous bila hasara kwa mkulima.

Ikiwa hadhira itapata mada hii ya kufurahisha, basi katika nakala zijazo nitakuambia jinsi ya kugeuza programu au kazi ya kawaida kuwa equation inayoendana na njia rasmi, na kuitatua, na hivyo kufichua hali zote halali na udhaifu. Kwanza, juu ya kazi sawa, lakini iliyotolewa kwa namna ya programu, na kisha hatua kwa hatua kuifanya na kuendelea na mifano ya sasa kutoka kwa ulimwengu wa maendeleo ya programu.

Nakala inayofuata iko tayari:
Kuunda mfumo rasmi wa uthibitishaji kutoka mwanzo: Kuandika VM ya mfano katika PHP na Python

Ndani yake ninahama kutoka kwa uthibitishaji rasmi wa shida hadi programu, na kuelezea
zinawezaje kubadilishwa kuwa mifumo rasmi ya sheria moja kwa moja.

Chanzo: mapenzi.com