Ev gotareke wergerê ye . Lê beriya wê pêşgotineke kurt heye. Zombî çawa çêdibin? Her kes ketiye rewşeke wisa ku dixwaze heval an jî hevkarekî xwe bîne asta xwe, lê bi ser nakeve. Wekî din, "ew bi ser nakeve" ne ew qas ji bo we, lê ji bo wî: li aliyekî pîvanê meaşek normal, kar û hwd heye, û ji hêla din ve hewcedariya ramanê heye. Raman ne xweş û bi êş e. Ew zû dev jê berdide û bêyî ku mejiyê xwe qet bikar bîne nivîsandina kodê didomîne. Hûn fêm dikin ka çiqas hewldan hewce dike ku hûn astengiya bêhêziya fêrbûyî derbas bikin, û hûn bi hêsanî wiya nakin. Bi vî rengî zombî têne çêkirin, ku dixuye ku dermankirina wan gengaz e, lê wusa dixuye ku kes dê wiya neke.
Dema ku min ew dît (erê, heman heval ji pirtûkên dersan) û ne raporê dide, lê pirs û bersivan e, ez hinekî hişyar bûm. Tenê di rewşê de, Leslie zanyarek navdar a cîhanê ye, nivîskarê karên bingehîn ên di berhevoka belavbûyî de, û dibe ku hûn wî bi herfên La di LaTeX - "Lamport TeX" jî nas bikin. Faktora metirsîdar a duyemîn hewcedariya wî ye: her kesê ku tê divê (bi tevahî belaş) pêşî li çend raporên wî guhdarî bike, bi kêmanî pirsek li ser wan bike, û tenê hingê were. Min biryar da ku bibînim ka Lamport li wir çi weşan dike - û ew pir xweş e! Ev tam ew tişt e, ji bo dermankirina zozanan pêlekek girêdanek efsûnî ye. Ez we hişyar dikim: dibe ku nivîs bi giranî bişewitîne yên ku ji metodolojiyên super-aqilmend hez dikin û yên ku hez nakin ceribandina tiştên ku nivîsandine bikin.
Piştî habrokatê bi rastî wergera semînerê dest pê dike. Ji xwendinê kêfxweş bibin!
Çi karê ku hûn bigrin ser xwe, hûn her gav hewce ne ku sê gavan derbas bikin:
- biryar bidin ka hûn dixwazin bigihîjin çi armancê;
- biryar bidin ka hûn ê çawa bi rastî bigihîjin armanca xwe;
- bigihê armanca xwe.
Ev jî ji bo bernamekirinê derbas dibe. Dema ku em kodê dinivîsin, em hewce ne:
- biryar bidin ka bername bi rastî divê çi bike;
- tam diyar bike ka divê ew çawa peywira xwe pêk bîne;
- koda guncan binivîse.
Pêngava dawî, bê guman, pir girîng e, lê ez ê îro qala wê nekim. Di şûna wê de, em ê her du yekem nîqaş bikin. Her bernamenûs beriya ku dest bi xebatê bike wan pêk tîne. Heya ku we biryar nedaye ku hûn çi dinivîsin: gerokek an databasek hûn rûneniştine ku binivîse. Divê ramanek armancek diyar hebe. Û hûn bê guman difikirin ka bername dê bi rastî çi bike, û wê bi bêhemdî nenivîsin bi hêviya ku kod bixwe dê bi rengek gerokek veguherîne.
Bi rastî ev pêş-fikra kodê çawa dibe? Divê em çiqas hewl bidin vê yekê? Hemî bi wê yekê ve girêdayî ye ku pirsgirêka ku em çareser dikin çiqas tevlihev e. Ka em bibêjin ku em dixwazin pergalek belavbûyî-tehemûl a xeletiyê binivîsin. Di vê rewşê de, divê em berî ku li kodê rûnin bi baldarî tiştan bifikirin. Ger em tenê hewce bike ku guhêrbarek yekjimar bi 1 zêde bikin? Di nihêrîna pêşîn de, li vir her tişt piçûk e û ne hewceyî ramanê ye, lê dûv re em ji bîr dikin ku dibe ku zêdebûnek çêbibe. Ji ber vê yekê, tewra ji bo ku hûn fêm bikin ka pirsgirêk hêsan e an tevlihev e, divê hûn pêşî bifikirin.
Ger hûn di pêş de li çareseriyên gengaz ên pirsgirêkê bifikirin, hûn dikarin ji xeletiyan dûr bikevin. Lê ev hewce dike ku ramana we zelal be. Ji bo ku hûn bigihîjin vê yekê, hûn hewce ne ku ramanên xwe binivîsin. Ez ji gotina Dick Guindon hez dikim: "Gava ku hûn dinivîsin, xweza nîşanî we dide ku ramana we çiqasî şêlû ye." Heke hûn nenivîsin, hûn tenê difikirin ku hûn difikirin. Û hûn hewce ne ku ramanên xwe di forma taybetmendiyê de binivîsin.
Specifications ji gelek fonksiyonan re xizmet dikin, nemaze di projeyên mezin de. Lê ez ê tenê li ser yek ji wan biaxivim: ew ji me re dibin alîkar ku zelal bifikirin. Eşkere fikirîn pir girîng û pir dijwar e, ji ber vê yekê em li vir hewceyê alîkariyê ne. Divê em bi kîjan zimanî taybetmendiyan binivîsin? Bi gelemperî, ev her gav ji bo bernamenûsan pirsa yekem e: em ê bi kîjan zimanî binivîsin? Bersivek rast tune: Pirsgirêkên ku em çareser dikin pir cihêreng in. Ji bo hin kesan, TLA+ zimanek taybetmendiyê ye ku min pêşxistiye. Ji bo yên din, karanîna Çînî hêsantir e. Ew hemî li ser rewşê girêdayî ye.
Pirsa herî girîng ev e: em çawa dikarin bigihîjin ramanek zelal? Bersiv: Divê em wek zanyaran bifikirin. Ev awayê ramanê ye ku di van 500 salên dawî de baş xebitiye. Di zanistiyê de em modelên matematîkî yên rastiyê ava dikin. Astronomî belkî di wateya hişk ya peyvê de zanista yekem bû. Di modela matematîkî ya ku di astronomiyê de tê bikar anîn, cesedên ezmanî wekî xalên bi girse, pozîsyon û leza xwe xuya dikin, her çend di rastiyê de ew bi çiya û okyanûsan, eywan û herikînên pir tevlihev in. Ev model, wekî her din, ji bo çareserkirina hin pirsgirêkan hate afirandin. Ji bo destnîşankirina ku hûn dixwazin gerstêrkek bibînin hûn ê li ku derê teleskopê destnîşan bikin pir baş e. Lê heke hûn bixwazin hewaya li ser vê gerstêrkê pêşbînî bikin, ev model dê nexebite.
Matematîk rê dide me ku em taybetmendiyên modelê diyar bikin. Û zanist nîşan dide ka ev taybetmendî çawa bi rastiyê re têkildar in. Ka em behsa zanista xwe, zanista kompîturê bikin. Rastiya ku em pê re dixebitin pergalên komputerê yên gelek celeb e: pêvajoker, konsolên lîstikê, komputerên ku bernameyan dimeşînin, û hwd. Ez ê li ser darvekirina bernameyek li ser komputerê biaxivim, lê, bi gelemperî, van hemî encam ji bo her pergalek hesabkirinê derbas dibe. Di zanistiya xwe de em gelek modelên cihêreng bikar tînin: makîneya Turing, komên bûyeran bi qismî rêzkirî û gelekên din.
Bername çi ye? Ev her kodek e ku dikare bi serê xwe were hesibandin. Em bêjin ku divê em gerokek binivîsin. Em sê karan pêk tînin: Pêşniyara bernameyê ji hêla bikarhêner ve sêwirînin, dûv re diyagrama asta bilind a bernameyê binivîsin, û di dawiyê de kodê binivîsin. Gava ku em kodê dinivîsin, em pê dihesin ku pêdivî ye ku em formatkerek nivîsê binivîsin. Li vir dîsa divê em sê pirsgirêkan çareser bikin: diyar bikin ka ev amûr dê çi nivîsê vegerîne; algorîtmayek ji bo formatkirinê hilbijêrin; kodê binivîse. Ev peywira binekarê xwe heye: xistina dafikan di peyvan de rast. Em di heman demê de vê binerdê di sê gavan de çareser dikin - wekî ku em dibînin, ew di gelek astan de têne dubare kirin.
Ka em ji nêz ve li gava yekem binêrin: bername çi pirsgirêkê çareser dike. Li vir em pirî caran bernameyekê wekî fonksiyonek model dikin ku hin têketinê digire û hin encam dide. Di matematîkê de, fonksiyonek bi gelemperî wekî komek rêzkirî ya cotan tê binav kirin. Mînakî, fonksiyona çargoşeyê ji bo jimareyên xwezayî wekî komika {<0,0>, <1,1>, <2,4>, <3,9>,…} tê binavkirin. Qada pênasekirina fonksiyonek weha koma hêmanên pêşîn ên her cotek, ango hejmarên xwezayî ye. Ji bo danasîna fonksiyonek, divê em domain û formula wê diyar bikin.
Lê fonksiyonên di matematîkê de ne wekî fonksiyonên di zimanên bernamesaziyê de ne. Matematîk pir hêsan e. Ji ber ku wextê min ji bo mînakên tevlihev tune, bila em yek hêsan bifikirin: fonksiyonek di C de an rêbazek statîk a Java-yê ku dabeşkera hevpar a herî mezin a du hejmaran vedigerîne. Di taybetmendiya vê rêbazê de em ê binivîsin: hesab dike GCD(M,N) ji bo argumanan M и Nko GCD(M,N) - Fonksiyona ku domaina wê komek cotên hejmaran e, û nirxa vegerê hêjmara herî mezin e ku bi par ve tê dabeş kirin. M и N. Rastî bi vê modelê re çawa dide hev? Model bi hejmaran tevdigere, û di C an Java de me 32-bit heye int. Ev model dihêle ku em biryar bidin ka algorîtma rast e GCD, lê ew ê pêşî li xeletiyên zêdebûnê bigire. Ev dê modelek tevlihevtir hewce bike, ji bo ku dem tune.
Ka em li ser sînorên fonksiyonê wekî modelek biaxivin. Hin bername (wekî pergalên xebitandinê) ne tenê ji bo hin argumanan nirxek taybetî vedigerînin; ew dikarin bi domdarî bixebitin. Wekî din, fonksiyona wekî modelek ji bo gava duyemîn kêm maqûl e: plansaz kirin ka meriv çawa pirsgirêkê çareser dike. Bişkojka Quicksort û bişkokê heman fonksiyonê hesab dikin, lê ew bi tevahî algorîtmayên cûda ne. Ji ber vê yekê, ji bo ravekirina awayê gihîştina armanca bernameyê, ez modelek din bikar tînim, em jê re bibêjin modela behremendiya standard. Bername di wê de wekî komek ji hemî tevgerên derbasdar têne destnîşan kirin, ku her yek ji wan, rêzek dewletan e, û dewletek danasîna nirxan ji guhêrbaran re ye.
Ka em bibînin ka gava duyemîn ji bo algorîtmaya Euclidean dê çawa xuya bike. Divê em hesab bikin GCD(M, N). Em dest pê dikin M çawa xû N çawa y, paşê çend caran ji van guherbaran piçûktir ji ya mezin derxînin heta ku bibin yek. Ji bo nimûne, eger M = 12û N = 18, em dikarin tevgera jêrîn diyar bikin:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
If heke M = 0 и N = 0? Sifir li ser hemû jimareyan tê dabeşkirin, loma di vê rewşê de dabeşkerê herî mezin tune. Di vê rewşê de, pêdivî ye ku em vegerin gava yekem û bipirsin: Ma em bi rastî hewce ne ku GCD-ê ji bo hejmarên ne-erênî hesab bikin? Ger ev ne hewce be, wê hingê hûn tenê hewce ne ku taybetmendiyê biguherînin.
Li vir vekolînek kurt li ser hilberînê heye. Ew pir caran bi hejmara rêzikên kodê yên ku her roj têne nivîsandin tê pîvandin. Lê heke hûn ji hejmarek rêzan xilas bibin xebata we pir bikêrtir e, ji ber ku cîhê we ji xeletiyan kêmtir e. Û awayê herî hêsan ku meriv ji kodê xilas bike di gava yekem de ye. Mimkun e ku hûn tenê ne hewce nebin hemî zengil û bilbilên ku hûn hewl didin bicîh bînin. Rêya herî bilez a hêsankirina bernameyekê û xilaskirina demê ev e ku hûn tiştên ku divê neyên kirin nekin. Pêngava duyemîn duyemîn potansiyela teserûfa demê ya herî bilind e. Ger hûn hilberîneriyê bi rêzikên nivîskî bipîvin, wê hingê hûn difikirin ka meriv çawa karekî biqedîne dê we bike kêm berhemdar, ji ber ku hûn dikarin heman pirsgirêkê bi kodê kêmtir çareser bikin. Ez nikarim li vir statîstîkek rast bidim, ji ber ku rêyek min tune ku ez hejmara rêzikên ku min nenivîsandiye ji ber dema ku min li ser taybetmendiyê derbas kiriye, ango li ser gavên yekem û duyemîn bijmêrim. Û em nikarin li vir ceribandinek jî bikin, ji ber ku di ceribandinê de mafê me tune ku gava yekem biqedînin; peywir ji berê ve tê destnîşankirin.
Di taybetmendiyên nefermî de meriv pir zehmetiyan ji bîr nake. Di nivîsandina taybetmendiyên hişk ên fonksiyonan de tiştek dijwar tune; ez ê li ser vê nîqaş nekim. Di şûna wê de, em ê li ser nivîsandina taybetmendiyên bihêz ên ji bo tevgerên standard biaxivin. Teoremek heye ku dibêje ku her komek tevger dikare bi karanîna taybetmendiya ewlehiyê were vegotin (ewlekarî) û taybetmendiyên zindîbûnê (jiyane). Ewlehî tê vê wateyê ku dê tiştek xirab nebe, bername dê bersivek xelet nede. Zindîbûn tê vê wateyê ku zû an dereng dê tiştek baş çêbibe, ango bername zû an dereng dê bersiva rast bide. Wekî qaîdeyek, ewlehî nîşanek girîngtir e; xeletî pir caran li vir çêdibin. Ji ber vê yekê, ji bo ku dem xilas bike, ez ê qala zindîbûnê nekim, her çend ew, bê guman, ew jî girîng e.
Em bi destnîşankirina komek rewşên destpêkê yên gengaz ve digihîjin ewlehiyê. Û ya duyemîn, têkiliyên bi hemû dewletên din ên gengaz ên her dewletê re. Werin em wek zanyaran tevbigerin û dewletan bi matematîkî diyar bikin. Komek rewşên destpêkê bi formula, mînakî, di rewşa algorîtmaya Euclidean de tê vegotin: (x = M) ∧ (y = N). Ji bo hin nirxan M и N tenê yek dewleta destpêkê heye. Têkiliya bi rewşa paşerojê re bi formulek tête diyar kirin ku tê de guhêrbarên rewşa paşerojê bi tîpa yekem, û guhêrbarên rewşa heyî jî bêyî yekem têne nivîsandin. Di mijara algorîtmaya Euclidean de, em ê bi veqetandina du formulan re mijûl bibin, di yek ji wan de x nirxa herî mezin e, û di ya duyemîn de - y:
Di rewşa yekem de, nirxa nû ya y bi nirxa berê ya y re wekhev e, û em nirxa nû ya x-ê bi derxistina guhêrbara piçûktir ji ya mezin distînin. Di rewşa duyemîn de, em berevajî dikin.
Ka em vegerin ser algorîtmaya Euclidean. Dîsa wisa bifikirin M = 12, N = 18. Ev yek dewletek destpêkê diyar dike, (x = 12) ∧ (y = 18). Dûv re em van nirxan têxin nav formula jorîn û werdigirin:
Li vir tenê çareseriya gengaz e: x' = 18 - 12 ∧ y' = 12, û em tevgerê digirin: [x = 12, y = 18]. Bi heman awayî, em dikarin hemî dewletan di tevgera xwe de diyar bikin: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
Di rewşa dawî de [x = 6, y = 6] her du beşên bêjeyê dê derew bin, ji ber vê yekê ew ne xwediyê rewşek din e. Ji ber vê yekê, me diyariyek bêkêmasî ya gava duyemîn heye - wekî ku em dibînin, ev matematîkî pir asayî ye, mîna ya endezyar û zanyaran, û ne xerîb e, mîna di zanistiya computer de.
Ev her du formul dikarin di yek formulek mantiqa demkî de werin berhev kirin. Ew xweş û hêsan e ku meriv rave bike, lê niha wextê wê tune. Dibe ku ji me re mantiqa demkî tenê ji bo milkê zindîtiyê hewce bike; ji bo ewlehiyê ew ne hewce ye. Ez ji mantiqê demkî hez nakim, ew ne matematîkek asayî ye, lê di rewşa jîndarbûnê de xirabiyek pêdivî ye.
Di algorîtmaya Euclidean de ji bo her nirxê x и y nirxên yekta hene x' и y', ku têkiliya bi dewleta din re rast dike. Bi gotineke din, algorîtmaya Euclidean diyarker e. Ji bo modela algorîtmayek nedetermînîst, divê rewşa heyî gelek rewşên paşerojê yên mimkun hebin, û her nirxek guhêrbarek neprimed divê xwedan çend nirxên guhêrbara pêşîn be, wusa ku têkiliya bi rewşa din re rast be. Ev ne zehmet e ku were kirin, lê ez ê niha mînakan nekim.
Ji bo çêkirina amûrek xebatê, hûn hewceyê matematîkên fermî ne. Meriv çawa diyariyek fermî dike? Ji bo vê yekê em ê hewceyê zimanek fermî, wek mînak. . Taybetmendiya algorîtmaya Euclidean di vî zimanî de dê wiha xuya bike:
Nîşana nîşana wekhevî ya bi sêgoşe tê vê wateyê ku nirxa li milê çepê nîşaneyê wekî nirxa li milê rastê nîşanê tê destnîşankirin. Di eslê xwe de, diyardeyek pênase ye, di rewşa me de du pênasîn e. Li ser taybetmendiya di TLA+ de hûn hewce ne ku wekî di slideya jor de danezan û hin hevoksaziyê lê zêde bikin. Di ASCII de ew ê bi vî rengî xuya bike:
Wekî ku hûn dikarin bibînin, tiştek tevlihev. Taybetmendiya li ser TLA + dikare were verast kirin, ango, mimkun e ku di modelek piçûk de hemî tevgerên gengaz derbas bibin. Di rewşa me de, ev model dê hin nirx be M и N. Ev rêbazek verastkirinê ya pir bi bandor û hêsan e ku bi tevahî otomatîk e. Wekî din, gengaz e ku meriv delîlên rastîn ên fermî binivîsîne û wan bi mekanîkî kontrol bike, lê ev pir wext digire, ji ber vê yekê hema kes vê yekê nake.
Kêmasiya sereke ya TLA+ ew e ku matematîk e, û bernamenûs û zanyarên kompîturê ji matematîkê ditirsin. Di nihêrîna pêşîn de ev wekî henekek xuya dike, lê mixabin, ez vê yekê bi ciddî dibêjim. Hevalekî min tenê ji min re digot ka wî çawa hewl da ku TLA + ji gelek pêşdebiran re rave bike. Hema ku formul li ser ekranê xuya bûn, çavên wan tavilê cam dibûn. Ji ber vê yekê heke TLA + tirsnak e, hûn dikarin bikar bînin , cureyek zimanê bernamesaziya pêlîstokê ye. Vebêjek di PlusCal de dikare her îfadeyek TLA+ be, ango, bi bingehîn her îfadeyek matematîkî. Wekî din, PlusCal ji bo algorîtmayên ne-determînîst hevoksaziyek heye. Ji ber ku PlusCal dikare her bêjeyek TLA+ binivîse, ew ji her zimanek bernamesaziya rastîn bi girîngî diyarker e. Dûv re, PlusCal di nav taybetmendiyek TLA+ ya hêsan a xwendinê de tête berhev kirin. Ev nayê vê wateyê, bê guman, ku taybetmendiya tevlihev a PlusCal dê li ser TLA+ veguhere yek sade - tenê ku pêwendiya di navbera wan de diyar e, dê tevliheviyek zêde xuya neke. Di dawiyê de, ev taybetmendî dikare bi karanîna amûrên TLA + ve were verast kirin. Bi gelemperî, PlusCal dikare alîkariya têkbirina fobiya matematîkê bike; ji bo bernamenûs û zanyarên kompîturê jî hêsan e ku were fam kirin. Min berê demekê (nêzîkî 10 salan) algorîtmayên li ser wê weşand.
Dibe ku kesek îtiraz bike ku TLA+ û PlusCal matematîk in, û matematîk tenê bi mînakên çêkirî re dixebite. Di pratîkê de, hûn hewceyê zimanek rastîn bi celeb, rêbaz, tiştan, û hwd. Ev xelet e. Li vir tiştê ku Chris Newcomb, ku li Amazon-ê dixebitî, dinivîse: "Me TLA+ li ser deh projeyên mezin bikar aniye, û di her rewşê de karanîna wê di pêşkeftinê de cûdahiyek girîng çêkir ji ber ku me karîbû xeletiyên xeternak berî ku ew bikevin hilberînê bigirin, û ji ber ku ew têgihîştin û pêbaweriya ku me hewce dikir da ku em êrîşkar bikin. xweşbîniyên performansê bêyî ku bandorê li rastiya bernameyê bike". Hûn pir caran dikarin bibihîzin ku dema ku rêbazên fermî bikar tînin em kodek bêkêmasî digirin - di pratîkê de, her tişt tam berevajî ye. Wekî din, têgihîştinek heye ku rêvebir nikarin bi hewcedariya rêbazên fermî bawer bin, her çend bernamenûs ji kêrhatina wan bawer bin. Û Newcomb dinivîse: "Rêveber naha bi her awayî zextê li ser nivîsandina taybetmendiyan di TLA+ de dikin, û bi taybetî ji bo vê yekê dem vediqetînin.". Ji ber vê yekê gava ku rêvebir dibînin ku TLA+ dixebite, ew hembêz dikin. Chris Newcomb ev nêzîkî şeş meh berê (Cotmeh 2014) nivîsand, lê niha, bi qasî ku ez dizanim, TLA+ di 14 projeyan de tê bikar anîn, ne 10. Nimûneyek din bi sêwirana XBox 360 ve girêdayî ye. Karkerek hat Charles Thacker û ji bo pergala bîranînê taybetmendî nivîsand. Bi saya vê taybetmendiyê, xeletiyek hate dîtin ku wekî din nedihate kifş kirin û dê bibe sedem ku her XBox 360 piştî çar demjimêran bikar bîne têk biçe. Endezyarên ji IBM piştrast kirin ku ceribandinên wan dê ev xeletî nebînin.
Hûn dikarin li ser Înternetê li ser TLA+ bêtir bixwînin, lê naha em li ser taybetmendiyên nefermî biaxivin. Em kêm caran neçar in ku bernameyên ku dabeşkera herî kêm hevpar û yên wekî wan hesab dikin binivîsin. Pir caran em bernameyên mîna amûra çapkerê xweşik a ku min ji bo TLA+ nivîsand dinivîsin. Piştî pêvajoya herî hêsan, koda TLA + dê bi vî rengî xuya bike:
Lê di mînaka li jor de, bikarhêner bi îhtîmalek mezin dixwest ku pêwend û nîşanên wekhev bêne hev kirin. Ji ber vê yekê formatkirina rast dê bêtir bi vî rengî xuya bike:
Nimûnek din bibînin:
Li vir, berevajî, lihevhatina nîşaneyên wekhev, zêdekirin û zêdekirin di çavkaniyê de rasthatî bû, ji ber vê yekê pêvajoyek herî hêsan têra xwe ye. Bi gelemperî, pênase matematîkî ya rastîn a formatkirina rast tune, ji ber ku "rast" di vê rewşê de tê wateya "bikarhêner çi dixwaze," û ev bi matematîkî nayê destnîşankirin.
Wusa dixuye ku heke me pênaseyek rastiyê tune be, wê hingê diyarde bêkêr e. Lê ev ne rast e. Tenê ji ber ku em nizanin bernameyek divê çi bike, nayê vê wateyê ku em ne hewce ne ku bifikirin ka ew çawa divê bixebite - berevajî, divê em hê bêtir hewl bidin ser wê. Taybetmendî li vir bi taybetî girîng e. Ne mimkûn e ku meriv bernameya çêtirîn ji bo çapkirina birêkûpêk diyar bike, lê ev nayê vê wateyê ku divê em qet wiya nekin, û nivîsandina kodê wekî çemek hişmendiyê ne wusa ye. Min dawî li nivîsandina taybetmendiyek şeş rêzikên bi pênase kir di forma şîroveyan de di pelek Java de. Li vir mînakek yek ji rêbazan e: a left-comment token is LeftComment aligned with its covering token. Ev qayde bi îngilîzî ya matematîkî hatiye nivîsandin: LeftComment aligned, left-comment и covering token - şertên bi pênase. Matematîkzan matematîkê bi vî rengî vedibêjin: ew pênaseyên terman dinivîsin û li ser bingeha wan, qaîdeyan diafirînin. Feydeya vê taybetmendiyê ev e ku şeş rêzik ji 850 rêzikên kodê pir hêsantir têne famkirin û debugkirin. Divê ez bibêjim ku nivîsandina van qaîdeyan ne hêsan bû; ji bo rakirina wan pir dem girt. Min kodek bi taybetî ji bo vê armancê nivîsand ku ji min re got ka kîjan qaîdeyek tê bikar anîn. Ji ber ku min ev şeş qaîdeyên bi çend mînakan ceriband, ne hewce bû ku ez 850 rêzikên kodê xelet bikim, û dîtina xeletiyan pir hêsan bû. Java ji bo vê yekê amûrên mezin hene. Ger min tenê kod binivîsanda, wê ji min re pir dirêjtir bikira û formatkirin dê ji kalîteya xirabtir bûya.
Çima nekare taybetmendiyek fermî were bikar anîn? Ji aliyekî ve, pêkanîna rast li vir ne pir girîng e. Bê guman çapek birêkûpêk ji hin kesan re ne razî ye, ji ber vê yekê ez neçar bûm ku ew di hemî rewşên neasayî de rast bixebitim. Ya girîngtir jî ev e ku amûrên min ên têr tunebûn. Kontrola modela TLA+ li vir bêkêr e, ji ber vê yekê divê ez mînakan bi destan binivîsim.
Taybetmendiya hatî dayîn taybetmendiyên hevpar ên hemî taybetmendiyan heye. Ew ji kodê bilindtir e. Di her zimanî de dikare were pêkanîn. Ji bo nivîsandina wê tu alav û rêbaz nîn in. Tu qursa bernamekirinê dê ji we re bibe alîkar ku hûn vê taybetmendiyê binivîsin. Û tu amûrên ku dikarin vê taybetmendiyê nehewce bikin tune ne, heya ku bê guman hûn zimanek bi taybetî ji bo nivîsandina bernameyên çapkirinê yên birêkûpêk di TLA+ de nenivîsin. Di dawiyê de, ev taybetmendî tiştek nabêje ka em ê çawa bi rastî kodê binivîsin, ew tenê diyar dike ku kod çi dike. Em taybetmendiyek dinivîsin da ku ji me re bibe alîkar ku em di pirsgirêkê de bifikirin berî ku em dest bi ramana kodê bikin.
Lê ev taybetmendî di heman demê de taybetmendiyên ku wê ji taybetmendiyên din cuda dike jî hene. 95% ji taybetmendiyên din pir kurttir û hêsan in:
Wekî din, ev taybetmendî komek rêzik e. Ev bi gelemperî nîşanek taybetmendiyek belengaz e. Fêmkirina encamên komek qaîdeyan pir dijwar e, ji ber vê yekê ez neçar bûm ku gelek wext derbas bikim da ku wan xelet bikim. Lêbelê, di vê rewşê de min nikarî rêyek çêtir bibînim.
Li ser bernameyên ku bi berdewamî dimeşin hêja ye ku çend peyvan bê gotin. Bi gelemperî ew di paralel de dixebitin, wekî pergalên xebitandinê an pergalên belavkirî. Pir hindik kes dikarin wan di hişê xwe de an li ser kaxezê fam bikin, û ez ne yek ji wan im, her çend min carekê karîbû wiya bikim. Ji ber vê yekê, em hewceyê amûrên ku dê xebata me kontrol bikin - ji bo nimûne, TLA + an PlusCal.
Ger min berê dizanibû ku kod divê çi bike, çima hewce bû ku ez taybetmendiyek binivîsim? Bi rastî, min tenê difikirî ku ez wê dizanim. Digel vê yekê, digel diyariyek di cîh de, kesek biyanî êdî hewce nake ku li kodê bigere da ku fêm bike ka ew bi rastî çi dike. Rêgezek min heye: Divê rêzikên gelemperî tune bin. Ji vê qaîdeyê re îstîsnayek heye bê guman, ev yekane qaîdeya giştî ye ku ez dişopînim: danasîna ku kod çi dike divê ji mirovan re her tiştê ku divê dema karanîna wê kodê zanibin vebêje.
Ji ber vê yekê bernamenûs bi rastî çi hewce dike ku di derbarê ramanê de zanibin? Ji bo destpêkê, ji bo her kesî heman: heke hûn nenivîsin, wê hingê tenê ji we re xuya dike ku hûn difikirin. Di heman demê de, hûn hewce ne ku berî kodê bifikirin, ku tê vê wateyê ku hûn hewce ne ku berî kodê binivîsin. Beriya ku em dest bi kodkirinê bikin, diyariyek ew e ku em dinivîsin. Ji bo her kodek ku dikare ji hêla her kesî ve were bikar anîn an biguhezîne taybetmendiyek pêdivî ye. Û ev "kesek" dibe ku mehek piştî nivîsandina kodê bibe nivîskarê kodê. Ji bo bername û pergalên mezin, ji bo dersan, ji bo rêbazan, û carinan jî ji bo beşên tevlihev ên rêbazek yekane diyariyek pêdivî ye. Bi rastî divê hûn li ser kodê çi binivîsin? Pêdivî ye ku hûn rave bikin ka ew çi dike, ango tiştek ku dikare ji her kesê ku vê kodê bikar tîne re kêrhatî be. Carinan dibe ku pêdivî be ku meriv diyar bike ka kod çawa bi rastî digihîje armanca xwe. Ger em di qursa algorîtmayan de vê rêbazê derbas bikin, wê hingê em jê re dibêjin algorîtma. Ger ew tiştek pisportir û nû ye, wê hingê em jê re sêwirana asta bilind dibêjin. Li vir cûdahiyek fermî tune: her du jî modelên razber ên bernameyê ne.
Çawa bi rastî divê hûn taybetmendiyek kodê binivîsin? Ya sereke: divê ew yek astek ji kodê xwe bilindtir be. Divê rewş û reftaran vebêje. Divê ew bi qasî ku peywir hewce dike hişk be. Heke hûn diyariyek çawa dinivîsin ka meriv çawa peywirek bicîh tîne, wê hingê ew dikare bi pseudocode an jî bi karanîna PlusCal were nivîsandin. Pêdivî ye ku hûn fêr bibin ku bi karanîna taybetmendiyên fermî binivîsin. Ev ê jêhatîbûnên pêwîst bide we ku dê bi yên nefermî re jî bibin alîkar. Hûn çawa dikarin fêrî nivîsandina taybetmendiyên fermî bibin? Dema ku em fêrî bernamekirinê bûn, me bername dinivîsand û dûv re wan debug dikir. Heman tişt li vir: hûn hewce ne ku taybetmendiyek binivîsin, wê bi kontrolkerek modelê ve kontrol bikin, û xeletiyan rast bikin. TLA + dibe ku ji bo taybetmendiyek fermî ne zimanê çêtirîn be, û zimanek din dê ji bo hewcedariyên we yên taybetî çêtir be. Tişta girîng di derbarê TLA + de ev e ku ew di hînkirina ramîna matematîkî de karek mezin dike.
Meriv çawa taybetmendî û kodê girêdide? Bikaranîna şîroveyên ku têgînên matematîkî û pêkanîna wan girêdidin. Ger hûn bi grafikan re bixebitin, wê hingê di asta bernameyê de hûn ê rêzikên girêk û rêzikên girêdanan hebin. Ji ber vê yekê hûn hewce ne ku binivîsin ka tam grafîk ji hêla van strukturên bernamekirinê ve çawa tête bicîh kirin.
Divê were zanîn ku yek ji van jorîn ji bo pêvajoya nivîsandina kodê bixwe derbas nabe. Gava ku hûn kodê dinivîsin, ango gava sêyemîn pêk tînin, hûn jî hewce ne ku bi bernameyê bihizirin û bifikirin. Ger subkariyek tevlihev bibe an ne diyar be, hûn hewce ne ku ji bo wê taybetmendiyek binivîsin. Lê ez li vir behsa kodê bixwe nakim. Hûn dikarin her zimanek bernamekirinê, her metodolojiyê bikar bînin, ev ne li ser wan e. Di heman demê de, yek ji jor hewcedariya ceribandin û xeletkirina koda xwe ji holê ranake. Heke modela razber rast were nivîsandin jî, dibe ku di pêkanîna wê de xeletî hebin.
Taybetmendiyên nivîsandinê di pêvajoya kodkirinê de gavek din e. Bi saya wê, gelek xeletî dikarin bi hewildanek kêmtir werin girtin - em vê yekê ji ezmûna bernamenûsên Amazon dizanin. Bi taybetmendiyan, kalîteya bernameyan bilindtir dibe. Wê hingê çima em pir caran bêyî wan diçin? Ji ber ku nivîsandin zehmet e. Lê nivîsandin zehmet e, ji ber ku ji bo vê yekê hûn hewce ne ku bifikirin, û fikirîn jî dijwar e. Her gav hêsantir e ku meriv bifikire ku hûn difikirin. Li vir hûn dikarin bi bazdanê re analojiyek derxînin - hûn çiqas kêmtir direvin, hûn hêdî hêdî diherikin. Pêdivî ye ku hûn masûlkeyên xwe perwerde bikin û nivîsandinê bikin. Ew pratîkê digire.
Specification dibe ku xelet be. Dibe ku we li deverek xeletiyek kiribe, an jî dibe ku pêdivî hatine guhertin, an jî dibe ku pêdivî be ku çêtirbûnek were çêkirin. Pêdivî ye ku kodek ku kesek bikar tîne were guheztin, ji ber vê yekê zû an dereng dê taybetmendî êdî bi bernameyê re nebe hev. Bi îdeal, di vê rewşê de, hûn hewce ne ku taybetmendiyek nû binivîsin û kodê bi tevahî ji nû ve binivîsin. Em baş dizanin ku kes vê yekê nake. Di pratîkê de, em kodê paqij dikin û dibe ku taybetmendiyê nûve bikin. Ger ev yek zû an dereng çêbibe, wê hingê çima bi tevahî taybetmendiyan binivîsin? Ya yekem, ji bo kesê ku dê koda we biguhezîne, her peyva zêde ya di taybetmendiyê de dê giraniya xwe bi zêr be, û ev kes dibe ku hûn jî bin. Ez bi gelemperî gava ku ez koda xwe diguhezînim ji ber ku ez têra xwe taybetî nekim xwe diavêjim. Û ez ji kodê bêtir taybetmendiyan dinivîsim. Ji ber vê yekê, gava ku hûn kodê biguherînin, pêdivî ye ku pêdivî her gav were nûve kirin. Ya duyemîn, bi her guhertinê re kod xirabtir dibe, xwendin û domandina wê dijwartir dibe. Ev zêdebûna entropiyê ye. Lê heke hûn bi taybetmendiyek dest pê nekin, wê hingê her rêza ku hûn dinivîsin dê bibe guherandinek, û kod dê ji destpêkê ve giran û xwendina dijwar be.
Wek tê gotin , ne şer li gor plan û ne jî şerek bê plan bi ser ket. Û wî tiştek di derbarê şeran de dizanibû. Nerînek heye ku nivîsandina taybetmendiyan windakirina demê ye. Carinan ev rast e, û peywir ew qas hêsan e ku meriv wê yekê bifikire tine ye. Lê divê hûn her gav ji bîr mekin ku gava ji we tê şîret kirin ku hûn taybetmendiyan nenivîsin, ev tê vê wateyê ku hûn têne şîret kirin ku hûn nefikirin. Û divê hûn her dem li ser vê yekê bifikirin. Fikirîna bi peywirekê garantî nake ku hûn ê xeletiyan nekin. Wekî ku em dizanin, tu kesî çîçek efsûnî îcad nekiriye, û bername karekî dijwar e. Lê heger hûn bi peywirê nefikirin, hûn garantî dikin ku hûn xeletiyan bikin.
Hûn dikarin li ser malperek taybetî li ser TLA+ û PlusCal bêtir bixwînin, hûn dikarin ji rûpela min a malê biçin wir . Ev hemû ji bo min e, spas ji bo baldariya we.
Ji kerema xwe ji bîr mekin ku ev werger e. Dema ku hûn şîroveyan dinivîsin, ji bîr mekin ku nivîskar dê wan nexwîne. Ger hûn bi rastî dixwazin bi nivîskar re sohbet bikin, ew ê di konferansa Hydra 2019 de be, ku dê di 11-12 Tîrmeh 2019 de li St. Bilêt dikarin bên kirîn .
Source: www.habr.com