Programmering är mer än kodning

Denna artikel är en översättning Stanford Seminarium. Men före henne en liten introduktion. Hur bildas zombies? Alla hamnade i en situation där de vill dra upp en vän eller kollega till sin nivå, men det går inte. Och det är inte så mycket med dig som med honom som "det går inte": på ena sidan av skalan finns en normal lön, uppgifter och så vidare, och på den andra, behovet av att tänka. Att tänka är obehagligt och smärtsamt. Han ger snabbt upp och fortsätter skriva kod utan att slå på hjärnan alls. Du föreställer dig hur mycket ansträngning det krävs för att övervinna barriären av inlärd hjälplöshet, och du gör det bara inte. Så här bildas zombies, som, det verkar, kan botas, men det verkar som om ingen kommer att göra det.

När jag såg det Leslie Lamport (ja, samma kamrat från läroböckerna) kommer till Ryssland och gör inte en rapport, utan en frågestund, var jag lite försiktig. För säkerhets skull är Leslie en världsberömd vetenskapsman, författare till grundläggande verk inom distribuerad datoranvändning, och du kan också känna honom genom bokstäverna La i ordet LaTeX - "Lamport TeX". Den andra alarmerande faktorn är hans krav: alla som kommer måste (helt kostnadsfritt) lyssna på ett par av hans rapporter i förväg, komma med minst en fråga om dem och först därefter komma. Jag bestämde mig för att se vad Lamport sände där – och det är fantastiskt! Det är precis den saken, det magiska länkpillret för att bota zombies. Jag varnar dig: från texten kan älskare av superflexibla metoder och de som inte gillar att testa vad som skrivs, särskilt bränna ut.

Efter habrokat börjar faktiskt översättningen av seminariet. Njut av att läsa!

Vilken uppgift du än tar dig an behöver du alltid gå igenom tre steg:

• bestämma vilket mål du vill uppnå;
• bestämma hur du ska uppnå ditt mål;
• komma till ditt mål.

Detta gäller även programmering. När vi skriver kod måste vi:

• bestämma vad programmet ska göra;
• bestämma hur den ska utföra sin uppgift;
• skriv motsvarande kod.

Det sista steget är naturligtvis väldigt viktigt, men jag ska inte prata om det i dag. Istället kommer vi att diskutera de två första. Varje programmerare utför dem innan de börjar arbeta. Du sätter dig inte ner för att skriva om du inte har bestämt dig för om du ska skriva en webbläsare eller en databas. En viss uppfattning om målet måste finnas. Och du funderar definitivt över vad exakt programmet kommer att göra, och skriver inte på något sätt i hopp om att koden på något sätt ska förvandlas till en webbläsare.

Hur exakt går det här koden för tänkande till? Hur mycket ansträngning ska vi lägga på detta? Allt beror på hur komplext problemet vi löser. Anta att vi vill skriva ett feltolerant distribuerat system. I det här fallet bör vi tänka igenom saker noga innan vi sätter oss ner för att koda. Vad händer om vi bara behöver öka en heltalsvariabel med 1? Vid första anblicken är allt trivialt här, och ingen tanke behövs, men sedan kommer vi ihåg att ett överflöde kan uppstå. Därför, även för att förstå om ett problem är enkelt eller komplext, måste du först tänka.

Om du tänker på möjliga lösningar på problemet i förväg kan du undvika misstag. Men detta kräver att ditt tänkande är tydligt. För att uppnå detta måste du skriva ner dina tankar. Jag gillar verkligen Dick Guindon-citatet: "När du skriver visar naturen dig hur slarvigt ditt tänkande är." Om du inte skriver så tror du bara att du tänker. Och du behöver skriva ner dina tankar i form av specifikationer.

Specifikationer har många funktioner, särskilt i stora projekt. Men jag kommer bara att tala om en av dem: de hjälper oss att tänka klart. Att tänka klart är väldigt viktigt och ganska svårt, så här behöver vi all hjälp. Vilket språk ska vi skriva specifikationer på? I allmänhet är detta alltid den första frågan för programmerare: vilket språk kommer vi att skriva på. Det finns inget korrekt svar på det: de problem vi löser är för olika. För vissa är TLA+ ett specifikationsspråk som jag utvecklat. För andra är det bekvämare att använda kinesiska. Allt beror på situationen.

