Ĉi tio estas traduka artikolo . Sed antaŭ tio estas mallonga enkonduko. Kiel formiĝas zombioj? Ĉiuj trovis sin en situacio, kie ili volas alporti amikon aŭ kolegon ĝis sia nivelo, sed ĝi ne funkcias. Krome, "ĝi ne funkcias" ne tiom por vi, sed por li: ĉe unu flanko de la skalo estas normala salajro, taskoj, kaj tiel plu, kaj aliflanke estas la bezono pensi. Pensi estas malagrabla kaj dolora. Li rapide rezignas kaj daŭre skribas kodon tute sen uzi sian cerbon. Vi rimarkas kiom da penado necesas por venki la baron de lernita senpoveco, kaj vi simple ne faras ĝin. Tiel formiĝas zombioj, kiuj ŝajnas esti resanigeblaj, sed ŝajnas, ke neniu faros tion.
Kiam mi vidis tion (jes, tiu sama amiko el la lernolibroj) kaj ne donas raporton, sed demandon kaj respondan sesion, mi estis iom singarda. Ĉiaokaze, Leslie estas mondfama sciencisto, la aŭtoro de pioniraj verkoj en distribuita komputado, kaj vi eble ankaŭ konas lin per la literoj La en LaTeX - "Lamport TeX". La dua alarma faktoro estas lia postulo: ĉiu, kiu venas, devas (tute senpage) aŭskulti kelkajn siajn raportojn anticipe, elpensi almenaŭ unu demandon pri ili, kaj nur tiam veni. Mi decidis vidi kion Lampport dissendas tie - kaj ĝi estas bonega! Ĉi tio estas ĝuste tiu afero, magia ligilo-pilolo por trakti zombiojn. Mi avertas vin: la teksto eble serioze bruligos tiujn, kiuj amas super-facilemajn metodikojn kaj kiuj ne ŝatas testi tion, kion ili skribis.
Post la habrokato efektive komenciĝas la tradukado de la seminario. Ĝuu legadon!
Kian ajn taskon vi prenas, vi ĉiam devas trairi tri paŝojn:
- decidi kian celon vi volas atingi;
- decidi kiel precize vi atingos vian celon;
- atingi vian celon.
Ĉi tio validas ankaŭ por programado. Kiam ni skribas kodon, ni bezonas:
- decidi kion ĝuste la programo devus fari;
- determini precize kiel ĝi devas plenumi sian taskon;
- skribu la taŭgan kodon.
La lasta paŝo, kompreneble, estas tre grava, sed mi ne parolos pri ĝi hodiaŭ. Anstataŭe, ni diskutos la unuajn du. Ĉiu programisto plenumas ilin antaŭ ol komenci labori. Vi ne sidas por skribi krom se vi decidis kion vi skribas: retumilo aŭ datumbazo. Certa ideo pri la celo devas ĉeesti. Kaj vi certe pensas pri tio, kion ĝuste faros la programo, kaj ne skribu ĝin hazarde kun la espero, ke la kodo mem iel fariĝos retumilo.
Kiel ĝuste okazas ĉi tiu antaŭpensado de kodo? Kiom da penado ni devus meti en ĉi tio? Ĉio dependas de kiom kompleksa la problemo ni solvas. Ni diru, ke ni volas skribi mistolereman distribuitan sistemon. En ĉi tiu kazo, ni devus pripensi aferojn zorge antaŭ ol sidiĝi al kodo. Kio se ni nur bezonas pligrandigi entjeran variablon per 1? Unuavide, ĉio ĉi tie estas bagatela kaj neniu penso necesas, sed poste ni memoras, ke superfluo povas okazi. Tial, eĉ por kompreni ĉu problemo estas simpla aŭ kompleksa, vi unue devas pensi.
Se vi anticipe pripensas eblajn solvojn al problemo, vi povas eviti erarojn. Sed ĉi tio postulas, ke via penso estu klara. Por atingi ĉi tion, vi devas skribi viajn pensojn. Mi amas la citaĵon de Dick Guindon: "Kiam vi skribas, la naturo montras al vi kiom malzorgema estas via pensado." Se vi ne skribas, vi nur pensas, ke vi pensas. Kaj vi devas noti viajn pensojn en formo de specifoj.
Specifoj servas multajn funkciojn, precipe en grandaj projektoj. Sed mi parolos nur pri unu el ili: ili helpas nin pensi klare. Pensi klare estas tre grava kaj sufiĉe malfacila, do ni bezonas ajnan helpon ĉi tie. En kiu lingvo ni skribu specifojn? Ĝenerale ĉi tio estas ĉiam la unua demando por programistoj: en kiu lingvo ni skribos? Ne ekzistas unu ĝusta respondo: la problemoj, kiujn ni solvas, estas tro diversaj. Por kelkaj homoj, TLA+ estas utila - ĝi estas speciflingvo kiun mi evoluigis. Por aliaj, estas pli oportune uzi la ĉinan. Ĉio dependas de la situacio.
La pli grava demando estas: kiel ni povas atingi pli klaran pensadon? Respondo: Ni devas pensi kiel sciencistoj. Ĉi tio estas pensmaniero, kiu bone funkciis dum la lastaj 500 jaroj. En scienco ni konstruas matematikajn modelojn de realeco. Astronomio estis eble la unua scienco en la strikta signifo de la vorto. En la matematika modelo uzata en astronomio, ĉielaj korpoj aperas kiel punktoj kun maso, pozicio kaj impeto, kvankam fakte ili estas ekstreme kompleksaj objektoj kun montoj kaj oceanoj, malfluoj kaj fluoj. Ĉi tiu modelo, kiel ĉiu alia, estis kreita por solvi iujn problemojn. Ĝi estas bonega por determini kien direkti teleskopon se vi volas trovi planedon. Sed se vi volas antaŭdiri la veteron sur ĉi tiu planedo, ĉi tiu modelo ne funkcios.
Matematiko permesas al ni determini la ecojn de modelo. Kaj scienco montras kiel ĉi tiuj propraĵoj rilatas al la realo. Ni parolu pri nia scienco, komputiko. La realo kun kiu ni laboras estas komputilaj sistemoj de multaj malsamaj tipoj: procesoroj, ludkonzoloj, komputiloj kiuj ruligas programojn, ktp. Mi parolos pri ekzekuto de programo en komputilo, sed, ĝenerale, ĉiuj ĉi tiuj konkludoj validas por ajna komputika sistemo. En nia scienco ni uzas multajn malsamajn modelojn: la Turing-maŝinon, parte ordigitajn arojn de eventoj, kaj multajn aliajn.
Kio estas la programo? Ĉi tio estas ajna kodo, kiu povas esti konsiderata memstare. Ni diru, ke ni devas skribi retumilon. Ni plenumas tri taskojn: desegni la prezenton de la uzanto de la programo, poste verki la altnivelan diagramon de la programo, kaj fine verki la kodon. Dum ni skribas la kodon, ni rimarkas, ke ni devas skribi tekstformatilon. Ĉi tie denove ni devas solvi tri problemojn: determini kian tekston redonos ĉi tiu ilo; elektu algoritmon por formatado; skribi kodon. Tiu ĉi tasko havas sian propran subtaskon: ĝuste enmeti streketojn en vortojn. Ni ankaŭ solvas ĉi tiun subtaskon en tri paŝoj - kiel ni vidas, ili ripetiĝas je multaj niveloj.
Ni rigardu pli detale la unuan paŝon: kian problemon la programo solvas. Ĉi tie ni plej ofte modeligas programon kiel funkcion kiu prenas iom da enigo kaj donas iom da eligo. En matematiko, funkcio estas kutime priskribita kiel ordigita aro de paroj. Ekzemple, la kvadrata funkcio por naturaj nombroj estas priskribita kiel la aro {<0,0>, <1,1>, <2,4>, <3,9>, ...}. La domajno de difino de tia funkcio estas la aro de la unuaj elementoj de ĉiu paro, tio estas, naturaj nombroj. Por difini funkcion, ni devas specifi ĝian domajnon kaj formulon.
Sed funkcioj en matematiko ne samas kiel funkcioj en programlingvoj. La matematiko estas multe pli simpla. Ĉar mi ne havas tempon por kompleksaj ekzemploj, ni konsideru simplan: funkcion en C aŭ statikan metodon en Java, kiu liveras la plej grandan komunan dividon de du entjeroj. En la specifo de ĉi tiu metodo ni skribos: kalkulas GCD(M,N) por argumentoj M и Nkie GCD(M,N) - funkcio kies domajno estas aro de paroj de entjeroj, kaj la revena valoro estas la plej granda entjero kiu estas dividita per M и N. Kiel realo komparas kun ĉi tiu modelo? La modelo funkcias per entjeroj, kaj en C aŭ Java ni havas 32-bitojn int. Ĉi tiu modelo permesas al ni decidi ĉu la algoritmo estas ĝusta GCD, sed ĝi ne malhelpos superfluajn erarojn. Ĉi tio postulus pli kompleksan modelon, por kiu mankas tempo.
Ni parolu pri la limigoj de la funkcio kiel modelo. Kelkaj programoj (kiel ekzemple operaciumoj) ne nur resendas specifan valoron por certaj argumentoj; ili povas funkcii senĉese. Krome, la funkcio kiel modelo estas malbone taŭga por la dua paŝo: plani kiel solvi la problemon. Quicksort kaj bubble sort komputas la saman funkcion, sed ili estas tute malsamaj algoritmoj. Tial, por priskribi la manieron atingi la celon de la programo, mi uzas alian modelon, ni nomu ĝin la norma kondutmodelo. La programo estas reprezentita en ĝi kiel aro de ĉiuj validaj kondutoj, ĉiu el kiuj, siavice, estas sekvenco de statoj, kaj stato estas la atribuo de valoroj al variabloj.
Ni vidu kiel aspektus la dua paŝo por la eŭklida algoritmo. Ni devas kalkuli GCD(M, N). Ni pravalorigas M kiom xkaj N kiom y, tiam plurfoje subtrahi la pli malgrandan el tiuj variabloj de la pli granda ĝis ili estas egalaj. Ekzemple, se M = 12kaj N = 18, ni povas priskribi la sekvan konduton:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
Kaj se M = 0 и N = 0? Nulo estas dividebla per ĉiuj nombroj, do ne ekzistas plej granda dividanto en ĉi tiu kazo. En ĉi tiu situacio, ni devas reiri al la unua paŝo kaj demandi: ĉu ni vere bezonas kalkuli GCD por ne-pozitivaj nombroj? Se ĉi tio ne estas necesa, tiam vi nur bezonas ŝanĝi la specifon.
Mallonga deturniĝo pri produktiveco estas en ordo ĉi tie. Ĝi estas ofte mezurita en la nombro da linioj de kodo skribitaj tage. Sed via laboro estas multe pli utila se vi forigas certan nombron da linioj, ĉar vi havas malpli da loko por cimoj. Kaj la plej facila maniero forigi kodon estas en la unua paŝo. Eblas, ke vi simple ne bezonas ĉiujn sonorilojn kaj fajfilojn, kiujn vi provas efektivigi. La plej rapida maniero por simpligi programon kaj ŝpari tempon estas ne fari aferojn, kiuj ne devus esti faritaj. La dua paŝo havas la duan plej altan tempoŝparan potencialon. Se vi mezuras produktivecon laŭ skribitaj linioj, tiam pensi pri kiel plenumi taskon faros vin malpli produktiva, ĉar vi povas solvi la saman problemon per malpli da kodo. Mi ne povas doni precizajn statistikojn ĉi tie, ĉar mi ne havas manieron kalkuli la nombron da linioj, kiujn mi ne skribis pro la tempo, kiun mi pasigis pri la specifo, tio estas, pri la unua kaj dua paŝoj. Kaj ankaŭ ĉi tie ni ne povas fari eksperimenton, ĉar en eksperimento ni ne rajtas plenumi la unuan paŝon; la tasko estas antaŭdeterminita.
Estas facile preteratenti multajn malfacilaĵojn en neformalaj specifoj. Estas nenio malfacila pri skribado de striktaj specifoj por funkcioj; mi ne diskutos tion. Anstataŭe, ni parolos pri verkado de fortaj specifoj por normaj kondutoj. Estas teoremo kiu deklaras ke ajna aro de kondutoj povas esti priskribita uzante la sekurecan posedaĵon (sekureco) kaj traviveblaj ecoj (viveco). Sekureco signifas, ke nenio malbona okazos, la programo ne donos malĝustan respondon. Travivebleco signifas, ke baldaŭ io bona okazos, t.e. la programo pli aŭ malpli frue donos la ĝustan respondon. Kiel regulo, sekureco estas pli grava indikilo; eraroj plej ofte okazas ĉi tie. Tial, por ŝpari tempon, mi ne parolos pri travivebleco, kvankam ĝi, kompreneble, ankaŭ gravas.
Ni atingas sekurecon unue specifante aron da eblaj komencaj statoj. Kaj due, rilatoj kun ĉiuj eblaj venontaj ŝtatoj por ĉiu ŝtato. Ni kondutu kiel sciencistoj kaj difinu statojn matematike. La aro de komencaj statoj estas priskribita per la formulo, ekzemple, en la kazo de la eŭklida algoritmo: (x = M) ∧ (y = N). Por certaj valoroj M и N ekzistas nur unu komenca stato. La rilato kun la sekva stato estas priskribita per formulo en kiu la variabloj de la sekva stato estas skribitaj kun primo, kaj la variabloj de la nuna stato estas skribitaj sen primo. En la kazo de la eŭklida algoritmo, ni traktos la disjunkcion de du formuloj, en unu el kiuj x estas la plej granda valoro, kaj en la dua - y:
En la unua kazo, la nova valoro de y estas egala al la antaŭa valoro de y, kaj ni ricevas la novan valoron de x subtrahante la pli malgrandan variablon de la pli granda. En la dua kazo, ni faras la malon.
Ni revenu al la eŭklida algoritmo. Supozu denove tion M = 12, N = 18. Ĉi tio difinas ununuran komencan staton, (x = 12) ∧ (y = 18). Ni tiam ŝtopas ĉi tiujn valorojn en la supran formulon kaj ricevas:
Jen la sola ebla solvo: x' = 18 - 12 ∧ y' = 12, kaj ni ricevas la konduton: [x = 12, y = 18]. En la sama maniero, ni povas priskribi ĉiujn statojn en nia konduto: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
En lasta stato [x = 6, y = 6] ambaŭ partoj de la esprimo estos malveraj, tial ĝi ne havas sekvan staton. Do, ni havas kompletan specifon de la dua paŝo - kiel ni vidas, tio estas sufiĉe ordinara matematiko, kiel tiu de inĝenieroj kaj sciencistoj, kaj ne stranga, kiel en komputiko.
Tiuj du formuloj povas esti kombinitaj en unu formulon de tempa logiko. Ĝi estas eleganta kaj facile klarigebla, sed ne estas tempo por ĝi nun. Ni eble bezonas tempan logikon nur por la propraĵo de viveco; por sekureco ĝi ne estas bezonata. Mi ne ŝatas tempan logiko kiel tia, ĝi ne estas tute ordinara matematiko, sed en la kazo de viveco ĝi estas necesa malbono.
En eŭklida algoritmo por ĉiu valoro x и y estas unikaj valoroj x' и y', kiuj faras la rilaton kun la sekva stato vera. Alivorte, la eŭklida algoritmo estas determinisma. Por modeligi nedeterminisman algoritmon, la nuna stato devas havi plurajn eblajn estontajn statojn, kaj ĉiu valoro de la neprema variablo devas havi multoblajn valorojn de la primata variablo tia ke la rilato al la sekva stato estas vera. Ĉi tio ne estas malfacile fari, sed mi ne donos ekzemplojn nun.
Por fari laborilon, vi bezonas formalan matematikon. Kiel fari specifon formala? Por fari tion ni bezonos formalan lingvon, ekz. . La specifo de la eŭklida algoritmo en ĉi tiu lingvo aspektos jene:
La simbolo de egala signo kun triangulo signifas, ke la valoro maldekstre de la signo estas determinita esti egala al la valoro dekstre de la signo. En esenco, specifo estas difino, en nia kazo du difinoj. Al la specifo en TLA+ vi devas aldoni deklarojn kaj iom da sintakso, kiel en la supra lumbildo. En ASCII ĝi aspektus jene:
Kiel vi povas vidi, nenio komplika. La specifo pri TLA+ povas esti kontrolita, t.e., estas eble preteriri ĉiujn eblajn kondutojn en malgranda modelo. En nia kazo, ĉi tiu modelo estos certaj valoroj M и N. Ĉi tio estas tre efika kaj simpla konfirma metodo, kiu estas tute aŭtomata. Krome, eblas verki formalajn pruvojn de vero kaj kontroli ilin meĥanike, sed tio bezonas multan tempon, do preskaŭ neniu faras tion.
La ĉefa malavantaĝo de TLA+ estas, ke ĝi estas matematiko, kaj programistoj kaj komputikistoj timas matematikon. Unuavide tio sonas kiel ŝerco, sed, bedaŭrinde, mi diras tion tute serioze. Mia kolego ĵus rakontis al mi kiel li provis klarigi TLA+ al pluraj programistoj. Tuj kiam la formuloj aperis sur la ekrano, iliaj okuloj tuj fariĝis vitraj. Do se TLA+ estas timiga, vi povas uzi , estas speco de ludila programlingvo. Esprimo en PlusCal povas esti ajna TLA+-esprimo, tio estas, esence iu ajn matematika esprimo. Plie, PlusCal havas sintakson por ne-determinismaj algoritmoj. Ĉar PlusCal povas skribi ajnan TLA+-esprimon, ĝi estas signife pli esprimplena ol iu reala programlingvo. Poste, PlusCal estas kompilita en facile legeblan TLA+-specifon. Ĉi tio ne signifas, kompreneble, ke la kompleksa PlusCal-specifo fariĝos simpla sur TLA+ - nur ke la korespondado inter ili estas evidenta, neniu plia komplekseco aperos. Fine, ĉi tiu specifo povas esti kontrolita per TLA+-iloj. Ĝenerale, PlusCal povas helpi venki fobion de matematiko; ĝi estas facile komprenebla eĉ por programistoj kaj komputikistoj. Mi publikigis algoritmojn pri ĝi dum iom da tempo (ĉirkaŭ 10 jaroj) en la pasinteco.
Eble iu kontraŭstaros, ke TLA+ kaj PlusCal estas matematiko, kaj matematiko funkcias nur kun faritaj ekzemploj. Praktike oni bezonas veran lingvon kun tipoj, proceduroj, objektoj ktp. Ĉi tio estas malĝusta. Jen kion Chris Newcomb, kiu laboris ĉe Amazon, skribas: "Ni uzis TLA+ en dek grandaj projektoj, kaj en ĉiu kazo ĝia uzo faris gravan diferencon al evoluo ĉar ni povis kapti danĝerajn cimojn antaŭ ol ili trafis produktadon, kaj ĉar ĝi donis al ni la komprenon kaj fidon, kiujn ni bezonis por fari agresemajn. agado-optimumigoj sen influi la veron de la programo". Ofte oni povas aŭdi, ke kiam oni uzas formalajn metodojn ni ricevas malefikan kodon - praktike ĉio estas ĝuste la malo. Krome, ekzistas percepto ke administrantoj ne povas esti konvinkitaj pri la bezono de formalaj metodoj, eĉ se programistoj estas konvinkitaj pri sia utileco. Kaj Newcomb skribas: "Manaĝeroj nun premas ĉiumaniere por skribi specifojn en TLA+, kaj specife asignas tempon por ĉi tio". Do kiam administrantoj vidas, ke TLA+ funkcias, ili akceptas ĝin. Chris Newcomb skribis ĉi tion antaŭ proksimume ses monatoj (oktobro 2014), sed nun, laŭ mia scio, TLA+ estas uzata en 14 projektoj, ne 10. Alia ekzemplo rilatas al la dezajno de la XBox 360. Staĝanto venis al Charles Thacker kaj skribis specifon por la memorsistemo. Danke al ĉi tiu specifo, cimo estis trovita, kiu alie estus nerimarkita kaj kaŭzus ĉiun XBox 360 kraŝi post kvar horoj da uzo. Inĝenieroj de IBM konfirmis, ke iliaj provoj ne detektus ĉi tiun cimon.
Vi povas legi pli pri TLA+ en la Interreto, sed nun ni parolu pri neformalaj specifoj. Ni malofte devas skribi programojn, kiuj kalkulas la malplej komunan dividon kaj similajn. Multe pli ofte ni skribas programojn kiel la bela-presilo, kiun mi skribis por TLA+. Post la plej simpla prilaborado, la TLA+-kodo aspektus jene:
Sed en la supra ekzemplo, la uzanto plej verŝajne volis, ke la konjunkcio kaj egalaj signoj estu vicigitaj. Do la ĝusta formatado aspektus pli kiel ĉi tio:
Ni konsideru alian ekzemplon:
Ĉi tie, male, la vicigo de egalaj signoj, aldono kaj multipliko en la fonto estis hazarda, do la plej simpla prilaborado sufiĉas. Ĝenerale, ne ekzistas preciza matematika difino de ĝusta formatado, ĉar "ĝusta" ĉi-kaze signifas "tion, kion la uzanto volas", kaj ĉi tio ne povas esti determinita matematike.
Ŝajnus, ke se ni ne havas difinon de vero, tiam la specifo estas senutila. Sed tio ne estas vera. Nur ĉar ni ne scias, kion programo devas fari, ne signifas, ke ni ne bezonas pensi pri kiel ĝi devus funkcii—kontraŭe, ni devus elspezi eĉ pli da peno por ĝi. La specifo estas precipe grava ĉi tie. Estas neeble determini la optimuman programon por strukturita presado, sed tio ne signifas, ke ni tute ne devas entrepreni ĝin, kaj skribi kodon kiel fluo de konscio ne estas la kazo. Mi finis skribi specifon de ses reguloj kun difinoj en formo de komentoj en Java dosiero. Jen ekzemplo de unu el la reguloj: a left-comment token is LeftComment aligned with its covering token. Ĉi tiu regulo estas skribita en, ni diru, matematika angla: LeftComment aligned, left-comment и covering token — terminoj kun difinoj. Jen kiel matematikistoj priskribas matematikon: ili skribas difinojn de terminoj kaj, surbaze de ili, kreas regulojn. La avantaĝo de ĉi tiu specifo estas ke ses reguloj estas multe pli facile kompreneblaj kaj sencimigitaj ol 850 linioj de kodo. Mi devas diri, ke skribi ĉi tiujn regulojn ne estis facila; necesis sufiĉe da tempo por sencimigi ilin. Mi skribis kodon specife por ĉi tiu celo, kiu diris al mi, kiu regulo estas uzata. Ĉar mi provis ĉi tiujn ses regulojn per kelkaj ekzemploj, mi ne devis sencimigi 850 liniojn de kodo, kaj la eraroj estis sufiĉe facile troveblaj. Java havas bonegajn ilojn por tio. Se mi ĵus skribus la kodon, ĝi prenus min multe pli longe kaj la formatado estus pli malbona kvalito.
Kial formala specifo ne povus esti uzata? Unuflanke, ĝusta ekzekuto ne tro gravas ĉi tie. Strukturita printaĵo nepre estos malkontentiga por iuj, do mi ne devis korekti ĝin en ĉiuj nekutimaj situacioj. Eĉ pli grava estas la fakto, ke mi ne havis taŭgajn ilojn. La TLA+ modelkontrolilo estas senutila ĉi tie, do mi devus skribi la ekzemplojn permane.
La donita specifo havas trajtojn komunajn al ĉiuj specifoj. Ĝi estas pli alta nivelo ol kodo. Ĝi povas esti efektivigita en ajna lingvo. Ne ekzistas iloj aŭ metodoj por skribi ĝin. Neniu programa kurso helpos vin skribi ĉi tiun specifon. Kaj ne ekzistas iloj, kiuj povus igi ĉi tiun specifon nenecesa, krom se vi kompreneble skribas lingvon specife por verki strukturitajn presitajn programojn en TLA+. Fine, ĉi tiu specifo diras nenion pri kiel precize ni skribos la kodon, ĝi nur deklaras kion faras la kodo. Ni skribas specifon por helpi nin pripensi la problemon antaŭ ol ni komencas pensi pri la kodo.
Sed ĉi tiu specifo ankaŭ havas trajtojn, kiuj distingas ĝin de aliaj specifoj. 95% de aliaj specifoj estas multe pli mallongaj kaj pli simplaj:
Plue, ĉi tiu specifo estas aro de reguloj. Ĉi tio estas kutime signo de malbona specifo. Kompreni la sekvojn de aro de reguloj estas sufiĉe malfacila, tial mi devis pasigi multe da tempo sencimigi ilin. Tamen en ĉi tiu kazo mi ne povis trovi pli bonan manieron.
Indas diri kelkajn vortojn pri programoj, kiuj funkcias senĉese. Tipe ili funkcias paralele, kiel operaciumoj aŭ distribuitaj sistemoj. Tre malmultaj homoj povas kompreni ilin en sia menso aŭ sur papero, kaj mi ne estas unu el ili, kvankam mi iam povis fari ĝin. Tial ni bezonas ilojn, kiuj kontrolos nian laboron - ekzemple TLA+ aŭ PlusCal.
Kial mi devis skribi specifon se mi jam sciis, kion la kodo devas fari? Fakte, mi nur pensis, ke mi sciis ĝin. Krome, kun specifo en loko, eksterulo ne plu bezonas rigardi en la kodon por kompreni kion ĝuste ĝi faras. Mi havas regulon: ne estu ĝeneralaj reguloj. Estas escepto al ĉi tiu regulo kompreneble, ĉi tiu estas la nura ĝenerala regulo, kiun mi sekvas: la specifo pri tio, kion faras la kodo, devus diri al homoj ĉion, kion ili bezonas scii kiam ili uzas tiun kodon.
Do kion precize programistoj bezonas scii pri pensado? Komence, same kiel por ĉiuj: se vi ne skribas, tiam ŝajnas al vi nur, ke vi pensas. Ankaŭ vi devas pensi antaŭ ol vi kodi, kio signifas, ke vi devas skribi antaŭ ol vi kodi. Specifo estas tio, kion ni skribas antaŭ ol ni komencas kodigi. Specifo necesas por iu ajn kodo, kiu povas esti uzata aŭ ŝanĝita de iu ajn. Kaj ĉi tiu "iu" povas montriĝi esti la aŭtoro de la kodo monaton post kiam ĝi estis skribita. Specifo necesas por grandaj programoj kaj sistemoj, por klasoj, por metodoj, kaj foje eĉ por kompleksaj sekcioj de ununura metodo. Kion precize vi skribu pri la kodo? Vi devas priskribi, kion ĝi faras, tio estas, ion, kio povas esti utila al iu ajn, kiu uzas ĉi tiun kodon. Foje eble ankaŭ necesas specifi kiel precize la kodo atingas sian celon. Se ni ekzamenis ĉi tiun metodon en la kurso de algoritmoj, tiam ni nomas ĝin algoritmo. Se ĝi estas io pli specialigita kaj nova, tiam ni nomas ĝin altnivela dezajno. Ne estas formala diferenco ĉi tie: ambaŭ estas abstraktaj modeloj de la programo.
Kiel precize vi skribu kodan specifon? La ĉefa afero: ĝi devus esti unu nivelo pli alta ol la kodo mem. Ĝi devas priskribi statojn kaj kondutojn. Ĝi devus esti tiel strikta kiel la tasko postulas. Se vi skribas specifon pri kiel efektivigi taskon, tiam ĝi povas esti skribita en pseŭdokodo aŭ uzante PlusCal. Vi devas lerni skribi specifojn uzante formalajn specifojn. Ĉi tio donos al vi la necesajn kapablojn, kiuj ankaŭ helpos kun neformalaj. Kiel vi povas lerni skribi formalajn specifojn? Kiam ni lernis programi, ni skribis programojn kaj poste sencimigis ilin. Same ĉi tie: vi devas skribi specifon, kontroli ĝin per modelkontrolilo kaj ripari la erarojn. TLA+ eble ne estas la plej bona lingvo por formala specifo, kaj alia lingvo verŝajne pli taŭgas por viaj specifaj bezonoj. La bonega afero pri TLA+ estas, ke ĝi faras bonegan laboron por instrui matematikan pensadon.
Kiel ligi specifon kaj kodon? Uzante komentojn kiuj ligas matematikajn konceptojn kaj ilian efektivigon. Se vi laboras kun grafikaĵoj, tiam ĉe la programnivelo vi havos tabelojn de nodoj kaj tabelojn de ligiloj. Do vi devas skribi kiel ĝuste la grafeo estas efektivigita de ĉi tiuj programaj strukturoj.
Oni devas rimarki, ke neniu el ĉi-supraj validas por la procezo de skribado de kodo mem. Kiam vi skribas kodon, tio estas, plenumas la trian paŝon, vi ankaŭ devas pensi kaj pensi tra la programo. Se subtasko montriĝas kompleksa aŭ ne evidenta, vi devas skribi specifon por ĝi. Sed mi ne parolas pri la kodo mem ĉi tie. Vi povas uzi ajnan programlingvon, ajnan metodaron, ĉi tio ne temas pri ili. Ankaŭ, neniu el ĉi-supraj forigas la bezonon testi kaj sencimigi vian kodon. Eĉ se la abstrakta modelo estas skribita ĝuste, povas esti eraroj en ĝia efektivigo.
Skribi specifojn estas plia paŝo en la kodiga procezo. Danke al ĝi, multaj eraroj povas esti kaptitaj per malpli da peno - tion ni scias el la sperto de programistoj de Amazon. Kun specifoj, la kvalito de programoj iĝas pli alta. Kial do ni tiel ofte iras sen ili? Ĉar skribi estas malfacila. Sed skribi estas malfacila, ĉar por tio necesas pensi, kaj pensi ankaŭ malfacilas. Ĉiam estas pli facile ŝajnigi, ke vi pensas. Ĉi tie vi povas desegni analogion kun kurado - ju malpli vi kuras, des pli malrapide vi kuras. Vi devas trejni viajn muskolojn kaj praktiki skribadon. Necesas praktiko.
La specifo povas esti malĝusta. Vi eble faris eraron ie, aŭ la postuloj eble ŝanĝiĝis, aŭ eble necesas plibonigo. Ajna kodo, kiun iu ajn uzas, devas esti ŝanĝita, do pli aŭ malpli frue la specifo ne plu kongruos kun la programo. Ideale, en ĉi tiu kazo, vi devas skribi novan specifon kaj tute reverki la kodon. Ni scias tre bone, ke neniu faras ĉi tion. En la praktiko, ni flikigas la kodon kaj eble ĝisdatigas la specifon. Se ĉi tio nepre okazos baldaŭ aŭ malfrue, kial do skribi specifojn entute? Unue, por la persono, kiu redaktos vian kodon, ĉiu kroma vorto en la specifo valoros sian pezon en oro, kaj ĉi tiu persono eble estos vi. Mi ofte piedbatas min pro ne esti sufiĉe specifa kiam mi redaktas mian kodon. Kaj mi skribas pli da specifoj ol kodo. Tial, kiam vi redaktas la kodon, la specifo ĉiam devas esti ĝisdatigita. Due, kun ĉiu redakto la kodo plimalboniĝas, ĝi fariĝas pli malfacila legi kaj konservi. Ĉi tio estas pliiĝo de entropio. Sed se vi ne komencas per specifo, tiam ĉiu linio, kiun vi skribos, estos redakto, kaj la kodo estos dika kaj malfacile legebla de la komenco.
Kiel dirite , neniu batalo estis venkita laŭ plano, kaj neniu batalo estis venkita sen plano. Kaj li sciis ion pri bataloj. Estas opinio, ke skribi specifojn estas tempoperdo. Kelkfoje tio estas vera, kaj la tasko estas tiel simpla, ke ne utilas pripensi ĝin. Sed vi ĉiam devas memori, ke kiam oni konsilas al vi ne skribi specifojn, tio signifas, ke oni konsilas al vi ne pensi. Kaj vi devus pensi pri tio ĉiufoje. Pensi pri tasko ne garantias, ke vi ne faros erarojn. Kiel ni scias, neniu inventis magian vergon, kaj programado estas malfacila tasko. Sed se vi ne pripensas la taskon, vi estas garantiita fari erarojn.
Vi povas legi pli pri TLA+ kaj PlusCal en speciala retejo, vi povas iri tien de mia hejmpaĝo . Tio estas ĉio por mi, dankon pro via atento.
Bonvolu memori, ke ĉi tio estas traduko. Kiam vi skribas komentojn, memoru, ke la aŭtoro ne legos ilin. Se vi vere volas babili kun la aŭtoro, li estos ĉe la konferenco Hydra 2019, kiu okazos la 11-12-an de julio 2019 en Sankt-Peterburgo. Biletoj estas aĉeteblaj .
fonto: www.habr.com