Fikrimcə, internetin rusdilli sektorunda formal yoxlama mövzusu yetərincə işıqlandırılmır və xüsusən də kifayət qədər sadə və illüstrativ nümunələr yoxdur.
Xarici mənbədən belə bir misal çəkəcəm, canavar, keçi və kələmin çayın o biri tərəfinə keçməsi kimi məlum məsələyə öz həllini əlavə edəcəyəm.
Ancaq əvvəlcə rəsmi yoxlamanın nə olduğunu və nə üçün lazım olduğunu qısaca təsvir edəcəyəm.
Formal yoxlama dedikdə adətən bir proqramın və ya alqoritmin digərinin köməyi ilə yoxlanılması başa düşülür.
Bu, proqramın davranışının gözlənildiyi kimi olmasına əmin olmaq, həmçinin onun təhlükəsizliyini təmin etmək üçün lazımdır.
Formal yoxlama zəiflikləri tapmaq və aradan qaldırmaq üçün ən güclü vasitədir: o, proqramda bütün mövcud boşluqları və səhvləri tapmağa və ya onların olmadığını sübut etməyə imkan verir.
Qeyd etmək lazımdır ki, bəzi hallarda bu mümkün deyil, məsələn, lövhənin eni 8 hüceyrə olan 1000 kraliça problemində: hər şey alqoritmik mürəkkəbliyə və ya dayandırma probleminə əsaslanır.
Lakin istənilən halda üç cavabdan biri alınacaq: proqram düzgündür, səhvdir və ya cavabı hesablamaq mümkün olmayıb.
Cavab tapmaq mümkün deyilsə, çox vaxt konkret bəli və ya yox cavabını almaq üçün proqramın qaranlıq hissələrini onların alqoritmik mürəkkəbliyini azaltmaqla yenidən işləmək mümkündür.
Və rəsmi yoxlama, məsələn, Windows nüvəsində və Darpa dronlarının əməliyyat sistemlərində maksimum qorunma səviyyəsini təmin etmək üçün istifadə olunur.
Avtomatlaşdırılmış teoremlərin sübutu və tənliklərin həlli üçün çox güclü vasitə olan Z3Proverdən istifadə edəcəyik.
Üstəlik, Z3 sadəcə tənlikləri həll edir və onların dəyərlərini kobud qüvvə ilə seçmir.
Bu o deməkdir ki, o, hətta giriş variantları və 10 ^ 100 birləşmələrinin olduğu hallarda cavab tapa bilir.
Lakin bu, yalnız Integer tipli onlarla giriş arqumentidir və bu, praktikada tez-tez baş verir.
8 kraliçanın problemi (İngilis dilindən götürülmüşdür ).
# 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 işlədərək həlli əldə edirik:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
Kraliçalarla bağlı problem, 8 ana arıların koordinatlarını giriş kimi qəbul edən və ana arıların bir-birini döyüb döymədiyinə cavab verən bir proqramla müqayisə edilə bilər.
Əgər belə bir proqramı rəsmi yoxlamadan istifadə edərək həll etsəydik, problemlə müqayisədə proqram kodunu tənliyə çevirmək şəklində sadəcə bir addım atmalıyıq: o, bizimkinə mahiyyətcə eyni olacaq ( təbii ki, proqram səhvsiz yazılıbsa).
Demək olar ki, eyni şey zəifliklərin axtarışı vəziyyətində baş verəcək: biz sadəcə ehtiyac duyduğumuz çıxış şərtlərini təyin edirik, məsələn, administrator parolu, mənbəni və ya dekompilyasiya edilmiş kodu yoxlama ilə uyğun gələn tənliklərə çevirin və sonra hansı məlumatlar barədə cavab alırıq. məqsədə çatmaq üçün daxil olmaq lazımdır.
Məncə, canavar, keçi və kələm problemi daha maraqlıdır, çünki onu həll etmək üçün çoxlu (7) addım lazımdır.
Kraliçaların problemi bir GET və ya POST sorğusu ilə serverə girə biləcəyiniz halla müqayisə edilə bilərsə, o zaman canavar, keçi və kələm məqsədə çata biləcəyiniz daha mürəkkəb və ümumi bir kateqoriyadan bir nümunə göstərir. yalnız bir neçə xahişlə.
Bu, məsələn, SQL inyeksiyasını tapmalı, onun vasitəsilə fayl yazmalı, sonra hüquqlarınızı yüksəltməli və yalnız bundan sonra parol əldə etməli olduğunuz ssenari ilə müqayisə edilə bilər.
Problemin şərtləri və onun həlliFermer bir canavar, bir keçi və bir kələmi çaydan keçirməlidir. Fermerin kəndlinin özündən başqa yalnız bir obyekti sığdıra bilən qayığı var. Əgər fermer onları nəzarətsiz qoysa, canavar keçini, keçi isə kələm yeyəcək.
Cavab budur ki, 4-cü addımda fermer keçini geri götürməli olacaq.
İndi proqramlı şəkildə həll etməyə başlayaq.
Gəlin fermer, canavar, keçi və kələmi yalnız 4 və ya 0 qiyməti alan 1 dəyişən kimi təyin edək. Sıfır onların sol sahildə, biri isə sağda olduğunu bildirir.
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 həll etmək üçün lazım olan addımların sayıdır. Hər bir addım çayın, qayığın və bütün obyektlərin vəziyyətini təmsil edir.
Hələlik onu təsadüfi və marjla seçək, 10 götürək.
Hər bir obyekt 10 instansiyada təmsil olunur - bu, 10 addımın hər birində onun dəyəridir.
İndi başlanğıc və bitiş üçün şərtləri təyin edək.
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 ]
Sonra qurdun keçi və ya keçi kələmini yediyi şərtləri tənlikdə məhdudiyyətlər kimi təyin edirik.
(Əkinçinin yanında aqressiya mümkün deyil)
# 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) ]
Və nəhayət, ordan keçərkən və ya geri dönərkən fermerin bütün mümkün hərəkətlərini müəyyən edək.
Ya özü ilə canavar, keçi, kələm götürə bilər, ya da heç kimi götürə bilməz, ya da heç yerə getməz.
Təbii ki, heç kəs əkinçisiz keçə bilməz.
Bu, çayın, qayığın və obyektlərin hər bir sonrakı vəziyyətinin əvvəlkindən yalnız ciddi məhdud şəkildə fərqlənə biləcəyi ilə ifadə ediləcəkdir.
2 bitdən çox deyil və bir çox digər məhdudiyyətlərlə, çünki fermer bir anda yalnız bir mahiyyət daşıya bilər və hamısı bir yerdə qala bilməz.
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) ]
Həllini işə salaq.
solve(Side + Start + Finish + Safe + Travel)
Və cavabı alırıq!
Z3 ardıcıl və qaneedici vəziyyətlər toplusunu tapdı.
Kosmos-zamanın dördölçülü bir növü.
Gəlin nə baş verdiyini anlayaq.
Görürük ki, axırda hamı keçdi, yalnız əvvəldə fermerimiz istirahət etmək qərarına gəldi və o, ilk 2 pillədə heç yerdə üzmür.
Human_2 = 0
Human_3 = 0
Bu onu göstərir ki, biz həddən artıq çox sayda dövlət seçmişik və 8-i kifayət qədər olacaq.
Bizim vəziyyətimizdə fermer bunu etdi: başla, dincəl, dincəl, keçini bərə, geri qayıdıb, kələmi gəmiyə, keçi ilə qayıt, canavar bərə, tək qayıt, keçini yenidən təslim et.
Amma sonda problem həll olunur.
#Старт.
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
İndi gəlin şərtləri dəyişdirməyə və həll yollarının olmadığını sübut etməyə çalışaq.
Bunu etmək üçün canavarımıza ot yemi bəxş edəcəyik və o, kələm yemək istəyəcək.
Bu, bizim məqsədimizin tətbiqi qorumaq olduğu və heç bir boşluq olmadığına əmin olmalıyıq.
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 bizə aşağıdakı cavabı verdi:
no solution
Bu o deməkdir ki, həqiqətən həll yolları yoxdur.
Beləliklə, fermer üçün itkisiz hər şeyi yeyən canavarla keçməyin mümkünsüzlüyünü proqramlı şəkildə sübut etdik.
Əgər tamaşaçılar bu mövzunu maraqlı hesab edərsə, onda gələcək məqalələrdə mən sizə adi proqramı və ya funksiyanı formal metodlara uyğun gələn tənliyə necə çevirmək və həll etmək yollarını izah edəcəyəm, bununla da həm bütün qanunauyğun ssenariləri, həm də zəiflikləri üzə çıxaracam. Birincisi, eyni tapşırıq üzrə, lakin artıq proqram şəklində təqdim olunur, sonra isə onu tədricən çətinləşdirir və proqram təminatının inkişafı dünyasından aktual nümunələrə keçir.
Növbəti məqalə hazırdır:
Orada problemlərin rəsmi yoxlanışından proqramlara keçirəm və təsvir edirəm:
onları avtomatik olaraq formal qaydalar sisteminə necə çevirə bilərsiniz.
Mənbə: www.habr.com