Viktigare är en annan fråga: hur uppnår man ett tydligare tänkande? Svar: Vi måste tänka som vetenskapsmän. Detta är ett sätt att tänka som har bevisat sig självt under de senaste 500 åren. Inom naturvetenskap bygger vi matematiska modeller av verkligheten. Astronomi var kanske den första vetenskapen i ordets strikta mening. I den matematiska modellen som används inom astronomi uppträder himlakroppar som punkter med massa, position och fart, även om de i verkligheten är extremt komplexa objekt med berg och hav, tidvatten och tidvatten. Denna modell, som alla andra, skapades för att lösa vissa problem. Det är bra för att avgöra vart du ska rikta teleskopet om du behöver hitta en planet. Men om du vill förutsäga vädret på den här planeten, kommer den här modellen inte att fungera.

Matematik låter oss bestämma egenskaperna hos en modell. Och vetenskapen visar hur dessa egenskaper relaterar till verkligheten. Låt oss prata om vår vetenskap, datavetenskap. Den verklighet som vi arbetar med är datorsystem av olika slag: processorer, spelkonsoler, datorer, exekverande program och så vidare. Jag kommer att prata om att köra ett program på en dator, men i stort sett gäller alla dessa slutsatser för alla datorsystem. I vår vetenskap använder vi många olika modeller: Turing-maskinen, delvis beställda uppsättningar av händelser och många andra.

Vad är ett program? Detta är vilken kod som helst som kan övervägas oberoende. Anta att vi behöver skriva en webbläsare. Vi utför tre uppgifter: vi designar användarens syn på programmet, sedan skriver vi programmets högnivådiagram och slutligen skriver vi koden. När vi skriver koden inser vi att vi måste skriva en textformaterare. Här måste vi återigen lösa tre problem: bestämma vilken text detta verktyg kommer att returnera; välj en algoritm för formatering; skriva kod. Denna uppgift har sin egen deluppgift: infoga ett bindestreck korrekt i ord. Vi löser även denna deluppgift i tre steg – som du kan se upprepas de på många nivåer.

Låt oss överväga mer i detalj det första steget: vilket problem programmet löser. Här modellerar vi oftast ett program som en funktion som tar en del input och producerar en del output. I matematik brukar en funktion beskrivas som en ordnad uppsättning par. Till exempel beskrivs kvadreringsfunktionen för naturliga tal som mängden {<0,0>, <1,1>, <2,4>, <3,9>, …}. Domänen för en sådan funktion är mängden av de första elementen i varje par, det vill säga de naturliga talen. För att definiera en funktion måste vi specificera dess omfattning och formel.

Men funktioner i matematik är inte detsamma som funktioner i programmeringsspråk. Matematiken är mycket lättare. Eftersom jag inte har tid för komplexa exempel, låt oss överväga ett enkelt: en funktion i C eller en statisk metod i Java som returnerar den största gemensamma divisorn av två heltal. I specifikationen av denna metod kommer vi att skriva: beräknar GCD(M,N) för argument M и Nvar GCD(M,N) - en funktion vars domän är uppsättningen av par av heltal, och returvärdet är det största heltal som är delbart med M и N. Hur förhåller sig denna modell till verkligheten? Modellen arbetar på heltal, medan vi i C eller Java har en 32-bitars int. Denna modell låter oss avgöra om algoritmen är korrekt GCD, men det kommer inte att förhindra överflödesfel. Detta skulle kräva en mer komplex modell, som det inte finns tid för.

Låt oss prata om begränsningarna för en funktion som modell. Vissa program (som operativsystem) returnerar inte bara ett visst värde för vissa argument, de kan köras kontinuerligt. Funktionen som modell är dessutom inte väl lämpad för det andra steget: planera hur problemet ska lösas. Snabbsortering och bubbelsortering beräknar samma funktion, men de är helt olika algoritmer. För att beskriva hur målet med programmet uppnås använder jag därför en annan modell, låt oss kalla den standardbeteendemodellen. Programmet i det representeras som en uppsättning av alla tillåtna beteenden, som var och en i sin tur är en sekvens av tillstånd, och tillståndet är tilldelningen av värden till variabler.

