Is e dearbhadh foirmeil dearbhadh aon phrògram no algairim a’ cleachdadh fear eile.
Is e seo aon de na dòighean as cumhachdaiche a leigeas leat a h-uile so-leòntachd a lorg ann am prògram no dearbhadh nach eil iad ann.
Tha tuairisgeul nas mionaidiche air dearbhadh foirmeil ri fhaicinn anns an eisimpleir de bhith a’ fuasgladh na trioblaid anns an artaigil agam roimhe.
San artaigil seo bidh mi a’ gluasad bho dhearbhadh foirmeil air duilgheadasan gu prògraman agus ag innse mar a tha
ciamar a ghabhas an tionndadh gu siostaman riaghlaidh foirmeil gu fèin-ghluasadach.
Gus seo a dhèanamh, sgrìobh mi an analogue agam fhèin de inneal brìgheil, a’ cleachdadh prionnsapalan samhlachail.
Bidh e a’ parsadh còd a’ phrògraim agus ga eadar-theangachadh gu siostam co-aontaran (SMT), a dh’ fhaodar a rèiteach gu prògramach mu thràth.
Leis gu bheil fiosrachadh mu àireamhachadh samhlachail air a thaisbeanadh air an eadar-lìn gu ìre bheag,
Bheir mi cunntas goirid air dè a th’ ann.
Tha àireamhachadh samhlachail na dhòigh air prògram a chuir an gnìomh aig an aon àm air raon farsaing de dhàta agus is e am prìomh inneal airson dearbhadh prògram foirmeil.
Mar eisimpleir, is urrainn dhuinn suidheachaidhean cuir a-steach a shuidheachadh far an gabh a’ chiad argamaid luachan dearbhach sam bith, an dàrna àicheil, an treas neoni, agus an argamaid toraidh, mar eisimpleir, 42.
Bheir àireamhachadh samhlachail ann an aon ruith am freagairt dhuinn a bheil e comasach dhuinn an toradh a tha thu ag iarraidh fhaighinn agus eisimpleir de sheata de pharaimearan cuir a-steach mar sin. No dearbhadh nach eil crìochan mar sin ann.
A bharrachd air an sin, is urrainn dhuinn na h-argamaidean cuir a-steach a shuidheachadh gu gach fear a tha comasach, agus dìreach an fheadhainn toraidh a thaghadh, mar eisimpleir, facal-faire an rianaire.
Anns a 'chùis seo, lorgaidh sinn a h-uile so-leòntachd a' phrògram no gheibh sinn dearbhadh gu bheil facal-faire an rianaire sàbhailte.
Faodar a thoirt fa-near gu bheil coileanadh clasaigeach prògram le dàta inntrigidh sònraichte na chùis shònraichte de choileanadh samhlachail.
Mar sin, faodaidh mo charactar VM obrachadh cuideachd ann am modh emulation de inneal brìgheil àbhaisteach.
Anns na beachdan don artaigil roimhe seo lorgar càineadh cothromach air dearbhadh foirmeil le deasbad air na laigsean aige.
Is iad na prìomh dhuilgheadasan:
- Spreadh co-phàirteach, leis gu bheil dearbhadh foirmeil mu dheireadh a’ tighinn sìos gu P = NP
- Tha e nas duilghe fiosan a ghiullachd chun t-siostam faidhle, lìonraidhean agus stòradh taobh a-muigh eile
- Bugs anns an t-sònrachadh, nuair a bha an neach-ceannach no am prògramadair an dùil aon rud, ach nach tug iad cunntas ceart gu leòr air anns an t-sònrachadh teignigeach.
Mar thoradh air an sin, thèid am prògram a dhearbhadh agus gèilleadh ris an t-sònrachadh, ach nì e rudeigin gu tur eadar-dhealaichte bho na bha an luchd-cruthachaidh a’ sùileachadh bhuaithe.
Leis gu bheil mi san artaigil seo sa mhòr-chuid a’ beachdachadh air cleachdadh dearbhadh foirmeil ann an cleachdadh, cha bhith mi a’ bualadh mo cheann an aghaidh a’ bhalla airson a-nis, agus taghaidh mi siostam far nach eil cho iom-fhillteachd algorithmach agus an àireamh de ghairmean bhon taobh a-muigh ach glè bheag.
Leis gu bheil cùmhnantan snasail a’ freagairt air na riatanasan sin, thuit an roghainn air cùmhnantan RIDE bho àrd-ùrlar Waves: chan eil iad Turing coileanta, agus tha an iom-fhillteachd as àirde aca cuibhrichte gu saor-thoileach.
Ach beachdaichidh sinn orra a-mhàin bhon taobh theicnigeach.
A bharrachd air a h-uile càil, bidh dearbhadh foirmeil gu sònraichte ann an iarrtas airson cùmhnantan sam bith: mar as trice tha e do-dhèanta mearachd cùmhnant a cheartachadh às deidh dha a bhith air a chuir air bhog.
Agus faodaidh cosgais leithid de mhearachdan a bhith glè àrd, leis gu bheil tòrr airgead gu tric air a stòradh air cùmhnantan sgairteil.
Tha an inneal brìgheil samhlachail agam sgrìobhte ann am PHP agus Python, agus a’ cleachdadh Z3Prover bho Microsoft Research gus fuasgladh fhaighinn air na foirmlean SMT a thig às.
Aig a chridhe tha rannsachadh ioma-ghnìomhach cumhachdach, a tha
leigeil leat fuasglaidhean no so-leòntachd a lorg, eadhon ged a dh’ fheumas e mòran ghnothaichean.
Eadhon an , aon de na frèaman samhlachail as cumhachdaiche airson so-leòntachd Ethereum a lorg, cha do chuir e ach an comas seo beagan mhìosan air ais.
Ach is fhiach a bhith mothachail gu bheil cùmhnantan ether nas iom-fhillte agus Turing coileanta.
Bidh PHP ag eadar-theangachadh còd stòr cùmhnant smart RIDE gu sgriobt python, anns a bheil am prògram air a thaisbeanadh mar shiostam de stàitean cùmhnant Z3 SMT-co-chosmhail agus cumhachan airson an eadar-ghluasad:
A-nis bheir mi cunntas nas mionaidiche air na tha a’ tachairt a-staigh.
Ach an toiseach, beagan fhaclan mun chànan cùmhnant smart RIDE.
Is e cànan prògramadh gnìomh agus faireachdainn a th’ ann a tha leisg a thaobh dealbhadh.
Bidh RIDE a’ ruith leotha fhèin taobh a-staigh an blockchain agus is urrainn dha fiosrachadh fhaighinn air ais agus a sgrìobhadh bho stòradh ceangailte ri wallet an neach-cleachdaidh.
Faodaidh tu cùmhnant RIDE a cheangal ri gach wallet, agus cha bhi toradh a’ chuir gu bàs ach TRUE no FALSE.
Tha TRUE a’ ciallachadh gu bheil an cùmhnant snasail a’ ceadachadh a’ ghnothaich, agus tha FALSE a’ ciallachadh gu bheil e ga thoirmeasg.
Eisimpleir shìmplidh: faodaidh sgriobt casg a chuir air gluasad ma tha cothromachadh wallet nas lugha na 100.
Mar eisimpleir, gabhaidh mi an aon Madadh-allaidh, Gobhar, agus Càl, ach air a thaisbeanadh mar-thà ann an cruth cùmhnant snasail.
Cha bhith e comasach don neach-cleachdaidh airgead a tharraing air ais bhon wallet air a bheil an cùmhnant air a chleachdadh gus am bi e air a h-uile duine a chuir chun taobh eile.
#Извлекаем положение всех объектов из блокчейна
let contract = tx.sender
let human= extract(getInteger(contract,"human"))
let wolf= extract(getInteger(contract,"wolf"))
let goat= extract(getInteger(contract,"goat"))
let cabbage= extract(getInteger(contract,"cabbage"))
#Это так называемая дата-транзакция, в которой пользователь присылает новые 4 переменные.
#Контракт разрешит её только в случае если все объекты останутся в сохранности.
match tx {
case t:DataTransaction =>
#Извлекаем будущее положение всех объектов из транзакции
let newHuman= extract(getInteger(t.data,"human"))
let newWolf= extract(getInteger(t.data,"wolf"))
let newGoat= extract(getInteger(t.data,"goat"))
let newCabbage= extract(getInteger(t.data,"cabbage"))
#0 обозначает, что объект на левом берегу, а 1 что на правом
let humanSide= human == 0 || human == 1
let wolfSide= wolf == 0 || wolf == 1
let goatSide= goat == 0 || goat == 1
let cabbageSide= cabbage == 0 || cabbage == 1
let side= humanSide && wolfSide && goatSide && cabbageSide
#Будут разрешены только те транзакции, где с козой никого нет в отсутствии фермера.
let safeAlone= newGoat != newWolf && newGoat != newCabbage
let safe= safeAlone || newGoat == newHuman
let humanTravel= human != newHuman
#Способы путешествия фермера туда и обратно, с кем-то либо в одиночку.
let t1= humanTravel && newWolf == wolf + 1 && newGoat == goat && newCabbage == cabbage
let t2= humanTravel && newWolf == wolf && newGoat == goat + 1 && newCabbage == cabbage
let t3= humanTravel && newWolf == wolf && newGoat == goat && newCabbage == cabbage + 1
let t4= humanTravel && newWolf == wolf - 1 && newGoat == goat && newCabbage == cabbage
let t5= humanTravel && newWolf == wolf && newGoat == goat - 1 && newCabbage == cabbage
let t6= humanTravel && newWolf == wolf && newGoat == goat && newCabbage == cabbage - 1
let t7= humanTravel && newWolf == wolf && newGoat == goat && newCabbage == cabbage
let objectTravel = t1 || t2 || t3 || t4 || t5 || t6 || t7
#Последняя строка в разделе транзакции описывает разрешающее транзакцию условие.
#Переменные транзакции должны иметь значения 1 или 0, все объекты должны
#быть в безопасности, а фермер должен переплывать реку в одиночку
#или с кем-то на каждом шагу
side && safe && humanTravel && objectTravel
case s:TransferTransaction =>
#Транзакция вывода средств разрешена только в случае если все переплыли на другой берег
human == 1 && wolf == 1 && goat == 1 && cabbage == 1
#Все прочие типы транзакций запрещены
case _ => false
}
Bidh PHP an-toiseach a’ toirt a-mach na caochladairean gu lèir bhon chùmhnant snasail ann an cruth na h-iuchraichean aca agus an caochladair abairt Boolean co-fhreagarrach.
cabbage: extract ( getInteger ( contract , "cabbage" ) )
goat: extract ( getInteger ( contract , "goat" ) )
human: extract ( getInteger ( contract , "human" ) )
wolf: extract ( getInteger ( contract , "wolf" ) )
fState: human== 1 && wolf== 1 && goat== 1 && cabbage== 1
fState:
wolf:
goat:
cabbage:
cabbageSide: cabbage== 0 || cabbage== 1
human: extract ( getInteger ( contract , "human" ) )
newGoat: extract ( getInteger ( t.data , "goat" ) )
newHuman: extract ( getInteger ( t.data , "human" ) )
goatSide: goat== 0 || goat== 1
humanSide: human== 0 || human== 1
t7: humanTravel && newWolf== wolf && newGoat== goat && newCabbage== cabbage
t3: humanTravel && newWolf== wolf && newGoat== goat && newCabbage== cabbage + 1
t6: humanTravel && newWolf== wolf && newGoat== goat && newCabbage== cabbage - 1
t2: humanTravel && newWolf== wolf && newGoat== goat + 1 && newCabbage== cabbage
t5: humanTravel && newWolf== wolf && newGoat== goat - 1 && newCabbage== cabbage
t1: humanTravel && newWolf== wolf + 1 && newGoat== goat && newCabbage== cabbage
t4: humanTravel && newWolf== wolf - 1 && newGoat== goat && newCabbage== cabbage
safeAlone: newGoat != newWolf && newGoat != newCabbage
wolfSide: wolf== 0 || wolf== 1
humanTravel: human != newHuman
side: humanSide && wolfSide && goatSide && cabbageSide
safe: safeAlone || newGoat== newHuman
objectTravel: t1 || t2 || t3 || t4 || t5 || t6 || t7
Bidh PHP an uairsin gan tionndadh gu tuairisgeul siostam Z3Prover a tha co-chosmhail ri SMT ann am Python.
Tha an dàta air a phasgadh ann an lùb, far am faigh caochladairean stòraidh clàr-amais i, clàr-amais caochladairean malairt i + 1, agus caochladairean le abairtean a’ suidheachadh nan riaghailtean airson gluasad bhon stàit roimhe chun ath stàit.
Is e seo fìor chridhe an inneal brìgheil againn, a tha a’ toirt seachad inneal sgrùdaidh ioma-ghnìomhach.
fState: And( And( And( human[Steps] == 1 , wolf[Steps] == 1 ) , goat[Steps] == 1 ) , cabbage[Steps] == 1 )
final: fState[Steps]
fState:
wolf:
goat:
cabbage:
cabbageSide: Or( cabbage[i] == 0 , cabbage[i] == 1 )
goatSide: Or( goat[i] == 0 , goat[i] == 1 )
humanSide: Or( human[i] == 0 , human[i] == 1 )
t7: And( And( And( humanTravel[i] , wolf == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage == cabbage[i] )
t3: And( And( And( humanTravel[i] , wolf == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage == cabbage[i] + 1 )
t6: And( And( And( humanTravel[i] , wolf == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage == cabbage[i] - 1 )
t2: And( And( And( humanTravel[i] , wolf == wolf[i] ) , goat[i+1] == goat[i] + 1 ) , cabbage == cabbage[i] )
t5: And( And( And( humanTravel[i] , wolf == wolf[i] ) , goat[i+1] == goat[i] - 1 ) , cabbage == cabbage[i] )
t1: And( And( And( humanTravel[i] , wolf == wolf[i] + 1 ) , goat[i+1] == goat[i] ) , cabbage == cabbage[i] )
t4: And( And( And( humanTravel[i] , wolf == wolf[i] - 1 ) , goat[i+1] == goat[i] ) , cabbage == cabbage[i] )
safeAlone: And( goat[i+1] != wolf , goat[i+1] != cabbage )
wolfSide: Or( wolf[i] == 0 , wolf[i] == 1 )
humanTravel: human[i] != human[i+1]
side: And( And( And( humanSide[i] , wolfSide[i] ) , goatSide[i] ) , cabbageSide[i] )
safe: Or( safeAlone[i] , goat[i+1] == human[i+1] )
objectTravel: Or( Or( Or( Or( Or( Or( t1[i] , t2[i] ) , t3[i] ) , t4[i] ) , t5[i] ) , t6[i] ) , t7[i] )
data: And( And( And( side[i] , safe[i] ) , humanTravel[i] ) , objectTravel[i] )
Tha na cumhaichean air an òrdachadh agus air an cur a-steach do theamplaid sgriobt a chaidh a dhealbhadh gus cunntas a thoirt air an t-siostam SMT ann am Python.
Teamplaid bàn
import json
from z3 import *
s = Solver()
Steps=7
Num= Steps+1
$code$
#template, only start rest
s.add(data + start)
#template
s.add(final)
ind = 0
f = open("/var/www/html/all/bin/python/log.txt", "a")
while s.check() == sat:
ind = ind +1
print ind
m = s.model()
print m
print "traversing model..."
#for d in m.decls():
#print "%s = %s" % (d.name(), m[d])
f.write(str(m))
f.write("nn")
exit()
#s.add(Or(goat[0] != s.model()[data[0]] )) # prevent next model from using the same assignment as a previous model
print "Total solution number: "
print ind
f.close()
Airson an stàit mu dheireadh san t-sreath gu lèir, tha na riaghailtean a tha air an sònrachadh anns an roinn malairt gluasaid air an cur an sàs.
Tha seo a’ ciallachadh gum bi Z3Prover a’ coimhead airson dìreach seataichean de chumhachan a leigeas le airgead a tharraing air ais bhon chùmhnant aig a’ cheann thall.
Mar thoradh air an sin, bidh sinn gu fèin-ghluasadach a’ faighinn modal SMT làn-ghnìomhach den chùmhnant againn.
Chì thu gu bheil e glè choltach ris a’ mhodail bhon artaigil a rinn mi roimhe, a chuir mi ri chèile le làimh.
Teamplaid crìochnaichte
import json
from z3 import *
s = Solver()
Steps=7
Num= Steps+1
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) ]
nothing= [ And( human[i] == human[i+1], wolf[i] == wolf[i+1], goat[i] == goat[i+1], cabbage[i] == cabbage[i+1] ) for i in range(Num-1) ]
start= [ human[0] == 1, wolf[0] == 0, goat[0] == 1, cabbage[0] == 0 ]
safeAlone= [ And( goat[i+1] != wolf[i+1] , goat[i+1] != cabbage[i+1] ) for i in range(Num-1) ]
safe= [ Or( safeAlone[i] , goat[i+1] == human[i+1] ) for i in range(Num-1) ]
humanTravel= [ human[i] != human[i+1] for i in range(Num-1) ]
cabbageSide= [ Or( cabbage[i] == 0 , cabbage[i] == 1 ) for i in range(Num-1) ]
goatSide= [ Or( goat[i] == 0 , goat[i] == 1 ) for i in range(Num-1) ]
humanSide= [ Or( human[i] == 0 , human[i] == 1 ) for i in range(Num-1) ]
t7= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage[i+1] == cabbage[i] ) for i in range(Num-1) ]
t3= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage[i+1] == cabbage[i] + 1 ) for i in range(Num-1) ]
t6= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage[i+1] == cabbage[i] - 1 ) for i in range(Num-1) ]
t2= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] ) , goat[i+1] == goat[i] + 1 ) , cabbage[i+1] == cabbage[i] ) for i in range(Num-1) ]
t5= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] ) , goat[i+1] == goat[i] - 1 ) , cabbage[i+1] == cabbage[i] ) for i in range(Num-1) ]
t1= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] + 1 ) , goat[i+1] == goat[i] ) , cabbage[i+1] == cabbage[i] ) for i in range(Num-1) ]
t4= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] - 1 ) , goat[i+1] == goat[i] ) , cabbage[i+1] == cabbage[i] ) for i in range(Num-1) ]
wolfSide= [ Or( wolf[i] == 0 , wolf[i] == 1 ) for i in range(Num-1) ]
side= [ And( And( And( humanSide[i] , wolfSide[i] ) , goatSide[i] ) , cabbageSide[i] ) for i in range(Num-1) ]
objectTravel= [ Or( Or( Or( Or( Or( Or( t1[i] , t2[i] ) , t3[i] ) , t4[i] ) , t5[i] ) , t6[i] ) , t7[i] ) for i in range(Num-1) ]
data= [ Or( And( And( And( side[i] , safe[i] ) , humanTravel[i] ) , objectTravel[i] ) , nothing[i]) for i in range(Num-1) ]
fState= And( And( And( human[Steps] == 1 , wolf[Steps] == 1 ) , goat[Steps] == 1 ) , cabbage[Steps] == 1 )
final= fState
#template, only start rest
s.add(data + start)
#template
s.add(final)
ind = 0
f = open("/var/www/html/all/bin/python/log.txt", "a")
while s.check() == sat:
ind = ind +1
print ind
m = s.model()
print m
print "traversing model..."
#for d in m.decls():
#print "%s = %s" % (d.name(), m[d])
f.write(str(m))
f.write("nn")
exit()
#s.add(Or(goat[0] != s.model()[data[0]] )) # prevent next model from using the same assignment as a previous model
print "Total solution number: "
print ind
f.close()
Às deidh a chuir air bhog, bidh Z3Prover a ’fuasgladh a’ chùmhnant snasail agus a ’toirt dhuinn sreath de ghnothaichean a leigeas leinn airgead a tharraing air ais:
Winning transaction chain found:
Data transaction: human= 0, wolf= 0, goat= 1, cabbage= 0
Data transaction: human= 1, wolf= 0, goat= 1, cabbage= 1
Data transaction: human= 0, wolf= 0, goat= 0, cabbage= 1
Data transaction: human= 1, wolf= 1, goat= 0, cabbage= 1
Data transaction: human= 0, wolf= 1, goat= 0, cabbage= 1
Data transaction: human= 1, wolf= 1, goat= 1, cabbage= 1
Data transaction: human= 1, wolf= 1, goat= 1, cabbage= 1
Transfer transaction
A bharrachd air a’ chùmhnant aiseig, faodaidh tu na cùmhnantan agad fhèin fheuchainn no an eisimpleir shìmplidh seo fheuchainn, a tha air fhuasgladh ann an 2 ghnothach.
let contract = tx.sender
let a= extract(getInteger(contract,"a"))
let b= extract(getInteger(contract,"b"))
let c= extract(getInteger(contract,"c"))
let d= extract(getInteger(contract,"d"))
match tx {
case t:DataTransaction =>
let na= extract(getInteger(t.data,"a"))
let nb= extract(getInteger(t.data,"b"))
let nc= extract(getInteger(t.data,"c"))
let nd= extract(getInteger(t.data,"d"))
nd == 0 || a == 100 - 5
case s:TransferTransaction =>
( a + b - c ) * d == 12
case _ => true
}
Leis gur e seo a’ chiad dreach, tha an co-chòrdadh glè chuingealaichte agus dh’ fhaodadh bugaichean a bhith ann.
Anns na h-artaigilean a leanas, tha mi an dùil tuilleadh leasachaidh air an VM a chòmhdach, agus sealltainn mar as urrainn dhut cùmhnantan snasail a tha air an dearbhadh gu foirmeil a chruthachadh le a chuideachadh, agus chan ann dìreach am fuasgladh.
Tha an inneal brìgheil caractar ri fhaighinn aig
Às deidh dhomh còd stòr an VM samhlachail a chuir ann an òrdugh agus beachdan a chuir ris an sin, tha mi an dùil a chuir air GitHub airson ruigsinneachd an-asgaidh.
Source: www.habr.com