Yn myn miening, yn 'e Russysktalige sektor fan it ynternet, is it ûnderwerp fan formele ferifikaasje net genôch behannele, en d'r is benammen in gebrek oan ienfâldige en dúdlike foarbylden.
Ik sil in foarbyld jaan út in bûtenlânske boarne en myn eigen oplossing tafoegje foar it bekende probleem fan it oerstekken fan in wolf, in geit en in koal nei de oare kant fan de rivier.
Mar earst sil ik koart beskriuwe wat formele ferifikaasje is en wêrom it nedich is.
Formele ferifikaasje betsjut gewoanlik it kontrolearjen fan ien programma of algoritme mei in oar.
Dit is nedich om te soargjen dat it programma gedraacht lykas ferwachte en ek om de feiligens te garandearjen.
Formele ferifikaasje is it machtichste middel om kwetsberens te finen en te eliminearjen: it lit jo alle besteande gatten en bugs yn in programma fine, of bewize dat se net bestean.
It is de muoite wurdich op te merken dat dit yn guon gefallen ûnmooglik is, lykas yn it probleem fan 8 keninginnen mei in boerdbreedte fan 1000 fjilden: it komt allegear del op algoritmyske kompleksiteit of it stopprobleem.
Lykwols, yn alle gefallen, ien fan de trije antwurden wurdt ûntfongen: it programma is goed, ferkeard, of it wie net mooglik om te berekkenjen it antwurd.
As it ûnmooglik is om in antwurd te finen, is it faaks mooglik om ûndúdlike dielen fan it programma opnij te meitsjen, har algoritmyske kompleksiteit te ferminderjen, om in spesifyk ja of nee antwurd te krijen.
En formele ferifikaasje wurdt brûkt, bygelyks, yn 'e Windows kernel en Darpa drone bestjoeringssystemen, om it maksimale nivo fan beskerming te garandearjen.
Wy sille Z3Prover brûke, in heul krêftich ark foar automatisearre stellingbewiis en fergelikingsoplossing.
Boppedat lost Z3 fergelikingen op, en selekteart har wearden net mei brute krêft.
Dit betsjut dat it it antwurd kin fine, sels yn gefallen wêr't d'r 10 ^ 100 kombinaasjes fan ynfieropsjes binne.
Mar dit is mar oer in tsiental ynfier arguminten fan type Integer, en dit wurdt faak tsjinkaam yn de praktyk.
Probleem oer 8 keninginnen (Ut it Ingelsk nommen ).
# 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)
Troch Z3 te rinnen krije wy de oplossing:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
It keninginneprobleem is te fergelykjen mei in programma dat de koördinaten fan 8 keninginnen as ynfier nimt en it antwurd jout oft de keninginnen inoar slaan.
As wy sa'n programma soene oplosse mei formele ferifikaasje, dan soene wy yn ferliking mei it probleem gewoan noch ien stap moatte nimme yn 'e foarm fan it konvertearjen fan de programmakoade yn in fergeliking: it soe yn essinsje identyk wêze oan ús ( fansels, as it programma goed skreaun is).
Hast itselde ding sil barre yn it gefal fan sykjen nei kwetsberens: wy sette gewoan de útfierbetingsten yn dy't wy nedich binne, bygelyks it admin wachtwurd, transformearje de boarne of dekompilearre koade yn fergelikingen kompatibel mei ferifikaasje, en krije dan in antwurd oer wat gegevens moatte wurde levere as ynput om it doel te berikken.
Yn myn miening is it probleem oer de wolf, de geit en de koal noch nijsgjirriger, om't it oplossen al in protte (7) stappen fereasket.
As it probleem fan 'e keninginne te fergelykjen is mei it gefal wêr't jo in tsjinner kinne penetrearje mei in inkeld GET- of POST-fersyk, dan lit de wolf, geit en koal in foarbyld sjen út in folle kompleksere en wiidferspraat kategory, wêryn it doel allinich kin wurde berikt troch ferskate oanfragen.
Dit is bygelyks te fergelykjen mei in senario wêr't jo in SQL-ynjeksje moatte fine, in bestân der troch skriuwe, dan jo rjochten ferheegje en allinich dan in wachtwurd krije.
Betingsten fan it probleem en syn oplossingDe boer moat in wolf, in geit en koal oer de rivier ferfiere. De boer hat in boat dêr't mar ien foarwerp plak yn kin, neist de boer sels. De wolf sil de geit ite en de geit sil de koal ite as de boer se sûnder opsicht lit.
De oplossing is dat yn stap 4 de boer de geit weromhelje moat.
No litte wy it programmatysk begjinne op te lossen.
Lit ús denote de boer, wolf, geit en koal as 4 fariabelen dy't nimme de wearde allinne 0 of 1. Nul betsjut dat se binne op de linker iver, en ien betsjut dat se binne oan de rjochterkant.
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 is it oantal stappen nedich om op te lossen. Elke stap stiet foar de steat fan 'e rivier, de boat en alle entiteiten.
Litte wy it no willekeurich kieze en mei in marzje, nim 10.
Elke entiteit is fertsjintwurdige yn 10 eksimplaren - dit is har wearde by elk fan 'e 10 stappen.
Litte wy no de betingsten ynstelle foar de start en finish.
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 ]
Dan stelle wy de betingsten dêr't de wolf de geit yt, of de geit de koal yt, as beheiningen yn 'e fergeliking.
(Yn it bywêzen fan in boer is agresje ûnmooglik)
# 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) ]
En as lêste sille wy alle mooglike aksjes fan de boer definiearje by it oerstekken derhinne of werom.
Hy kin of in wolf, in geit of in koal meinimme, of nimmen meinimme, of hielendal net farre.
Fansels kin nimmen oerstekke sûnder in boer.
Dit sil útdrukt wurde troch it feit dat elke folgjende steat fan 'e rivier, boat en entiteiten allinich op in strikt beheinde manier kinne ferskille fan' e foarige.
Net mear as 2 bits, en mei in protte oare grinzen, om't de boer mar ien entiteit tagelyk kin ferfiere en net allegear byinoar litte kinne.
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) ]
Litte wy de oplossing útfiere.
solve(Side + Start + Finish + Safe + Travel)
En wy krije it antwurd!
Z3 fûn in konsekwint set fan steaten dy't foldocht oan alle betingsten.
In soarte fan fjouwerdiminsjonale cast fan romte-tiid.
Litte wy útfine wat der bard is.
Wy sjogge dat op it lêst elkenien oerstuts, allinich besleat ús boer earst te rêstjen, en yn 'e earste 2 stappen swimt er nergens.
Human_2 = 0
Human_3 = 0
Dit suggerearret dat it oantal steaten dat wy hawwe keazen te grut is, en 8 sil frij genôch wêze.
By ús hat de boer dit dien: begjinne, rêste, rêste, oer de geit, oerstekke, oer de koal, werom mei de geit, oer de wolf, werom allinne werom, de geit wer leverje.
Mar úteinlik waard it probleem oplost.
#Старт.
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
Litte wy no besykje de betingsten te feroarjen en te bewizen dat d'r gjin oplossingen binne.
Om dit te dwaan, sille wy ús wolf herbivory jaan, en hy sil koal wolle ite.
Dit kin fergelike wurde mei it gefal wêryn ús doel is om de applikaasje te befeiligjen en wy moatte soargje dat d'r gjin gatten binne.
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 joech ús it folgjende antwurd:
no solution
It betsjut dat d'r echt gjin oplossingen binne.
Sa hawwe wy programmatysk bewiisd de ûnmooglikheid fan oerstekken mei in omnivore wolf sûnder ferliezen foar de boer.
As it publyk dit ûnderwerp ynteressant fynt, dan sil ik jo yn 'e takomstige artikels fertelle hoe't jo in gewoane programma of funksje kinne omsette yn in fergeliking kompatibel mei formele metoaden, en it oplosse, sadat alle legitime senario's en kwetsberens iepenbierje. Earst, op deselde taak, mar presintearre yn 'e foarm fan in programma, en dan stadichoan komplisearjend en fierder nei aktuele foarbylden út' e wrâld fan software ûntwikkeling.
It folgjende artikel is al klear:
Dêryn gean ik fan formele ferifikaasje fan problemen nei programma's, en beskriuw
hoe kinne se wurde omsetten yn formele regel systemen automatysk.
Boarne: www.habr.com