Låt oss se hur det andra steget för euklidalgoritmen skulle se ut. Vi måste räkna GCD(M, N). Vi initierar M как xOch N как ysubtrahera sedan upprepade gånger den minsta av dessa variabler från den större tills de är lika. Till exempel om M = 12Och N = 18, kan vi beskriva följande beteende:

[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]

Och om M = 0 и N = 0? Noll är delbart med alla tal, så det finns ingen största divisor i detta fall. I den här situationen måste vi gå tillbaka till det första steget och fråga: behöver vi verkligen beräkna GCD för icke-positiva tal? Om detta inte är nödvändigt behöver du bara ändra specifikationen.

Här bör vi göra en liten avvikelse om produktivitet. Det mäts ofta i antalet rader kod som skrivs per dag. Men ditt arbete är mycket mer användbart om du blir av med ett visst antal rader, eftersom du har mindre utrymme för buggar. Och det enklaste sättet att bli av med koden är i första steget. Det är fullt möjligt att du helt enkelt inte behöver alla klockor och visselpipor du försöker implementera. Det snabbaste sättet att förenkla ett program och spara tid är att inte göra saker som inte borde göras. Det andra steget är den näst mest tidsbesparande potentialen. Om du mäter produktivitet i termer av skrivna rader kommer du att tänka på hur du utför en uppgift mindre produktiv, eftersom du kan lösa samma problem med mindre kod. Jag kan inte ge exakt statistik här, eftersom jag inte har något sätt att räkna antalet rader som jag inte skrev på grund av det faktum att jag spenderade tid på specifikationen, det vill säga på det första och andra steget. Och experimentet går inte att lägga upp här heller, eftersom vi i experimentet inte har rätt att genomföra det första steget, uppgiften är förutbestämd.

Det är lätt att förbise många svårigheter i informella specifikationer. Det är inget svårt att skriva strikta specifikationer för funktioner, jag kommer inte att diskutera detta. Istället kommer vi att prata om att skriva starka specifikationer för standardbeteenden. Det finns ett teorem som säger att alla beteenden kan beskrivas med säkerhetsegenskapen (säkerhet) och överlevnadsegenskaper (livlighet). Säkerhet innebär att inget dåligt kommer att hända, programmet kommer inte att ge ett felaktigt svar. Överlevnadsförmåga innebär att det förr eller senare händer något bra, det vill säga programmet kommer att ge rätt svar förr eller senare. Som regel är säkerhet en viktigare indikator, här uppstår oftast fel. Därför, för att spara tid, kommer jag inte att prata om överlevnadsförmåga, även om det naturligtvis också är viktigt.

Vi uppnår säkerhet genom att först föreskriva uppsättningen av möjliga initiala tillstånd. Och för det andra, relationer med alla möjliga nästa tillstånd för varje stat. Låt oss agera som vetenskapsmän och definiera tillstånd matematiskt. Uppsättningen av initialtillstånd beskrivs av en formel, till exempel i fallet med Euklids algoritm: (x = M) ∧ (y = N). För vissa värden M и N det finns bara ett initialtillstånd. Sambandet med nästa tillstånd beskrivs av en formel där variablerna för nästa tillstånd skrivs med ett primtal och variablerna för det aktuella tillståndet skrivs utan ett primtal. När det gäller Euklids algoritm kommer vi att behandla disjunktionen av två formler, varav en x är det största värdet, och i det andra - y:

I det första fallet är det nya värdet på y lika med det tidigare värdet på y, och vi får det nya värdet på x genom att subtrahera den mindre variabeln från den större variabeln. I det andra fallet gör vi tvärtom.

Låt oss gå tillbaka till Euklids algoritm. Låt oss anta det igen M = 12, N = 18. Detta definierar ett enda initialtillstånd, (x = 12) ∧ (y = 18). Vi kopplar sedan in dessa värden till formeln ovan och får:

Här är den enda möjliga lösningen: x' = 18 - 12 ∧ y' = 12och vi får beteendet: [x = 12, y = 18]. På liknande sätt kan vi beskriva alla tillstånd i vårt beteende: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].

I sista tillståndet [x = 6, y = 6] båda delarna av uttrycket kommer att vara falskt, så det har inget nästa tillstånd. Så vi har en fullständig specifikation av det andra steget - som du kan se är detta ganska vanlig matematik, som hos ingenjörer och vetenskapsmän, och inte konstigt, som inom datavetenskap.

Dessa två formler kan kombineras till en formel för tidslogik. Hon är elegant och lätt att förklara, men det finns inte tid för henne nu. Vi kanske behöver temporär logik bara för livlighetens egendom, den behövs inte för säkerheten. Jag gillar inte tidslogik som sådan, det är inte helt vanlig matematik, men i fallet med livlighet är det ett nödvändigt ont.

I Euklids algoritm, för varje värde x и y har unika värden x' и y', som gör relationen med nästa tillstånd sann. Euklids algoritm är med andra ord deterministisk. För att modellera en icke-deterministisk algoritm måste det aktuella tillståndet ha flera möjliga framtida tillstånd, och att varje oprimat variabelvärde har flera primerade variabelvärden så att relationen till nästa tillstånd är sann. Detta är lätt att göra, men jag ska inte ge några exempel nu.

För att göra ett arbetsredskap behöver du formell matematik. Hur gör man specifikationen formell? För att göra detta behöver vi ett formellt språk, t.ex. TLA+. Specifikationen för Euclid-algoritmen skulle se ut så här på detta språk:

En likhetsteckensymbol med en triangel betyder att värdet till vänster om tecknet definieras till att vara lika med värdet till höger om tecknet. I huvudsak är specifikationen en definition, i vårt fall två definitioner. Till specifikationen i TLA+ behöver du lägga till deklarationer och viss syntax, som i bilden ovan. I ASCII skulle det se ut så här:

Som du kan se, inget komplicerat. Specifikationen för TLA+ kan testas, d.v.s. kringgå alla möjliga beteenden i en liten modell. I vårt fall kommer denna modell att vara vissa värden M и N. Detta är en mycket effektiv och enkel verifieringsmetod som är helt automatisk. Det går även att skriva formella sanningsbevis och kontrollera dem mekaniskt, men detta tar mycket tid, så nästan ingen gör detta.

Den största nackdelen med TLA+ är att det är matematik, och programmerare och datavetare är rädda för matematik. Vid första anblicken låter detta som ett skämt, men tyvärr menar jag det på fullt allvar. Min kollega berättade precis hur han försökte förklara TLA+ för flera utvecklare. Så fort formlerna dök upp på skärmen blev de genast glasiga ögon. Så om TLA+ skrämmer dig kan du använda PlusCal, det är ett slags leksaksprogrammeringsspråk. Ett uttryck i PlusCal kan vara vilket TLA+-uttryck som helst, det vill säga i stort sett vilket matematiskt uttryck som helst. PlusCal har dessutom en syntax för icke-deterministiska algoritmer. Eftersom PlusCal kan skriva vilket TLA+-uttryck som helst, är PlusCal mycket mer uttrycksfullt än något riktigt programmeringsspråk. Därefter sammanställs PlusCal till en lättläsbar TLA+-specifikation. Detta betyder naturligtvis inte att den komplexa PlusCal-specifikationen kommer att förvandlas till en enkel sådan på TLA + - bara korrespondensen mellan dem är uppenbar, det kommer inte att finnas någon ytterligare komplexitet. Slutligen kan denna specifikation verifieras av TLA+-verktyg. Sammantaget kan PlusCal hjälpa till att övervinna matematikfobi och är lätt att förstå även för programmerare och datavetare. Tidigare publicerade jag algoritmer på det under en tid (cirka 10 år).

