Yn fy marn i, yn y sector Rwsieg-iaith y Rhyngrwyd, nid yw'r pwnc o wirio ffurfiol yn cael sylw digonol, ac yn arbennig mae diffyg enghreifftiau syml a chlir.
Rhoddaf enghraifft o ffynhonnell dramor, ac ychwanegu fy ateb fy hun i’r broblem adnabyddus o groesi blaidd, gafr a bresych i ochr arall yr afon.
Ond yn gyntaf, byddaf yn disgrifio'n fyr beth yw dilysu ffurfiol a pham mae ei angen.
Mae dilysu ffurfiol fel arfer yn golygu gwirio un rhaglen neu algorithm gan ddefnyddio un arall.
Mae hyn yn angenrheidiol i sicrhau bod y rhaglen yn ymddwyn yn ôl y disgwyl a hefyd i sicrhau ei diogelwch.
Gwirio ffurfiol yw'r ffordd fwyaf pwerus o ddod o hyd i wendidau a'u dileu: mae'n caniatáu ichi ddod o hyd i'r holl dyllau a bygiau presennol mewn rhaglen, neu brofi nad ydynt yn bodoli.
Mae'n werth nodi bod hyn yn amhosibl mewn rhai achosion, megis yn y broblem o 8 brenhines gyda lled bwrdd o 1000 sgwâr: mae hyn i gyd yn dibynnu ar gymhlethdod algorithmig neu'r broblem stopio.
Fodd bynnag, beth bynnag, bydd un o dri ateb yn dod i law: mae'r rhaglen yn gywir, yn anghywir, neu nid oedd yn bosibl cyfrifo'r ateb.
Os yw'n amhosibl dod o hyd i ateb, mae'n aml yn bosibl ail-weithio rhannau aneglur o'r rhaglen, gan leihau eu cymhlethdod algorithmig, er mwyn cael ateb ie neu na penodol.
A defnyddir dilysu ffurfiol, er enghraifft, yn systemau gweithredu drôn Windows a Darpa, i sicrhau'r lefel uchaf o amddiffyniad.
Byddwn yn defnyddio Z3Prover, offeryn pwerus iawn ar gyfer profi theorem awtomataidd a datrys hafaliadau.
Ar ben hynny, mae Z3 yn datrys hafaliadau, ac nid yw'n dewis eu gwerthoedd gan ddefnyddio grym 'n ysgrublaidd.
Mae hyn yn golygu ei fod yn gallu dod o hyd i'r ateb, hyd yn oed mewn achosion lle mae 10^100 cyfuniad o opsiynau mewnbwn.
Ond dim ond tua dwsin o ddadleuon mewnbwn o fath Cyfanrif yw hyn, a deuir ar draws hyn yn aml yn ymarferol.
Problem tua 8 brenhines (Cymerwyd o'r Saesneg ).
# 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)
Wrth redeg Z3, rydyn ni'n cael yr ateb:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
Mae problem y frenhines yn debyg i raglen sy'n cymryd cyfesurynnau 8 brenhines fel mewnbwn ac yn allbynnu'r ateb a yw'r breninesau'n curo ei gilydd.
Pe baem yn datrys rhaglen o'r fath gan ddefnyddio dilysu ffurfiol, yna o'i gymharu â'r broblem, byddai angen i ni gymryd un cam arall ar ffurf trosi cod y rhaglen yn hafaliad: yn ei hanfod byddai'n union yr un fath â'n un ni ( wrth gwrs, os ysgrifennwyd y rhaglen yn gywir).
Bydd bron yr un peth yn digwydd yn achos chwilio am wendidau: rydym yn gosod yr amodau allbwn sydd eu hangen arnom, er enghraifft, y cyfrinair gweinyddol, yn trawsnewid y ffynhonnell neu'r cod wedi'i ddadgrynhoi yn hafaliadau sy'n gydnaws â dilysu, ac yna'n cael ateb ynghylch beth mae angen darparu data fel mewnbwn i gyrraedd y nod.
Yn fy marn i, mae'r broblem am y blaidd, y gafr a'r bresych hyd yn oed yn fwy diddorol, gan fod angen llawer o (7) o gamau i'w datrys eisoes.
Os yw problem y frenhines yn debyg i'r achos lle gallwch chi dreiddio i weinydd gan ddefnyddio un cais GET neu POST, yna mae'r blaidd, gafr a bresych yn dangos enghraifft o gategori llawer mwy cymhleth ac eang, lle gellir cyflawni'r nod yn unig gan nifer o geisiadau.
Mae hyn yn debyg, er enghraifft, i senario lle mae angen i chi ddod o hyd i chwistrelliad SQL, ysgrifennu ffeil drwyddo, yna dyrchafu'ch hawliau a dim ond wedyn cael cyfrinair.
Amodau'r broblem a'i datrysiadMae angen i'r ffermwr gludo blaidd, gafr a bresych ar draws yr afon. Mae gan y ffermwr gwch na all gynnwys ond un gwrthrych, ar wahân i'r ffermwr ei hun. Bydd y blaidd yn bwyta'r gafr a bydd yr afr yn bwyta'r bresych os bydd y ffermwr yn eu gadael heb neb yn gofalu amdanynt.
Yr ateb yw y bydd angen i'r ffermwr, yng ngham 4, gymryd yr afr yn ôl.
Nawr, gadewch i ni ddechrau ei ddatrys yn rhaglennol.
Gadewch i ni ddynodi'r ffermwr, blaidd, gafr a bresych fel 4 newidyn sy'n cymryd y gwerth dim ond 0 neu 1. Mae sero yn golygu eu bod ar y lan chwith, ac mae un yn golygu eu bod ar y dde.
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
Nifer yw nifer y camau sydd eu hangen i'w datrys. Mae pob cam yn cynrychioli cyflwr yr afon, y cwch a phob endid.
Am y tro, gadewch i ni ei ddewis ar hap a chydag ymyl, cymerwch 10.
Cynrychiolir pob endid mewn 10 copi - dyma ei werth ar bob un o'r 10 cam.
Nawr, gadewch i ni osod yr amodau ar gyfer y dechrau a'r diwedd.
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 ]
Yna rydyn ni'n gosod yr amodau lle mae'r blaidd yn bwyta'r gafr, neu'r gafr yn bwyta'r bresych, fel cyfyngiadau yn yr hafaliad.
(Ym mhresenoldeb ffermwr, mae ymosodedd yn amhosibl)
# 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) ]
Ac yn olaf, byddwn yn diffinio holl gamau gweithredu posibl y ffermwr wrth groesi yno neu yn ôl.
Gall naill ai fynd â blaidd, gafr neu fresych gydag ef, neu beidio â mynd â neb, neu beidio â hwylio i unman o gwbl.
Wrth gwrs, ni all neb groesi heb ffermwr.
Bydd hyn yn cael ei fynegi gan y ffaith y gall pob cyflwr dilynol yr afon, cwch ac endidau fod yn wahanol i'r un blaenorol mewn ffordd gyfyngedig yn unig.
Dim mwy na 2 did, a gyda llawer o derfynau eraill, gan mai dim ond un endid y gall y ffermwr ei gludo ar y tro ac ni ellir gadael pob un gyda'i gilydd.
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) ]
Gadewch i ni redeg yr ateb.
solve(Side + Start + Finish + Safe + Travel)
A chawn yr ateb!
Canfu Z3 set gyson o gyflyrau sy'n bodloni'r holl amodau.
Math o gast pedwar dimensiwn o ofod-amser.
Gadewch i ni ddarganfod beth ddigwyddodd.
Gwelwn fod pawb wedi croesi yn y diwedd, dim ond ar y dechrau y penderfynodd ein ffermwr orffwys, ac yn y 2 gam cyntaf nid yw'n nofio yn unman.
Human_2 = 0
Human_3 = 0
Mae hyn yn awgrymu bod nifer y taleithiau a ddewiswyd gennym yn ormodol, a bydd 8 yn eithaf digonol.
Yn ein hachos ni, gwnaeth y ffermwr hyn: cychwyn, gorffwys, gorffwys, croesi'r gafr, croesi'n ôl, croesi'r bresych, dychwelyd gyda'r gafr, croesi'r blaidd, dychwelyd yn ôl ar ei ben ei hun, ail-gyflwyno'r gafr.
Ond yn y diwedd cafodd y broblem ei datrys.
#Старт.
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
Nawr, gadewch i ni geisio newid yr amodau a phrofi nad oes unrhyw atebion.
I wneud hyn, byddwn yn rhoi llysysydd i'n blaidd, a bydd eisiau bwyta bresych.
Gellir cymharu hyn â'r achos lle ein nod yw sicrhau'r cais ac mae angen i ni sicrhau nad oes unrhyw fylchau.
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) ]
Rhoddodd Z3 yr ymateb canlynol i ni:
no solution
Mae'n golygu nad oes unrhyw atebion mewn gwirionedd.
Felly, rydym yn rhaglennol wedi profi ei bod yn amhosibl croesi gyda blaidd omnivorous heb golledion i'r ffermwr.
Os bydd y gynulleidfa'n gweld y pwnc hwn yn ddiddorol, yna mewn erthyglau yn y dyfodol byddaf yn dweud wrthych sut i droi rhaglen neu swyddogaeth arferol yn hafaliad sy'n gydnaws â dulliau ffurfiol, a'i ddatrys, a thrwy hynny ddatgelu'r holl senarios cyfreithlon a gwendidau. Yn gyntaf, ar yr un dasg, ond wedi'i gyflwyno ar ffurf rhaglen, ac yna ei gymhlethu'n raddol a symud ymlaen at enghreifftiau cyfredol o fyd datblygu meddalwedd.
Mae'r erthygl nesaf yn barod:
Ynddo rwy'n symud o ddilysu problemau'n ffurfiol i raglenni, ac yn disgrifio
sut y gellir eu trosi'n systemau rheolau ffurfiol yn awtomatig.
Ffynhonnell: hab.com