Pormal nga pag-verify gamit ang pananglitan sa problema sa lobo, kanding ug repolyo

Sa akong opinyon, sa Russian nga pinulongan nga sektor sa Internet, ang hilisgutan sa pormal nga verification dili igo nga sakop, ug adunay ilabi na sa usa ka kakulang sa yano ug tin-aw nga mga panig-ingnan.

Maghatag ako usa ka pananglitan gikan sa usa ka langyaw nga gigikanan, ug idugang ang akong kaugalingon nga solusyon sa nahibal-an nga problema sa pagtabok sa usa ka lobo, usa ka kanding ug usa ka repolyo sa pikas nga bahin sa suba.

Apan una, akong lakbit nga ihulagway kung unsa ang pormal nga pag-verify ug ngano nga kini gikinahanglan.

Ang pormal nga pag-verify kasagaran nagpasabut sa pagsusi sa usa ka programa o algorithm gamit ang lain.

Kinahanglan kini aron masiguro nga ang programa molihok sama sa gipaabut ug aron masiguro usab ang seguridad niini.

Ang pormal nga pag-verify mao ang labing kusgan nga paagi sa pagpangita ug pagwagtang sa mga kahuyangan: gitugotan ka nga makit-an ang tanan nga adunay mga lungag ug mga bug sa usa ka programa, o pamatud-an nga wala sila.
Angay nga matikdan nga sa pipila ka mga kaso imposible kini, sama sa problema sa 8 nga mga rayna nga adunay gilapdon nga tabla nga 1000 ka mga kwadro: kining tanan moabut sa pagkakomplikado sa algorithm o sa paghunong sa problema.

Bisan pa, sa bisan unsang kaso, usa sa tulo nga mga tubag ang madawat: ang programa husto, sayup, o dili posible nga makalkula ang tubag.

Kung imposible nga makit-an ang usa ka tubag, kanunay nga posible nga i-rework ang dili klaro nga mga bahin sa programa, nga makunhuran ang ilang pagkakomplikado sa algorithm, aron makakuha usa ka piho nga tubag nga oo o dili.

Ug gigamit ang pormal nga pag-verify, pananglitan, sa Windows kernel ug Darpa drone operating system, aron masiguro ang labing taas nga lebel sa proteksyon.

Gamiton namo ang Z3Prover, usa ka gamhanan kaayo nga himan para sa automated theorem proving ug equation solving.

Dugang pa, gisulbad sa Z3 ang mga equation, ug wala gipili ang ilang mga kantidad gamit ang brute force.
Kini nagpasabot nga kini makahimo sa pagpangita sa tubag, bisan sa mga kaso diin adunay 10^100 nga mga kombinasyon sa mga kapilian sa input.

Apan kini mga usa lamang ka dosena nga input nga mga argumento sa tipo nga Integer, ug kini kanunay nga masugatan sa praktis.

Problema mahitungod sa 8 ka rayna (Gikuha gikan sa English manwal).

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

Pagdagan sa Z3, makuha namon ang solusyon:

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

Ang problema sa rayna ikatandi sa usa ka programa nga nagkuha isip input sa mga coordinate sa 8 ka rayna ug nagpagawas sa tubag kon ang mga rayna nagpildi sa usag usa.

Kung among sulbaron ang ingon nga programa gamit ang pormal nga pag-verify, unya kung itandi sa problema, kinahanglan na lang namon nga maghimo usa pa nga lakang sa porma sa pag-convert sa code sa programa sa usa ka equation: kini mahimong parehas sa amon ( siyempre, kung ang programa gisulat sa husto).

Halos parehas nga butang ang mahitabo sa kaso sa pagpangita sa mga kahuyangan: gitakda lang namo ang mga kondisyon sa output nga among gikinahanglan, pananglitan, ang admin password, pagbag-o sa tinubdan o decompiled code ngadto sa mga equation nga compatible sa verification, ug dayon makakuha og tubag kon unsa data kinahanglan nga gihatag ingon nga input sa pagkab-ot sa tumong.

Sa akong hunahuna, ang problema bahin sa lobo, kanding ug repolyo labi pa nga makapaikag, tungod kay ang pagsulbad niini nanginahanglan daghang (7) mga lakang.

Kung ang problema sa rayna ikatandi sa kaso diin mahimo nimong masulud ang usa ka server gamit ang usa ka hangyo nga GET o POST, nan ang lobo, kanding ug repolyo nagpakita usa ka pananglitan gikan sa labi ka labi ka komplikado ug kaylap nga kategorya, diin ang katuyoan makab-ot ra. pinaagi sa daghang mga hangyo.

Ikatandi kini, pananglitan, sa usa ka senaryo diin kinahanglan nimo pangitaon ang usa ka SQL injection, pagsulat og usa ka file pinaagi niini, unya ipataas ang imong mga katungod ug dayon pagkuha usa ka password.

Kondisyon sa problema ug sa solusyon niiniAng mag-uuma kinahanglan nga magdala sa usa ka lobo, usa ka kanding ug repolyo tabok sa suba. Ang mag-uuma adunay usa ka sakayan nga usa ra ka butang ang masudlan, gawas sa mag-uuma mismo. Ang lobo mokaon sa kanding ug ang kanding mokaon sa repolyo kon ang mag-uuma mobiya kanila nga walay pagtagad.

