Nire ustez, Interneten errusierazko sektorean, egiaztapen formalaren gaia ez da behar bezain landu, eta adibide sinple eta argien falta dago bereziki.
Atzerriko iturri bateko adibide bat jarriko dut, eta otsoa, ahuntza eta aza ibaiaren beste aldera igarotzearen arazo ezagunari neure irtenbidea gehituko diot.
Baina lehenik eta behin, laburki deskribatuko dut egiaztapen formala zer den eta zergatik behar den.
Egiaztapen formalak normalean programa edo algoritmo bat beste bat erabiliz egiaztatzea esan nahi du.
Hori beharrezkoa da programak espero bezala jokatzen duela ziurtatzeko eta baita bere segurtasuna bermatzeko ere.
Egiaztapen formala ahuleziak aurkitzeko eta ezabatzeko biderik indartsuena da: programa batean dauden zulo eta akats guztiak aurkitzeko edo existitzen ez direla frogatzeko aukera ematen du.
Aipatzekoa da kasu batzuetan hori ezinezkoa dela, adibidez 8 laukiko taula zabalera duten 1000 erreginen arazoan: dena konplexutasun algoritmikoa edo geldialdiaren arazoa da.
Nolanahi ere, hiru erantzunetako bat jasoko da: programa zuzena da, okerra edo ezin izan da erantzuna kalkulatu.
Erantzuna aurkitzea ezinezkoa bada, sarritan programaren zati argirik gabe birlantzea posible da, haien konplexutasun algoritmikoa murriztuz, baiezko edo ezezko erantzun zehatz bat lortzeko.
Eta egiaztapen formala erabiltzen da, adibidez, Windows nukleoan eta Darpa drone sistema eragileetan, babes-maila handiena bermatzeko.
Z3Prover erabiliko dugu, teorema automatikoki frogatzeko eta ekuazioak ebazteko tresna oso indartsua.
Gainera, Z3-k ekuazioak ebazten ditu eta ez ditu haien balioak hautatzen indar gordina erabiliz.
Horrek esan nahi du erantzuna aurkitzeko gai dela, sarrerako aukeren 10^100 konbinazio dauden kasuetan ere.
Baina hau Integer motako dozena bat sarrera argumentu baino ez dira, eta praktikan askotan aurkitzen da.
8 erregin inguruko arazoa (ingelesetik hartua ).
# 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 exekutatuz, irtenbidea lortuko dugu:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
Erreginaren arazoa sarrera gisa 8 erreginen koordenatuak hartzen dituen programa baten parekoa da eta erreginek elkarri irabazten dioten erantzuna ematen du.
Horrelako programa bat egiaztapen formala erabiliz ebatziko bagenu, orduan arazoarekin alderatuta, programaren kodea ekuazio bihurtzeko urrats bat gehiago eman beharko genuke: funtsean gurearen berdin-berdina izango litzateke ( noski, programa zuzen idatzi bada).
Ia gauza bera gertatuko da ahuleziak bilatzeko kasuan: behar ditugun irteera-baldintzak ezarri besterik ez dugu egiten, adibidez, administratzailearen pasahitza, iturburua edo deskonpilatutako kodea egiaztapenarekin bateragarriak diren ekuazioetan eraldatzen dugu eta, ondoren, zer erantzun. datuak sarrera gisa eman behar dira helburua lortzeko.
Nire ustez, otsoaren, ahuntzaren eta azaren inguruko arazoa are interesgarriagoa da, hori konpontzeko dagoeneko urrats asko (7) behar baitira.
Erreginaren arazoa GET edo POST eskaera bakarra erabiliz zerbitzari batean sar zaitezkeen kasuaren parekoa bada, orduan otsoa, ahuntza eta aza kategoria askoz konplexuago eta hedatuago bateko adibide bat erakusten du, zeinetan helburua bakarrik lor daitekeen. hainbat eskaeraren bidez.
Hau konparagarria da, adibidez, SQL injekzio bat aurkitu behar duzun agertoki batekin, haren bidez fitxategi bat idatzi, gero zure eskubideak igo eta gero pasahitza lortu behar duzun.
Arazoaren baldintzak eta bere konponbideaBaserritarrak otsoa, ahuntza eta aza garraiatu behar ditu ibaian zehar. Baserritarrak objektu bat baino ezin duen txalupa dauka, baserritarraz gain. Otsoak ahuntza jango du eta ahuntzak aza jango du nekazariak zaindu gabe uzten baditu.
Konponbidea da 4. urratsean baserritarrak ahuntza itzuli beharko duela.
Orain has gaitezen programatikoki konpontzen.
Adierazi ditzagun baserritarra, otsoa, ahuntza eta aza 4 edo 0 balioa hartzen duten 1 aldagai gisa. Zerok esan nahi du ezkerreko ertzean daudela, eta batek eskuinaldean daudela.
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
Zenbakia ebazteko behar diren urratsen kopurua da. Urrats bakoitzak ibaiaren, itsasontziaren eta entitate guztien egoera adierazten du.
Oraingoz, aukera dezagun ausaz eta marjina batekin, hartu 10.
Entitate bakoitza 10 kopietan irudikatzen da - hau da bere balioa 10 urratsetako bakoitzean.
Orain ezar ditzagun hasiera eta bukatzeko baldintzak.
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 ]
Ondoren, otsoak ahuntza jaten duen edo ahuntzak aza jaten duen baldintzak ezartzen ditugu ekuazioaren muga gisa.
(Nekazari baten aurrean, erasoa ezinezkoa da)
# 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) ]
Eta azkenik, baserritarrak hara edo itzultzean egin ditzakeen ekintza guztiak zehaztuko ditugu.
Berarekin otsoa, ahuntza edo aza eraman dezake, edo inor ez eraman, edo inora ez nabigatu.
Noski, inork ezin du gurutzatu baserritarrik gabe.
Hori adieraziko da ibaiaren, itsasontziaren eta entitateen ondorengo egoera bakoitza aurrekoarekiko modu hertsiki mugatuan bakarrik desberdina izan daitekeela.
2 bit baino gehiago, eta beste muga askorekin, nekazariak aldi berean entitate bat bakarrik garraiatu dezakeelako eta ezin baita guztiak batera utzi.
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) ]
Exekutatu dezagun irtenbidea.
solve(Side + Start + Finish + Safe + Travel)
Eta erantzuna jasoko dugu!
Z3-k baldintza guztiak betetzen dituen egoera multzo koherentea aurkitu zuen.
Espazio-denboraren lau dimentsioko antzezpen moduko bat.
Azter dezagun zer gertatu den.
Ikusten dugu azkenean denak gurutzatu zirela, hasieran bakarrik gure baserritarrak atseden hartzea erabaki zuen, eta lehenengo 2 pausuetan ez du inon igeri egiten.
Human_2 = 0
Human_3 = 0
Horrek iradokitzen du aukeratu dugun estatu kopurua gehiegizkoa dela, eta 8 nahikoa izango direla.
Gure kasuan, baserritarrak hau egiten zuen: hasi, atseden hartu, atseden hartu, ahuntza gurutzatu, atzera gurutzatu, aza gurutzatu, ahuntzarekin itzuli, otsoa gurutzatu, bakarrik itzuli, ahuntza berriro entregatu.
Baina azkenean arazoa konpondu zen.
#Старт.
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
Orain saia gaitezen baldintzak aldatzen eta konponbiderik ez dagoela frogatzen.
Horretarako, gure otsoari belarjalea emango diogu, eta aza jan nahi izango du.
Hau gure helburua aplikazioa ziurtatzea den kasuarekin alderatu daiteke eta zirrikiturik ez dagoela ziurtatu behar dugu.
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) ]
Z3k erantzun hau eman digu:
no solution
Benetan irtenbiderik ez dagoela esan nahi du.
Horrela, programatikoki frogatu genuen otso orojale batekin gurutzatzeko ezintasuna baserritarrentzat galerarik gabe.
Ikusleek gai hau interesgarria iruditzen bazaio, etorkizuneko artikuluetan programa edo funtzio arrunt bat metodo formalekin bateragarria den ekuazio batean nola bihurtu eta nola konpondu esango dizut, horrela agertoki eta ahultasun legitimo guztiak agerian utziz. Lehenik eta behin, zeregin berean, baina programa moduan aurkeztua, eta gero pixkanaka zailduz eta software garapenaren munduko egungo adibideetara pasaz.
Dagoeneko prest dago hurrengo artikulua:
Bertan arazoen egiaztapen formaletik programetara pasatzen naiz, eta deskribatzen dut
nola bihurtu daitezke automatikoki arau sistema formaletan.
Iturria: www.habr.com