Dit is in oersettingsartikel . Mar dêrfoar is der in koarte ynlieding. Hoe wurde zombies foarme? Elkenien hat harsels yn in situaasje fûn wêr't se in freon of kollega op har nivo bringe wolle, mar it slagget net. Boppedat, "it slagget net" net sasear foar dy, mar foar him: oan de iene kant fan de skaal is der in gewoane salaris, taken, ensafuorthinne, en oan de oare is de needsaak om te tinken. Tinken is onaangenaam en pynlik. Hy jout gau op en bliuwt koade skriuwe sûnder syn harsens hielendal te brûken. Jo realisearje hoefolle muoite it kostet om de barriêre fan learde helpleazens te oerwinnen, en jo dogge it gewoan net. Dit is hoe't zombies wurde foarme, dy't lykje mooglik te genêzen, mar it liket derop dat gjinien dit sil dwaan.
Doe't ik dat seach (ja, dyselde freon út 'e learboeken) en jout gjin rapport, mar in fraach-en-antwurd sesje, Ik wie in bytsje warskôge. Krekt foar it gefal, Leslie is in wrâldferneamde wittenskipper, de skriuwer fan seminale wurken yn ferspraat komputer, en jo kinne him ek kenne troch de letters La yn LaTeX - "Lamport TeX". De twadde alarmearjende faktor is syn eask: elkenien dy't komt moat (folslein fergees) fan tefoaren nei in pear fan syn reportaazjes harkje, der op syn minst ien fraach oer komme en dan pas komme. Ik besleat om te sjen wat Lamport dêr útstjoerde - en it is geweldich! Dit is krekt dat ding, in magyske linkpil foar it behanneljen fan zombies. Ik warskôgje jo: de tekst kin dejingen dy't fan super-agile metodologyen hâlde en dy't net graach testje wat se skreaun hawwe serieus ferbaarne.
Nei de habrokat begjint eins de oersetting fan it seminar. Genietsje fan it lêzen!
Hokker taak jo ek nimme, jo moatte altyd trije stappen trochgean:
- beslute hokker doel jo wolle berikke;
- beslute hoe't jo jo doel krekt sille berikke;
- berikke jo doel.
Dat jildt ek foar programmearring. As wy koade skriuwe, moatte wy:
- beslute wat it programma krekt dwaan moat;
- bepale krekt hoe't it syn taak útfiere moat;
- skriuw de passende koade.
De lêste stap is fansels tige wichtich, mar ik sil der hjoed net oer prate. Ynstee dêrfan sille wy de earste twa beprate. Elke programmeur docht se foardat se begjinne te wurkjen. Jo sitte net te skriuwen as jo net besletten hawwe wat jo skriuwe: in browser of in databank. In bepaald idee fan it doel moat oanwêzich wêze. En jo tinke grif oer wat it programma krekt sil dwaan, en skriuw it net samar yn 'e hope dat de koade sels op ien of oare manier in browser sil wurde.
Hoe krekt komt dit pre-tinken fan koade? Hoefolle muoite moatte wy hjir yn stekke? It hinget allegear ôf fan hoe kompleks it probleem wy oplosse. Litte wy sizze dat wy in fouttolerant ferdield systeem wolle skriuwe. Yn dit gefal moatte wy dingen goed neitinke foardat wy sitte te koade. Wat as wy gewoan in heule getal fariabele moatte ferheegje mei 1? Op it earste each is alles hjir triviaal en gjin gedachte nedich, mar dan betinke wy dat der in oerstreaming kin foarkomme. Dêrom, sels om te begripen oft in probleem is ienfâldich of kompleks, moatte jo earst tinke.
As jo foarôf tinke oer mooglike oplossingen foar in probleem, kinne jo flaters foarkomme. Mar dit fereasket dat jo tinken dúdlik is. Om dit te berikken, moatte jo jo gedachten opskriuwe. Ik hâld fan it sitaat fan Dick Guindon: "As jo skriuwe, lit de natuer jo sjen hoe slordig jo tinken is." As jo net skriuwe, tinke jo allinich dat jo tinke. En jo moatte jo gedachten opskriuwe yn 'e foarm fan spesifikaasjes.
Spesifikaasjes tsjinje in protte funksjes, benammen yn grutte projekten. Mar ik sil it mar oer ien hawwe: se helpe ús dúdlik te tinken. Dúdlik tinken is heul wichtich en frij lestich, dus wy hawwe hjir help nedich. Yn hokker taal moatte wy spesifikaasjes skriuwe? Yn 't algemien is dit altyd de earste fraach foar programmeurs: yn hokker taal sille wy skriuwe? D'r is gjin ien goed antwurd: de problemen dy't wy oplosse binne te ferskaat. Foar guon minsken is TLA + nuttich - it is in spesifikaasjetaal dy't ik ûntwikkele. Foar oaren is it handiger om Sineesk te brûken. It hinget allegear ôf fan 'e situaasje.
De wichtiger fraach is: hoe kinne wy helderder tinken berikke? Antwurd: Wy moatte tinke as wittenskippers. Dit is in manier fan tinken dy't de lêste 500 jier goed wurke hat. Yn 'e wittenskip bouwe wy wiskundige modellen fan' e realiteit. Astronomy wie faaks de earste wittenskip yn 'e strikte sin fan it wurd. Yn it wiskundige model dat brûkt wurdt yn de astronomy, komme himellichems foar as punten mei massa, posysje en momentum, hoewol't it yn werklikheid ekstreem komplekse objekten binne mei bergen en oseanen, eb en floed. Dit model, lykas alle oare, waard makke om bepaalde problemen op te lossen. It is geweldich om te bepalen wêr't jo in teleskoop moatte rjochtsje as jo in planeet fine wolle. Mar as jo it waar op dizze planeet wolle foarsizze, sil dit model net wurkje.
Wiskunde lit ús de eigenskippen fan in model bepale. En wittenskip lit sjen hoe't dizze eigenskippen relatearje oan de realiteit. Litte wy prate oer ús wittenskip, kompjûterwittenskip. De realiteit wêrmei wy wurkje is komputersystemen fan in protte ferskillende soarten: processors, spielkonsoles, kompjûters dy't programma's útfiere, ensfh. Ik sil prate oer it útfieren fan in programma op in kompjûter, mar, yn 't algemien, binne al dizze konklúzjes fan tapassing op elk komputersysteem. Yn ús wittenskip brûke wy in protte ferskillende modellen: de Turing-masine, foar in part bestelde sets fan eveneminten, en in protte oaren.
Wat is it programma? Dit is elke koade dy't op himsels kin wurde beskôge. Litte wy sizze dat wy in browser moatte skriuwe. Wy fiere trije taken: ûntwerpe de brûker syn presintaasje fan it programma, dan skriuwe it heech nivo diagram fan it programma, en úteinlik skriuwe de koade. Wylst wy de koade skriuwe, realisearje wy dat wy in tekstopmaak skriuwe moatte. Hjir moatte wy wer trije problemen oplosse: bepale hokker tekst dit ark weromkomt; selektearje in algoritme foar opmaak; skriuw koade. Dizze taak hat in eigen subtaak: koppeltekens korrekt yn wurden ynfoegje. Wy oplosse dizze subtaak ek yn trije stappen - lykas wy sjogge, wurde se op in protte nivo's werhelle.
Lit ús nimme in tichterby de earste stap: wat probleem oplost it programma. Hjir modelje wy meast in programma as in funksje dy't wat ynfier nimt en wat útfier jout. Yn de wiskunde wurdt in funksje meastentiids beskreaun as in oardere set fan pearen. Bygelyks, de kwadraatfunksje foar natuerlike getallen wurdt beskreaun as de set {<0,0>, <1,1>, <2,4>, <3,9>, …}. It domein fan definysje fan sa'n funksje is de set fan 'e earste eleminten fan elk pear, dat is natuerlike getallen. Om in funksje te definiearjen, moatte wy syn domein en formule opjaan.
Mar funksjes yn wiskunde binne net itselde as funksjes yn programmeartalen. De wiskunde is folle ienfâldiger. Om't ik gjin tiid haw foar komplekse foarbylden, litte wy in ienfâldige beskôgje: in funksje yn C of in statyske metoade yn Java dy't de grutste mienskiplike divisor fan twa heule getallen werombringt. Yn 'e spesifikaasje fan dizze metoade sille wy skriuwe: berekkent GCD(M,N) foar arguminten M и Nwêr GCD(M,N) - in funksje wêrfan it domein in set is fan pearen fan heule getallen, en de weromkommende wearde is it grutste heule getal dat wurdt dield troch M и N. Hoe fergelyket de realiteit mei dit model? It model wurket mei heule getallen, en yn C of Java hawwe wy 32-bit int. Dit model lit ús beslute oft it algoritme goed is GCD, mar it sil net foarkomme oerlêst flaters. Dit soe in komplekser model nedich wêze, dêr't gjin tiid foar is.
Litte wy prate oer de beheiningen fan 'e funksje as model. Guon programma's (lykas bestjoeringssystemen) jouwe net allinich in spesifike wearde werom foar bepaalde arguminten; se kinne kontinu rinne. Derneist is de funksje as model min geskikt foar de twadde stap: plannen hoe't jo it probleem oplosse kinne. Quicksort en bubble sort berekkenje deselde funksje, mar se binne folslein ferskillende algoritmen. Dêrom, om de manier te beskriuwen om it doel fan it programma te berikken, brûk ik in oar model, litte wy it it standert gedrachsmodel neame. It programma wurdt dêryn fertsjintwurdige as in set fan alle jildige gedrach, elk dêrfan is op syn beurt in sekwinsje fan steaten, en in steat is de tawizing fan wearden oan fariabelen.
Litte wy sjen hoe't de twadde stap foar it Euklidyske algoritme der útsjen soe. Wy moatte berekkenje GCD(M, N). Wy initialisearje M hoe xen N hoe y, lûk dan de lytste fan dizze fariabelen hieltyd wer ôf fan de gruttere oant se gelyk binne. Bygelyks, as M = 12en N = 18, kinne wy it folgjende gedrach beskriuwe:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
En as M = 0 и N = 0? Nul is te dielen troch alle getallen, dus d'r is gjin grutste divisor yn dit gefal. Yn dizze situaasje moatte wy weromgean nei de earste stap en freegje: moatte wy echt GCD foar net-positive nûmers berekkenje? As dit net nedich is, dan moatte jo gewoan de spesifikaasje feroarje.
In koarte eftergrûn oer produktiviteit is hjir op oarder. It wurdt faak metten yn it oantal rigels koade skreaun per dei. Mar jo wurk is folle brûkberer as jo in bepaald oantal rigels kwytreitsje, om't jo minder romte hawwe foar bugs. En de maklikste manier om koade kwyt te reitsjen is yn 'e earste stap. It is mooglik dat jo gewoan net alle toeters en bellen nedich hawwe dy't jo besykje te ymplementearjen. De rapste manier om in programma te ferienfâldigjen en tiid te besparjen is om dingen net te dwaan dy't net dien wurde moatte. De twadde stap hat it op ien nei heechste potinsjeel foar tiidbesparring. As jo de produktiviteit mjitte yn termen fan skreaune rigels, dan sil jo tinke oer hoe't jo in taak foltôgje minder produktyf, omdat jo kinne oplosse itselde probleem mei minder koade. Ik kin hjir gjin krekte statistiken jaan, om't ik gjin manier haw om it oantal rigels te tellen dy't ik net skreaun haw fanwegen de tiid dy't ik oan 'e spesifikaasje bestege, dat is op' e earste en twadde stap. En in eksperimint kinne wy hjir ek net dwaan, want yn in eksperimint hawwe wy net it rjocht om de earste stap te foltôgjen, de taak is foarôf fêststeld.
It is maklik om in protte swierrichheden te oersjen yn ynformele spesifikaasjes. D'r is neat dreech oer it skriuwen fan strikte spesifikaasjes foar funksjes; Ik sil dit net besprekke. Ynstee dêrfan sille wy prate oer it skriuwen fan sterke spesifikaasjes foar standert gedrach. D'r is in teorem dat stelt dat elke set fan gedrach kin wurde beskreaun mei it feiligenseigenskip (feilichheid) en survivability eigenskippen (libbens). Feiligens betsjut dat der neat slims bart, it programma sil net it ferkearde antwurd jaan. Oerlibberens betsjut dat der ier of let wat goeds barre sil, dus it programma jout ier of let it goede antwurd. As regel is feiligens in wichtiger yndikator; flaters komme hjir meast foar. Dêrom, om tiid te besparjen, sil ik net prate oer survivability, hoewol it, fansels, ek wichtich is.
Wy berikke feiligens troch earst in set fan mooglike begjinsteaten oan te jaan. En twadde, relaasjes mei alle mooglike folgjende steaten foar elke steat. Litte wy ús gedrage as wittenskippers en steaten wiskundich definiearje. De set fan begjinsteaten wurdt beskreaun troch de formule, bygelyks yn it gefal fan it Euklidyske algoritme: (x = M) ∧ (y = N). Foar bepaalde wearden M и N der is mar ien initial steat. De relaasje mei de folgjende steat wurdt beskreaun troch in formule wêryn't de fariabelen fan 'e folgjende steat mei in prime skreaun wurde, en de fariabelen fan' e hjoeddeistige steat wurde skreaun sûnder prime. Yn it gefal fan it Euklidyske algoritme sille wy te krijen hawwe mei de disjunksje fan twa formules, wêrfan ien x is de grutste wearde, en yn 'e twadde - y:
Yn it earste gefal is de nije wearde fan y lyk oan de foarige wearde fan y, en wy krije de nije wearde fan x troch it subtrahearjen fan de lytsere fariabele fan de gruttere. Yn it twadde gefal dogge wy it tsjinoerstelde.
Litte wy weromgean nei it Euklidyske algoritme. Stel dat nochris M = 12, N = 18. Dit definiearret ien inisjele steat, (x = 12) ∧ (y = 18). Wy plug dan dizze wearden yn 'e formule hjirboppe en krije:
Hjir is de ienige mooglike oplossing: x' = 18 - 12 ∧ y' = 12, en wy krije it gedrach: [x = 12, y = 18]. Op deselde wize kinne wy alle steaten yn ús gedrach beskriuwe: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
Yn lêste steat [x = 6, y = 6] beide dielen fan 'e útdrukking sille falsk wêze, dêrom hat it gjin folgjende steat. Dus, wy hawwe in folsleine spesifikaasje fan 'e twadde stap - sa't wy sjogge, dit is gewoan gewoane wiskunde, lykas dy fan yngenieurs en wittenskippers, en net frjemd, lykas yn kompjûterwittenskip.
Dizze twa formules kinne wurde kombinearre yn ien formule fan tydlike logika. It is elegant en maklik te ferklearjen, mar der is no gjin tiid foar. Wy kinne tydlike logika allinich nedich hawwe foar it eigendom fan libbenens; foar feiligens is it net nedich. Ik hâld net fan tydlike logika as sadanich, it is net hielendal gewoane wiskunde, mar yn it gefal fan libbenens is it in needsaaklik kwea.
Yn Euklidyske algoritme foar elke wearde x и y der binne unike wearden x' и y', dy't de relaasje mei de folgjende steat wier meitsje. Mei oare wurden, it Euklidyske algoritme is deterministysk. Om in net-deterministysk algoritme te modellearjen, moat de hjoeddeistige steat meardere mooglike takomstige steaten hawwe, en elke wearde fan 'e unprimed fariabele moat meardere wearden hawwe fan' e prime fariabele, sadat de relaasje mei de folgjende steat wier is. Dit is net dreech om te dwaan, mar ik sil no gjin foarbylden jaan.
Om in wurkjend ark te meitsjen, hawwe jo formele wiskunde nedich. Hoe meitsje in spesifikaasje formeel? Dêrfoar hawwe wy in formele taal nedich, bgl. . De spesifikaasje fan it Euklidyske algoritme yn dizze taal sil der sa útsjen:
It lykweardich tekensymboal mei in trijehoek betsjut dat de wearde oan de lofterkant fan it teken wurdt bepaald om gelyk te wêzen oan de wearde rjochts fan it teken. Yn essinsje is in spesifikaasje in definysje, yn ús gefal twa definysjes. Oan de spesifikaasje yn TLA + moatte jo deklaraasjes en wat syntaksis tafoegje, lykas yn 'e dia hjirboppe. Yn ASCII soe it der sa útsjen:
Sa't jo sjen kinne, neat yngewikkeld. De spesifikaasje op TLA + kin wurde ferifiearre, dat wol sizze, it is mooglik om te omgean alle mooglike gedrach yn in lyts model. Yn ús gefal sil dit model bepaalde wearden wêze M и N. Dit is in heul effektive en ienfâldige ferifikaasjemetoade dy't folslein automatysk is. Dêrnjonken is it mooglik om formele wierheidsbewizen te skriuwen en meganysk te kontrolearjen, mar dit nimt in protte tiid, dus hast gjinien docht dit.
It wichtichste neidiel fan TLA + is dat it wiskunde is, en programmeurs en kompjûterwittenskippers binne bang foar wiskunde. Op it earste each klinkt dit as in grap, mar spitigernôch sis ik dit yn alle earnst. In kollega fan my fertelde my krekt hoe't hy besocht TLA + te ferklearjen oan ferskate ûntwikkelders. Sadree't de formules op it skerm ferskynden, waarden har eagen fuortendaliks glêzen. Dus as TLA + eng is, kinne jo gebrûk meitsje , is in soarte fan boartersguodprogrammearringstaal. In útdrukking yn PlusCal kin elke TLA + útdrukking wêze, dat is yn prinsipe elke wiskundige útdrukking. Derneist hat PlusCal syntaksis foar net-deterministyske algoritmen. Om't PlusCal elke TLA+-ekspresje kin skriuwe, is it signifikant ekspressiverer dan elke echte programmeartaal. Folgjende, PlusCal wurdt gearstald yn in maklik te lêzen TLA + spesifikaasje. Dit betsjut fansels net dat de komplekse PlusCal-spesifikaasje sil feroarje yn in ienfâldige op TLA + - allinich dat de korrespondinsje tusken har dúdlik is, sil gjin ekstra kompleksiteit ferskine. Uteinlik kin dizze spesifikaasje wurde ferifiearre mei TLA + ark. Yn 't algemien kin PlusCal helpe om in foby foar wiskunde te oerwinnen; it is maklik te begripen, sels foar programmeurs en kompjûterwittenskippers. Ik publisearre der in skoft (sawat 10 jier) yn it ferline algoritmen op.
Miskien sil immen beswier meitsje dat TLA + en PlusCal wiskunde binne, en wiskunde wurket allinich mei opmakke foarbylden. Yn 'e praktyk hawwe jo in echte taal nedich mei soarten, prosedueres, objekten, ensfh. Dit is ferkeard. Hjir is wat Chris Newcomb, dy't wurke by Amazon, skriuwt: "Wy hawwe TLA + brûkt op tsien grutte projekten, en yn alle gefallen makke it gebrûk derfan in signifikant ferskil foar ûntwikkeling, om't wy gefaarlike bugs koenen fange foardat se de produksje sloegen, en om't it ús it ynsjoch en it fertrouwen joech dat wy nedich wiene om agressyf te meitsjen prestaasjesoptimalisaasjes sûnder de wierheid fan it programma te beynfloedzjen". Jo kinne faak hearre dat by it brûken fan formele metoaden wy ineffisjinte koade krije - yn 'e praktyk is alles krekt oarsom. Dêrnjonken is der in opfetting dat managers net oertsjûge wurde kinne fan 'e needsaak foar formele metoaden, sels as programmeurs oertsjûge binne fan har nut. En Newcomb skriuwt: "Managers drukke no op alle mooglike manieren om spesifikaasjes yn TLA + te skriuwen, en jouwe hjir spesifyk tiid foar". Dus as managers sjogge dat TLA + wurket, omearmje se it. Chris Newcomb skreau dit sawat seis moanne lyn (oktober 2014), mar no, sa fier as ik wit, wurdt TLA+ brûkt yn 14 projekten, net 10. In oar foarbyld hat te krijen mei it ûntwerp fan de XBox 360. In stazjêre kaam nei Charles Thacker en skreau spesifikaasje foar it ûnthâld systeem. Mei tank oan dizze spesifikaasje waard in brek fûn dy't oars net ûntdutsen wêze soe en soe feroarsaakje dat elke Xbox 360 nei fjouwer oeren gebrûk crashte. Yngenieurs fan IBM befêstige dat har tests dizze brek net soene hawwe ûntdutsen.
Jo kinne mear lêze oer TLA + op it ynternet, mar litte wy no prate oer ynformele spesifikaasjes. Wy moatte selden programma's skriuwe dy't de minste mienskiplike divisor en sa berekkenje. Folle faker skriuwe wy programma's lykas it moaie-printer-ark dat ik skreau foar TLA+. Nei de ienfâldichste ferwurking soe de TLA + koade der sa útsjen:
Mar yn it foarbyld hjirboppe woe de brûker nei alle gedachten dat de konjunksje en gelikense tekens wurde ôfstimd. Dat de juste opmaak soe der mear sa útsjen:
Litte wy in oar foarbyld beskôgje:
Hjir, krekt oarsom, de ôfstimming fan gelikense tekens, tafoeging en fermannichfâldigjen yn 'e boarne wie willekeurich, dus de ienfâldichste ferwurking is genôch. Yn it algemien is d'r gjin krekte wiskundige definysje fan juste opmaak, om't "korrekt" yn dit gefal betsjut "wat de brûker wol", en dit kin net wiskundich bepaald wurde.
It soe lykje dat as wy gjin definysje fan wierheid hawwe, dan is de spesifikaasje nutteloos. Mar dat is net wier. Krekt omdat wy net witte wat in programma moat dwaan, betsjut net dat wy net hoege te tinken oer hoe't it moat wurkje - krekt oarsom, wy moatte besteegje noch mear muoite. De spesifikaasje is hjir foaral wichtich. It is ûnmooglik om it optimale programma foar strukturearre printsjen te bepalen, mar dit betsjut net dat wy it hielendal net moatte ûndernimme, en it skriuwen fan koade as in stream fan bewustwêzen is net it gefal. Ik einige mei it skriuwen fan in spesifikaasje fan seis regels mei definysjes yn 'e foarm fan opmerkings yn in Java-bestân. Hjir is in foarbyld fan ien fan 'e regels: a left-comment token is LeftComment aligned with its covering token. Dizze regel is skreaun yn, lit ús sizze, wiskundige Ingelsk: LeftComment aligned, left-comment и covering token - termen mei definysjes. Sa beskriuwe wiskundigen de wiskunde: se skriuwe definysjes fan termen en meitsje op basis dêrfan regels. It foardiel fan dizze spesifikaasje is dat seis regels folle makliker te begripen en debuggen binne as 850 rigels koade. Ik moat sizze dat it skriuwen fan dizze regels net maklik wie; it duorre in protte tiid om se te debuggen. Ik skreau koade spesifyk foar dit doel dat fertelde my hokker regel waard brûkt. Om't ik dizze seis regels hifke mei in pear foarbylden, hoegde ik 850 rigels koade net te debuggen, en de bugs wiene frij maklik te finen. Java hat geweldige ark foar dit. As ik de koade krekt skreaun hie, hie it my folle langer duorre en soe de opmaak fan mindere kwaliteit west hawwe.
Wêrom koe in formele spesifikaasje net brûkt wurde? Oan de iene kant is de korrekte útfiering hjir net al te wichtich. In strukturearre ôfdruk sil foar guon ûnfoldwaande wêze, dus ik hoegde it net yn alle ûngewoane situaasjes goed te wurkjen. Noch wichtiger is it feit dat ik net genôch ark hie. De TLA + modelkontrôler is hjir nutteloos, dus ik soe de foarbylden mei de hân skriuwe moatte.
De opjûne spesifikaasje hat funksjes mienskiplik foar alle spesifikaasjes. It is heger nivo dan koade. It kin yn elke taal ynfierd wurde. D'r binne gjin ark of metoaden om it te skriuwen. Gjin programmearkursus sil jo helpe om dizze spesifikaasje te skriuwen. En d'r binne gjin ark dy't dizze spesifikaasje ûnnedich meitsje kinne, útsein as jo fansels in taal skriuwe spesifyk foar it skriuwen fan strukturearre printprogramma's yn TLA+. Uteinlik seit dizze spesifikaasje neat oer hoe't wy de koade krekt skriuwe, it stelt gewoan wat de koade docht. Wy skriuwe in spesifikaasje om ús te helpen troch it probleem te tinken foardat wy begjinne te tinken oer de koade.
Mar dizze spesifikaasje hat ek funksjes dy't it ûnderskiede fan oare spesifikaasjes. 95% fan oare spesifikaasjes binne folle koarter en ienfâldiger:
Fierder is dizze spesifikaasje in set regels. Dit is normaal in teken fan in minne spesifikaasje. De gefolgen fan in set regels te begripen is frij lestich, en dêrom moast ik in protte tiid besteegje oan debuggen. Yn dit gefal koe ik lykwols gjin bettere manier fine.
It is it wurdich in pear wurden te sizzen oer programma's dy't kontinu rinne. Typysk wurkje se parallel, lykas bestjoeringssystemen of ferdielde systemen. Hiel pear minsken kinne begripe se yn har tinzen of op papier, en ik bin net ien fan harren, hoewol't ik wie ien kear by steat om te dwaan. Dêrom hawwe wy ark nedich dy't ús wurk sille kontrolearje - bygelyks TLA + of PlusCal.
Wêrom moast ik in spesifikaasje skriuwe as ik al wist wat de koade moat dwaan? Eins tocht ik allinnich dat ik it wist. Derneist, mei in spesifikaasje yn plak, hoecht in bûtensteander net mear yn 'e koade te sjen om te begripen wat it krekt docht. Ik haw in regel: der moatte gjin algemiene regels. D'r is in útsûndering op dizze regel fansels, dit is de ienige algemiene regel dy't ik folgje: de spesifikaasje fan wat de koade docht moat minsken alles fertelle wat se witte moatte by it brûken fan dy koade.
Dus wat krekt moatte programmeurs witte oer tinken? Om te begjinnen itselde as foar elkenien: as jo net skriuwe, dan liket it jo allinich dat jo tinke. Jo moatte ek tinke foardat jo kodearje, wat betsjut dat jo moatte skriuwe foardat jo kodearje. In spesifikaasje is wat wy skriuwe foardat wy begjinne te kodearjen. In spesifikaasje is nedich foar elke koade dy't kin wurde brûkt of feroare troch elkenien. En dizze "ien" kin in moanne nei't it skreaun is de skriuwer fan 'e koade blike te wêzen. In spesifikaasje is nedich foar grutte programma's en systemen, foar klassen, foar metoaden, en soms sels foar komplekse seksjes fan ien metoade. Wat krekt moatte jo skriuwe oer de koade? Jo moatte beskriuwe wat it docht, dat is, eat dat nuttich kin wêze foar elkenien dy't dizze koade brûkt. Soms kin it ek nedich wêze om oan te jaan hoe krekt de koade syn doel berikt. As wy troch dizze metoade gienen yn 'e kursus algoritmen, dan neame wy it in algoritme. As it wat mear spesjalisearre en nij is, dan neame wy it ûntwerp op heech nivo. D'r is hjir gjin formeel ferskil: beide binne abstrakte modellen fan it programma.
Hoe krekt moatte jo in koade spesifikaasje skriuwe? It wichtichste ding: it moat ien nivo heger wêze as de koade sels. It moat steaten en gedrach beskriuwe. It moat sa strang wêze as de taak fereasket. As jo in spesifikaasje skriuwe oer hoe't jo in taak útfiere, dan kin it skreaun wurde yn pseudokoade of mei PlusCal. Jo moatte leare om spesifikaasjes te skriuwen mei formele spesifikaasjes. Dit sil jou jo de nedige feardichheden dy't ek sille helpe mei ynformele. Hoe kinne jo leare formele spesifikaasjes te skriuwen? Doe't wy learden te programmearjen, skreaunen wy programma's en hawwe se dan debuggen. Itselde ding hjir: jo moatte in spesifikaasje skriuwe, kontrolearje it mei in modelkontrôler en reparearje de flaters. TLA + is miskien net de bêste taal foar in formele spesifikaasje, en in oare taal soe wierskynlik better geskikt wêze foar jo spesifike behoeften. It geweldige ding oer TLA + is dat it in geweldige baan docht mei it learen fan wiskundige tinken.
Hoe kinne spesifikaasje en koade keppelje? Gebrûk fan opmerkings dy't wiskundige begripen en har ymplemintaasje keppelje. As jo mei grafiken wurkje, dan sille jo op programmanivo arrays hawwe fan knopen en arrays fan keppelings. Dat jo moatte skriuwe hoe krekt de grafyk wurdt ymplementearre troch dizze programmearstruktueren.
Dêrby moat opmurken wurde dat net ien fan 'e boppesteande jildt foar it proses fan it skriuwen fan koade sels. As jo koade skriuwe, dat is, de tredde stap útfiere, moatte jo ek tinke en tinke troch it programma. As in subtaak kompleks of net fanselssprekkend blykt te wêzen, moatte jo der in spesifikaasje foar skriuwe. Mar ik bin it net oer de koade sels hjir. Jo kinne elke programmeartaal, elke metodyk brûke, dit giet net oer har. Ek net ien fan 'e boppesteande elimineert de needsaak om jo koade te testen en te debuggen. Sels as it abstrakte model goed skreaun is, kinne d'r bugs wêze yn 'e ymplemintaasje.
It skriuwen fan spesifikaasjes is in ekstra stap yn it kodearingsproses. Mei tank oan it kinne in protte flaters wurde fongen mei minder ynspanning - wy witte dit út 'e ûnderfining fan programmeurs fan Amazon. Mei spesifikaasjes wurdt de kwaliteit fan programma's heger. Dus wêrom geane wy dan sa faak sûnder har? Want skriuwen is dreech. Mar skriuwen is dreech, want dêrfoar moatte jo tinke, en tinken is ek lestich. It is altyd makliker om te dwaan as jo tinke. In analogy kin hjir lutsen wurde mei rinnen - hoe minder jo rinne, hoe stadiger jo rinne. Jo moatte jo spieren traine en skriuwen oefenje. It nimt praktyk.
De spesifikaasje kin ferkeard wêze. Jo hawwe miskien earne in flater makke, of de easken binne feroare, of in ferbettering moat makke wurde. Elke koade dy't elkenien brûkt moat feroare wurde, dus ier of letter sil de spesifikaasje net mear oerienkomme mei it programma. Ideaal, yn dit gefal moatte jo in nije spesifikaasje skriuwe en de koade folslein oerskriuwe. Wy witte hiel goed dat nimmen dit docht. Yn 'e praktyk patchje wy de koade en miskien de spesifikaasje bywurkje. As dit is bûn te barren ier of let, wêrom dan skriuwe spesifikaasjes? As earste, foar de persoan dy't jo koade sil bewurkje, sil elk ekstra wurd yn 'e spesifikaasje syn gewicht yn goud wurdich wêze, en dizze persoan kin jo wêze. Ik skop mysels faaks foar net spesifyk genôch as ik myn koade bewurkje. En ik skriuw mear spesifikaasjes as koade. Dêrom, as jo de koade bewurkje, moat de spesifikaasje altyd bywurke wurde. Twad, mei elke bewurking wurdt de koade slimmer, it wurdt dreger om te lêzen en te ûnderhâlden. Dit is in ferheging fan entropy. Mar as jo net begjinne mei in spesifikaasje, dan sil elke rigel dy't jo skriuwe in bewurking wêze, en de koade sil fan it begjin ôf bulk wêze en dreech te lêzen.
Lykas sein , gjin slach waard wûn neffens in plan, en gjin slach waard wûn sûnder in plan. En hy wist wat oer fjildslaggen. D'r is in miening dat it skriuwen fan spesifikaasjes in fergriemerij fan tiid is. Soms is dit wier, en de taak is sa ienfâldich dat it gjin punt hat om it troch te tinken. Mar jo moatte altyd ûnthâlde dat as jo wurde advisearre gjin spesifikaasjes te skriuwen, it betsjut dat jo advisearre wurde net te tinken. En hjir moatte jo elke kear oer tinke. Troch in taak troch te tinken garandearret net dat jo gjin flaters meitsje. Sa't wy witte, gjinien útfûn in toverstok, en programmearring is in drege taak. Mar as jo de taak net trochtinke, sille jo garandearre flaters meitsje.
Jo kinne mear lêze oer TLA+ en PlusCal op in spesjale webside, jo kinne der hinne gean fan myn thússide . Dat is alles foar my, tank foar jo oandacht.
Unthâld dat dit in oersetting is. As jo opmerkings skriuwe, tink dan dat de skriuwer se net sil lêze. As jo echt wolle petearje mei de skriuwer, sil hy wêze by de Hydra 2019-konferinsje, dy't op 11-12 july 2019 yn Sint-Petersburch hâlden wurdt. Kaarten kinne kocht wurde .
Boarne: www.habr.com