Að mínu mati er ekki nægjanlega fjallað um formlega sannprófun í rússneskumælandi geira internetsins og sérstaklega skortir einföld og skýr dæmi.
Ég mun nefna dæmi úr erlendri heimild og bæta við eigin lausn á hinu þekkta vandamáli að fara yfir úlf, geit og kál hinum megin við ána.
En fyrst mun ég lýsa stuttlega hvað formleg sannprófun er og hvers vegna hennar er þörf.
Formleg staðfesting þýðir venjulega að athuga eitt forrit eða reiknirit með því að nota annað.
Þetta er nauðsynlegt til að tryggja að forritið hagi sér eins og búist er við og einnig til að tryggja öryggi þess.
Formleg sannprófun er öflugasta leiðin til að finna og útrýma veikleikum: hún gerir þér kleift að finna allar núverandi göt og villur í forriti, eða sanna að þær séu ekki til.
Það er athyglisvert að í sumum tilfellum er þetta ómögulegt, eins og í vandamálinu með 8 drottningar með borðbreidd 1000 ferninga: allt snýst þetta um flókið reiknirit eða stöðvunarvandamálið.
Hins vegar, í öllum tilvikum, mun eitt af þremur svörum berast: forritið er rétt, rangt eða ekki var hægt að reikna út svarið.
Ef það er ómögulegt að finna svar er oft hægt að endurvinna óljósa hluta forritsins, draga úr reiknireglum þeirra, til að fá ákveðið já eða nei svar.
Og formleg sannprófun er notuð, til dæmis, í Windows kjarna og Darpa dróna stýrikerfum, til að tryggja hámarks vernd.
Við munum nota Z3Prover, mjög öflugt tól til að sanna sjálfvirka setningar og leysa jöfnur.
Þar að auki, Z3 leysir jöfnur og velur ekki gildi þeirra með því að nota skepnakraft.
Þetta þýðir að það er hægt að finna svarið, jafnvel í þeim tilvikum þar sem það eru 10^100 samsetningar af innsláttarvalkostum.
En þetta snýst aðeins um tugi inntaksrafræða af gerðinni Heiltala, og þetta kemur oft fyrir í reynd.
Vandamál um 8 drottningar (Tekið úr ensku ).
# 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)
Með því að keyra Z3 fáum við lausnina:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
Drottningarvandamálið er sambærilegt við forrit sem tekur sem inntak hnit 8 drottna og gefur út svarið hvort drottningarnar slái hvor aðra.
Ef við myndum leysa slíkt forrit með formlegri sannprófun, þá þyrftum við, miðað við vandamálið, einfaldlega að taka eitt skref í viðbót í formi þess að breyta forritskóðanum í jöfnu: hann myndi reynast í meginatriðum eins og okkar ( auðvitað, ef forritið var rétt skrifað).
Næstum það sama mun gerast ef leitað er að veikleikum: við stillum bara úttaksskilyrðin sem við þurfum, til dæmis stjórnandalykilorðið, umbreytum frumkóðanum eða afteknum kóða í jöfnur sem eru samhæfðar við sannprófun og fáum síðan svar við því hvað gögn þarf að afhenda sem inntak til að ná markmiðinu.
Að mínu mati er vandamálið um úlfinn, geitina og kálið enn áhugaverðara, þar sem að leysa það þarf þegar mörg (7) skref.
Ef drottningarvandamálið er sambærilegt við það tilvik þar sem hægt er að komast inn á netþjón með einni GET eða POST beiðni, þá sýnir úlfurinn, geitin og kálið dæmi úr miklu flóknari og útbreiddari flokki, þar sem markmiðinu er aðeins hægt að ná. með nokkrum beiðnum.
Þetta er til dæmis sambærilegt við atburðarás þar sem þú þarft að finna SQL innspýtingu, skrifa skrá í gegnum hana, hækka síðan réttindi þín og aðeins þá fá lykilorð.
Skilyrði vandamálsins og lausn þessBóndinn þarf að flytja úlf, geit og kál yfir ána. Bóndinn á bát sem rúmar aðeins einn hlut, fyrir utan bóndann sjálfan. Úlfurinn étur geitina og geitin étur kálið ef bóndinn skilur þá eftir án eftirlits.
Lausnin er sú að í skrefi 4 þarf bóndinn að taka geitina aftur.
Nú skulum við byrja að leysa það forritunarlega.
Við skulum tákna bóndann, úlfinn, geitina og kálið sem 4 breytur sem taka gildið aðeins 0 eða 1. Núll þýðir að þeir eru á vinstri bakka og ein þýðir að þeir eru á hægri.
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
Númer er fjöldi skrefa sem þarf til að leysa. Hvert skref táknar ástand árinnar, bátsins og allra eininga.
Í bili skulum við velja það af handahófi og með framlegð, tökum 10.
Hver eining er táknuð í 10 eintökum - þetta er gildi hennar í hverju af 10 þrepunum.
Nú skulum við setja skilyrði fyrir upphafi og endalokum.
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 ]
Síðan setjum við skilyrðin þar sem úlfurinn étur geitina, eða geitin étur kálið, sem skorður í jöfnunni.
(Í viðurvist bónda er árásargirni ómögulegt)
# 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) ]
Og að lokum munum við skilgreina allar mögulegar aðgerðir bóndans þegar farið er þangað eða til baka.
Hann getur annað hvort tekið með sér úlf, geit eða kál eða ekki tekið neinn eða ekki siglt neitt.
Auðvitað kemst enginn yfir án bónda.
Þetta kemur fram í þeirri staðreynd að hvert síðari ástand árinnar, bátsins og aðila getur aðeins verið frábrugðið því fyrra á stranglega takmarkaðan hátt.
Ekki meira en 2 bita, og með mörgum öðrum takmörkunum, þar sem bóndinn getur aðeins flutt eina heild í einu og ekki er hægt að skilja alla eftir saman.
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) ]
Við skulum keyra lausnina.
solve(Side + Start + Finish + Safe + Travel)
Og við fáum svarið!
Z3 fann samræmt sett af ríkjum sem uppfyllir öll skilyrði.
Eins konar fjórvíð afsteypa tímarúms.
Við skulum reikna út hvað gerðist.
Við sjáum að á endanum fóru allir yfir, aðeins í fyrstu ákvað bóndinn okkar að hvíla sig og í fyrstu 2 skrefunum syndir hann hvergi.
Human_2 = 0
Human_3 = 0
Þetta bendir til þess að fjöldi ríkja sem við völdum sé óhóflegur og 8 dugi alveg.
Í okkar tilfelli gerði bóndinn þetta: byrja, hvíla, hvíla sig, fara yfir geitina, fara yfir til baka, fara yfir kálið, fara aftur með geitina, fara yfir úlfinn, snúa aftur einn, skila geitinni aftur.
En á endanum var vandinn leystur.
#Старт.
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
Nú skulum við reyna að breyta skilyrðunum og sanna að það eru engar lausnir.
Til að gera þetta munum við gefa úlfinn okkar grasbít, og hann mun vilja borða hvítkál.
Það má líkja þessu við málið þar sem markmið okkar er að tryggja umsóknina og við þurfum að gæta þess að það séu engar glufur.
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 gaf okkur eftirfarandi svar:
no solution
Það þýðir að það eru í raun engar lausnir.
Þannig sönnuðum við forritunarlega að ómögulegt væri að fara yfir með alætur úlfi án taps fyrir bóndann.
Ef áhorfendum finnst þetta efni áhugavert, þá mun ég í framtíðargreinum segja þér hvernig á að breyta venjulegu forriti eða aðgerð í jöfnu sem er samhæft við formlegar aðferðir, og leysa það og þar með sýna bæði allar lögmætar aðstæður og veikleika. Í fyrsta lagi í sama verkefni, en sett fram í formi forrits, og síðan flækjast það smám saman og fara yfir í núverandi dæmi úr heimi hugbúnaðarþróunar.
Næsta grein er þegar tilbúin:
Í því fer ég frá formlegri sannprófun á vandamálum yfir í forrit og lýsi
hvernig er hægt að breyta þeim í formleg reglukerfi sjálfkrafa.
Heimild: www.habr.com