Pada pendapat saya, dalam sektor Internet berbahasa Rusia, topik pengesahan rasmi tidak diliputi dengan secukupnya, dan terutamanya kekurangan contoh yang mudah dan jelas.
Saya akan memberikan contoh dari sumber asing, dan menambah penyelesaian saya sendiri kepada masalah yang terkenal menyeberangi serigala, kambing dan kubis ke seberang sungai.
Tetapi pertama-tama, saya akan menerangkan secara ringkas apakah pengesahan rasmi dan mengapa ia diperlukan.
Pengesahan rasmi biasanya bermaksud menyemak satu program atau algoritma menggunakan yang lain.
Ini adalah perlu untuk memastikan program berkelakuan seperti yang diharapkan dan juga untuk memastikan keselamatannya.
Pengesahan rasmi ialah cara yang paling berkuasa untuk mencari dan menghapuskan kelemahan: ia membolehkan anda mencari semua lubang dan pepijat yang sedia ada dalam program, atau membuktikan bahawa ia tidak wujud.
Perlu diingat bahawa dalam beberapa kes ini adalah mustahil, seperti dalam masalah 8 ratu dengan lebar papan 1000 petak: semuanya berpunca daripada kerumitan algoritma atau masalah berhenti.
Walau bagaimanapun, dalam apa jua keadaan, satu daripada tiga jawapan akan diterima: program itu betul, salah, atau tidak mungkin untuk mengira jawapan.
Sekiranya mustahil untuk mencari jawapan, selalunya mungkin untuk mengolah semula bahagian program yang tidak jelas, mengurangkan kerumitan algoritmanya, untuk mendapatkan jawapan ya atau tidak khusus.
Dan pengesahan rasmi digunakan, contohnya, dalam kernel Windows dan sistem pengendalian drone Darpa, untuk memastikan tahap perlindungan maksimum.
Kami akan menggunakan Z3Prover, alat yang sangat berkuasa untuk pembuktian teorem automatik dan penyelesaian persamaan.
Selain itu, Z3 menyelesaikan persamaan, dan tidak memilih nilainya menggunakan kekerasan.
Ini bermakna ia dapat mencari jawapan, walaupun dalam kes di mana terdapat 10^100 kombinasi pilihan input.
Tetapi ini hanya kira-kira sedozen argumen input jenis Integer, dan ini sering ditemui dalam amalan.
Masalah tentang 8 ratu (Diambil daripada bahasa Inggeris ).
# 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)
Menjalankan Z3, kami mendapat penyelesaiannya:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
Masalah ratu adalah setanding dengan program yang mengambil sebagai input koordinat 8 ratu dan mengeluarkan jawapan sama ada ratu mengalahkan satu sama lain.
Sekiranya kami menyelesaikan program sedemikian menggunakan pengesahan rasmi, maka berbanding dengan masalahnya, kami hanya perlu mengambil satu langkah lagi dalam bentuk menukar kod program menjadi persamaan: ia akan menjadi pada dasarnya sama dengan kami ( sudah tentu, jika program itu ditulis dengan betul).
Perkara yang hampir sama akan berlaku dalam kes mencari kelemahan: kami hanya menetapkan syarat output yang kami perlukan, sebagai contoh, kata laluan pentadbir, mengubah sumber atau kod yang dinyahkompilasi menjadi persamaan yang serasi dengan pengesahan, dan kemudian mendapatkan jawapan tentang apa data perlu dibekalkan sebagai input untuk mencapai matlamat.
Pada pendapat saya, masalah tentang serigala, kambing dan kubis adalah lebih menarik, kerana menyelesaikannya sudah memerlukan banyak (7) langkah.
Jika masalah ratu adalah setanding dengan kes di mana anda boleh menembusi pelayan dengan satu permintaan GET atau POST, maka serigala, kambing dan kubis menunjukkan contoh dari kategori yang lebih kompleks dan meluas, di mana matlamat hanya boleh dicapai dengan beberapa permintaan.
Ini adalah setanding, sebagai contoh, dengan senario di mana anda perlu mencari suntikan SQL, menulis fail melaluinya, kemudian meningkatkan hak anda dan hanya kemudian mendapatkan kata laluan.
Keadaan masalah dan penyelesaiannyaPetani perlu mengangkut seekor serigala, kambing dan kubis menyeberangi sungai. Petani mempunyai bot yang hanya boleh memuatkan satu objek, selain petani itu sendiri. Serigala akan memakan kambing dan kambing akan memakan kubis jika petani meninggalkannya tanpa pengawasan.
Penyelesaiannya ialah dalam langkah 4 penternak perlu mengambil semula kambing tersebut.
Sekarang mari kita mula menyelesaikannya secara pemrograman.
Mari kita nyatakan petani, serigala, kambing dan kubis sebagai 4 pembolehubah yang mengambil nilai hanya 0 atau 1. Sifar bermakna mereka berada di tebing kiri, dan satu bermakna mereka berada di sebelah kanan.
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 ialah bilangan langkah yang diperlukan untuk menyelesaikan. Setiap langkah mewakili keadaan sungai, bot dan semua entiti.
Buat masa ini, mari pilih secara rawak dan dengan margin, ambil 10.
Setiap entiti diwakili dalam 10 salinan - ini ialah nilainya pada setiap 10 langkah.
Sekarang mari kita tetapkan syarat untuk permulaan dan penamat.
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 ]
Kemudian kami menetapkan syarat di mana serigala makan kambing, atau kambing makan kubis, sebagai kekangan dalam persamaan.
(Dengan kehadiran seorang petani, pencerobohan adalah mustahil)
# 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) ]
Dan akhirnya, kami akan menentukan semua kemungkinan tindakan petani apabila menyeberang ke sana atau kembali.
Dia boleh sama ada membawa seekor serigala, kambing atau kubis bersamanya, atau tidak membawa sesiapa, atau tidak belayar ke mana-mana sama sekali.
Sudah tentu, tiada siapa yang boleh menyeberang tanpa seorang petani.
Ini akan dinyatakan oleh fakta bahawa setiap keadaan sungai, bot dan entiti berikutnya boleh berbeza daripada yang sebelumnya hanya dengan cara yang sangat terhad.
Tidak lebih daripada 2 bit, dan dengan banyak had lain, kerana petani hanya boleh mengangkut satu entiti pada satu masa dan tidak semua boleh dibiarkan bersama.
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) ]
Mari jalankan penyelesaiannya.
solve(Side + Start + Finish + Safe + Travel)
Dan kami mendapat jawapannya!
Z3 menemui set keadaan yang konsisten yang memenuhi semua syarat.
Sejenis lakonan empat dimensi ruang-masa.
Mari kita fikirkan apa yang berlaku.
Kami melihat bahawa pada akhirnya semua orang menyeberang, hanya pada mulanya petani kami memutuskan untuk berehat, dan dalam 2 langkah pertama dia tidak berenang di mana-mana.
Human_2 = 0
Human_3 = 0
Ini menunjukkan bahawa bilangan negeri yang kami pilih adalah berlebihan, dan 8 akan cukup mencukupi.
Dalam kes kami, petani melakukan ini: mula, berehat, berehat, menyeberangi kambing, menyeberang kembali, menyeberangi kubis, kembali dengan kambing, menyeberangi serigala, kembali sendiri, menghantar semula kambing.
Tetapi akhirnya masalah itu selesai.
#Π‘ΡΠ°ΡΡ.
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
Sekarang mari cuba ubah syarat dan buktikan bahawa tiada penyelesaian.
Untuk melakukan ini, kami akan memberikan herbivori serigala kami, dan dia akan mahu makan kubis.
Ini boleh dibandingkan dengan kes di mana matlamat kami adalah untuk mendapatkan aplikasi dan kami perlu memastikan bahawa tiada kelemahan.
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 memberi kami respons berikut:
no solution
Ini bermakna bahawa tidak ada penyelesaian.
Oleh itu, kami secara pemrograman membuktikan kemustahilan menyeberang dengan serigala omnivor tanpa kerugian bagi petani.
Jika penonton mendapati topik ini menarik, maka dalam artikel akan datang saya akan memberitahu anda cara menukar program atau fungsi biasa menjadi persamaan yang serasi dengan kaedah formal, dan menyelesaikannya, dengan itu mendedahkan kedua-dua senario dan kelemahan yang sah. Pertama, pada tugas yang sama, tetapi dibentangkan dalam bentuk program, dan kemudian secara beransur-ansur merumitkannya dan beralih kepada contoh semasa dari dunia pembangunan perisian.
Artikel seterusnya sudah sedia:
Di dalamnya saya beralih daripada pengesahan formal masalah kepada program, dan menerangkan
bagaimana ia boleh ditukar menjadi sistem peraturan formal secara automatik.
Sumber: www.habr.com