Менимче, интернеттин орус тилдүү секторунда формалдуу текшерүү темасы жетиштүү камтылган эмес, өзгөчө жөнөкөй жана түшүнүктүү мисалдар жетишсиз.
Чет элдик булактан мисал келтирип, карышкыр, теке, капустаны дарыянын аркы өйүзүнө кечип өтүү боюнча белгилүү маселеге өзүмдүн чечимимди кошом.
Бирок адегенде мен формалдуу текшерүү деген эмне жана ал эмне үчүн керек экенин кыскача айтып берейин.
Расмий текшерүү, адатта, бир программаны же алгоритмди башкасын колдонуу менен текшерүүнү билдирет.
Бул программа күтүлгөндөй иштешин камсыз кылуу жана анын коопсуздугун камсыз кылуу үчүн зарыл.
Формалдуу текшерүү – алсыздыктарды табуу жана жок кылуунун эң күчтүү каражаты: ал программадагы бардык тешиктерди жана мүчүлүштүктөрдү табууга же алардын жок экенин далилдөөгө мүмкүндүк берет.
Белгилей кетчү нерсе, кээ бир учурларда бул мүмкүн эмес, мисалы, тактасынын туурасы 8 чарчы болгон 1000 ханыша маселесинде: мунун баары алгоритмдик татаалдыкка же токтотуу маселесине байланыштуу.
Бирок, кандай болгон күндө да, үч жооптун бири алынат: программа туура, туура эмес, же жоопту эсептөө мүмкүн эмес.
Эгерде жооп табуу мүмкүн болбосо, анда белгилүү бир ооба же жок деген жоопту алуу үчүн программанын түшүнүксүз бөлүктөрүн алгоритмдик татаалдыгын азайтып кайра иштеп чыгууга болот.
Ал эми расмий текшерүү, мисалы, Windows ядросунда жана Darpa учкучсуз иштөө тутумдарында, коргоонун максималдуу деңгээлин камсыз кылуу үчүн колдонулат.
Биз Z3Prover, автоматташтырылган теореманы далилдөө жана теңдемелерди чечүү үчүн абдан күчтүү куралды колдонобуз.
Мындан тышкары, Z3 теңдемелерди чечет жана алардын баалуулуктарын орой күч менен тандабайт.
Бул киргизүү варианттарынын 10^100 комбинациясы болгон учурларда да жооп таба алат дегенди билдирет.
Бирок бул Integer түрүндөгү онго жакын гана киргизүү аргументтери жана бул практикада көп кездешет.
8 ханыша жөнүндө маселе (Англис тилинен алынган ).
# 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 иштетип, биз чечимди алабыз:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
Эне аары проблемасын 8 эне аарынын координаталарын киргизген жана аарылар бири-бирин урабы же жокпу деген суроого жооп берген программага салыштырууга болот.
Эгерде биз мындай программаны формалдуу текшерүү аркылуу чече турган болсок, анда маселеге салыштырмалуу программанын кодун теңдемеге айландыруу түрүндөгү дагы бир кадамды жасашыбыз керек болот: ал түпкүлүгүндө биздикиге окшош болуп чыгат ( албетте, программа туура жазылган болсо).
Кемчиликтерди издөөдө дээрлик ушундай болот: биз жөн гана керектүү чыгуу шарттарын орнотобуз, мисалы, администратордун сырсөзүн, булакты же декомпиляцияланган кодду текшерүүгө шайкеш келген теңдемелерге айландырып, анан эмне деген суроого жооп алабыз. маалыматтар максатка жетүү үчүн киргизүү катары берилиши керек.
Менин оюмча, карышкыр, эчки жана капуста маселеси андан да кызыктуу, анткени аны чечүү үчүн буга чейин эле көп (7) кадам талап кылынат.
Эгер ханышанын көйгөйү бир GET же POST сурамынын жардамы менен серверге кире турган учурга окшош болсо, анда карышкыр, эчки жана капуста бир топ татаал жана кеңири таралган категориядан үлгү көрсөтөт, анда максатка гана жетүүгө болот. бир нече өтүнүчтөр менен.
Бул, мисалы, SQL инъекциясын таап, ал аркылуу файл жазып, андан кийин өз укуктарыңызды жогорулатып, андан кийин гана паролду алышыңыз керек болгон сценарий менен салыштырууга болот.
Проблеманын шарттары жана аны чечүүДыйканга карышкыр, эчки жана капустаны дарыядан өткөрүү керек. Дыйкандын өзүнөн башка бир гана объект бата турган кайыгы бар. Дыйкан кароосуз калтырса, карышкыр эчкинин, эчки капуста жейт.
Чечим 4-кадамда фермер эчкинин кайтарып алышы керек болот.
Эми аны программалык түрдө чечүүгө киришели.
Дыйкан, карышкыр, эчки жана капустаны 4 же 0 гана маанисин алган 1 өзгөрмө катары белгилейли. Нөл алардын сол жээкте, ал эми бир оң жагында экенин билдирет.
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 - чечүү үчүн зарыл болгон кадамдардын саны. Ар бир кадам дарыянын, кайыктын жана бардык объекттердин абалын билдирет.
Азырынча келгиле, аны туш келди жана маржа менен тандап алалы, 10ду алалы.
Ар бир объект 10 нускада көрсөтүлөт - бул 10 кадамдын ар биринде анын мааниси.
Эми старт жана бүтүрүү шарттарын белгилейли.
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 ]
Андан кийин теңдемеде чектөө катары карышкыр текени же эчки капустаны жей турган шарттарды койдук.
(Дыйкан бар жерде агрессия болбойт)
# 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) ]
Акыр-аягы, дыйкандын ошол жерден өтүүдө же кайра артка өтүүдө мүмкүн болгон бардык аракеттерин аныктайбыз.
Ал өзү менен карышкыр, эчки, капуста ала алат, же эч кимди ала албайт, же такыр эч жакка сүзбөйт.
Албетте, дыйкансыз эч ким өтө албайт.
Бул дарыянын, кайыктын жана объекттеринин ар бир кийинки абалы мурдагысынан катуу чектелген түрдө гана айырмаланышы мүмкүн экендиги менен түшүндүрүлөт.
2 биттен ашык эмес жана башка көптөгөн чектөөлөр менен, анткени фермер бир эле учурда бир объектти ташый алат жана бардыгын чогуу калтырууга болбойт.
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) ]
Келгиле, чечимди иштетели.
solve(Side + Start + Finish + Safe + Travel)
Жана биз жооп алабыз!
Z3 бардык шарттарды канааттандырган мамлекеттердин ырааттуу топтомун тапты.
Убакыттын мейкиндигинин төрт өлчөмдүү бир түрү.
Келгиле, эмне болгонун аныктап көрөлү.
Акыры баары өтүп кеткенин көрүп жатабыз, адегенде дыйканыбыз эс алууну чечип, алгачкы 2 кадамда эч жерде сүзбөйт.
Human_2 = 0
Human_3 = 0
Бул биз тандаган штаттардын саны өтө көп экенин көрсөтүп турат жана 8 жетиштүү болот.
Бизде дыйкан мындай кылган: баштоо, эс алуу, эс алуу, текени кечүү, артка кайтуу, капустадан өтүү, эчки менен кайтуу, карышкыр кечүү, жалгыз кайтуу, эчкинин кайра тапшыруу.
Бирок акырында маселе чечилди.
#Старт.
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
Эми шарттарды өзгөртүүгө аракет кылып, эч кандай чечимдер жок экенин далилдеп көрөлү.
Ал үчүн карышкырыбызга чөп жегиси келет, ал капуста жегиси келет.
Бул биздин максат тиркемени камсыз кылуу болуп саналат жана биз эч кандай жылчыктар жок экенине ынануу керек болгон учурга салыштырууга болот.
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 бизге төмөнкүдөй жооп берди:
no solution
Бул чындап эле эч кандай чечимдер жок дегенди билдирет.
Мына ошентип, дыйканга ар кандай жегич карышкыр менен чыгашасыз өтүү мүмкүн эместигин программалык түрдө далилдедик.
Эгерде аудитория бул теманы кызыктуу деп тапса, анда кийинки макалаларда мен сизге кадимки программаны же функцияны формалдуу методдор менен шайкеш келген теңдемеге кантип айландыруу жана аны чечүү жолдорун айтып берем. Биринчиден, ошол эле тапшырма боюнча, бирок программа түрүндө берилген, андан кийин аны акырындык менен татаалдаштырып, программалык камсыздоону иштеп чыгуу дүйнөсүнүн учурдагы мисалдарына өтүү.
Кийинки макала даяр:
Анда мен көйгөйлөрдү формалдуу текшерүүдөн программаларга өтүп, сүрөттөп берем
аларды кантип автоматтык түрдө формалдуу эреже системаларына айландырса болот.
Source: www.habr.com