Ang solusyon mao nga sa lakang 4 kinahanglan nga ibalik sa mag-uuma ang kanding.
Karon magsugod kita sa pagsulbad niini pinaagi sa programa.

Atong itudlo ang mag-uuma, lobo, kanding ug repolyo isip 4 ka variables nga nagkuha sa kantidad nga 0 o 1 lamang. Ang zero nagpasabot nga naa sila sa wala nga bangko, ug ang usa nagpasabot nga naa sila sa tuo.

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

Ang Num mao ang gidaghanon sa mga lakang nga gikinahanglan aron masulbad. Ang matag lakang nagrepresentar sa kahimtang sa suba, sakayan ug tanan nga mga entidad.

Sa pagkakaron, pilion nato kini sa random ug uban ang margin, kuhaa ang 10.

Ang matag entidad girepresentahan sa 10 ka kopya - kini ang kantidad niini sa matag usa sa 10 ka lakang.

Karon atong ibutang ang mga kondisyon alang sa pagsugod ug pagkahuman.

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 ]

Dayon among gibutang ang mga kondisyon diin ang lobo mokaon sa kanding, o ang kanding mokaon sa repolyo, ingon nga mga pagpugong sa equation.
(Sa presensya sa usa ka mag-uuma, imposible ang agresyon)

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

Ug sa katapusan, atong ipasabut ang tanan nga posible nga mga aksyon sa mag-uuma kung motabok didto o pabalik.
Mahimo siyang magdala og lobo, kanding o repolyo uban kaniya, o dili magdala ni bisan kinsa, o dili molayag bisan asa.

Siyempre, walay makatabok nga walay mag-uuma.

Kini ipahayag sa kamatuoran nga ang matag sunod nga kahimtang sa suba, sakayan ug mga entidad mahimong magkalahi gikan sa nauna sa usa lamang ka limitado nga paagi.

Dili mosobra sa 2 ka bit, ug uban sa daghang uban pang mga limitasyon, tungod kay ang mag-uuma mahimo lamang nga magdala sa usa ka entidad sa usa ka higayon ug dili tanan mahimong ibilin nga magkauban.

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

Atong padaganon ang solusyon.

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

Ug atong makuha ang tubag!

Ang Z3 nakakaplag usa ka makanunayon nga hugpong sa mga estado nga nagtagbaw sa tanan nga mga kondisyon.
Usa ka matang sa upat ka dimensyon nga cast sa space-time.

Atong tan-awon kon unsay nahitabo.

Nakita namon nga sa katapusan ang tanan mitabok, lamang sa una ang among mag-uuma nakahukom nga mopahulay, ug sa unang 2 nga mga lakang dili siya molangoy bisan asa.

Human_2 = 0
Human_3 = 0

Kini nagsugyot nga ang gidaghanon sa mga estado nga among gipili sobra ra, ug ang 8 igo na.

Sa among kahimtang, gibuhat kini sa mag-uuma: sugod, pahulay, pahulay, tabok sa kanding, tabok balik, tabok sa repolyo, balik uban sa kanding, tabok sa lobo, balik nga nag-inusara, ihatod pag-usab ang kanding.

Apan sa katapusan ang problema nasulbad.

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

Karon atong sulayan nga usbon ang mga kondisyon ug pamatud-an nga wala'y mga solusyon.

Sa pagbuhat niini, kita sa paghatag sa atong lobo herbivory, ug siya gusto sa pagkaon sa cabbage.
Mahimo kini itandi sa kaso diin ang among katuyoan mao ang pagsiguro sa aplikasyon ug kinahanglan namon nga masiguro nga wala’y mga lungag.

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

Gihatagan kami ni Z3 sa mosunod nga tubag:

 no solution

Nagpasabot kini nga wala'y mga solusyon.

Sa ingon, napamatud-an namon sa programa nga imposible ang pagtabok sa usa ka omnivorous nga lobo nga wala’y kapildihan alang sa mag-uuma.

Kung makit-an sa mga mamiminaw nga makapaikag kini nga hilisgutan, unya sa umaabot nga mga artikulo isulti ko kanimo kung giunsa ang paghimo sa usa ka ordinaryo nga programa o pag-obra sa usa ka equation nga nahiuyon sa pormal nga mga pamaagi, ug pagsulbad niini, sa ingon gipadayag ang tanan nga lehitimong mga senaryo ug mga kahuyangan. Una, sa parehas nga buluhaton, apan gipresentar sa porma sa usa ka programa, ug unya hinayhinay nga gikomplikado kini ug nagpadayon sa karon nga mga pananglitan gikan sa kalibutan sa pagpalambo sa software.

Andam na ang sunod nga artikulo:
Paghimo usa ka pormal nga sistema sa pag-verify gikan sa wala: Pagsulat usa ka simbolo nga VM sa PHP ug Python

Diha niini mobalhin ko gikan sa pormal nga pag-verify sa mga problema ngadto sa mga programa, ug ihulagway
kung giunsa nimo kini mahimo nga mga sistema sa pormal nga mga lagda awtomatiko.

Source: www.habr.com