Is éard atá i bhfíorú foirmiúil ná fíorú clár nó algartam amháin a úsáideann clár eile.
Is é seo ceann de na modhanna is cumhachtaí a ligeann duit gach leochaileacht a aimsiú i gclár nó a chruthú nach bhfuil siad ann.
Tá cur síos níos mionsonraithe ar an bhfíorú foirmiúil le feiceáil i sampla réiteach na faidhbe i mo alt roimhe seo.
San Airteagal seo aistrím ó fhíorú foirmiúil fadhbanna go cláir agus déan cur síos ar conas
conas is féidir iad a thiontú go córais fhoirmiúla rialacha go huathoibríoch.
Chun seo a dhéanamh, scríobh mé mo analóg féin de mheaisín fíorúil, ag baint úsáide as prionsabail siombalach.
Parsálann sé cód an chláir agus aistríonn sé go córas cothromóidí (SMT) é, ar féidir é a réiteach go ríomhchláraithe cheana féin.
Ós rud é go gcuirtear faisnéis faoi ríomhaireachtaí siombalacha i láthair ar an Idirlíon go hannamh,
Déanfaidh mé cur síos gairid ar a bhfuil ann.
Is bealach é ríomh siombalach chun clár a fheidhmiú go comhuaineach ar raon leathan sonraí agus is í an phríomhuirlis í le haghaidh fíorú foirmiúil clár.
Mar shampla, is féidir linn coinníollacha ionchuir a shocrú nuair is féidir leis an gcéad argóint aon luachanna dearfacha a ghlacadh, an dara diúltach, an tríú náid, agus an argóint aschuir, mar shampla, 42.
Tabharfaidh ríomhaireachtaí siombalacha in aon rith amháin an freagra dúinn maidir le cibé an féidir linn an toradh inmhianaithe a fháil agus sampla de shraith paraiméadair ionchuir dá leithéid. Nó cruthúnas nach bhfuil paraiméadair den sórt sin ann.
Thairis sin, is féidir linn na hargóintí ionchuir a shocrú do gach ceann is féidir, agus na cinn aschuir amháin a roghnú, mar shampla, pasfhocal an riarthóra.
Sa chás seo, aimseoimid leochaileachtaí uile an chláir nó gheobhaidh muid cruthúnas go bhfuil pasfhocal an riarthóra sábháilte.
Is féidir a thabhairt faoi deara gur cás speisialta de fhorghníomhú siombalach é cur i gcrích clasaiceach clár le sonraí ionchuir ar leith.
Mar sin, is féidir le mo charachtar VM oibriú freisin i modh aithrise ar mheaisín fíorúil caighdeánach.
Sna tuairimí don alt roimhe seo is féidir cáineadh cothrom a fháil ar an bhfíorú foirmiúil agus plé á dhéanamh ar a laigí.
Is iad na príomhfhadhbanna:
- Pléascadh comhcheangailte, toisc go dtagann fíorú foirmiúil síos go P=NP ar deireadh
- Tá sé níos deacra glaonna ar an gcóras comhad, ar líonraí agus ar stóráil sheachtrach eile a fhíorú
- Bugs sa tsonraíocht, nuair a bheartaigh an custaiméir nó an ríomhchláraitheoir rud amháin, ach níor chuir sé síos cruinn go leor air sa tsonraíocht theicniúil.
Mar thoradh air sin, déanfar an clár a fhíorú agus comhlíonfaidh sé an tsonraíocht, ach déanfaidh sé rud éigin go hiomlán difriúil ón méid a raibh súil ag na cruthaitheoirí uaidh.
Ós rud é go bhfuil mé ag smaoineamh go príomha ar úsáid fíoraithe foirmiúil go praiticiúil san Airteagal seo, ní bhacfaidh mé mo cheann i gcoinne an bhalla go dtí seo, agus roghnóidh mé córas ina bhfuil an chastacht algartamaíoch agus líon na nglaonna seachtracha íosta.
Ós rud é go n-oireann conarthaí cliste is fearr leis na ceanglais seo, thit an rogha ar chonarthaí RIDE ó ardán Waves: níl siad Turing iomlán, agus tá a gcastacht uasta teoranta go saorga.
Ach déanfaimid iad a mheas go heisiach ón taobh teicniúil.
Chomh maith le gach rud, beidh fíorú foirmiúil go háirithe san éileamh ar aon chonarthaí: de ghnáth ní féidir earráid chonartha a cheartú tar éis é a sheoladh.
Agus is féidir le costas earráidí den sórt sin a bheith an-ard, ós rud é go minic go stóráiltear suimeanna móra cistí ar chonarthaí cliste.
Tá mo mheaisín fíorúil siombalach scríofa i PHP agus Python, agus úsáideann sé Z3Prover ó Microsoft Research chun na foirmlí SMT mar thoradh air a réiteach.
Ag a chroí tá cuardach cumhachtach il-idirbheart, a
ligeann duit réitigh nó leochaileachtaí a aimsiú, fiú má éilíonn sé go leor idirbheart.
Fiú , ar cheann de na creataí siombalach is cumhachtaí chun leochaileachtaí Ethereum a aimsiú, níor chuir sé ach an cumas seo cúpla mí ó shin.
Ach is fiú a thabhairt faoi deara go bhfuil conarthaí éitear níos casta agus Turing iomlán.
Aistríonn PHP cód foinse an chonartha cliste RIDE go script python, ina gcuirtear an clár i láthair mar chóras Z3 SMT-comhoiriúnach de stáit chonartha agus coinníollacha dá n-aistrithe:
Anois déanfaidh mé cur síos níos mine ar a bhfuil ag tarlú taobh istigh.
Ach ar dtús, cúpla focal faoin teanga chonartha cliste RIDE.
Is teanga ríomhchláraithe feidhmiúil atá bunaithe ar chaint í atá leisciúil ó thaobh dearaidh de.
Ritheann RIDE ina aonar laistigh den blockchain agus féadann sé faisnéis a aisghabháil agus a scríobh ó stóráil atá nasctha le sparán an úsáideora.
Is féidir leat conradh RIDE a cheangal le gach sparán, agus ní bheidh ach toradh an fhorghníomhaithe ach FÍOR nó BRÉAGACH.
Ciallaíonn TRUE go gceadaíonn an conradh cliste an t-idirbheart, agus ciallaíonn FALSE go gcuireann sé cosc air.
Sampla simplí: is féidir le script aistriú a thoirmeasc má tá an t-iarmhéid sparán níos lú ná 100.
Mar shampla, tógfaidh mé an Wolf, Goat, agus Cabáiste céanna, ach curtha i láthair cheana féin i bhfoirm conradh cliste.
Ní bheidh an t-úsáideoir in ann airgead a tharraingt siar ón sparán ar a bhfuil an conradh imscaradh go dtí go mbeidh gach duine seolta aige chuig an 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
}
Baineann PHP na hathróga go léir a bhaint as an gconradh cliste ar dtús i bhfoirm a n-eochracha agus an athróg slonn Boole comhfhreagrach.
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
Tiontaíonn PHP ansin iad i gcur síos córais Z3Prover SMT-comhoiriúnach i Python.
Tá na sonraí fillte i lúb, áit a bhfaigheann athróga stórála innéacs i, athróga idirbhirt innéacs i + 1, agus athróga le habairtí a leagann síos na rialacha maidir le haistriú ón staid roimhe go dtí an chéad stát eile.
Is é seo croílár ár meaisín fíorúil, a sholáthraíonn meicníocht cuardaigh il-idirbheart.
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] )
Déantar na coinníollacha a shórtáil agus a chur isteach i dteimpléad scripte atá deartha chun cur síos a dhéanamh ar an gcóras SMT i Python.
Teimpléad 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()
Maidir leis an stát deireanach sa slabhra iomlán, cuirtear i bhfeidhm na rialacha a shonraítear sa chuid idirbheart aistrithe.
Ciallaíonn sé seo go bhféachfaidh Z3Prover go beacht tacair coinníollacha den sórt sin a cheadóidh cistí a tharraingt siar ón gconradh ar deireadh thiar.
Mar thoradh air sin, faigheann muid múnla SMT lánfheidhmiúil dár gconradh go huathoibríoch.
Is féidir leat a fheiceáil go bhfuil sé an-chosúil leis an tsamhail ó mo alt roimhe seo, a thiomsaigh mé de láimh.
Teimpléad críochnaithe
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()
Tar éis é a sheoladh, réitíonn Z3Prover an conradh cliste agus soláthraíonn sé slabhra idirbheart dúinn a ligfidh dúinn cistí a tharraingt siar:
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
Chomh maith leis an gconradh farantóireachta, is féidir leat triail a bhaint as do chonarthaí féin nó triail a bhaint as an sampla simplí seo, a réitítear i 2 idirbheart.
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
}
Ós é seo an chéad leagan, tá an chomhréir an-teoranta agus d'fhéadfadh go mbeadh fabhtanna ann.
Sna hailt seo a leanas, tá sé beartaithe agam forbairt bhreise an VM a chlúdach, agus a thaispeáint conas is féidir leat conarthaí cliste atá fíoraithe go foirmiúil a chruthú lena chabhair, agus ní hamháin iad a réiteach.
Tá an meaisín fíorúil carachtar ar fáil ag
Tar éis cód foinse an VM siombalach a chur in ord agus tuairimí a chur leis, tá sé beartaithe agam é a chur ar GitHub le haghaidh rochtain saor in aisce.
Foinse: will.com