Hierdie artikel is 'n vertaling . Maar voor haar 'n klein inleiding. Hoe word zombies gevorm? Almal het in 'n situasie gekom waar hulle 'n vriend of kollega tot hul vlak wil optrek, maar dit werk nie uit nie. En dit is nie soseer by jou as by hom dat “dit nie uitwerk nie” nie: aan die een kant van die skaal is ’n normale salaris, take, ensovoorts, en aan die ander kant die behoefte om te dink. Dink is onaangenaam en pynlik. Hy gee vinnig op en gaan voort om kode te skryf sonder om enigsins sy brein aan te skakel. Jy verbeel jou hoeveel moeite dit verg om die hindernis van aangeleerde hulpeloosheid te oorkom, en jy doen dit net nie. Dit is hoe zombies gevorm word, wat blykbaar genees kan word, maar dit lyk asof niemand dit sal doen nie.
Toe ek dit sien (ja, dieselfde kameraad uit die handboeke) en maak nie 'n verslag nie, maar 'n vraag-en-antwoord-sessie, ek was 'n bietjie versigtig. Net vir ingeval, Leslie is 'n wêreldbekende wetenskaplike, die skrywer van fundamentele werke in verspreide rekenaars, en jy kan hom ook ken aan die letters La in die woord LaTeX - "Lamport TeX". Die tweede kommerwekkende faktor is sy vereiste: almal wat kom moet (absoluut gratis) vooraf na 'n paar van sy verslae luister, met ten minste een vraag daaroor vorendag kom, en dan eers kom. Ek het besluit om te kyk wat Lamport daar uitsaai – en dit is wonderlik! Dit is presies daardie ding, die magiese skakelpil om zombies te genees. Ek waarsku jou: uit die teks kan liefhebbers van super-buigsame metodologieë en diegene wat nie daarvan hou om te toets wat geskryf is nie, veral uitbrand.
Na habrokat begin trouens die vertaling van die seminaar. Lekker lees!
Watter taak jy ook al aanpak, jy moet altyd deur drie stappe gaan:
- besluit watter doel jy wil bereik;
- besluit hoe jy jou doelwit sal bereik;
- kom na jou doel.
Dit geld ook vir programmering. Wanneer ons kode skryf, moet ons:
- besluit wat die program moet doen;
- bepaal hoe dit sy taak moet verrig;
- skryf die ooreenstemmende kode.
Die laaste stap is natuurlik baie belangrik, maar ek sal nie vandag daaroor praat nie. In plaas daarvan sal ons die eerste twee bespreek. Elke programmeerder voer dit uit voordat hy begin werk. Jy gaan nie sit om te skryf tensy jy besluit het of jy 'n blaaier of 'n databasis skryf nie. 'n Sekere idee van die doel moet teenwoordig wees. En jy dink beslis oor wat presies die program sal doen, en skryf nie op een of ander manier in die hoop dat die kode op een of ander manier in 'n blaaier sal verander nie.
Hoe presies gebeur hierdie kodevoordenke? Hoeveel moeite moet ons hierin doen? Dit hang alles af van hoe kompleks die probleem is wat ons oplos. Gestel ons wil 'n fouttolerante verspreide stelsel skryf. In hierdie geval moet ons dinge noukeurig deurdink voordat ons gaan sit om te kodeer. Wat as ons net 'n heelgetalveranderlike met 1 moet verhoog? Met die eerste oogopslag is alles hier onbenullig, en geen gedagte is nodig nie, maar dan onthou ons dat 'n oorloop kan voorkom. Daarom, selfs om te verstaan of 'n probleem eenvoudig of kompleks is, moet jy eers dink.
As jy vooraf dink oor moontlike oplossings vir die probleem, kan jy foute vermy. Maar dit vereis dat jou denke duidelik is. Om dit te bereik, moet jy jou gedagtes neerskryf. Ek hou baie van die Dick Guindon-aanhaling: "Wanneer jy skryf, wys die natuur jou hoe slordig jou denke is." As jy nie skryf nie, dink jy net dat jy dink. En jy moet jou gedagtes in die vorm van spesifikasies neerskryf.
Spesifikasies verrig baie funksies, veral in groot projekte. Maar ek sal net oor een van hulle praat: hulle help ons om helder te dink. Om duidelik te dink is baie belangrik en nogal moeilik, so hier het ons enige hulp nodig. In watter taal moet ons spesifikasies skryf? Oor die algemeen is dit altyd die eerste vraag vir programmeerders: in watter taal sal ons skryf. Daar is nie een korrekte antwoord daarop nie: die probleme wat ons oplos is te divers. Vir sommige is TLA+ 'n spesifikasietaal wat ek ontwikkel het. Vir ander is dit geriefliker om Chinees te gebruik. Alles hang af van die situasie.
Belangriker is 'n ander vraag: hoe om duideliker denke te bereik? Antwoord: Ons moet soos wetenskaplikes dink. Dit is 'n manier van dink wat homself oor die afgelope 500 jaar bewys het. In die wetenskap bou ons wiskundige modelle van die werklikheid. Sterrekunde was miskien die eerste wetenskap in die streng sin van die woord. In die wiskundige model wat in sterrekunde gebruik word, verskyn hemelliggame as punte met massa, posisie en momentum, hoewel dit in werklikheid uiters komplekse voorwerpe met berge en oseane, getye en getye is. Hierdie model, soos enige ander, is geskep om sekere probleme op te los. Dit is wonderlik om te bepaal waarheen om die teleskoop te wys as jy 'n planeet moet vind. Maar as jy die weer op hierdie planeet wil voorspel, sal hierdie model nie werk nie.
Wiskunde stel ons in staat om die eienskappe van die model te bepaal. En die wetenskap wys hoe hierdie eienskappe verband hou met die werklikheid. Kom ons praat oor ons wetenskap, rekenaarwetenskap. Die realiteit waarmee ons werk, is rekenaarstelsels van verskeie soorte: verwerkers, speletjiekonsoles, rekenaars, uitvoering van programme, ensovoorts. Ek sal praat oor die bestuur van 'n program op 'n rekenaar, maar oor die algemeen geld al hierdie gevolgtrekkings vir enige rekenaarstelsel. In ons wetenskap gebruik ons baie verskillende modelle: die Turing-masjien, gedeeltelik geordende stelle gebeurtenisse, en vele ander.
Wat is 'n program? Dit is enige kode wat onafhanklik oorweeg kan word. Gestel ons moet 'n blaaier skryf. Ons voer drie take uit: ons ontwerp die gebruiker se siening van die program, dan skryf ons die hoëvlakdiagram van die program, en laastens skryf ons die kode. Terwyl ons die kode skryf, besef ons dat ons 'n teksformateerder moet skryf. Hier moet ons weer drie probleme oplos: bepaal watter teks hierdie hulpmiddel sal terugstuur; kies 'n algoritme vir formatering; skryf kode. Hierdie taak het sy eie subtaak: voeg 'n koppelteken korrek in woorde in. Ons los hierdie subtaak ook in drie stappe op – soos jy kan sien, word dit op baie vlakke herhaal.
Kom ons kyk in meer besonderhede na die eerste stap: watter probleem die program oplos. Hier modelleer ons meestal 'n program as 'n funksie wat 'n mate van insette neem en 'n mate van uitset produseer. In wiskunde word 'n funksie gewoonlik beskryf as 'n geordende stel pare. Byvoorbeeld, die kwadraatfunksie vir natuurlike getalle word beskryf as die versameling {<0,0>, <1,1>, <2,4>, <3,9>, …}. Die domein van so 'n funksie is die versameling van die eerste elemente van elke paar, dit wil sê die natuurlike getalle. Om 'n funksie te definieer, moet ons die omvang en formule daarvan spesifiseer.
Maar funksies in wiskunde is nie dieselfde as funksies in programmeertale nie. Die wiskunde is baie makliker. Aangesien ek nie tyd het vir komplekse voorbeelde nie, kom ons kyk na 'n eenvoudige een: 'n funksie in C of 'n statiese metode in Java wat die grootste gemene deler van twee heelgetalle gee. In die spesifikasie van hierdie metode sal ons skryf: bereken GCD(M,N) vir argumente M и NWaar GCD(M,N) - 'n funksie waarvan die domein die stel pare heelgetalle is, en die terugkeerwaarde is die grootste heelgetal wat deelbaar is deur M и N. Hoe hou hierdie model verband met die werklikheid? Die model werk op heelgetalle, terwyl ons in C of Java 'n 32-bis het int. Hierdie model laat ons toe om te besluit of die algoritme korrek is GCD, maar dit sal nie oorloopfoute voorkom nie. Dit sal 'n meer komplekse model vereis, waarvoor daar nie tyd is nie.
Kom ons praat oor die beperkings van 'n funksie as 'n model. Sommige programme (soos bedryfstelsels) gee nie net 'n sekere waarde vir sekere argumente terug nie, hulle kan deurlopend loop. Daarbenewens is die funksie as 'n model nie goed geskik vir die tweede stap nie: beplanning hoe om die probleem op te los. Vinnige sorteer en borrelsortering bereken dieselfde funksie, maar dit is heeltemal verskillende algoritmes. Daarom, om te beskryf hoe die doel van die program bereik word, gebruik ek 'n ander model, kom ons noem dit die standaard gedragsmodel. Die program daarin word voorgestel as 'n stel van alle toelaatbare gedrag, wat elkeen op sy beurt 'n reeks toestande is, en die toestand is die toewysing van waardes aan veranderlikes.
Kom ons kyk hoe die tweede stap vir die Euklidiese algoritme sal lyk. Ons moet bereken GCD(M, N). Ons inisialiseer M hoe xEn N hoe y, trek dan herhaaldelik die kleinste van hierdie veranderlikes van die groter af totdat hulle gelyk is. Byvoorbeeld, as M = 12En N = 18, kan ons die volgende gedrag beskryf:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
En as M = 0 и N = 0? Nul is deelbaar deur alle getalle, so daar is geen grootste deler in hierdie geval nie. In hierdie situasie moet ons teruggaan na die eerste stap en vra: moet ons werklik GCD vir nie-positiewe getalle bereken? As dit nie nodig is nie, moet u net die spesifikasie verander.
Hier moet ons 'n klein afwyking maak oor produktiwiteit. Dit word dikwels gemeet in die aantal reëls kode wat per dag geskryf word. Maar jou werk is baie nuttiger as jy van 'n sekere aantal lyne ontslae raak, want jy het minder plek vir goggas. En die maklikste manier om van die kode ontslae te raak, is by die eerste stap. Dit is heeltemal moontlik dat jy net nie al die klokkies en fluitjies nodig het wat jy probeer implementeer nie. Die vinnigste manier om 'n program te vereenvoudig en tyd te bespaar, is om nie dinge te doen wat nie gedoen moet word nie. Die tweede stap is die tweede mees tydbesparende potensiaal. As jy produktiwiteit meet in terme van lyne wat geskryf is, sal jy dink oor hoe om 'n taak uit te voer minder produktief, want jy kan dieselfde probleem oplos met minder kode. Ek kan nie presiese statistieke hier gee nie, want ek het geen manier om die aantal reëls te tel wat ek nie geskryf het nie as gevolg van die feit dat ek tyd spandeer het aan die spesifikasie, dit wil sê aan die eerste en tweede stappe. En die eksperiment kan ook nie hier opgestel word nie, want in die eksperiment het ons nie die reg om die eerste stap te voltooi nie, die taak is vooraf bepaal.
Dit is maklik om baie probleme in informele spesifikasies oor die hoof te sien. Daar is niks moeilik om streng spesifikasies vir funksies te skryf nie, ek sal dit nie bespreek nie. In plaas daarvan sal ons praat oor die skryf van sterk spesifikasies vir standaardgedrag. Daar is 'n stelling wat sê dat enige stel gedrag beskryf kan word deur die sekuriteitseienskap te gebruik (veiligheid) en oorlewingseienskappe (lewendigheid). Sekuriteit beteken dat niks sleg sal gebeur nie, die program sal nie 'n verkeerde antwoord gee nie. Oorlewing beteken dat daar vroeër of later iets goeds sal gebeur, dit wil sê die program sal vroeër of later die korrekte antwoord gee. As 'n reël is sekuriteit 'n meer belangrike aanwyser, foute kom meestal hier voor. Daarom, om tyd te bespaar, sal ek nie oor oorlewing praat nie, hoewel dit natuurlik ook belangrik is.
Ons bereik sekuriteit deur eerstens die stel moontlike begintoestande voor te skryf. En tweedens, verhoudings met alle moontlike volgende state vir elke staat. Kom ons tree soos wetenskaplikes op en definieer state wiskundig. Die stel begintoestande word beskryf deur 'n formule, byvoorbeeld in die geval van die Euklidiese algoritme: (x = M) ∧ (y = N). Vir sekere waardes M и N daar is net een begintoestand. Die verwantskap met die volgende toestand word beskryf deur 'n formule waarin die veranderlikes van die volgende toestand met 'n priemgetal geskryf word, en die veranderlikes van die huidige toestand sonder 'n priemgetal geskryf word. In die geval van Euclides se algoritme, sal ons handel oor die disjunksie van twee formules, in een waarvan x is die grootste waarde, en in die tweede - y:
In die eerste geval is die nuwe waarde van y gelyk aan die vorige waarde van y, en ons kry die nuwe waarde van x deur die kleiner veranderlike van die groter een af te trek. In die tweede geval doen ons die teenoorgestelde.
Kom ons gaan terug na Euclides se algoritme. Kom ons aanvaar dit weer M = 12, N = 18. Dit definieer 'n enkele aanvanklike toestand, (x = 12) ∧ (y = 18). Ons prop dan daardie waardes by die formule hierbo in en kry:
Hier is die enigste moontlike oplossing: x' = 18 - 12 ∧ y' = 12en ons kry die gedrag: [x = 12, y = 18]. Net so kan ons al die toestande in ons gedrag beskryf: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
In die laaste staat [x = 6, y = 6] beide dele van die uitdrukking sal vals wees, so dit het geen volgende toestand nie. So, ons het 'n volledige spesifikasie van die tweede stap - soos jy kan sien, is dit nogal gewone wiskunde, soos in ingenieurs en wetenskaplikes, en nie vreemd nie, soos in rekenaarwetenskap.
Hierdie twee formules kan gekombineer word in een formule van temporele logika. Sy is elegant en maklik om te verduidelik, maar daar is nie nou tyd vir haar nie. Ons het dalk net tydelike logika nodig vir die lewendige eiendom, dit is nie nodig vir sekuriteit nie. Ek hou nie van tydelike logika as sodanig nie, dit is nie heeltemal gewone wiskunde nie, maar in die geval van lewendigheid is dit 'n noodsaaklike euwel.
In Euclides se algoritme, vir elke waarde x и y unieke waardes het x' и y', wat die verband met die volgende toestand waar maak. Met ander woorde, Euclides se algoritme is deterministies. Om 'n nie-deterministiese algoritme te modelleer, moet die huidige toestand veelvuldige moontlike toekomstige toestande hê, en dat elke onvervulde veranderlike waarde veelvuldige gevorderde veranderlike waardes het, sodat die verhouding met die volgende toestand waar is. Dit is maklik om te doen, maar ek sal nie nou voorbeelde gee nie.
Om 'n werkende hulpmiddel te maak, benodig jy formele wiskunde. Hoe om die spesifikasie formeel te maak? Om dit te doen het ons 'n formele taal nodig, bv. . Die spesifikasie van die Euclid-algoritme sal so lyk in hierdie taal:
'n Gelyktekensimbool met 'n driehoek beteken dat die waarde links van die teken gedefinieer word om gelyk te wees aan die waarde regs van die teken. In wese is die spesifikasie 'n definisie, in ons geval twee definisies. By die spesifikasie in TLA+ moet u verklarings en 'n bietjie sintaksis byvoeg, soos in die skyfie hierbo. In ASCII sal dit so lyk:
Soos jy kan sien, niks ingewikkeld nie. Die spesifikasie vir TLA+ kan getoets word, dit wil sê omseil alle moontlike gedrag in 'n klein model. In ons geval sal hierdie model sekere waardes wees M и N. Dit is 'n baie doeltreffende en eenvoudige verifikasiemetode wat heeltemal outomaties is. Dit is ook moontlik om formele waarheidsbewyse te skryf en meganies na te gaan, maar dit neem baie tyd, so byna niemand doen dit nie.
Die grootste nadeel van TLA+ is dat dit wiskunde is, en programmeerders en rekenaarwetenskaplikes is bang vir wiskunde. Met die eerste oogopslag klink dit na 'n grap, maar ongelukkig bedoel ek dit in alle erns. My kollega het net vir my vertel hoe hy probeer het om TLA+ aan verskeie ontwikkelaars te verduidelik. Sodra die formules op die skerm verskyn het, het dit dadelik glasagtige oë geword. So as TLA+ jou bang maak, kan jy dit gebruik , dit is soort van 'n speelding programmeertaal. 'n Uitdrukking in PlusCal kan enige TLA+ uitdrukking wees, dit wil sê in die algemeen enige wiskundige uitdrukking. Boonop het PlusCal 'n sintaksis vir nie-deterministiese algoritmes. Omdat PlusCal enige TLA+ uitdrukking kan skryf, is PlusCal baie meer ekspressief as enige regte programmeertaal. Vervolgens word PlusCal saamgestel in 'n maklik leesbare TLA+ spesifikasie. Dit beteken natuurlik nie dat die komplekse PlusCal-spesifikasie in 'n eenvoudige een op TLA + sal verander nie - net die korrespondensie tussen hulle is duidelik, daar sal geen bykomende kompleksiteit wees nie. Laastens kan hierdie spesifikasie geverifieer word deur TLA+-instrumente. Al met al kan PlusCal help om wiskundefobie te oorkom en is dit maklik om te verstaan, selfs vir programmeerders en rekenaarwetenskaplikes. In die verlede het ek vir 'n geruime tyd (sowat 10 jaar) algoritmes daaroor gepubliseer.
Miskien sal iemand beswaar maak dat TLA + en PlusCal wiskunde is, en wiskunde werk net op uitgevindde voorbeelde. In die praktyk het jy 'n regte taal nodig met tipes, prosedures, voorwerpe, ensovoorts. Dis verkeerd. Hier is wat Chris Newcomb, wat by Amazon gewerk het, skryf: “Ons het TLA+ op tien groot projekte gebruik, en in elke geval het die gebruik daarvan 'n beduidende verskil aan ontwikkeling gemaak omdat ons gevaarlike foute kon vang voordat ons produksie bereik het, en omdat dit ons die insig en selfvertroue gegee het wat ons nodig gehad het om maak aggressiewe prestasieoptimalisasies sonder om die waarheid van die program te beïnvloed". Jy kan dikwels hoor dat wanneer ons formele metodes gebruik, ons ondoeltreffende kode kry - in die praktyk is alles presies die teenoorgestelde. Daarbenewens is daar 'n mening dat bestuurders nie oortuig kan word van die behoefte aan formele metodes nie, selfs al is programmeerders oortuig van die bruikbaarheid daarvan. En Newcomb skryf: "Bestuurders druk nou hard om spesifikasies vir TLA + te skryf, en spesifiek tyd hiervoor toe te ken". So wanneer bestuurders sien dat TLA+ werk, aanvaar hulle dit graag. Chris Newcomb het dit so ses maande gelede (Oktober 2014) geskryf, maar nou, sover ek weet, word TLA+ in 14 projekte gebruik, nie 10 nie. Nog 'n voorbeeld is in die ontwerp van die XBox 360. 'n Intern het na Charles Thacker gekom en het spesifikasie vir die geheuestelsel geskryf. Danksy hierdie spesifikasie is 'n fout gevind wat andersins ongemerk sou bly, en as gevolg daarvan sou elke XBox 360 na vier uur se gebruik ineenstort. IBM-ingenieurs het bevestig dat hul toetse nie hierdie fout sou gevind het nie.
Jy kan meer oor TLA + op die internet lees, maar kom ons praat nou oor informele spesifikasies. Ons hoef selde programme te skryf wat die minste gemene deler en dies meer bereken. Ons skryf baie meer gereeld programme soos die mooi drukker-instrument wat ek vir TLA+ geskryf het. Na die eenvoudigste verwerking sal die TLA +-kode soos volg lyk:
Maar in die voorbeeld hierbo wou die gebruiker heel waarskynlik hê dat die voegwoord en gelyke-tekens in lyn gebring moet word. Die korrekte formatering sal dus meer soos volg lyk:
Beskou nog 'n voorbeeld:
Hier, inteendeel, was die belyning van die gelyke-, optel- en vermenigvuldigingstekens in die bron ewekansig, so die eenvoudigste verwerking is heeltemal genoeg. Oor die algemeen is daar geen presiese wiskundige definisie van korrekte formatering nie, want "korrek" in hierdie geval beteken "wat die gebruiker wil hê", en dit kan nie wiskundig bepaal word nie.
Dit wil voorkom asof as ons nie 'n definisie van waarheid het nie, dan is die spesifikasie nutteloos. Maar dit is nie. Net omdat ons nie weet wat 'n program veronderstel is om te doen nie, beteken dit nie dat ons nie hoef te dink oor hoe dit werk nie - inteendeel, ons moet nog meer moeite doen. Die spesifikasie is veral hier belangrik. Dit is onmoontlik om die optimale program vir gestruktureerde drukwerk te bepaal, maar dit beteken nie dat ons dit glad nie moet neem nie, en om kode as 'n stroom van bewussyn te skryf is nie 'n goeie ding nie. Op die ou end het ek 'n spesifikasie van ses reëls met definisies geskryf in die vorm van kommentaar in 'n java-lêer. Hier is 'n voorbeeld van een van die reëls: a left-comment token is LeftComment aligned with its covering token. Hierdie reël is geskryf in, sal ons sê, wiskundige Engels: LeftComment aligned, left-comment и covering token - terme met definisies. Dit is hoe wiskundiges wiskunde beskryf: hulle skryf definisies van terme en, op grond daarvan, reëls. Die voordeel van so 'n spesifikasie is dat ses reëls baie makliker is om te verstaan en te ontfout as 850 reëls kode. Ek moet sê dat die skryf van hierdie reëls nie maklik was nie, dit het nogal baie tyd geneem om dit te ontfout. Ek het veral vir hierdie doel 'n kode geskryf wat gerapporteer het watter reël gebruik is. Danksy die feit dat ek hierdie ses reëls op verskeie voorbeelde getoets het, hoef ek nie 850 reëls kode te ontfout nie, en foute was redelik maklik om te vind. Java het wonderlike gereedskap hiervoor. As ek net die kode geskryf het, sou dit my baie langer geneem het, en die formatering sou van swakker gehalte gewees het.
Waarom kon 'n formele spesifikasie nie gebruik word nie? Aan die een kant is die korrekte uitvoering nie hier te belangrik nie. Strukturele drukstukke sal beslis niemand behaag nie, so ek hoef dit nie reg te kry in al die vreemde situasies nie. Nog belangriker is die feit dat ek nie voldoende gereedskap gehad het nie. Die TLA+-modeltoetser is hier nutteloos, so ek sal die voorbeelde met die hand moet skryf.
Bogenoemde spesifikasie het kenmerke gemeen aan alle spesifikasies. Dit is hoër vlak as die kode. Dit kan in enige taal geïmplementeer word. Enige gereedskap of metodes is nutteloos om dit te skryf. Geen programmeringskursus sal jou help om hierdie spesifikasie te skryf nie. En daar is geen gereedskap wat hierdie spesifikasie onnodig kan maak nie, tensy jy natuurlik 'n taal skryf wat spesifiek is vir die skryf van gestruktureerde drukprogramme in TLA+. Ten slotte, hierdie spesifikasie sê niks oor presies hoe ons die kode sal skryf nie, dit sê net wat die kode doen. Ons skryf die spesifikasie om ons te help om deur die probleem te dink voordat ons aan die kode begin dink.
Maar hierdie spesifikasie het ook kenmerke wat dit van ander spesifikasies onderskei. 95% van ander spesifikasies is aansienlik korter en eenvoudiger:
Verder is hierdie spesifikasie 'n stel reëls. As 'n reël is dit 'n teken van swak spesifikasie. Dit is nogal moeilik om die gevolge van 'n stel reëls te verstaan, en daarom moes ek baie tyd daaraan bestee om dit te ontfout. In hierdie geval kon ek egter nie 'n beter manier vind nie.
Dit is die moeite werd om 'n paar woorde te sê oor programme wat voortdurend loop. As 'n reël werk hulle parallel, byvoorbeeld bedryfstelsels of verspreide stelsels. Baie min mense kan hulle verstandelik of op papier verstaan, en ek is nie een van hulle nie, alhoewel ek dit eens kon doen. Daarom het ons gereedskap nodig wat ons werk sal kontroleer - byvoorbeeld TLA + of PlusCal.
Hoekom was dit nodig om 'n spesifikasie te skryf as ek reeds geweet het wat presies die kode moet doen? Trouens, ek het net gedink ek weet dit. Daarbenewens, met 'n spesifikasie, hoef 'n buitestander nie meer in die kode te kom om te verstaan wat presies hy doen nie. Ek het 'n reël: daar moet geen algemene reëls wees nie. Daar is 'n uitsondering op hierdie reël, natuurlik, dit is die enigste algemene reël wat ek volg: die spesifikasie van wat die kode doen, moet mense alles vertel wat hulle moet weet wanneer hulle die kode gebruik.
So wat presies moet programmeerders oor denke weet? Om mee te begin, dieselfde as almal anders: as jy nie skryf nie, dan lyk dit net vir jou of jy dink. Jy moet ook dink voordat jy kodeer, wat beteken dat jy moet skryf voordat jy kodeer. Die spesifikasie is wat ons skryf voordat ons begin kodeer. 'n Spesifikasie is nodig vir enige kode wat deur enigiemand gebruik of gewysig kan word. En hierdie “iemand” is dalk self die skrywer van die kode ’n maand nadat dit geskryf is. 'n Spesifikasie is nodig vir groot programme en stelsels, vir klasse, vir metodes, en soms selfs vir komplekse afdelings van 'n enkele metode. Wat presies moet oor die kode geskryf word? Jy moet beskryf wat dit doen, dit wil sê wat nuttig kan wees vir enige persoon wat hierdie kode gebruik. Soms kan dit ook nodig wees om te spesifiseer hoe die kode sy doel bereik. As ons deur hierdie metode in die loop van algoritmes gegaan het, dan noem ons dit 'n algoritme. As dit iets meer spesiaal en nuut is, noem ons dit hoëvlakontwerp. Hier is geen formele verskil nie: albei is 'n abstrakte model van 'n program.
Hoe presies moet jy 'n kodespesifikasie skryf? Die belangrikste ding: dit moet een vlak hoër wees as die kode self. Dit moet toestande en gedrag beskryf. Dit moet so streng wees as wat die taak vereis. As jy 'n spesifikasie skryf vir hoe 'n taak geïmplementeer moet word, kan jy dit in pseudokode of met PlusCal skryf. Jy moet leer hoe om spesifikasies op formele spesifikasies te skryf. Dit sal jou die nodige vaardighede gee wat jou ook met informele sal help. Hoe leer jy om formele spesifikasies te skryf? Toe ons geleer het om te programmeer, het ons programme geskryf en dit dan ontfout. Dit is dieselfde hier: skryf die spesifikasie, kontroleer dit met die modelkontroleerder, en maak die foute reg. TLA+ is dalk nie die beste taal vir 'n formele spesifikasie nie, en 'n ander taal sal waarskynlik beter wees vir jou spesifieke behoeftes. Die voordeel van TLA+ is dat dit wiskundige denke baie goed leer.
Hoe om spesifikasie en kode te koppel? Met behulp van kommentaar wat wiskundige konsepte en die implementering daarvan verbind. As jy met grafieke werk, sal jy op programvlak skikkings nodusse en skikkings skakels hê. Daarom moet jy presies skryf hoe die grafiek deur hierdie programmeringstrukture geïmplementeer word.
Daar moet kennis geneem word dat nie een van die bogenoemde van toepassing is op die werklike proses om kode te skryf nie. Wanneer jy die kode skryf, dit wil sê jy voer die derde stap uit, moet jy ook deur die program dink en deurdink. As 'n subtaak kompleks of nie-vanselfsprekend blyk te wees, moet jy 'n spesifikasie daarvoor skryf. Maar ek praat nie hier van die kode self nie. Jy kan enige programmeertaal, enige metodologie gebruik, dit gaan nie oor hulle nie. Ook, nie een van die bogenoemde skakel die behoefte uit om kode te toets en te ontfout nie. Selfs as die abstrakte model korrek geskryf is, kan daar foute in die implementering daarvan wees.
Die skryf van spesifikasies is 'n bykomende stap in die koderingsproses. Danksy dit kan baie foute met minder moeite opgevang word - ons weet dit uit die ervaring van programmeerders van Amazon. Met spesifikasies word die gehalte van programme hoër. So hoekom gaan ons dan so dikwels sonder hulle? Want skryf is moeilik. En skryf is moeilik, want hiervoor moet jy dink, en dink is ook moeilik. Dit is altyd makliker om voor te gee wat jy dink. Hier kan jy 'n analogie met hardloop trek - hoe minder jy hardloop, hoe stadiger hardloop jy. Jy moet jou spiere oefen en skryf oefen. Benodig oefening.
Die spesifikasie kan verkeerd wees. Jy het dalk iewers 'n fout gemaak, of die vereistes het dalk verander, of 'n verbetering moet dalk aangebring word. Enige kode wat iemand gebruik moet verander word, so vroeër of later sal die spesifikasie nie meer ooreenstem met die program nie. Ideaal gesproke, in hierdie geval, moet jy 'n nuwe spesifikasie skryf en die kode heeltemal herskryf. Ons weet baie goed dat niemand dit doen nie. In die praktyk pleister ons die kode en werk moontlik die spesifikasie op. As dit seker vroeër of later sal gebeur, hoekom dan hoegenaamd spesifikasies skryf? Eerstens, vir die persoon wat jou kode sal wysig, sal elke ekstra woord in die spesifikasie goud werd wees, en hierdie persoon kan heel moontlik jy self wees. Ek beledig myself dikwels omdat ek nie genoeg spesifikasies kry wanneer ek my kode wysig nie. En ek skryf meer spesifikasies as kode. Daarom, wanneer jy die kode wysig, moet die spesifikasie altyd opgedateer word. Tweedens, met elke hersiening word die kode erger, dit word al hoe moeiliker om te lees en in stand te hou. Dit is 'n toename in entropie. Maar as jy nie met 'n spesifikasie begin nie, sal elke reël wat jy skryf 'n wysiging wees, en die kode sal van die begin af onhandelbaar en moeilik wees om te lees.
Soos gesê , geen stryd is volgens plan gewen nie, en geen stryd is gewen sonder 'n plan nie. En hy het 'n ding of twee van gevegte geweet. Daar is 'n mening dat die skryf van spesifikasies 'n mors van tyd is. Soms is dit waar, en die taak is so eenvoudig dat daar niks is om deur te dink nie. Maar jy moet altyd onthou dat wanneer jy aangesê word om nie spesifikasies te skryf nie, jy aangesê word om nie te dink nie. En jy moet elke keer daaroor dink. Deur die taak deur te dink, waarborg nie dat jy nie foute sal maak nie. Soos ons weet, het niemand die towerstaffie uitgevind nie, en programmering is 'n moeilike taak. Maar as jy nie deur die probleem dink nie, is jy gewaarborg om foute te maak.
Jy kan meer lees oor TLA + en PlusCal op 'n spesiale webwerf, jy kan daarheen gaan vanaf my tuisblad . Dis al vir my, dankie vir jou aandag.
Neem asseblief kennis dat dit 'n vertaling is. Wanneer jy kommentaar skryf, onthou dat die skrywer dit nie sal lees nie. As jy regtig met die skrywer wil gesels, dan sal hy by die Hydra 2019-konferensie wees wat 11-12 Julie 2019 in St. Petersburg gehou word. Kaartjies kan gekoop word .
Bron: will.com