Dapre mwen, nan sektè lang Ris la nan entènèt la, sijè a nan verifikasyon fòmèl pa ase kouvri, epi gen espesyalman yon mank de egzanp senp ak klè.
Mwen pral bay yon egzanp ki soti nan yon sous etranje, epi ajoute pwòp solisyon mwen an nan pwoblèm ki byen koni nan travèse yon lou, yon kabrit ak yon chou lòt bò larivyè Lefrat la.
Men, anvan, mwen pral yon ti tan dekri sa verifikasyon fòmèl se ak poukisa li nesesè.
Verifikasyon fòmèl anjeneral vle di tcheke yon pwogram oswa algorithm lè l sèvi avèk yon lòt.
Sa a nesesè pou asire ke pwogram nan konpòte yo jan yo espere epi tou asire sekirite li yo.
Verifikasyon fòmèl se mwayen ki pi pwisan pou jwenn ak elimine frajilite yo: li pèmèt ou jwenn tout twou ak ensèk ki egziste deja nan yon pwogram, oswa pwouve ke yo pa egziste.
Li se vo anyen ke nan kèk ka sa a se enposib, tankou nan pwoblèm nan nan 8 Queens ak yon lajè tablo nan 1000 kare: li tout vini desann nan konpleksite algoritmik oswa pwoblèm nan kanpe.
Sepandan, nan nenpòt ka, youn nan twa repons yo pral resevwa: pwogram nan kòrèk, kòrèk, oswa li pa t posib yo kalkile repons lan.
Si li enposib jwenn yon repons, li souvan posib pou retravay pati ki pa klè nan pwogram nan, diminye konpleksite algoritmik yo, yo nan lòd yo jwenn yon repons espesifik wi oswa non.
Ak verifikasyon fòmèl yo itilize, pou egzanp, nan nwayo a Windows ak sistèm operasyon abèy Darpa, asire nivo maksimòm pwoteksyon an.
Nou pral sèvi ak Z3Prover, yon zouti trè pwisan pou pwouve teyorèm otomatik ak rezoud ekwasyon.
Anplis, Z3 rezoud ekwasyon, epi li pa chwazi valè yo lè l sèvi avèk fòs brital.
Sa vle di ke li kapab jwenn repons lan, menm nan ka kote gen 10 ^ 100 konbinezon opsyon opinyon.
Men, sa a se sèlman sou yon douzèn agiman opinyon nan kalite Integer, ak sa a se souvan rankontre nan pratik.
Pwoblèm sou 8 rèn (Te pran nan lang angle ).
# 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)
Kouri Z3, nou jwenn solisyon an:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
Pwoblèm larenn nan konparab ak yon pwogram ki pran kòm opinyon kowòdone 8 larenn ak rezilta repons lan si wi ou non larenn yo bat youn ak lòt.
Si nou ta dwe rezoud yon pwogram konsa lè l sèvi avèk verifikasyon fòmèl, Lè sa a, konpare ak pwoblèm nan, nou ta tou senpleman bezwen fè yon lòt etap nan fòm lan nan konvèti kòd pwogram nan nan yon ekwasyon: li ta tounen esansyèlman idantik ak nou an ( nan kou, si pwogram nan te ekri kòrèkteman).
Prèske menm bagay la pral rive nan ka a nan rechèch pou frajilite: nou jis mete kondisyon yo pwodiksyon nou bezwen, pou egzanp, modpas la admin, transfòme sous la oswa kòd dekonpile nan ekwasyon konpatib ak verifikasyon, ak Lè sa a, jwenn yon repons sou sa ki. done yo dwe apwovizyone kòm opinyon pou reyalize objektif la.
Dapre mwen, pwoblèm nan sou bèt nan bwa, kabrit la ak chou a se menm plis enteresan, depi rezoud li deja mande anpil (7) etap.
Si pwoblèm nan larenn se konparab ak ka a kote ou ka antre nan yon sèvè lè l sèvi avèk yon sèl demann GET oswa POST, Lè sa a, bèt nan bwa, kabrit ak chou demontre yon egzanp ki soti nan yon kategori pi konplèks ak toupatou, nan ki objektif la ka reyalize sèlman. pa plizyè demann.
Sa a se konparab, pou egzanp, ak yon senaryo kote ou bezwen jwenn yon piki SQL, ekri yon dosye atravè li, Lè sa a, elve dwa ou epi sèlman Lè sa a, jwenn yon modpas.
Kondisyon pwoblèm nan ak solisyon li yoKiltivatè a bezwen transpòte yon bèt nan bwa, yon kabrit ak chou atravè rivyè a. Kiltivatè a gen yon bato ki ka sèlman akomode yon objè, san konte kiltivatè a li menm. Lou ap manje kabrit la epi kabrit la ap manje chou a si kiltivatè a kite yo poukont li.
Solisyon an se ke nan etap 4 kiltivatè a pral bezwen pran kabrit la tounen.
Koulye a, an n kòmanse rezoud li pwogramasyon.
Ann endike kiltivatè a, bèt nan bwa, kabrit ak chou kòm 4 varyab ki pran valè a sèlman 0 oswa 1. Zewo vle di ke yo sou bò gòch la, ak youn vle di ke yo sou bò dwat la.
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 se kantite etap ki nesesè pou rezoud. Chak etap reprezante eta a nan rivyè a, bato a ak tout antite.
Pou kounye a, ann chwazi li o aza epi ak yon maj, pran 10.
Chak antite reprezante nan 10 kopi - sa a se valè li nan chak nan 10 etap yo.
Koulye a, kite a mete kondisyon yo pou kòmansman an ak fini.
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 ]
Lè sa a, nou mete kondisyon yo kote bèt nan bwa manje kabrit la, oswa kabrit la manje chou a, kòm kontrent nan ekwasyon an.
(An prezans yon kiltivatè, agresyon enposib)
# 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) ]
Epi finalman, nou pral defini tout aksyon posib nan kiltivatè a lè travèse la oswa tounen.
Li ka swa pran yon bèt nan bwa, yon kabrit oswa yon chou avè l ', oswa pa pran pèsonn, oswa pa navige nenpòt kote ditou.
Natirèlman, pèsonn pa ka travèse san yon kiltivatè.
Sa a pral eksprime pa lefèt ke chak eta ki vin apre nan gwo larivyè Lefrat la, bato ak antite ka diferan de yon sèl anvan an sèlman nan yon fason estrikteman limite.
Pa plis pase 2 bit, ak anpil lòt limit, depi kiltivatè a ka sèlman transpòte yon antite nan yon moman epi yo pa tout ka rete ansanm.
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) ]
Ann kouri solisyon an.
solve(Side + Start + Finish + Safe + Travel)
Epi nou jwenn repons lan!
Z3 te jwenn yon seri eta ki konsistan ki satisfè tout kondisyon yo.
Yon kalite jete kat dimansyon nan espas-tan.
Ann kalkile sa ki te pase.
Nou wè finalman tout moun te travèse, se sèlman okòmansman kiltivatè nou an te deside repoze, epi nan 2 premye etap yo li pa naje okenn kote.
Human_2 = 0
Human_3 = 0
Sa a sijere ke kantite eta nou te chwazi a twòp, epi 8 pral ase.
Nan ka nou an, kiltivatè a te fè sa: kòmanse, repoze, repoze, kwa kabrit la, travèse dèyè, kwaze chou a, retounen ak kabrit la, kwaze bèt nan bwa, retounen tounen pou kont li, re-livre kabrit la.
Men, nan fen pwoblèm nan te rezoud.
#Старт.
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
Koulye a, ann eseye chanje kondisyon yo ak pwouve ke pa gen okenn solisyon.
Pou fè sa, nou pral bay bèt nan bwa èbivò nou an, epi li pral vle manje chou.
Sa a ka konpare ak ka a nan ki objektif nou an se sekirize aplikasyon an epi nou bezwen asire w ke pa gen okenn brèch.
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 te ban nou repons sa a:
no solution
Sa vle di ke vrèman pa gen solisyon.
Kidonk, nou pwograme pwouve enposib pou kwaze ak yon bèt nan bwa omnivor san pèt pou kiltivatè a.
Si odyans lan jwenn sijè sa a enteresan, Lè sa a, nan atik lavni mwen pral di w ki jan yo vire yon pwogram òdinè oswa fonksyon nan yon ekwasyon konpatib ak metòd fòmèl, epi rezoud li, kidonk revele tou de tout senaryo lejitim ak frajilite. Premyèman, sou travay la menm, men prezante nan fòm lan nan yon pwogram, ak Lè sa a, piti piti konplike li ak deplase sou egzanp aktyèl soti nan mond lan nan devlopman lojisyèl.
Pwochen atik la deja pare:
Nan li mwen deplase soti nan verifikasyon fòmèl nan pwoblèm nan pwogram, ak dekri
ki jan yo ka konvèti nan sistèm règ fòmèl otomatikman.
Sous: www.habr.com