Kanske kommer någon att invända att TLA + och PlusCal är matematik, och matematik fungerar bara på påhittade exempel. I praktiken behöver du ett riktigt språk med typer, procedurer, objekt och så vidare. Detta är fel. Här är vad Chris Newcomb, som arbetade på Amazon, skriver: "Vi har använt TLA+ på tio stora projekt, och i varje fall har användningen av det gjort en betydande skillnad för utvecklingen eftersom vi kunde fånga farliga buggar innan vi började producera, och för att det gav oss den insikt och det förtroende vi behövde för att göra aggressiva prestandaoptimeringar utan att påverka programmets sanning". Man kan ofta höra att när vi använder formella metoder får vi ineffektiv kod – i praktiken är allt precis tvärtom. Dessutom finns det en åsikt att chefer inte kan övertygas om behovet av formella metoder, även om programmerare är övertygade om deras användbarhet. Och Newcomb skriver: "Hantera pressar nu hårt på att skriva specifikationer för TLA + och avsätter specifikt tid för detta". Så när chefer ser att TLA+ fungerar accepterar de det gärna. Chris Newcomb skrev detta för ungefär ett halvår sedan (oktober 2014), men nu, så vitt jag vet, används TLA+ i 14 projekt, inte 10. Ett annat exempel är designen av XBox 360. En praktikant kom till Charles Thacker och skrev specifikation för minnessystemet. Tack vare denna specifikation hittades en bugg som annars skulle förbli obemärkt, och på grund av vilket varje Xbox 360 skulle krascha efter fyra timmars användning. IBM-ingenjörer bekräftade att deras tester inte skulle ha hittat denna bugg.

Du kan läsa mer om TLA + på Internet, men nu ska vi prata om informella specifikationer. Vi behöver sällan skriva program som räknar ut minsta gemensamma divisor och liknande. Mycket oftare skriver vi program som pretty-printer-verktyget jag skrev för TLA+. Efter den enklaste bearbetningen skulle TLA +-koden se ut så här:

Men i exemplet ovan ville användaren sannolikt att konjunktionen och likhetstecknen skulle vara anpassade. Så den korrekta formateringen skulle se ut mer så här:

Låt oss titta på ett annat exempel:

Här var tvärtom anpassningen av likhetstecken, addition och multiplikationstecken i källan slumpmässig, så den enklaste bearbetningen räcker. I allmänhet finns det ingen exakt matematisk definition av korrekt formatering, eftersom "korrekt" i det här fallet betyder "vad användaren vill ha", och detta kan inte bestämmas matematiskt.

Det verkar som att om vi inte har en definition av sanning så är specifikationen värdelös. Men det är inte. Bara för att vi inte vet vad ett program ska göra betyder det inte att vi inte behöver tänka på hur det fungerar – tvärtom måste vi lägga ännu mer kraft på det. Specifikationen är särskilt viktig här. Det är omöjligt att bestämma det optimala programmet för strukturerad utskrift, men det betyder inte att vi inte ska ta det alls, och att skriva kod som en ström av medvetande är inte bra. Till slut skrev jag en specifikation av sex regler med definitioner i form av kommentarer i en java-fil. Här är ett exempel på en av reglerna: a left-comment token is LeftComment aligned with its covering token. Denna regel är skriven på, ska vi säga, matematisk engelska: LeftComment aligned, left-comment и covering token - termer med definitioner. Det är så matematiker beskriver matematik: de skriver definitioner av termer och, utifrån dem, regler. Fördelen med en sådan specifikation är att sex regler är mycket lättare att förstå och felsöka än 850 rader kod. Jag måste säga att det inte var lätt att skriva dessa regler, det tog ganska lång tid att felsöka dem. Speciellt för detta ändamål skrev jag en kod som rapporterade vilken regel som användes. Tack vare det faktum att jag testade dessa sex regler på flera exempel, behövde jag inte felsöka 850 rader kod, och buggar visade sig vara ganska lätta att hitta. Java har bra verktyg för detta. Om jag bara hade skrivit koden hade det tagit mycket längre tid, och formateringen hade varit av sämre kvalitet.

Varför kunde inte en formell specifikation användas? Å ena sidan är det korrekta utförandet inte alltför viktigt här. Strukturella utskrifter är skyldiga att inte glädja någon, så jag behövde inte få det att fungera rätt i alla udda situationer. Ännu viktigare är det faktum att jag inte hade tillräckliga verktyg. TLA+-modellkontrollen är värdelös här, så jag måste skriva exemplen manuellt.

