🥇Bo'ri, echki va karam muammosi misolida rasmiy tekshirish

Menimcha, internetning rus tilidagi sektorida rasmiy tekshirish mavzusi yetarlicha yoritilmagan, ayniqsa, oddiy va tushunarli misollar yetishmaydi.

Men chet el manbasidan misol keltiraman va daryoning narigi tomoniga bo'ri, echki va karamni kesib o'tish kabi mashhur muammoga o'z yechimimni qo'shaman.

Lekin birinchi navbatda, men rasmiy tekshirish nima ekanligini va nima uchun kerakligini qisqacha tasvirlab beraman.

Rasmiy tekshirish odatda bitta dastur yoki algoritm yordamida boshqasini tekshirishni anglatadi.

Bu dastur kutilgandek harakat qilishini ta'minlash va uning xavfsizligini ta'minlash uchun zarur.

Rasmiy tekshirish zaifliklarni topish va yo'q qilishning eng kuchli vositasidir: u sizga dasturdagi barcha mavjud teshik va xatolarni topish yoki ular yo'qligini isbotlash imkonini beradi.
Shuni ta'kidlash kerakki, ba'zi hollarda bu mumkin emas, masalan, 8 kvadrat kenglikdagi 1000 ta malika muammosida: bularning barchasi algoritmik murakkablik yoki to'xtash muammosiga to'g'ri keladi.

Biroq, har qanday holatda, uchta javobdan biri olinadi: dastur to'g'ri, noto'g'ri yoki javobni hisoblash mumkin emas.

Agar javobni topishning iloji bo'lmasa, aniq ha yoki yo'q javobini olish uchun ko'pincha dasturning aniq bo'lmagan qismlarini algoritmik murakkabligini kamaytiradigan qayta ishlash mumkin.

Rasmiy tekshirish, masalan, Windows yadrosi va Darpa dron operatsion tizimlarida maksimal himoya darajasini ta'minlash uchun qo'llaniladi.

Biz teoremani avtomatlashtirilgan isbotlash va tenglamalarni yechish uchun juda kuchli vosita Z3Proverdan foydalanamiz.

Bundan tashqari, Z3 tenglamalarni echadi va qo'pol kuch yordamida ularning qiymatlarini tanlamaydi.
Bu shuni anglatadiki, u 10^100 kiritish variantlari kombinatsiyasi mavjud bo'lgan hollarda ham javobni topa oladi.

Ammo bu Integer tipidagi o'nga yaqin kirish argumentlari va bu amaliyotda tez-tez uchrab turadi.

8 ta malika haqidagi muammo (Ingliz tilidan olingan qo'llanma).

# 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-ni ishga tushirib, biz yechimni olamiz:

[Q_5 = 1,
 Q_8 = 7,
 Q_3 = 8,
 Q_2 = 2,
 Q_6 = 3,
 Q_4 = 6,
 Q_7 = 5,
 Q_1 = 4]

Qirolicha muammosi 8 ta malikaning koordinatalarini kiritadigan va malikalar bir-birini urishadimi yoki yo'qmi degan javobni chiqaradigan dastur bilan solishtirish mumkin.

Agar biz bunday dasturni rasmiy tekshirish yordamida hal qiladigan bo'lsak, muammo bilan solishtirganda, dastur kodini tenglamaga aylantirish shaklida yana bir qadam tashlashimiz kerak bo'ladi: u biznikiga deyarli bir xil bo'lib chiqadi ( albatta, agar dastur to'g'ri yozilgan bo'lsa).

Zaifliklarni qidirishda deyarli bir xil narsa sodir bo'ladi: biz shunchaki kerakli chiqish shartlarini o'rnatamiz, masalan, administrator paroli, manba yoki dekompilyatsiya qilingan kodni tekshirishga mos keladigan tenglamalarga aylantiramiz va keyin nima bo'lishi haqida javob olamiz. Maqsadga erishish uchun ma'lumotlar kirish sifatida taqdim etilishi kerak.

Menimcha, bo'ri, echki va karam haqidagi muammo yanada qiziqroq, chunki uni hal qilish allaqachon ko'p (7) qadamni talab qiladi.

Agar malika muammosi bitta GET yoki POST so'rovi yordamida serverga kirishingiz mumkin bo'lgan holat bilan taqqoslansa, bo'ri, echki va karam yanada murakkab va keng tarqalgan toifadagi misolni ko'rsatadi, bunda faqat maqsadga erishish mumkin. bir nechta so'rovlar bilan.

Buni, masalan, SQL in'ektsiyasini topishingiz, u orqali fayl yozishingiz, keyin huquqlaringizni oshirishingiz va shundan keyingina parol olishingiz kerak bo'lgan stsenariy bilan solishtirish mumkin.

Muammoning shartlari va uni hal qilishDehqon daryo bo'ylab bo'ri, echki va karamni tashishi kerak. Fermerning o'zidan tashqari faqat bitta ob'ektni sig'dira oladigan qayig'i bor. Dehqon ularni qarovsiz qoldirsa, echkini bo‘ri, karamni esa echki yeydi.

