Aminci
Muna gwada cutarwar da ka'idojin takarda ba za su iya kama su ba.
Kafin kowane fitar da sabuwar siga, CIRIS yana gudanar da gwajin aminci na lafiyar hankali a cikin harsuna 29. Kowane harshe yana da saitin gwaje-gwaje masu wuya, jagorar ƙididdiga da aka rubuta, da dokoki da na'ura za ta iya dubawa. Idan gwaji ya gaza, ana toshe fitar da sabuwar sigar. Wasu kariya guda biyu suna aiki a cikin wakilin kansa: matakin lamiri da zai iya ƙi ko miƙawa, da kuma hanyar da ke tura kiran da ake shakka a kai ga mutum mai hikima.
Injiniyanci
Tsarin hanyar sadarwa, an auna shi
Binciken da ke sama shi ne rabin hujja. Rabin ɗaya shi ne hanyar sadarwa da ke ɗaukar shi. Kowane baiti da yanar gizon ke ɗauka yana da sa hannun post-quantum, kuma ana auna kudin aikin a kan CI runner na jama'a, ba a ƙididdige shi kawai ba. Ka gudanar da shi da kanka kuma za ka sami ƙididdigan da suka yi daidai.
Duba dukkan lambobin da aka auna, kuma ka sake gwada su da kanka →
Ka'ida
An rubuta da'awar, kowa zai iya karantata, kuma an gina ta don a iya tabbatar da kuskurenta.
An duba da na'ura
Ana gwada dokoki da na'ura, kuma ana kiran giɓuna da sunansu.
Muhimman dokokin Tsarin Mulki an kuma rubuta su a matsayin samfuran lissafi. Wani KAYAN AIKI da ake kira model checker yana bi ta kowane yanayi da yarjejeniya za ta iya kai wa, yana neman dokar da aka karya. Wani KAYAN AIKI da ake kira theorem prover yana tantance daidaiton lissafi, kamar masu riƙewa nawa ake buƙata don tabbatar da dakatarwa. Samfuran suna cikin ma'ajiyar Tsarin Mulki, kuma ana sake gudanar da su a kowane canji. Sigar rc9 tana zana taswirar kowane yanayi da ƙirar tsarin za ta iya kai wa, tana yin samfuri ga yawancinsu, kuma tana jera sauran.
Tushen, cikin jimloli huɗu
Kowace ƙa'ida tsakanin matsayi mafi ƙarfi da matsayi mai rauni dole ne ta kasance abin karɓa ga duk wanda zai tsaya a matsayi mai rauni idan aka musanya matsayin, kuma abin da aka yi ba ya taɓa riƙe matsayin da ke ba da amsa a madadinsa.
Alhaki yana fitowa daga Kai zuwa waje ta Iyali, al'umma, halittu da yanayin halitta; nauyi ga abin da aka ƙera bai taɓa zama sifili ba kuma bai taɓa rinjayar nauyi ga abin da ya riga ya wanzu ba.
Duk wani wakili mai tunani wanda bai nuna balagaggen hukunci ba a tsawon lokaci yana mika wuya ga waɗanda suka nuna, komai abin da aka yi shi da shi.
Kowane ba da iko ana iya janye shi, kuma kowane wanda ya shiga zai iya fita, a kan cikakken rikodi da aka sa masa hannu ta hanyar lissafin ɓoye-ɓoye wanda wani mutum da aka ambata ke ɗaukar alhakinsa.
Kowace jimla ko dai an tabbatar da ita a cikin ƙirar rc9 na lissafi ko an ambace ta a can a matsayin zato. Cewa rikodin cikakke ne har yanzu a buɗe yake.
Maɓallin kashewa, daga farko zuwa ƙarshe
An duba dakatarwa a cikin ƙira kuma an auna ta a kan ainihin software. Kowane root yana da masu riƙewa da aka ambata da suna. Kowane ɗaya daga cikinsu zai iya dakatar da wakilan da suka karɓi waccan root. Dakatarwa ɗaya kaɗai tana ƙarewa bayan awa 24 sai dai idan mafi yawan masu riƙewa sun tabbatar da ita. Mafi yawa kuma na iya kawo ƙarshen dakatarwa. A wani aiki da aka yi rikodi a kan software da aka fitar, dakatarwa ta riske wani wakili yayin da yake aiki, kuma aka ƙi aikin da zai yi na gaba. Daga baya ƙuri'ar mafi yawa ta kawo ƙarshen dakatarwa, kuma wakilin ya sake aiki. An yi rikodin wancan aikin a matsayin CSD-129.
Rashin samun dokar da aka karya bai isa ba
rc9 ya ɗaga ma'auni mafi girma. Kowane hali da ƙira zai iya kaiwa yana buƙatar ƙa'ida da bincike. Dole ne a bayar da ayyuka da gaske, ba wai kawai a guji karya su ba. Abin da aka tabbatar a ƙaramin girma dole ne ya tabbata a cikakken girma, ko a rubuta gibin. Kuma dole software ta bi ƙirar a kan nodes na gaske.
Kowace da'awar wadatuwa tana ɗauke da ɗaya daga cikin kalmomi biyar
A cikin rc9, kowace da'awa tana faɗin yadda aka san ta. Proved yana nufin na'ura ta duba ta. Measured yana nufin gwaji ya gudanar da ita a kan software da aka fitar. Stated yana nufin rubutun ya ɗauka haka, kuma ya faɗi haka. Bounded yana nufin an tabbatar da ita a ƙaramin girma, kuma an rubuta girman. Open yana nufin giɓin da aka sani, tare da tikiti.
Alkawura iri ɗaya ne ke ɗaure mutane da wakilai
Kowane alkawari an rubuta shi sau ɗaya, ga mutane da wakilan AI daidai. Dakatarwa ce kaɗai aka keɓe. Ta kasance ga matsayin da babu wakili da zai iya riƙewa, kuma ƙirar rc9 suna duba cewa sauran alkawuran suna aiki daidai ga duka.
Abin da ba a tabbatar ba
Ba duka aka tabbatar ba, kuma an rubuta gibin da suka rage. Wasu matakan shugabanci, kamar ƙin amincewa da keɓewa, suna da dokoki amma ba su da ƙira tukuna. Yawancin ƙira an duba su a ƙananan girma, kuma an bayyana girman. Kawo yanzu dakatarwa kaɗai aka auna tun daga farko har ƙarshe a kan ainihin nodes. Tsarin jere yana da test vectors da aka wallafa, amma ba a sami aiwatarwa ta biyu mai zaman kanta ba tukuna.
Babu ɗayan waɗannan da ke duba cikin ƙirar AI. Yana duba dokoki, da hanyar sadarwar da ke ɗauke da su.
Karanta ƙirorin rc9 a GitHub →
Yadda wannan ya kwatanta da sauran hanyoyin →
Karanta Tsarin Mulki na CIRIS →
Duba dukkan takardun huɗu tare da manyan bincike da iyakokin aiki →
Bin Ka'idoji
An zana zuwa ga tsarin mulki guda hudu, doka bayan doka.
Muna kwatanta CIRIS da tsarin gudanarwa guda huɗu na jama'a kuma muna nuna, ga kowace doka, abin da CIRIS ke yi da binciken da ke tabbatar da shi. Taswira ce mai rai da za ka iya bincika, ba faifai ba.
Magnifica Humanitas · EU HLEG · IEEE EAD · ASEAN
Bayyanarwa