Ovanstående specifikation har gemensamma egenskaper för alla specifikationer. Det är högre nivå än koden. Det kan implementeras på vilket språk som helst. Alla verktyg eller metoder är värdelösa för att skriva det. Ingen programmeringskurs hjälper dig att skriva denna specifikation. Och det finns inga verktyg som kan göra den här specifikationen onödig, såvida du inte, naturligtvis, skriver ett språk specifikt för att skriva strukturerade utskriftsprogram i TLA+. Slutligen, den här specifikationen säger ingenting om exakt hur vi kommer att skriva koden, den anger bara vad den här koden gör. Vi skriver specifikationen för att hjälpa oss att tänka igenom problemet innan vi börjar tänka på koden.

Men den här specifikationen har också funktioner som skiljer den från andra specifikationer. 95 % av andra specifikationer är betydligt kortare och enklare:

Vidare är denna specifikation en uppsättning regler. Som regel är detta ett tecken på dålig specifikation. Att förstå konsekvenserna av en uppsättning regler är ganska svårt, varför jag var tvungen att lägga mycket tid på att felsöka dem. Men i det här fallet kunde jag inte hitta ett bättre sätt.

Det är värt att säga några ord om program som körs kontinuerligt. Som regel arbetar de parallellt, till exempel operativsystem eller distribuerade system. Väldigt få människor kan förstå dem mentalt eller på papper, och jag är inte en av dem, även om jag en gång kunde göra det. Därför behöver vi verktyg som kontrollerar vårt arbete - till exempel TLA + eller PlusCal.

Varför var det nödvändigt att skriva en specifikation om jag redan visste vad exakt koden skulle göra? Jag trodde faktiskt att jag visste det. Dessutom, med en specifikation, behöver en utomstående inte längre komma in i koden för att förstå exakt vad han gör. Jag har en regel: det ska inte finnas några allmänna regler. Det finns ett undantag från denna regel, naturligtvis, det är den enda allmänna regeln jag följer: specifikationen av vad koden gör ska berätta för folk allt de behöver veta när de använder koden.

Så vad exakt behöver programmerare veta om att tänka? Till att börja med samma sak som alla andra: om du inte skriver så verkar det bara för dig som du tänker. Dessutom måste du tänka innan du kodar, vilket betyder att du måste skriva innan du kodar. Specifikationen är vad vi skriver innan vi börjar koda. En specifikation behövs för alla koder som kan användas eller modifieras av vem som helst. Och denna "någon" kan vara författaren till koden själv en månad efter att den skrevs. En specifikation behövs för stora program och system, för klasser, för metoder och ibland även för komplexa delar av en enskild metod. Vad exakt ska skrivas om koden? Du måste beskriva vad den gör, det vill säga vad som kan vara användbart för alla som använder den här koden. Ibland kan det också vara nödvändigt att specificera hur koden uppnår sitt syfte. Om vi ​​gick igenom denna metod under algoritmer, så kallar vi det en algoritm. Om det är något mer speciellt och nytt, så kallar vi det design på hög nivå. Det finns ingen formell skillnad här: båda är en abstrakt modell av ett program.

Hur exakt ska man skriva en kodspecifikation? Huvudsaken: den ska vara en nivå högre än själva koden. Den ska beskriva tillstånd och beteenden. Det ska vara så strikt som uppgiften kräver. Om du skriver en specifikation för hur en uppgift ska implementeras kan du skriva den i pseudokod eller med PlusCal. Du måste lära dig hur man skriver specifikationer på formella specifikationer. Detta kommer att ge dig de nödvändiga färdigheterna som också hjälper dig med informella sådana. Hur lär man sig att skriva formella specifikationer? När vi lärde oss att programmera skrev vi program och debuggade dem sedan. Det är samma sak här: skriv specen, kontrollera den med modellkontrollen och fixa felen. TLA+ kanske inte är det bästa språket för en formell specifikation, och ett annat språk är troligen bättre för dina specifika behov. Fördelen med TLA+ är att det lär ut matematiskt tänkande väldigt bra.

