Isa itong artikulo sa pagsasalin . Ngunit bago iyon ay may isang maikling pagpapakilala. Paano nabuo ang mga zombie? Ang bawat isa ay natagpuan ang kanilang sarili sa isang sitwasyon kung saan gusto nilang dalhin ang isang kaibigan o kasamahan sa kanilang antas, ngunit hindi ito gumana. Bukod dito, "hindi ito gumagana" hindi gaanong para sa iyo, ngunit para sa kanya: sa isang bahagi ng sukat ay may normal na suweldo, mga gawain, at iba pa, at sa kabilang banda ay ang pangangailangang mag-isip. Ang pag-iisip ay hindi kasiya-siya at masakit. Mabilis siyang sumuko at nagpatuloy sa pagsulat ng code nang hindi man lang ginagamit ang kanyang utak. Napagtanto mo kung gaano karaming pagsisikap ang kinakailangan upang mapagtagumpayan ang hadlang ng natutunan na kawalan ng kakayahan, at hindi mo ito ginagawa. Ganito nabubuo ang mga zombie na tila kayang gamutin ngunit tila walang gagawa nito.
Nung nakita ko yun (oo, ang parehong kaibigan mula sa mga aklat-aralin) at hindi nagbibigay ng ulat, ngunit isang sesyon ng tanong-at-sagot, medyo nag-iingat ako. Kung sakali, si Leslie ay isang kilalang siyentipiko sa buong mundo, ang may-akda ng seminal na gumagana sa distributed computing, at maaari mo rin siyang makilala sa pamamagitan ng mga titik na La sa LaTeX - "Lamport TeX". Ang pangalawang nakababahala na kadahilanan ay ang kanyang kinakailangan: lahat ng darating ay dapat (ganap na walang bayad) makinig sa ilang mga ulat nang maaga, mag-isip ng hindi bababa sa isang katanungan tungkol sa mga ito, at pagkatapos ay dumating. Nagpasya akong tingnan kung ano ang ibino-broadcast ng Lamport doon - at ito ay mahusay! Ito ay eksaktong bagay na iyon, isang magic link-pill para sa pagpapagamot ng mga zombie. Binabalaan kita: ang teksto ay maaaring seryosong masunog ang mga mahilig sa napakabilis na pamamaraan at hindi gustong subukan ang kanilang isinulat.
Pagkatapos ng habrokat, nagsimula na talaga ang pagsasalin ng seminar. Enjoy reading!
Anuman ang iyong gawain, kailangan mong laging dumaan sa tatlong hakbang:
- magpasya kung anong layunin ang nais mong makamit;
- magpasya kung paano eksaktong makakamit mo ang iyong layunin;
- abutin ang Layunin.
Nalalapat din ito sa programming. Kapag nagsusulat kami ng code, kailangan namin:
- magpasya kung ano ang eksaktong dapat gawin ng programa;
- tiyakin kung paano ito dapat gawin ang gawain nito;
- isulat ang naaangkop na code.
Ang huling hakbang, siyempre, ay napakahalaga, ngunit hindi ko ito pag-uusapan ngayon. Sa halip, tatalakayin natin ang unang dalawa. Ginagawa ng bawat programmer ang mga ito bago magsimulang magtrabaho. Hindi ka uupo upang magsulat maliban kung napagpasyahan mo kung ano ang iyong isinusulat: isang browser o isang database. Ang isang tiyak na ideya ng layunin ay dapat na naroroon. At tiyak na iniisip mo kung ano ang eksaktong gagawin ng programa, at huwag isulat ito nang basta-basta sa pag-asa na ang code mismo ay kahit papaano ay magiging isang browser.
Paano eksaktong nangyayari ang paunang pag-iisip na ito ng code? Gaano karaming pagsisikap ang dapat nating ilagay dito? Ang lahat ay nakasalalay sa kung gaano kakomplikado ang problema na ating nilulutas. Sabihin nating gusto naming magsulat ng isang fault-tolerant distributed system. Sa kasong ito, dapat nating pag-isipang mabuti ang mga bagay bago umupo sa code. Paano kung kailangan lang nating dagdagan ang isang integer variable ng 1? Sa unang sulyap, ang lahat dito ay walang kabuluhan at hindi kailangan ng pag-iisip, ngunit pagkatapos ay naaalala natin na ang isang pag-apaw ay maaaring mangyari. Samakatuwid, kahit na upang maunawaan kung ang isang problema ay simple o kumplikado, kailangan mo munang mag-isip.
Kung nag-iisip ka ng mga posibleng solusyon sa isang problema nang maaga, maiiwasan mo ang mga pagkakamali. Ngunit kailangan nitong maging malinaw ang iyong pag-iisip. Upang makamit ito, kailangan mong isulat ang iyong mga saloobin. Gustung-gusto ko ang quote ni Dick Guindon: "Kapag nagsusulat ka, ipinapakita sa iyo ng kalikasan kung gaano kabaliw ang iyong pag-iisip." Kung hindi ka nagsusulat, iniisip mo lang na iniisip mo. At kailangan mong isulat ang iyong mga iniisip sa anyo ng mga pagtutukoy.
Ang mga pagtutukoy ay nagsisilbi sa maraming mga pag-andar, lalo na sa malalaking proyekto. Ngunit isa lang sa kanila ang sasabihin ko: tinutulungan nila tayong mag-isip nang malinaw. Ang pag-iisip ng malinaw ay napakahalaga at medyo mahirap, kaya kailangan natin ng anumang tulong dito. Sa anong wika tayo dapat sumulat ng mga pagtutukoy? Sa pangkalahatan, ito ang palaging unang tanong para sa mga programmer: anong wika ang isusulat natin? Walang tamang sagot: masyadong magkakaiba ang mga problemang nalulutas natin. Para sa ilang tao, ang TLA+ ay isang specification na wika na aking binuo. Para sa iba, mas maginhawang gumamit ng Chinese. Ang lahat ay nakasalalay sa sitwasyon.
Ang mas mahalagang tanong ay: paano natin makakamit ang mas malinaw na pag-iisip? Sagot: Dapat tayong mag-isip tulad ng mga siyentipiko. Ito ay isang paraan ng pag-iisip na gumana nang maayos sa nakalipas na 500 taon. Sa agham, bumuo tayo ng mga modelong matematikal ng katotohanan. Ang Astronomy ay marahil ang unang agham sa mahigpit na kahulugan ng salita. Sa modelong matematikal na ginamit sa astronomiya, lumilitaw ang mga celestial na katawan bilang mga punto na may masa, posisyon at momentum, bagaman sa katotohanan ang mga ito ay napakasalimuot na mga bagay na may mga bundok at karagatan, mga pag-agos at pag-agos. Ang modelong ito, tulad ng iba pa, ay nilikha upang malutas ang ilang mga problema. Ito ay mahusay para sa pagtukoy kung saan ituturo ang isang teleskopyo kung gusto mong makahanap ng isang planeta. Ngunit kung gusto mong hulaan ang lagay ng panahon sa planetang ito, hindi gagana ang modelong ito.
Pinapayagan tayo ng matematika na matukoy ang mga katangian ng isang modelo. At ipinapakita ng agham kung paano nauugnay ang mga katangiang ito sa katotohanan. Pag-usapan natin ang ating agham, agham sa kompyuter. Ang katotohanang pinagtatrabahuhan namin ay ang mga computing system ng maraming iba't ibang uri: mga processor, game console, mga computer na nagpapatakbo ng mga program, at iba pa. Magsasalita ako tungkol sa pagpapatupad ng isang programa sa isang computer, ngunit, sa pangkalahatan, ang lahat ng mga konklusyong ito ay nalalapat sa anumang sistema ng pag-compute. Sa aming agham ay gumagamit kami ng maraming iba't ibang mga modelo: ang Turing machine, bahagyang nakaayos na mga hanay ng mga kaganapan, at marami pang iba.
Ano ang programa? Ito ay anumang code na maaaring isaalang-alang sa sarili nitong. Sabihin nating kailangan nating magsulat ng browser. Nagsasagawa kami ng tatlong gawain: idisenyo ang pagtatanghal ng programa ng gumagamit, pagkatapos ay isulat ang mataas na antas ng diagram ng programa, at sa wakas ay isulat ang code. Habang isinusulat namin ang code, napagtanto namin na kailangan naming magsulat ng text formatter. Narito muli kailangan nating lutasin ang tatlong problema: tukuyin kung anong teksto ang ibabalik ng tool na ito; pumili ng isang algorithm para sa pag-format; sumulat ng code. Ang gawaing ito ay may sariling subtask: wastong pagpasok ng mga gitling sa mga salita. Niresolba din namin ang subtask na ito sa tatlong hakbang - tulad ng nakikita namin, inuulit ang mga ito sa maraming antas.
Tingnan natin ang unang hakbang: anong problema ang nalulutas ng programa. Dito madalas naming imodelo ang isang programa bilang isang function na kumukuha ng ilang input at nagbibigay ng ilang output. Sa matematika, ang isang function ay karaniwang inilalarawan bilang isang nakaayos na hanay ng mga pares. Halimbawa, ang squaring function para sa mga natural na numero ay inilarawan bilang set {<0,0>, <1,1>, <2,4>, <3,9>, β¦}. Ang domain ng kahulugan ng naturang function ay ang hanay ng mga unang elemento ng bawat pares, iyon ay, natural na mga numero. Upang tukuyin ang isang function, kailangan nating tukuyin ang domain at formula nito.
Ngunit ang mga function sa matematika ay hindi katulad ng mga function sa mga programming language. Ang matematika ay mas simple. Dahil wala akong oras para sa mga kumplikadong halimbawa, isaalang-alang natin ang isang simple: isang function sa C o isang static na pamamaraan sa Java na nagbabalik ng pinakamalaking karaniwang divisor ng dalawang integer. Sa pagtutukoy ng pamamaraang ito ay isusulat namin: kinakalkula GCD(M,N) para sa mga argumento M ΠΈ NSaan GCD(M,N) - isang function na ang domain ay isang set ng mga pares ng integer, at ang return value ay ang pinakamalaking integer na hinati sa M ΠΈ N. Paano maihahambing ang katotohanan sa modelong ito? Ang modelo ay gumagana sa mga integer, at sa C o Java mayroon kaming 32-bit int. Ang modelong ito ay nagpapahintulot sa amin na magpasya kung ang algorithm ay tama GCD, ngunit hindi nito mapipigilan ang mga error sa overflow. Mangangailangan ito ng isang mas kumplikadong modelo, kung saan walang oras.
Pag-usapan natin ang mga limitasyon ng function bilang isang modelo. Ang ilang mga programa (tulad ng mga operating system) ay hindi lamang nagbabalik ng isang partikular na halaga para sa ilang mga argumento; maaari silang tumakbo nang tuluy-tuloy. Bilang karagdagan, ang pag-andar bilang isang modelo ay hindi angkop para sa pangalawang hakbang: pagpaplano kung paano lutasin ang problema. Ang Quicksort at bubble sort ay nakalkula ang parehong function, ngunit ang mga ito ay ganap na magkaibang mga algorithm. Samakatuwid, upang ilarawan ang paraan upang makamit ang layunin ng programa, gumamit ako ng isa pang modelo, tawagin natin itong karaniwang modelo ng pag-uugali. Ang programa ay kinakatawan dito bilang isang hanay ng lahat ng wastong pag-uugali, na ang bawat isa, sa turn, ay isang pagkakasunud-sunod ng mga estado, at ang isang estado ay ang pagtatalaga ng mga halaga sa mga variable.
Tingnan natin kung ano ang magiging hitsura ng pangalawang hakbang para sa Euclidean algorithm. Kailangan nating kalkulahin GCD(M, N). Nagsisimula kami M bilang xAt N bilang y, pagkatapos ay paulit-ulit na ibawas ang mas maliit sa mga variable na ito mula sa mas malaki hanggang sila ay magkapantay. Halimbawa, kung M = 12At N = 18, maaari nating ilarawan ang sumusunod na pag-uugali:
[x = 12, y = 18] β [x = 12, y = 6] β [x = 6, y = 6]
At kung M = 0 ΠΈ N = 0? Ang zero ay nahahati sa lahat ng mga numero, kaya walang pinakamalaking divisor sa kasong ito. Sa sitwasyong ito, kailangan nating bumalik sa unang hakbang at itanong: kailangan ba talaga nating kalkulahin ang GCD para sa mga hindi positibong numero? Kung hindi ito kinakailangan, kailangan mo lamang baguhin ang detalye.
Ang isang maikling digression sa pagiging produktibo ay nasa order dito. Madalas itong sinusukat sa bilang ng mga linya ng code na isinulat bawat araw. Ngunit ang iyong trabaho ay higit na kapaki-pakinabang kung aalisin mo ang isang tiyak na bilang ng mga linya, dahil mayroon kang mas kaunting puwang para sa mga bug. At ang pinakamadaling paraan upang maalis ang code ay nasa unang hakbang. Posibleng hindi mo lang kailangan ang lahat ng mga kampana at sipol na sinusubukan mong ipatupad. Ang pinakamabilis na paraan upang pasimplehin ang isang programa at makatipid ng oras ay ang hindi paggawa ng mga bagay na hindi dapat gawin. Ang pangalawang hakbang ay may pangalawang pinakamataas na potensyal na makatipid ng oras. Kung susukatin mo ang pagiging produktibo sa mga tuntunin ng mga linyang nakasulat, kung gayon ang pag-iisip tungkol sa kung paano kumpletuhin ang isang gawain ay gagawin mo hindi gaanong produktibo, dahil malulutas mo ang parehong problema sa mas kaunting code. Hindi ako makapagbigay ng eksaktong mga istatistika dito, dahil wala akong paraan upang mabilang ang bilang ng mga linya na hindi ko isinulat dahil sa oras na ginugol ko sa detalye, iyon ay, sa una at pangalawang hakbang. At hindi rin kami makakagawa ng eksperimento dito, dahil sa isang eksperimento wala kaming karapatang kumpletuhin ang unang hakbang; ang gawain ay natukoy nang maaga.
Madaling makaligtaan ang maraming paghihirap sa mga impormal na detalye. Walang mahirap sa pagsulat ng mahigpit na mga pagtutukoy para sa mga pag-andar; hindi ko tatalakayin ito. Sa halip, pag-uusapan natin ang pagsusulat ng mga mahuhusay na detalye para sa mga karaniwang pag-uugali. Mayroong isang theorem na nagsasaad na ang anumang hanay ng mga pag-uugali ay maaaring ilarawan gamit ang ari-arian ng seguridad (kaligtasan) at mga katangian ng survivability (kabuhayan). Ang ibig sabihin ng kaligtasan ay walang masamang mangyayari, hindi magbibigay ng maling sagot ang programa. Ang survivability ay nangangahulugan na maya-maya ay may magandang mangyayari, ibig sabihin, ang programa ay maaga o huli ay magbibigay ng tamang sagot. Bilang isang patakaran, ang seguridad ay isang mas mahalagang tagapagpahiwatig; ang mga error ay kadalasang nangyayari dito. Samakatuwid, upang makatipid ng oras, hindi ako magsasalita tungkol sa survivability, bagaman ito, siyempre, ay mahalaga din.
Nakakamit natin ang kaligtasan sa pamamagitan ng unang pagtukoy ng isang hanay ng mga posibleng panimulang estado. At pangalawa, ang mga relasyon sa lahat ng posibleng susunod na estado para sa bawat estado. Mag-asal tayo tulad ng mga siyentipiko at tukuyin ang mga estado sa matematika. Ang hanay ng mga paunang estado ay inilalarawan ng formula, halimbawa, sa kaso ng Euclidean algorithm: (x = M) β§ (y = N). Para sa ilang mga halaga M ΠΈ N mayroon lamang isang paunang estado. Ang relasyon sa susunod na estado ay inilalarawan sa pamamagitan ng isang pormula kung saan ang mga variable ng susunod na estado ay isinusulat na may prime, at ang mga variable ng kasalukuyang estado ay isinusulat nang walang prime. Sa kaso ng Euclidean algorithm, haharapin natin ang disjunction ng dalawang formula, kung saan ang isa x ay ang pinakamalaking halaga, at sa pangalawa - y:
Sa unang kaso, ang bagong halaga ng y ay katumbas ng dating halaga ng y, at nakukuha natin ang bagong halaga ng x sa pamamagitan ng pagbabawas ng mas maliit na variable mula sa mas malaki. Sa pangalawang kaso, ginagawa namin ang kabaligtaran.
Bumalik tayo sa Euclidean algorithm. Kunwari na naman M = 12, N = 18. Tinutukoy nito ang isang paunang estado, (x = 12) β§ (y = 18). Pagkatapos ay isinasaksak namin ang mga halagang ito sa formula sa itaas at makuha ang:
Narito ang tanging posibleng solusyon: x' = 18 - 12 β§ y' = 12, at nakukuha namin ang pag-uugali: [x = 12, y = 18]. Sa parehong paraan, maaari naming ilarawan ang lahat ng mga estado sa aming pag-uugali: [x = 12, y = 18] β [x = 12, y = 6] β [x = 6, y = 6].
Sa huling estado [x = 6, y = 6] ang parehong bahagi ng expression ay magiging mali, kaya wala itong susunod na estado. Kaya, mayroon kaming kumpletong detalye ng pangalawang hakbang - tulad ng nakikita natin, ito ay medyo ordinaryong matematika, tulad ng sa mga inhinyero at siyentipiko, at hindi kakaiba, tulad ng sa computer science.
Ang dalawang formula na ito ay maaaring pagsamahin sa isang formula ng temporal na lohika. Ito ay elegante at madaling ipaliwanag, ngunit walang oras para dito ngayon. Maaaring kailanganin natin ang temporal na lohika para lamang sa pag-aari ng kasiglahan; para sa seguridad hindi ito kailangan. Hindi ko gusto ang temporal na lohika tulad nito, ito ay hindi masyadong ordinaryong matematika, ngunit sa kaso ng kasiglahan ito ay isang kinakailangang kasamaan.
Sa Euclidean algorithm para sa bawat halaga x ΠΈ y may mga natatanging halaga x' ΠΈ y', na ginagawang totoo ang kaugnayan sa susunod na estado. Sa madaling salita, ang Euclidean algorithm ay deterministic. Upang mag-modelo ng isang hindi tiyak na algorithm, ang kasalukuyang estado ay dapat magkaroon ng maraming posibleng hinaharap na estado, at ang bawat halaga ng hindi naka-primed na variable ay dapat magkaroon ng maraming mga halaga ng primed variable upang ang kaugnayan sa susunod na estado ay totoo. Hindi ito mahirap gawin, ngunit hindi ako magbibigay ng mga halimbawa ngayon.
Upang makagawa ng isang gumaganang tool, kailangan mo ng pormal na matematika. Paano gawing pormal ang isang detalye? Upang gawin ito, kakailanganin namin ng isang pormal na wika, hal. . Ang detalye ng Euclidean algorithm sa wikang ito ay magiging ganito:
Ang simbolo ng equal sign na may tatsulok ay nangangahulugan na ang value sa kaliwa ng sign ay tinutukoy na katumbas ng value sa kanan ng sign. Sa esensya, ang isang pagtutukoy ay isang kahulugan, sa aming kaso ay dalawang kahulugan. Sa detalye sa TLA+ kailangan mong magdagdag ng mga deklarasyon at ilang syntax, tulad ng sa slide sa itaas. Sa ASCII magiging ganito ang hitsura:
Tulad ng nakikita mo, walang kumplikado. Maaaring ma-verify ang detalye sa TLA+, ibig sabihin, posibleng i-bypass ang lahat ng posibleng pag-uugali sa isang maliit na modelo. Sa aming kaso, ang modelong ito ay magiging ilang mga halaga M ΠΈ N. Ito ay isang napaka-epektibo at simpleng paraan ng pag-verify na ganap na awtomatiko. Bilang karagdagan, posible na magsulat ng mga pormal na patunay ng katotohanan at suriin ang mga ito nang mekanikal, ngunit nangangailangan ito ng maraming oras, kaya halos walang gumagawa nito.
Ang pangunahing kawalan ng TLA+ ay ito ay matematika, at ang mga programmer at computer scientist ay natatakot sa matematika. Sa unang tingin ito ay parang isang biro, ngunit, sa kasamaang-palad, sinasabi ko ito nang buong kaseryosohan. Sinasabi lang sa akin ng isang kasamahan ko kung paano niya sinubukang ipaliwanag ang TLA+ sa ilang developer. Sa sandaling lumitaw ang mga formula sa screen, agad na naging malasalamin ang kanilang mga mata. Kaya kung ang TLA+ ay nakakatakot, maaari mong gamitin , ay isang uri ng laruang programming language. Ang isang expression sa PlusCal ay maaaring maging anumang TLA+ expression, iyon ay, karaniwang anumang mathematical expression. Bukod pa rito, ang PlusCal ay may syntax para sa mga hindi tiyak na algorithm. Dahil ang PlusCal ay maaaring sumulat ng anumang TLA+ expression, ito ay higit na nagpapahayag kaysa sa anumang totoong programming language. Susunod, ang PlusCal ay pinagsama-sama sa isang madaling basahin na detalye ng TLA+. Hindi ito nangangahulugan, siyempre, na ang kumplikadong detalye ng PlusCal ay magiging isang simple sa TLA+ - basta ang mga sulat sa pagitan ng mga ito ay malinaw, walang karagdagang pagiging kumplikado ang lilitaw. Panghuli, ang detalyeng ito ay maaaring ma-verify gamit ang mga tool ng TLA+. Sa pangkalahatan, makakatulong ang PlusCal na malampasan ang phobia sa matematika; madali itong maunawaan kahit para sa mga programmer at computer scientist. Nag-publish ako ng mga algorithm dito sa loob ng ilang panahon (mga 10 taon) sa nakaraan.
Marahil ay may tututol na ang TLA+ at PlusCal ay matematika, at gumagana lamang ang matematika sa mga ginawang halimbawa. Sa pagsasagawa, kailangan mo ng isang tunay na wika na may mga uri, pamamaraan, bagay, at iba pa. Mali ito. Narito ang isinulat ni Chris Newcomb, na nagtrabaho sa Amazon: βGumamit kami ng TLA+ sa sampung malalaking proyekto, at sa bawat pagkakataon ang paggamit nito ay gumawa ng makabuluhang pagkakaiba sa pag-unlad dahil nahuli namin ang mga mapanganib na bug bago sila tumama sa produksyon, at dahil nagbigay ito sa amin ng insight at kumpiyansa na kailangan namin para maging agresibo mga pag-optimize ng pagganap nang hindi naiimpluwensyahan ang katotohanan ng programa". Madalas mong marinig na kapag gumagamit ng mga pormal na pamamaraan nakakakuha kami ng hindi mahusay na code - sa pagsasagawa, ang lahat ay eksaktong kabaligtaran. Bilang karagdagan, mayroong isang pang-unawa na ang mga tagapamahala ay hindi maaaring kumbinsido sa pangangailangan para sa mga pormal na pamamaraan, kahit na ang mga programmer ay kumbinsido sa kanilang pagiging kapaki-pakinabang. At isinulat ni Newcomb: "Itinutulak na ngayon ng mga manager ang lahat ng posibleng paraan upang magsulat ng mga detalye sa TLA+, at partikular na naglalaan ng oras para dito". Kaya kapag nakita ng mga manager na gumagana ang TLA+, tinatanggap nila ito. Isinulat ito ni Chris Newcomb mga anim na buwan na ang nakalilipas (Oktubre 2014), ngunit ngayon, sa pagkakaalam ko, ang TLA+ ay ginagamit sa 14 na proyekto, hindi 10. Ang isa pang halimbawa ay nauugnay sa disenyo ng XBox 360. Isang intern ang dumating kay Charles Thacker at nagsulat ng mga detalye para sa sistema ng memorya. Salamat sa pagtutukoy na ito, may nakitang bug na kung hindi man ay hindi natukoy at magiging sanhi ng pag-crash ng bawat XBox 360 pagkatapos ng apat na oras na paggamit. Kinumpirma ng mga inhinyero mula sa IBM na hindi matukoy ng kanilang mga pagsubok ang bug na ito.
Maaari kang magbasa nang higit pa tungkol sa TLA+ sa Internet, ngunit ngayon ay pag-usapan natin ang tungkol sa mga impormal na detalye. Bihira tayong magsulat ng mga programa na kinakalkula ang hindi bababa sa karaniwang divisor at mga katulad nito. Mas madalas kaming nagsusulat ng mga programa tulad ng pretty-printer tool na isinulat ko para sa TLA+. Pagkatapos ng pinakasimpleng pagproseso, magiging ganito ang TLA+ code:
Ngunit sa halimbawa sa itaas, malamang na gusto ng user na ihanay ang conjunction at pantay na mga palatandaan. Kaya mas magiging ganito ang tamang pag-format:
Isaalang-alang ang isa pang halimbawa:
Dito, sa kabaligtaran, ang pagkakahanay ng pantay na mga palatandaan, pagdaragdag at pagpaparami sa pinagmulan ay random, kaya ang pinakasimpleng pagproseso ay sapat na. Sa pangkalahatan, walang eksaktong mathematical na kahulugan ng tamang pag-format, dahil ang "tama" sa kasong ito ay nangangahulugang "kung ano ang gusto ng user," at hindi ito matutukoy sa matematika.
Tila na kung wala tayong kahulugan ng katotohanan, kung gayon ang espesipikasyon ay walang silbi. Ngunit hindi iyon totoo. Dahil hindi natin alam kung ano ang dapat gawin ng isang programa ay hindi nangangahulugang hindi natin kailangang isipin kung paano ito gaganaβsa kabaligtaran, dapat tayong gumugol ng higit pang pagsisikap dito. Ang pagtutukoy ay lalong mahalaga dito. Imposibleng matukoy ang pinakamainam na programa para sa nakabalangkas na pag-print, ngunit hindi ito nangangahulugan na hindi natin ito dapat gawin, at ang pagsulat ng code bilang isang stream ng kamalayan ay hindi ang kaso. Natapos ko ang pagsulat ng isang detalye ng anim na panuntunan na may mga kahulugan sa anyo ng mga komento sa isang Java file. Narito ang isang halimbawa ng isa sa mga patakaran: a left-comment token is LeftComment aligned with its covering token. Ang panuntunang ito ay nakasulat sa, sabihin nating, mathematical English: LeftComment aligned, left-comment ΠΈ covering token β mga termino na may mga kahulugan. Ganito inilarawan ng mga mathematician ang matematika: sumusulat sila ng mga kahulugan ng mga termino at, batay sa mga ito, lumikha ng mga panuntunan. Ang pakinabang ng detalyeng ito ay ang anim na panuntunan ay mas madaling maunawaan at i-debug kaysa sa 850 linya ng code. Dapat kong sabihin na ang pagsusulat ng mga panuntunang ito ay hindi madali; kinailangan ito ng maraming oras upang i-debug ang mga ito. Sumulat ako ng code na partikular para sa layuning ito na nagsabi sa akin kung aling panuntunan ang ginagamit. Dahil sinubukan ko ang anim na panuntunang ito gamit ang ilang halimbawa, hindi ko na kinailangang mag-debug ng 850 linya ng code, at ang mga bug ay medyo madaling mahanap. Ang Java ay may mahusay na mga tool para dito. Kung isinulat ko lang ang code, ito ay tumagal sa akin nang mas matagal at ang pag-format ay magiging mas mahina ang kalidad.
Bakit hindi magagamit ang isang pormal na detalye? Sa isang banda, ang tamang pagpapatupad ay hindi masyadong mahalaga dito. Ang isang structured na pag-print ay tiyak na hindi kasiya-siya sa ilan, kaya hindi ko na kailangang gawin itong gumana nang tama sa lahat ng hindi pangkaraniwang sitwasyon. Ang mas mahalaga ay ang katotohanan na wala akong sapat na mga kasangkapan. Ang TLA+ model checker ay walang silbi dito, kaya kailangan kong isulat ang mga halimbawa sa pamamagitan ng kamay.
Ang ibinigay na detalye ay may mga tampok na karaniwan sa lahat ng mga pagtutukoy. Ito ay mas mataas na antas kaysa sa code. Maaari itong ipatupad sa anumang wika. Walang mga kasangkapan o pamamaraan para sa pagsulat nito. Walang kursong programming ang tutulong sa iyo na isulat ang detalyeng ito. At walang mga tool na maaaring gawing hindi kailangan ang detalyeng ito, maliban kung siyempre sumusulat ka ng isang wika na partikular para sa pagsusulat ng mga structured printout na programa sa TLA+. Sa wakas, ang detalyeng ito ay walang sinasabi tungkol sa kung paano eksaktong isusulat namin ang code, ito ay nagsasaad lamang kung ano ang ginagawa ng code. Sumulat kami ng isang detalye upang matulungan kaming pag-isipan ang problema bago namin simulan ang pag-iisip tungkol sa code.
Ngunit ang pagtutukoy na ito ay mayroon ding mga tampok na nagpapaiba nito sa iba pang mga pagtutukoy. 95% ng iba pang mga detalye ay mas maikli at mas simple:
Dagdag pa, ang pagtutukoy na ito ay isang hanay ng mga panuntunan. Ito ay karaniwang tanda ng hindi magandang detalye. Ang pag-unawa sa mga kahihinatnan ng isang hanay ng mga panuntunan ay medyo mahirap, kung kaya't kailangan kong gumugol ng maraming oras sa pag-debug sa mga ito. Gayunpaman, sa kasong ito ay hindi ako makahanap ng mas mahusay na paraan.
Ito ay nagkakahalaga ng pagsasabi ng ilang mga salita tungkol sa mga programa na patuloy na tumatakbo. Karaniwang gumagana ang mga ito nang magkatulad, tulad ng mga operating system o mga distributed system. Napakakaunting mga tao ang nakakaunawa sa kanila sa kanilang isip o sa papel, at hindi ako isa sa kanila, kahit na minsan ay nagawa ko ito. Samakatuwid, kailangan namin ng mga tool na susuri sa aming trabaho - halimbawa, TLA+ o PlusCal.
Bakit kailangan kong magsulat ng isang detalye kung alam ko na kung ano ang dapat gawin ng code? Sa totoo lang, akala ko lang alam ko na. Bilang karagdagan, sa isang detalye sa lugar, ang isang tagalabas ay hindi na kailangang tingnan ang code upang maunawaan kung ano ang eksaktong ginagawa nito. Mayroon akong panuntunan: dapat walang pangkalahatang tuntunin. Siyempre, may pagbubukod sa panuntunang ito, ito lang ang pangkalahatang tuntunin na sinusunod ko: ang detalye ng kung ano ang ginagawa ng code ay dapat sabihin sa mga tao ang lahat ng kailangan nilang malaman kapag ginagamit ang code na iyon.
Kaya ano ang eksaktong kailangang malaman ng mga programmer tungkol sa pag-iisip? Upang magsimula, katulad ng para sa lahat: kung hindi ka magsulat, kung gayon tila sa iyo lamang ang iniisip mo. Gayundin, kailangan mong mag-isip bago ka mag-code, na nangangahulugang kailangan mong magsulat bago ka mag-code. Ang isang pagtutukoy ay kung ano ang isinusulat natin bago tayo magsimulang mag-coding. Ang isang detalye ay kailangan para sa anumang code na maaaring gamitin o baguhin ng sinuman. At ang "isang tao" na ito ay maaaring lumabas na may-akda ng code isang buwan pagkatapos itong isulat. Ang isang detalye ay kailangan para sa malalaking programa at system, para sa mga klase, para sa mga pamamaraan, at kung minsan kahit para sa mga kumplikadong seksyon ng iisang pamamaraan. Ano ba talaga ang dapat mong isulat tungkol sa code? Kailangan mong ilarawan kung ano ang ginagawa nito, iyon ay, isang bagay na maaaring maging kapaki-pakinabang sa sinumang gumagamit ng code na ito. Minsan maaaring kailanganin ding tukuyin kung paano eksaktong nakakamit ng code ang layunin nito. Kung dumaan kami sa pamamaraang ito sa kurso ng algorithm, pagkatapos ay tinatawag namin itong isang algorithm. Kung ito ay isang bagay na mas dalubhasa at bago, pagkatapos ay tinatawag namin itong mataas na antas na disenyo. Walang pormal na pagkakaiba dito: pareho ang mga abstract na modelo ng programa.
Paano ka dapat magsulat ng isang detalye ng code? Ang pangunahing bagay: ito ay dapat na isang antas na mas mataas kaysa sa code mismo. Dapat itong ilarawan ang mga estado at pag-uugali. Dapat itong maging kasing higpit ng kailangan ng gawain. Kung nagsusulat ka ng isang detalye kung paano ipatupad ang isang gawain, maaari itong isulat sa pseudocode o gamit ang PlusCal. Kailangan mong matutong magsulat ng mga pagtutukoy gamit ang mga pormal na pagtutukoy. Bibigyan ka nito ng mga kinakailangang kasanayan na makakatulong din sa mga impormal. Paano ka matututong sumulat ng mga pormal na detalye? Noong natuto kaming magprograma, nagsulat kami ng mga programa at pagkatapos ay na-debug ang mga ito. Parehong bagay dito: kailangan mong magsulat ng isang detalye, suriin ito sa isang checker ng modelo, at ayusin ang mga error. Maaaring hindi ang TLA+ ang pinakamahusay na wika para sa isang pormal na detalye, at ang isa pang wika ay malamang na mas angkop para sa iyong mga partikular na pangangailangan. Ang magandang bagay tungkol sa TLA+ ay na ito ay gumagawa ng isang mahusay na trabaho ng pagtuturo ng matematikal na pag-iisip.
Paano i-link ang detalye at code? Paggamit ng mga komentong nag-uugnay sa mga konseptong pangmatematika at pagpapatupad ng mga ito. Kung nagtatrabaho ka sa mga graph, pagkatapos ay sa antas ng programa magkakaroon ka ng mga array ng mga node at array ng mga link. Kaya kailangan mong isulat kung paano eksaktong ipinatupad ang graph ng mga istrukturang ito ng programming.
Dapat tandaan na wala sa itaas ang nalalapat sa proseso ng pagsulat ng code mismo. Kapag sumulat ka ng code, iyon ay, gawin ang ikatlong hakbang, kailangan mo ring mag-isip at mag-isip sa pamamagitan ng programa. Kung ang isang subtask ay naging kumplikado o hindi halata, kailangan mong magsulat ng isang detalye para dito. Ngunit hindi ko pinag-uusapan ang mismong code dito. Maaari kang gumamit ng anumang programming language, anumang pamamaraan, hindi ito tungkol sa kanila. Gayundin, wala sa itaas ang nag-aalis ng pangangailangang subukan at i-debug ang iyong code. Kahit na naisulat nang tama ang abstract na modelo, maaaring may mga bug sa pagpapatupad nito.
Ang mga pagtutukoy sa pagsulat ay isang karagdagang hakbang sa proseso ng coding. Salamat dito, maraming mga error ang maaaring makuha sa mas kaunting pagsisikap - alam namin ito mula sa karanasan ng mga programmer mula sa Amazon. Sa mga pagtutukoy, ang kalidad ng mga programa ay nagiging mas mataas. Kaya bakit madalas tayong pumunta nang wala sila? Dahil mahirap magsulat. Ngunit ang pagsusulat ay mahirap, dahil para dito kailangan mong mag-isip, at ang pag-iisip ay mahirap din. Laging mas madaling magpanggap na nag-iisip ka. Dito maaari kang gumuhit ng pagkakatulad sa pagtakbo - kung gaano ka kaunting tumatakbo, mas mabagal ang iyong pagtakbo. Kailangan mong sanayin ang iyong mga kalamnan at magsanay sa pagsusulat. Kailangan ng practice.
Maaaring mali ang pagtutukoy. Maaaring nagkamali ka sa isang lugar, o maaaring nagbago ang mga kinakailangan, o maaaring kailanganin ang isang pagpapabuti. Ang anumang code na ginagamit ng sinuman ay kailangang baguhin, kaya sa lalong madaling panahon ang detalye ay hindi na tutugma sa programa. Sa isip, sa kasong ito, kailangan mong magsulat ng isang bagong detalye at ganap na muling isulat ang code. Alam na alam namin na walang gumagawa nito. Sa pagsasagawa, tina-patch namin ang code at marahil ay ina-update ang detalye. Kung ito ay tiyak na mangyayari sa lalong madaling panahon o huli, kung gayon bakit sumulat ng mga pagtutukoy? Una, para sa taong mag-e-edit ng iyong code, ang bawat dagdag na salita sa detalye ay magiging sulit sa ginto, at maaaring ikaw ang taong ito. Madalas kong sinisipa ang aking sarili dahil sa hindi sapat na tiyak kapag na-edit ko ang aking code. At nagsusulat ako ng higit pang mga pagtutukoy kaysa sa code. Samakatuwid, kapag na-edit mo ang code, palaging kailangang ma-update ang detalye. Pangalawa, sa bawat pag-edit ay lumalala ang code, nagiging mas mahirap basahin at panatilihin. Ito ay isang pagtaas sa entropy. Ngunit kung hindi ka magsisimula sa isang detalye, ang bawat linya na iyong isusulat ay magiging isang pag-edit, at ang code ay magiging napakalaki at mahirap basahin mula sa simula.
Gaya ng sinabi , walang laban ang napanalunan ayon sa plano, at walang laban ang napanalunan nang walang plano. At may alam siya tungkol sa mga laban. May isang opinyon na ang pagsusulat ng mga detalye ay isang pag-aaksaya ng oras. Minsan ito ay totoo, at ang gawain ay napakasimple na walang saysay na pag-isipan ito nang mabuti. Ngunit dapat mong laging tandaan na kapag pinayuhan kang huwag magsulat ng mga detalye, nangangahulugan ito na pinapayuhan kang huwag mag-isip. At dapat mong isipin ito sa bawat oras. Ang pag-iisip sa isang gawain ay hindi ginagarantiyahan na hindi ka magkakamali. Tulad ng alam natin, walang nag-imbento ng magic wand, at ang programming ay isang mahirap na gawain. Ngunit kung hindi mo pag-isipang mabuti ang gawain, garantisadong magkakamali ka.
Maaari kang magbasa nang higit pa tungkol sa TLA+ at PlusCal sa isang espesyal na website, maaari kang pumunta doon mula sa aking home page . Sa akin lang yan, salamat sa atensyon mo.
Mangyaring tandaan na ito ay isang pagsasalin. Kapag nagsusulat ka ng mga komento, tandaan na hindi ito babasahin ng may-akda. Kung gusto mo talagang makipag-chat sa may-akda, pupunta siya sa kumperensya ng Hydra 2019, na gaganapin sa Hulyo 11-12, 2019 sa St. Petersburg. Maaaring mabili ang mga tiket .
Pinagmulan: www.habr.com