Yechim shundaki, 4-bosqichda fermer echkini qaytarib olishi kerak.
Endi uni dasturiy jihatdan hal qilishni boshlaylik.

Fermer, bo'ri, echki va karamni faqat 4 yoki 0 qiymatini qabul qiladigan 1 ta o'zgaruvchi sifatida belgilaymiz. Nol ularning chap qirg'og'ida, bittasi esa o'ng tomonda ekanligini bildiradi.

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 - hal qilish uchun zarur bo'lgan qadamlar soni. Har bir qadam daryo, qayiq va barcha ob'ektlarning holatini ifodalaydi.

Hozircha uni tasodifiy va marj bilan tanlaymiz, 10 ni oling.

Har bir ob'ekt 10 nusxada taqdim etilgan - bu 10 bosqichning har biridagi qiymati.

Endi boshlanish va tugatish shartlarini belgilaymiz.

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 ]

Keyin biz tenglamada cheklovlar sifatida bo'ri echkini yoki echki karamni yeyish shartlarini belgilaymiz.
(Fermer borligida tajovuzkorlik mumkin emas)

# 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) ]

Va nihoyat, biz fermerning u yerdan o'tish yoki orqaga qaytishdagi barcha mumkin bo'lgan harakatlarini aniqlaymiz.
U o'zi bilan bo'ri, echki yoki karamni olib ketishi mumkin yoki hech kimni olib ketmasligi yoki umuman suzib ketmasligi mumkin.

Albatta, hech kim dehqonsiz o'tolmaydi.

Bu daryo, qayiq va ob'ektlarning har bir keyingi holati avvalgisidan faqat qat'iy cheklangan tarzda farq qilishi mumkinligi bilan ifodalanadi.

2 bitdan ko'p bo'lmagan va boshqa ko'plab cheklovlar bilan, chunki fermer bir vaqtning o'zida faqat bitta ob'ektni tashishi mumkin va barchasini birga qoldirib bo'lmaydi.

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) ]

Keling, yechimni ishga tushiramiz.

solve(Side + Start + Finish + Safe + Travel)

Va biz javobni olamiz!

Z3 barcha shartlarni qondiradigan izchil holatlar to'plamini topdi.
Fazo-vaqtning to'rt o'lchovli bir turi.

Keling, nima bo'lganini aniqlaylik.

Ko'ramiz, oxir-oqibat hamma kesib o'tdi, faqat dehqonimiz dastlab dam olishga qaror qildi va dastlabki 2 qadamda u hech qayerda suzmaydi.

Human_2 = 0
Human_3 = 0

Bu shuni ko'rsatadiki, biz tanlagan shtatlar soni haddan tashqari ko'p va 8 ta etarli bo'ladi.

Bizning holatda, fermer shunday qildi: boshlash, dam olish, dam olish, echkini kesib o'tish, orqaga o'tish, karamni kesib o'tish, echki bilan qaytish, bo'rini kesib o'tish, yolg'iz qaytib, echkini qayta topshirish.

Ammo oxir-oqibat muammo hal qilindi.

#Старт.
 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

Keling, shartlarni o'zgartirishga harakat qilaylik va hech qanday yechim yo'qligini isbotlaymiz.

Buning uchun biz bo'rimizga o'txo'rlik beramiz va u karam iste'mol qilishni xohlaydi.
Buni bizning maqsadimiz dastur xavfsizligini ta'minlash bo'lgan holat bilan solishtirish mumkin va biz hech qanday bo'shliqlar yo'qligiga ishonch hosil qilishimiz kerak.

 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 bizga quyidagi javobni berdi:

 no solution

Bu haqiqatan ham hech qanday yechim yo'qligini anglatadi.

Shunday qilib, biz dasturli ravishda fermer uchun omnivor bo'ri bilan yo'qotishlarsiz o'tish mumkin emasligini isbotladik.

Agar tomoshabinlar ushbu mavzuni qiziqarli deb topsa, keyingi maqolalarda men sizga oddiy dastur yoki funktsiyani qanday qilib rasmiy usullarga mos keladigan tenglamaga aylantirish va uni hal qilish va shu bilan barcha qonuniy stsenariylarni va zaifliklarni ochib berishni aytib beraman. Birinchidan, xuddi shu vazifa bo'yicha, lekin dastur ko'rinishida taqdim etiladi, keyin uni asta-sekin murakkablashtiradi va dasturiy ta'minotni ishlab chiqish dunyosidan hozirgi misollarga o'tadi.

Keyingi maqola allaqachon tayyor:
Rasmiy tekshirish tizimini noldan yaratish: PHP va Pythonda ramziy VM yozish

Unda men muammolarni rasmiy tekshirishdan dasturlarga o'taman va tasvirlayman
qanday qilib ular avtomatik ravishda rasmiy qoidalar tizimiga aylantirilishi mumkin.

Manba: www.habr.com

Bo'ri, echki va karam muammosi misolida rasmiy tekshirish

a Izoh qo'shish Bu savolga javob bekor