Hur länkar man specifikation och kod? Med hjälp av kommentarer som kopplar samman matematiska begrepp och deras genomförande. Om du arbetar med grafer kommer du på programnivå att ha arrayer av noder och arrayer av länkar. Därför måste du skriva exakt hur grafen implementeras av dessa programmeringsstrukturer.

Det bör noteras att inget av ovanstående gäller själva processen att skriva kod. När du skriver koden, det vill säga du utför det tredje steget, behöver du också tänka och tänka igenom programmet. Om en deluppgift visar sig vara komplex eller icke-uppenbar måste du skriva en specifikation för den. Men jag pratar inte om själva koden här. Du kan använda vilket programmeringsspråk som helst, vilken metod som helst, det handlar inte om dem. Dessutom eliminerar inget av ovanstående behovet av att testa och felsöka kod. Även om den abstrakta modellen är korrekt skriven kan det finnas buggar i dess implementering.

Att skriva specifikationer är ett ytterligare steg i kodningsprocessen. Tack vare det kan många fel fångas med mindre ansträngning - vi vet detta från erfarenheten från programmerare från Amazon. Med specifikationer blir kvaliteten på programmen högre. Så varför går vi så ofta utan dem? För att skriva är svårt. Och att skriva är svårt, för för detta behöver du tänka, och att tänka är också svårt. Det är alltid lättare att låtsas som man tycker. Här kan du dra en analogi med löpning – ju mindre du springer, desto långsammare springer du. Du måste träna dina muskler och träna på att skriva. Behöver övning.

Specifikationen kan vara felaktig. Du kanske har gjort ett misstag någonstans, eller kraven kan ha ändrats eller en förbättring kan behöva göras. Alla koder som någon använder måste ändras, så förr eller senare kommer specifikationen inte längre att matcha programmet. Helst, i det här fallet, måste du skriva en ny specifikation och helt skriva om koden. Vi vet mycket väl att ingen gör det. I praktiken patchar vi koden och uppdaterar eventuellt specifikationen. Om detta måste hända förr eller senare, varför skriva specifikationer överhuvudtaget? För det första, för den som ska redigera din kod kommer varje extra ord i specifikationen att vara guld värt, och den här personen kan mycket väl vara du själv. Jag kritiserar ofta mig själv för att jag inte får tillräckligt med specifikationer när jag redigerar min kod. Och jag skriver fler specifikationer än kod. Därför måste specifikationen alltid uppdateras när du redigerar koden. För det andra, för varje revision blir koden sämre, den blir svårare och svårare att läsa och underhålla. Detta är en ökning av entropin. Men om du inte börjar med en spec, så kommer varje rad du skriver att vara en redigering, och koden kommer att vara svårhanterlig och svår att läsa från början.

Som sagt Eisenhower, ingen strid vanns med plan, och ingen strid vanns utan en plan. Och han visste ett och annat om strider. Det finns en åsikt att skriva specifikationer är ett slöseri med tid. Ibland är detta sant, och uppgiften är så enkel att det inte finns något att tänka igenom. Men du ska alltid komma ihåg att när du blir tillsagd att inte skriva specifikationer, blir du tillsagd att inte tänka. Och du bör tänka på det varje gång. Att tänka igenom uppgiften garanterar inte att du inte kommer att göra misstag. Som vi vet var det ingen som uppfann trollstaven, och programmering är en svår uppgift. Men om du inte tänker igenom problemet kommer du garanterat att göra misstag.

Du kan läsa mer om TLA + och PlusCal på en speciell hemsida, du kan gå dit från min hemsida по ссылке. Det var allt för mig, tack för din uppmärksamhet.

Observera att detta är en översättning. När du skriver kommentarer, kom ihåg att författaren inte kommer att läsa dem. Om du verkligen vill chatta med författaren, då kommer han att vara med på Hydra 2019-konferensen, som kommer att hållas 11-12 juli 2019 i St. Petersburg. Biljetter kan köpas på den officiella webbplatsen.

Källa: will.com