Kini nga artikulo usa ka hubad . Apan sa wala pa ang iyang gamay nga pasiuna. Giunsa pagporma ang mga zombie? Ang tanan nakasulod sa usa ka sitwasyon diin gusto nila nga ibira ang usa ka higala o kauban sa ilang lebel, apan wala kini molampos. Ug kini dili kaayo uban kanimo sama sa uban kaniya nga "kini dili molihok": sa usa ka bahin sa sukdanan mao ang usa ka normal nga suweldo, mga buluhaton, ug uban pa, ug sa pikas nga bahin, ang panginahanglan sa paghunahuna. Ang paghunahuna dili maayo ug sakit. Siya dali nga mihunong ug nagpadayon sa pagsulat sa code nga wala gayoy sa iyang utok. Imong mahanduraw kon unsa ka dako nga paningkamot ang gikinahanglan aron mabuntog ang babag sa pagkat-on nga pagkawalay mahimo, ug wala nimo kini buhata. Ingon niini ang pagkaporma sa mga zombie, nga, ingon, mahimo’g ayohon, apan ingon og wala’y makahimo niini.
Pagkakita nako ana (oo, parehas nga kauban gikan sa mga libro) ug dili mohimo og report, apan usa ka pangutana-ug-tubag nga sesyon, medyo nagbantay ko. Sa kaso lang, si Leslie usa ka bantog nga siyentipiko sa kalibutan, ang tagsulat sa sukaranan nga mga buhat sa giapod-apod nga kompyuter, ug mahimo usab nimo siya mailhan pinaagi sa mga letra nga La sa pulong nga LaTeX - "Lamport TeX". Ang ikaduha nga makapaalarma nga hinungdan mao ang iyang kinahanglanon: ang matag usa nga moabut kinahanglan (hingpit nga wala’y bayad) maminaw sa usa ka pares sa iyang mga taho nga abante, maghimo usa ka pangutana bahin niini, ug pagkahuman moabut. Nakahukom ko nga tan-awon kung unsa ang gisibya ni Lamport didto - ug kini maayo! Mao gyud kana nga butang, ang magic link-pill sa pag-ayo sa mga zombie. Gipasidan-an ko ikaw: gikan sa teksto, ang mga mahigugmaon sa super-flexible nga mga pamaagi ug kadtong dili gusto nga sulayan kung unsa ang gisulat mahimo’g masunog.
Human sa habrokat, sa pagkatinuod, ang paghubad sa seminar nagsugod. Malingaw sa pagbasa!
Bisan unsa nga buluhaton ang imong buhaton, kinahanglan nimo kanunay nga moagi sa tulo ka mga lakang:
- paghukom unsa nga tumong ang gusto nimong makab-ot;
- pagdesisyon kon unsaon nimo pagkab-ot ang imong tumong;
- umabot sa imong tumong.
Kini magamit usab sa programming. Kung nagsulat kami og code, kinahanglan namon:
- pagdesisyon kung unsa ang kinahanglan buhaton sa programa;
- pagtino kon unsaon kini paghimo sa iyang buluhaton;
- isulat ang katugbang nga code.
Ang katapusang lakang, siyempre, hinungdanon kaayo, apan dili nako kini hisgutan karon. Hinunoa, atong hisgotan ang unang duha. Ang matag programmer naghimo niini sa wala pa magsugod sa pagtrabaho. Dili ka molingkod aron magsulat gawas kung nakahukom ka kung nagsulat ka usa ka browser o database. Kinahanglang anaa ang usa ka ideya sa tumong. Ug siguradong maghunahuna ka kung unsa gyud ang buhaton sa programa, ug ayaw pagsulat bisan unsang paagiha sa paglaum nga ang code mahimong usa ka browser.
Sa unsa nga paagi nga kini nga code pre-paghunahuna mahitabo? Unsa ka dako ang atong paningkamotan niini? Kini tanan nagdepende kung unsa ka komplikado ang problema nga atong gisulbad. Ibutang ta nga gusto namong magsulat og usa ka fault-tolerant distributed system. Niini nga kaso, kinahanglan natong hunahunaon pag-ayo ang mga butang sa dili pa kita molingkod sa code. Unsa kaha kung kinahanglan naton nga dugangan ang usa ka variable nga integer sa 1? Sa una nga pagtan-aw, ang tanan gamay ra dinhi, ug wala’y kinahanglan nga hunahunaon, apan pagkahuman nahinumduman namon nga mahimo’g mahitabo ang pag-awas. Busa, bisan aron masabtan kung ang usa ka problema yano o komplikado, kinahanglan nimo nga hunahunaon una.
Kung maghunahuna ka bahin sa posible nga mga solusyon sa problema nga abante, malikayan nimo ang mga sayup. Apan kini nagkinahanglan nga ang imong panghunahuna tin-aw. Aron makab-ot kini, kinahanglan nimo nga isulat ang imong mga hunahuna. Ganahan kaayo ko sa kinutlo ni Dick Guindon: "Kung nagsulat ka, gipakita sa kinaiyahan kung unsa ka palpak ang imong panghunahuna." Kung dili ka magsulat, naghunahuna ka lang nga naghunahuna ka. Ug kinahanglan nimo nga isulat ang imong mga hunahuna sa porma sa mga detalye.
Ang mga detalye naghimo sa daghang mga gimbuhaton, labi na sa dagkong mga proyekto. Apan hisgotan lang nako ang usa niini: makatabang kini kanato nga makahunahuna og maayo. Ang paghunahuna nga tin-aw hinungdanon kaayo ug medyo lisud, busa dinhi kinahanglan namon ang bisan unsang tabang. Unsa nga pinulongan ang kinahanglan natong isulat sa mga detalye? Sa kinatibuk-an, kini kanunay ang una nga pangutana alang sa mga programmer: unsa nga pinulongan ang atong isulat. Walay usa nga husto nga tubag niini: ang mga problema nga atong gisulbad kay lainlain kaayo. Alang sa pipila, ang TLA+ usa ka espesipikong lengguwahe nga akong naugmad. Alang sa uban, mas sayon ang paggamit sa Intsik. Ang tanan nagdepende sa sitwasyon.
Ang mas importante mao ang laing pangutana: unsaon pagkab-ot sa mas klaro nga panghunahuna? Tubag: Kinahanglan nga kita maghunahuna sama sa mga siyentista. Kini usa ka paagi sa paghunahuna nga napamatud-an ang kaugalingon sa miaging 500 ka tuig. Sa siyensya, nagtukod kami mga modelo sa matematika sa realidad. Ang astronomiya mao tingali ang unang siyensiya sa estrikto nga diwa sa pulong. Sa matematika nga modelo nga gigamit sa astronomiya, ang mga celestial nga lawas makita nga mga punto nga adunay masa, posisyon ug momentum, bisan kung sa tinuud kini labi ka komplikado nga mga butang nga adunay mga bukid ug kadagatan, pagtaob ug pagtaob. Kini nga modelo, sama sa uban, gimugna aron masulbad ang pipila ka mga problema. Kini maayo alang sa pagtino kung asa itudlo ang teleskopyo kung kinahanglan nimo pangitaon ang usa ka planeta. Apan kung gusto nimo nga matagna ang panahon sa kini nga planeta, kini nga modelo dili molihok.
Ang matematika nagtugot kanato sa pagtino sa mga kabtangan sa modelo. Ug gipakita sa siyensya kung giunsa kini nga mga kabtangan nalangkit sa kamatuoran. Maghisgot ta bahin sa atong siyensya, siyensya sa kompyuter. Ang reyalidad nga among gigamit mao ang mga sistema sa pag-compute sa lain-laing mga matang: mga processor, mga game console, mga kompyuter, mga programa sa pagpatuman, ug uban pa. Maghisgot ako bahin sa pagpadagan sa usa ka programa sa usa ka kompyuter, apan sa kadaghanan, kining tanan nga mga konklusyon magamit sa bisan unsang sistema sa kompyuter. Sa among siyensya, migamit kami ug daghang lain-laing mga modelo: ang Turing machine, partially ordered sets of events, ug daghan pang uban.
Unsa ang usa ka programa? Kini mao ang bisan unsa nga code nga mahimong giisip nga independente. Ibutang ta nga kita kinahanglan nga magsulat sa usa ka browser. Naghimo kami og tulo ka mga buluhaton: among gidesinyo ang panglantaw sa user sa programa, dayon among isulat ang taas nga lebel nga diagram sa programa, ug sa katapusan among gisulat ang code. Sa among pagsulat sa code, among naamgohan nga kinahanglan namong magsulat og text formatter. Dinhi kinahanglan na usab natong sulbaron ang tulo ka mga problema: pagtino kon unsa nga teksto ang ibalik niini nga himan; pagpili og algorithm alang sa pag-format; pagsulat code. Kini nga buluhaton adunay kaugalingon nga subtask: husto nga pagsulud sa hyphen sa mga pulong. Gisulbad usab namo kini nga subtask sa tulo ka mga lakang - sama sa imong makita, kini gisubli sa daghang lebel.
Atong tagdon sa mas detalyado ang unang lakang: unsa nga problema ang masulbad sa programa. Dinhi, kasagaran namong gimodelo ang usa ka programa isip usa ka function nga nagkinahanglan og pipila ka input ug nagpatunghag pipila ka output. Sa matematika, ang usa ka function sagad gihulagway nga usa ka han-ay nga hugpong sa mga pares. Pananglitan, ang function sa kuwadrado alang sa natural nga mga numero gihulagway nga set {<0,0>, <1,1>, <2,4>, <3,9>, …}. Ang dominyo sa ingon nga function mao ang set sa unang mga elemento sa matag pares, nga mao, ang natural nga mga numero. Aron mahibal-an ang usa ka function, kinahanglan naton ipiho ang sakup ug pormula niini.
Apan ang mga function sa matematika dili parehas sa mga function sa programming language. Ang math mas sayon. Tungod kay wala ako'y panahon alang sa komplikadong mga pananglitan, atong tagdon ang usa ka yano: usa ka function sa C o usa ka static nga pamaagi sa Java nga nagbalik sa pinakadako nga komon nga divisor sa duha ka integer. Sa espesipikasyon niini nga pamaagi, atong isulat: kalkulado GCD(M,N) alang sa mga argumento M и Ndiin GCD(M,N) - usa ka function kansang domain mao ang set sa mga pares sa mga integer, ug ang pagbalik nga kantidad mao ang pinakadako nga integer nga mabahin sa M и N. Sa unsang paagi kini nga modelo nalangkit sa kamatuoran? Ang modelo naglihok sa mga integer, samtang sa C o Java kita adunay 32-bit int. Kini nga modelo nagtugot kanato sa paghukom kon ang algorithm husto GCD, apan dili kini makapugong sa mga kasaypanan sa pag-awas. Nagkinahanglan kini og mas komplikado nga modelo, nga walay panahon.
Atong hisgutan ang mga limitasyon sa usa ka function isip usa ka modelo. Ang ubang mga programa (sama sa mga operating system) dili lang magbalik sa usa ka piho nga kantidad alang sa pipila nga mga argumento, mahimo kini nga magpadayon. Dugang pa, ang function isip usa ka modelo dili maayo alang sa ikaduhang lakang: pagplano unsaon pagsulbad ang problema. Ang dali nga pag-sort ug bubble sort nag-compute sa parehas nga function, apan lahi sila nga mga algorithm. Busa, aron ihulagway kung giunsa pagkab-ot ang katuyoan sa programa, naggamit ako usa ka lahi nga modelo, tawgon naton kini nga sumbanan nga modelo sa pamatasan. Ang programa niini girepresentahan ingon usa ka hugpong sa tanan nga gitugotan nga mga pamatasan, nga ang matag usa, sa baylo, usa ka han-ay sa mga estado, ug ang estado mao ang pagtudlo sa mga kantidad sa mga variable.
Atong tan-awon kung unsa ang hitsura sa ikaduhang lakang alang sa Euclid algorithm. Kinahanglan natong kuwentahon GCD(M, N). Nag-initialize mi M sa unsa nga paagi xug N sa unsa nga paagi y, unya balik-balik nga ibawas ang mas gamay niini nga mga variable gikan sa mas dako hangtud nga sila managsama. Pananglitan, kon M = 12ug N = 18, mahimo natong ihulagway ang mosunod nga kinaiya:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
Ug kon M = 0 и N = 0? Ang zero mabahin sa tanan nga mga numero, mao nga walay pinakadako nga divisor niini nga kaso. Niini nga sitwasyon, kinahanglan natong balikan ang unang lakang ug pangutan-on: kinahanglan ba gyud natong kuwentahon ang GCD alang sa dili positibo nga mga numero? Kung dili kini kinahanglan, nan kinahanglan nimo nga usbon ang detalye.
Dinhi kinahanglan nga maghimo kita usa ka gamay nga pagbag-o bahin sa pagka-produktibo. Kanunay kini gisukod sa gidaghanon sa mga linya sa code nga gisulat kada adlaw. Apan ang imong trabaho labi ka mapuslanon kung imong makuha ang usa ka piho nga gidaghanon sa mga linya, tungod kay gamay ra ang imong lugar alang sa mga bug. Ug ang pinakasayon nga paagi sa pagtangtang sa code mao ang una nga lakang. Posible nga dili nimo kinahanglan ang tanan nga mga kampana ug mga whistles nga imong gisulayan nga ipatuman. Ang labing paspas nga paagi sa pagpayano sa usa ka programa ug pagdaginot sa oras mao ang dili pagbuhat sa mga butang nga dili angay buhaton. Ang ikaduhang lakang mao ang ikaduha nga labing makadaginot sa panahon nga potensyal. Kung imong sukdon ang pagka-produktibo sa mga termino sa mga linya nga gisulat, unya ang paghunahuna kung giunsa nimo matuman ang usa ka buluhaton makahimo kanimo dili kaayo produktibo, tungod kay masulbad nimo ang parehas nga problema nga adunay gamay nga code. Dili ko makahatag og eksaktong estadistika dinhi, tungod kay wala akoy paagi sa pag-ihap sa gidaghanon sa mga linya nga wala nako isulat tungod sa kamatuoran nga migahin ako og panahon sa espesipikasyon, nga mao, sa una ug ikaduha nga mga lakang. Ug ang eksperimento dili usab mahimo dinhi, tungod kay sa eksperimento wala kami katungod sa pagkompleto sa unang lakang, ang buluhaton gitakda nang daan.
Sayon nga makalimtan ang daghang mga kalisud sa dili pormal nga mga detalye. Wala’y lisud sa pagsulat sa estrikto nga mga detalye alang sa mga gimbuhaton, dili nako kini hisgutan. Hinuon, maghisgot kami bahin sa pagsulat sa lig-on nga mga detalye alang sa naandan nga pamatasan. Adunay usa ka teorama nga nag-ingon nga ang bisan unsang hugpong sa mga pamatasan mahimong ihulagway gamit ang kabtangan sa seguridad (kaluwasan) ug survivability properties (kabuhi). Ang seguridad nagpasabot nga walay daotang mahitabo, ang programa dili mohatag ug sayop nga tubag. Ang pagkaluwas nagpasabot nga sa madugay o sa madali adunay maayo nga mahitabo, i.e. ang programa mohatag sa saktong tubag sa madugay o sa madali. Ingon sa usa ka lagda, ang seguridad usa ka mas hinungdanon nga timailhan, ang mga sayup nga kasagaran mahitabo dinhi. Busa, aron makadaginot sa oras, dili ako maghisgot bahin sa pagkaluwas, bisan kung kini, siyempre, hinungdanon usab.
Nakab-ot namon ang seguridad pinaagi sa pagreseta, una, ang set sa posible nga mga inisyal nga estado. Ug ikaduha, ang mga relasyon sa tanan nga posible nga sunod nga estado alang sa matag estado. Magbuhat kita sama sa mga siyentista ug maghubit sa mga estado sa matematika. Ang hugpong sa mga inisyal nga estado gihulagway sa usa ka pormula, pananglitan, sa kaso sa Euclid algorithm: (x = M) ∧ (y = N). Alang sa piho nga mga kantidad M и N adunay usa lamang ka inisyal nga estado. Ang relasyon sa sunod nga estado gihulagway pinaagi sa usa ka pormula diin ang mga variable sa sunod nga estado gisulat sa usa ka prime, ug ang mga variable sa kasamtangan nga estado gisulat nga walay prime. Sa kaso sa Euclid's algorithm, atong atubangon ang disjunction sa duha ka pormula, diin ang usa niini. x mao ang pinakadako nga kantidad, ug sa ikaduha - y:
Sa unang kaso, ang bag-ong bili sa y katumbas sa kanhi nga bili sa y, ug atong makuha ang bag-ong bili sa x pinaagi sa pagkub-ot sa mas gamay nga variable gikan sa mas dako nga variable. Sa ikaduha nga kaso, atong buhaton ang kaatbang.
Balikan nato ang algorithm ni Euclid. Atong isipon pag-usab kana M = 12, N = 18. Kini naghubit sa usa ka inisyal nga kahimtang, (x = 12) ∧ (y = 18). Dayon among i-plug ang mga kantidad sa pormula sa ibabaw ug makuha:
Ania ang bugtong posible nga solusyon: x' = 18 - 12 ∧ y' = 12ug atong makuha ang kinaiya: [x = 12, y = 18]. Sa susama, mahimo natong ihulagway ang tanang estado sa atong kinaiya: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
Sa katapusang estado [x = 6, y = 6] ang duha ka bahin sa ekspresyon mahimong bakak, mao nga kini walay sunod nga kahimtang. Busa, kami adunay usa ka kompleto nga detalye sa ikaduhang lakang - ingon sa imong makita, kini mao ang medyo ordinaryo nga matematika, sama sa mga inhenyero ug mga siyentipiko, ug dili talagsaon, sama sa computer science.
Kining duha ka mga pormula mahimong ihiusa ngadto sa usa ka pormula sa temporal nga lohika. Siya elegante ug dali ipasabut, apan wala nay panahon alang kaniya karon. Mahimong kinahanglan naton ang temporal nga lohika alang lamang sa kabuhi nga kabtangan, wala kini kinahanglan alang sa seguridad. Dili ko ganahan sa temporal nga lohika nga ingon niana, dili kini ordinaryo nga matematika, apan sa kaso sa kadasig kini usa ka kinahanglanon nga daotan.
Sa algorithm ni Euclid, alang sa matag kantidad x и y adunay talagsaon nga mga mithi x' и y', nga naghimo sa relasyon sa sunod nga estado nga tinuod. Sa laing pagkasulti, ang algorithm ni Euclid kay deterministiko. Sa pagmodelo sa usa ka non-deterministic nga algorithm, ang kasamtangan nga estado kinahanglan nga adunay daghang posible nga umaabot nga mga estado, ug nga ang matag unprimed variable value adunay daghang primed variable values nga ang relasyon sa sunod nga estado tinuod. Kini sayon buhaton, apan dili na ako mohatag og mga pananglitan karon.
Aron makahimo usa ka himan sa pagtrabaho, kinahanglan nimo ang pormal nga matematika. Unsaon paghimo nga pormal ang espesipikasyon? Aron mahimo kini, kinahanglan namon ang usa ka pormal nga pinulongan, pananglitan, . Ang espesipikasyon sa Euclid algorithm motan-aw niini sa niini nga pinulongan:
Ang parehas nga simbolo nga simbolo nga adunay triyanggulo nagpasabut nga ang kantidad sa wala sa timaan gihubit nga parehas sa kantidad sa tuo sa timaan. Sa esensya, ang detalye usa ka kahulugan, sa among kaso duha ka kahulugan. Sa espesipikasyon sa TLA+, kinahanglan nimong idugang ang mga deklarasyon ug pipila ka syntax, sama sa slide sa ibabaw. Sa ASCII kini tan-awon sama niini:
Sama sa imong nakita, wala’y komplikado. Ang espesipikasyon para sa TLA+ mahimong masulayan, ie bypass ang tanang posibleng gawi sa gamay nga modelo. Sa among kaso, kini nga modelo mahimong piho nga mga kantidad M и N. Kini usa ka episyente ug yano nga pamaagi sa pag-verify nga hingpit nga awtomatiko. Posible usab nga magsulat og pormal nga mga pruweba sa kamatuoran ug susihon kini sa mekanikal nga paagi, apan nagkinahanglan kini og daghang panahon, mao nga halos walay usa nga makahimo niini.
Ang nag-unang disbentaha sa TLA + mao nga kini math, ug ang mga programmer ug computer scientist nahadlok sa matematika. Sa una nga pagtan-aw, kini ingon usa ka komedya, apan, sa kasubo, gipasabut nako kini sa tanan nga kaseryoso. Gisultihan lang ako sa akong kauban kung giunsa niya pagsulay sa pagpatin-aw sa TLA + sa daghang mga developer. Sa diha nga ang mga pormula nagpakita sa screen, kini diha-diha dayon nahimo nga salamin nga mga mata. Busa kung ang TLA+ makahadlok kanimo, mahimo nimong gamiton , kini usa ka dulaan nga programming language. Ang usa ka ekspresyon sa PlusCal mahimong bisan unsang TLA+ nga ekspresyon, nga mao, sa kinatibuk-an, bisan unsang mathematical nga ekspresyon. Dugang pa, ang PlusCal adunay syntax alang sa mga non-deterministic nga mga algorithm. Tungod kay ang PlusCal makasulat ug bisan unsang TLA+ nga ekspresyon, ang PlusCal mas makapahayag kay sa bisan unsang tinuod nga programming language. Sunod, ang PlusCal gihugpong sa usa ka dali mabasa nga detalye sa TLA+. Wala kini magpasabut, siyempre, nga ang komplikado nga detalye sa PlusCal mahimong usa ka yano sa TLA + - klaro ra ang mga sulat tali kanila, wala’y dugang nga pagkakomplikado. Sa katapusan, kini nga detalye mahimong mapamatud-an pinaagi sa TLA + nga mga himan. Sa kinatibuk-an, ang PlusCal makatabang sa pagbuntog sa math phobia ug sayon sabton bisan sa mga programmer ug computer scientist. Kaniadto, gipatik nako ang mga algorithm niini sa pipila ka panahon (mga 10 ka tuig).
Tingali adunay mosupak nga ang TLA + ug PlusCal mga matematika, ug ang matematika nagtrabaho lamang sa mga naimbento nga mga pananglitan. Sa praktis, kinahanglan nimo ang usa ka tinuod nga pinulongan nga adunay mga tipo, pamaagi, mga butang, ug uban pa. Sayop kini. Ania ang gisulat ni Chris Newcomb, nga nagtrabaho sa Amazon: "Gigamit namon ang TLA + sa napulo ka dagkong mga proyekto, ug sa matag kaso, ang paggamit niini nakahatag usa ka hinungdanon nga kalainan sa pag-uswag tungod kay nakuha namon ang mga peligro nga mga bug sa wala pa kami naigo sa produksiyon, ug tungod kay naghatag kini kanamo nga panan-aw ug pagsalig nga kinahanglan namon. paghimo agresibo nga pag-optimize sa pasundayag nga wala makaapekto sa kamatuoran sa programa". Kanunay nimong madungog nga kung mogamit mga pormal nga pamaagi, nakakuha kami dili epektibo nga code - sa praktis, ang tanan sukwahi gyud. Dugang pa, adunay usa ka opinyon nga ang mga manedyer dili makombinsir sa panginahanglan alang sa pormal nga mga pamaagi, bisan kung ang mga programmer kombinsido sa ilang kapuslanan. Ug si Newcomb misulat: "Ang mga manedyer karon nagduso pag-ayo sa pagsulat sa mga detalye alang sa TLA +, ug espesipikong naggahin ug panahon alang niini". Mao nga kung nakita sa mga managers nga nagtrabaho ang TLA +, nalipay sila nga dawaton kini. Gisulat kini ni Chris Newcomb mga unom ka bulan ang milabay (Oktubre 2014), apan karon, sa akong nahibal-an, ang TLA + gigamit sa 14 nga mga proyekto, dili 10. Ang laing pananglitan mao ang disenyo sa XBox 360. Usa ka intern miadto kang Charles Thacker ug gisulat ang espesipikasyon alang sa sistema sa panumduman. Salamat sa kini nga detalye, nakit-an ang usa ka bug nga dili mamatikdan, ug tungod niini ang matag XBox 360 mahagsa pagkahuman sa upat ka oras nga paggamit. Gikumpirma sa mga inhenyero sa IBM nga ang ilang mga pagsulay dili makit-an kini nga bug.
Mahimo nimong mabasa ang dugang bahin sa TLA + sa Internet, apan karon maghisgot kita bahin sa dili pormal nga mga detalye. Talagsa ra kami kinahanglan nga magsulat sa mga programa nga nagkalkula sa labing gamay nga kasagarang divisor ug uban pa. Mas kanunay namong nagsulat og mga programa sama sa pretty-printer tool nga akong gisulat para sa TLA+. Human sa pinakasimple nga pagproseso, ang TLA + code mahimong sama niini:
Apan sa panig-ingnan sa ibabaw, ang tiggamit lagmit gusto nga ang conjunction ug patas nga mga senyales nga ipahiangay. Mao nga ang husto nga pag-format mahimong ingon niini:
Binagbinagon naton ang isa pa ka halimbawa:
Dinhi, sa sukwahi, ang pag-align sa mga managsama, pagdugang, ug pagpadaghan nga mga timaan sa gigikanan random, busa ang pinakasimple nga pagproseso igo na. Sa kinatibuk-an, wala'y eksaktong depinisyon sa matematika sa husto nga pag-format, tungod kay ang "husto" niini nga kaso nagpasabut nga "unsay gusto sa tiggamit", ug kini dili matino sa matematika.
Mopatim-aw nga kung wala kitay kahulugan sa kamatuoran, nan ang espesipikasyon walay kapuslanan. Apan dili. Tungod kay wala kita kahibalo kung unsa ang angay buhaton sa usa ka programa wala magpasabut nga dili na naton kinahanglan nga hunahunaon kung giunsa kini molihok-sa sukwahi, kinahanglan naton nga hatagan kini labi pa nga paningkamot. Ang detalye labi ka hinungdanon dinhi. Imposible nga mahibal-an ang kamalaumon nga programa alang sa istruktura nga pag-imprenta, apan wala kini magpasabut nga dili gyud naton kini kuhaon, ug ang pagsulat sa code ingon usa ka sapa sa panimuot dili maayo nga butang. Sa katapusan, nagsulat ako usa ka detalye sa unom ka mga lagda nga adunay mga kahulugan sa porma sa mga komento sa usa ka java file. Ania ang usa ka pananglitan sa usa sa mga lagda: a left-comment token is LeftComment aligned with its covering token. Kini nga lagda nahisulat sa, ingnon ta, mathematical English: LeftComment aligned, left-comment и covering token - mga termino nga adunay mga kahulugan. Ingon niini ang paghulagway sa mga mathematician sa matematika: nagsulat sila og mga kahulugan sa mga termino ug, base niini, mga lagda. Ang kaayohan sa maong espesipikasyon mao nga ang unom ka mga lagda mas sayon sabton ug i-debug kay sa 850 ka linya sa code. Kinahanglan kong isulti nga ang pagsulat niini nga mga lagda dili sayon, nagkinahanglan kini og daghang panahon sa pag-debug niini. Ilabi na alang niini nga katuyoan, nagsulat ako usa ka code nga nagtaho kung unsang lagda ang gigamit. Salamat sa kamatuoran nga gisulayan nako kini nga unom ka mga lagda sa daghang mga pananglitan, wala nako kinahanglana nga i-debug ang 850 nga linya sa code, ug ang mga bug dali ra makit-an. Ang Java adunay daghang mga himan alang niini. Kung gisulat pa lang nako ang code, dugay pa unta nako, ug ang pag-format dili maayo nga kalidad.
Ngano nga dili magamit ang usa ka pormal nga detalye? Sa usa ka bahin, ang husto nga pagpatuman dili kaayo hinungdanon dinhi. Ang mga istruktura nga pag-imprenta kinahanglan nga dili makapahimuot sa bisan kinsa, mao nga dili nako kinahanglan nga kini molihok nga husto sa tanan nga katingad-an nga mga sitwasyon. Ang mas importante mao ang kamatuoran nga wala koy igong mga himan. Ang TLA + model checker walay kapuslanan dinhi, mao nga kinahanglan nako nga mano-mano nga isulat ang mga pananglitan.
Ang mga detalye sa ibabaw adunay mga bahin nga komon sa tanan nga mga detalye. Mas taas kini nga lebel kaysa code. Mahimo kining ipatuman sa bisan unsang pinulongan. Ang bisan unsang himan o pamaagi walay kapuslanan sa pagsulat niini. Wala’y kurso sa programming ang makatabang kanimo sa pagsulat niini nga detalye. Ug walay mga himan nga makahimo niini nga espesipikasyon nga dili kinahanglan, gawas kon, siyempre, ikaw nagsulat og usa ka pinulongan nga espesipiko alang sa pagsulat sa structured print nga mga programa sa TLA+. Sa katapusan, kini nga espesipikasyon wala magsulti bisan unsa bahin sa eksakto kung giunsa naton isulat ang code, kini nagpahayag lamang kung unsa kini nga code. Gisulat namon ang detalye aron matabangan kami nga mahunahuna ang problema sa dili pa kami magsugod sa paghunahuna bahin sa code.
Apan kini nga espesipikasyon usab adunay mga bahin nga nagpalahi niini gikan sa ubang mga detalye. Ang 95% sa ubang mga spec mas mubo ug mas simple:
Dugang pa, kini nga espesipikasyon usa ka hugpong sa mga lagda. Ingon sa usa ka lagda, kini usa ka timaan sa dili maayo nga detalye. Ang pagsabut sa mga sangputanan sa usa ka hugpong sa mga lagda lisud kaayo, mao nga kinahanglan kong mogugol og daghang oras sa pag-debug niini. Bisan pa, sa kini nga kaso, wala ako makakita og mas maayo nga paagi.
Angayan nga isulti ang pipila ka mga pulong bahin sa mga programa nga padayon nga nagdagan. Ingon sa usa ka lagda, sila nagtrabaho nga managsama, pananglitan, mga operating system o gipang-apod-apod nga mga sistema. Diyutay ra nga mga tawo ang makasabut kanila sa hunahuna o sa papel, ug dili ako usa kanila, bisan kung nahimo nako kini kaniadto. Busa, kinahanglan namo ang mga himan nga magsusi sa among trabaho - pananglitan, TLA + o PlusCal.
Ngano nga gikinahanglan ang pagsulat sa usa ka detalye kung nahibal-an ko na kung unsa gyud ang kinahanglan buhaton sa code? Sa pagkatinuod, naghunahuna lang ko nga nahibalo ko niini. Dugang pa, nga adunay usa ka detalye, ang usa ka tagagawas dili na kinahanglan nga mosulod sa code aron masabtan kung unsa gyud ang iyang gibuhat. Ako adunay usa ka lagda: kinahanglan nga walay kinatibuk-ang mga lagda. Adunay usa ka eksepsiyon niini nga lagda, siyempre, kini lamang ang kinatibuk-ang lagda nga akong gisunod: ang espesipikasyon kung unsa ang gibuhat sa code kinahanglan isulti sa mga tawo ang tanan nga kinahanglan nilang mahibal-an kung gamiton ang code.
Busa unsa man gyud ang kinahanglan mahibal-an sa mga programmer bahin sa paghunahuna? Alang sa pagsugod, parehas sa tanan: kung dili ka magsulat, nan ingon ra kanimo ang imong gihunahuna. Usab, kinahanglan ka maghunahuna sa dili ka pa mag-code, nga nagpasabut nga kinahanglan nimo nga magsulat sa dili ka pa mag-code. Ang espesipikasyon mao ang atong gisulat sa wala pa kita magsugod sa coding. Kinahanglan ang usa ka espesipikasyon alang sa bisan unsang code nga magamit o usbon ni bisan kinsa. Ug kini nga "usa ka tawo" mahimong ang tagsulat sa code sa iyang kaugalingon usa ka bulan pagkahuman kini gisulat. Ang usa ka espesipikasyon gikinahanglan alang sa dagkong mga programa ug sistema, alang sa mga klase, alang sa mga pamaagi, ug usahay bisan alang sa komplikadong mga seksyon sa usa ka paagi. Unsa man gyud ang angay isulat bahin sa code? Kinahanglan nimo nga ihulagway kung unsa ang gibuhat niini, nga mao, kung unsa ang mahimong mapuslanon sa bisan kinsa nga tawo nga naggamit niini nga code. Usahay kinahanglan usab nga ipiho kung giunsa pagtuman sa code ang katuyoan niini. Kung giagian namon kini nga pamaagi sa dagan sa mga algorithm, nan gitawag namon kini nga usa ka algorithm. Kung kini usa ka butang nga labi ka espesyal ug bag-o, nan gitawag namon kini nga taas nga lebel nga disenyo. Walay pormal nga kalainan dinhi: ang duha usa ka abstract nga modelo sa usa ka programa.
Giunsa nimo pagsulat ang usa ka detalye sa code? Ang nag-unang butang: kini kinahanglan nga usa ka lebel nga mas taas kaysa sa code mismo. Kinahanglang ihulagway niini ang mga estado ug pamatasan. Kini kinahanglan nga ingon ka estrikto sama sa gikinahanglan sa buluhaton. Kung nagsulat ka usa ka detalye kung giunsa ipatuman ang usa ka buluhaton, mahimo nimo kini isulat sa pseudocode o sa PlusCal. Kinahanglan ka nga makakat-on unsaon pagsulat sa mga detalye sa pormal nga mga detalye. Kini maghatag kanimo sa gikinahanglan nga mga kahanas nga makatabang kanimo sa dili pormal nga mga kahanas usab. Giunsa nimo pagkat-on sa pagsulat sa pormal nga mga detalye? Sa dihang nakakat-on kami sa pagprograma, nagsulat kami og mga programa ug dayon gi-debug kini. Parehas ra dinhi: isulat ang spec, susiha kini sa modelo nga tigsusi, ug ayohon ang mga bug. Ang TLA+ mahimong dili ang kinamaayohang pinulongan para sa usa ka pormal nga espesipikasyon, ug ang laing pinulongan lagmit nga mas maayo alang sa imong piho nga mga panginahanglan. Ang bentaha sa TLA + mao nga kini nagtudlo sa matematika nga panghunahuna nga maayo.
Giunsa ang pag-link sa detalye ug code? Sa tabang sa mga komentaryo nga nagsumpay sa mga konsepto sa matematika ug sa ilang pagpatuman. Kung nagtrabaho ka sa mga graph, unya sa lebel sa programa adunay mga arrays sa mga node ug arrays sa mga link. Busa, kinahanglan nimo nga isulat sa eksakto kung giunsa ang graph gipatuman sa kini nga mga istruktura sa programming.
Kinahanglang hinumdoman nga walay bisan usa sa mga nahisgutan ang magamit sa aktuwal nga proseso sa pagsulat sa code. Kung gisulat nimo ang code, nga mao, gihimo nimo ang ikatulo nga lakang, kinahanglan nimo usab nga hunahunaon ug hunahunaon ang programa. Kung ang usa ka subtask nahimo nga komplikado o dili klaro, kinahanglan nimo nga magsulat usa ka detalye alang niini. Apan wala ako maghisgot bahin sa code mismo dinhi. Mahimo nimong gamiton ang bisan unsang programming language, bisan unsang pamaagi, dili kini bahin kanila. Usab, walay bisan usa sa ibabaw ang nagwagtang sa panginahanglan sa pagsulay ug pag-debug sa code. Bisan kung ang abstract nga modelo gisulat sa husto, mahimong adunay mga bug sa pagpatuman niini.
Ang mga detalye sa pagsulat usa ka dugang nga lakang sa proseso sa coding. Salamat niini, daghang mga kasaypanan ang madakpan sa gamay nga paningkamot - nahibal-an namon kini gikan sa kasinatian sa mga programmer gikan sa Amazon. Uban sa mga detalye, ang kalidad sa mga programa mahimong mas taas. Nan, nganong kanunay man ta nga wala sila? Kay lisod ang pagsulat. Ug ang pagsulat lisud, tungod kay alang niini kinahanglan ka maghunahuna, ug ang paghunahuna lisud usab. Kanunay nga mas sayon ang pagpakaaron-ingnon sa imong gihunahuna. Dinhi mahimo ka magdrowing og usa ka analohiya sa pagdagan - kung gamay ang imong pagdagan, labi ka hinay ang imong pagdagan. Kinahanglan nimong bansayon ang imong mga kaunuran ug magpraktis sa pagsulat. Kinahanglan praktis.
Mahimong sayop ang espesipikasyon. Mahimong nasayop ka sa usa ka lugar, o ang mga kinahanglanon mahimo’g nabag-o, o kinahanglan nga himuon ang usa ka pag-uswag. Ang bisan unsang kodigo nga gigamit ni bisan kinsa kinahanglang usbon, busa sa madugay o sa madali ang espesipikasyon dili na motakdo sa programa. Sa tinuud, sa kini nga kaso, kinahanglan nimo nga magsulat usa ka bag-ong detalye ug hingpit nga isulat pag-usab ang code. Nahibal-an kaayo namon nga wala’y naghimo niana. Sa praktis, among gi-patch ang code ug posible nga i-update ang detalye. Kung kini mahitabo sa madugay o sa madali, nan nganong isulat ang mga detalye? Una, alang sa tawo nga mag-edit sa imong code, ang matag dugang nga pulong sa espesipikasyon mahimong takus sa gibug-aton sa bulawan, ug kini nga tawo mahimo’g ikaw mismo. Kanunay nakong gibasol ang akong kaugalingon tungod sa dili igo nga espesipikasyon kung gi-edit nako ang akong code. Ug nagsulat ako labi pa nga mga detalye kaysa code. Busa, kung imong i-edit ang code, ang espesipikasyon kanunay kinahanglan nga bag-ohon. Ikaduha, sa matag pag-usab, ang code nagkagrabe, kini nahimong mas ug mas lisud sa pagbasa ug pagpadayon. Kini usa ka pagtaas sa entropy. Apan kung dili ka magsugod sa usa ka spec, nan ang matag linya nga imong gisulat mahimo’g usa ka pag-edit, ug ang code dili magamit ug lisud basahon gikan sa sinugdanan.
Ingon sa giingon , walay gubat nga nakadaog pinaagi sa plano, ug walay gubat nga nakadaog nga walay plano. Ug nahibal-an niya ang usa o duha bahin sa mga gubat. Adunay usa ka opinyon nga ang pagsulat sa mga detalye usa ka pag-usik sa oras. Usahay kini tinuod, ug ang buluhaton yano kaayo nga wala'y bisan unsa nga hunahunaon niini. Apan kinahanglan nimong hinumdoman kanunay nga kung gisultihan ka nga dili isulat ang mga detalye, giingnan ka nga dili maghunahuna. Ug kinahanglan nimong hunahunaon kini matag higayon. Ang paghunahuna sa buluhaton dili garantiya nga dili ka masayop. Sama sa nahibal-an namon, wala’y nag-imbento sa magic wand, ug ang pagprograma usa ka lisud nga buluhaton. Apan kung dili nimo hunahunaon ang problema, sigurado nga masayop ka.
Mahimo nimong mabasa ang dugang bahin sa TLA + ug PlusCal sa usa ka espesyal nga website, mahimo ka moadto gikan sa akong home page . Kana lang para nako, salamat sa imong pagtagad.
Palihug timan-i nga kini usa ka paghubad. Kung magsulat ka og mga komentaryo, hinumdumi nga dili kini basahon sa tagsulat. Kung gusto gyud nimo nga makig-chat sa tagsulat, nan naa siya sa komperensya sa Hydra 2019, nga ipahigayon sa Hulyo 11-12, 2019 sa St. Mahimong mapalit ang mga tiket .
Source: www.habr.com