Denne artikel er en oversættelse . Men før hende en lille introduktion. Hvordan dannes zombier? Alle kom i en situation, hvor de gerne vil trække en ven eller kollega op på deres niveau, men det lykkes ikke. Og det er ikke så meget hos dig som hos ham, at "det går ikke": På den ene side af skalaen er en normal løn, opgaver og så videre, og på den anden side behovet for at tænke. At tænke er ubehageligt og smertefuldt. Han giver hurtigt op og fortsætter med at skrive kode uden overhovedet at tænde for sin hjerne. Du forestiller dig, hvor mange kræfter det kræver at overvinde barrieren for indlært hjælpeløshed, og du gør det bare ikke. Sådan dannes zombier, som det ser ud til, kan helbredes, men det ser ud til, at ingen vil gøre det.
Da jeg så det (ja, samme kammerat fra lærebøgerne) og laver ikke en rapport, men en spørgsmål-og-svar session, var jeg lidt forsigtig. For en sikkerheds skyld er Leslie en verdensberømt videnskabsmand, forfatter til grundlæggende værker inden for distribueret databehandling, og du kan også kende ham med bogstaverne La i ordet LaTeX - "Lamport TeX". Den anden alarmerende faktor er hans krav: Alle, der kommer, skal (helt gratis) lytte til et par af hans rapporter på forhånd, komme med mindst et spørgsmål om dem, og først derefter komme. Jeg besluttede at se, hvad Lamport udsendte der - og det er fantastisk! Det er præcis den ting, den magiske link-pille til at helbrede zombier. Jeg advarer dig: Fra teksten kan elskere af superfleksible metoder og dem, der ikke kan lide at teste, hvad der er skrevet, især brænde ud.
Efter habrokat begynder oversættelsen af seminaret faktisk. God fornøjelse med at læse!
Uanset hvilken opgave du påtager dig, skal du altid gennemgå tre trin:
- beslutte hvilket mål du vil opnå;
- beslutte, hvordan du vil nå dit mål;
- komme til dit mål.
Det gælder også programmering. Når vi skriver kode, skal vi:
- beslutte, hvad programmet skal gøre;
- bestemme, hvordan den skal udføre sin opgave;
- skriv den tilsvarende kode.
Det sidste skridt er selvfølgelig meget vigtigt, men jeg vil ikke tale om det i dag. I stedet vil vi diskutere de to første. Hver programmør udfører dem, før de begynder at arbejde. Du sætter dig ikke ned for at skrive, medmindre du har besluttet dig for, om du skriver en browser eller en database. En vis idé om målet skal være til stede. Og du tænker bestemt over, hvad programmet præcist vil gøre, og skriv ikke på en eller anden måde i håb om, at koden på en eller anden måde bliver til en browser.
Hvordan sker denne kode-for-tænkning? Hvor meget indsats skal vi lægge i dette? Det hele afhænger af, hvor komplekst det problem, vi løser. Antag, at vi vil skrive et fejltolerant distribueret system. I dette tilfælde bør vi tænke tingene grundigt over, før vi sætter os ned for at kode. Hvad hvis vi bare skal øge en heltalsvariabel med 1? Umiddelbart er alt trivielt her, og der skal ingen tanke til, men så husker vi, at der kan opstå et overløb. Derfor, selv for at forstå, om et problem er simpelt eller komplekst, skal du først tænke.
Hvis du på forhånd tænker over mulige løsninger på problemet, kan du undgå fejl. Men dette kræver, at din tankegang er klar. For at opnå dette skal du skrive dine tanker ned. Jeg kan virkelig godt lide Dick Guindon-citatet: "Når du skriver, viser naturen dig, hvor sjusket din tankegang er." Hvis du ikke skriver, tror du kun, at du tænker. Og du skal skrive dine tanker ned i form af specifikationer.
Specifikationer udfører mange funktioner, især i store projekter. Men jeg vil kun tale om én af dem: de hjælper os med at tænke klart. At tænke klart er meget vigtigt og ret svært, så her har vi brug for hjælp. Hvilket sprog skal vi skrive specifikationer på? Generelt er dette altid det første spørgsmål for programmører: hvilket sprog vil vi skrive på. Der er ikke ét rigtigt svar på det: de problemer, vi løser, er for forskellige. For nogle er TLA+ et specifikationssprog, som jeg har udviklet. For andre er det mere bekvemt at bruge kinesisk. Alt afhænger af situationen.
Vigtigere er et andet spørgsmål: hvordan opnår man klarere tænkning? Svar: Vi skal tænke som videnskabsmænd. Dette er en måde at tænke på, som har bevist sig selv gennem de sidste 500 år. I naturvidenskab bygger vi matematiske modeller af virkeligheden. Astronomi var måske den første videnskab i ordets strenge forstand. I den matematiske model, der bruges i astronomi, optræder himmellegemer som punkter med masse, position og momentum, selvom de i virkeligheden er ekstremt komplekse objekter med bjerge og oceaner, tidevand og tidevand. Denne model, som enhver anden, blev skabt for at løse visse problemer. Det er fantastisk til at bestemme, hvor du skal pege teleskopet, hvis du skal finde en planet. Men hvis du vil forudsige vejret på denne planet, vil denne model ikke fungere.
Matematik giver os mulighed for at bestemme egenskaberne for en model. Og videnskaben viser, hvordan disse egenskaber relaterer sig til virkeligheden. Lad os tale om vores videnskab, datalogi. Den virkelighed, vi arbejder med, er computersystemer af forskellig art: processorer, spillekonsoller, computere, eksekverende programmer og så videre. Jeg vil tale om at køre et program på en computer, men i det store og hele gælder alle disse konklusioner for ethvert computersystem. I vores videnskab bruger vi mange forskellige modeller: Turing-maskinen, delvist bestilte sæt af begivenheder og mange andre.
Hvad er et program? Dette er enhver kode, der kan betragtes uafhængigt. Antag, at vi skal skrive en browser. Vi udfører tre opgaver: Vi designer brugerens syn på programmet, derefter skriver vi programmets højniveaudiagram, og til sidst skriver vi koden. Mens vi skriver koden, indser vi, at vi skal skrive en tekstformater. Her skal vi igen løse tre problemer: Bestem hvilken tekst dette værktøj vil returnere; vælg en algoritme til formatering; skrive kode. Denne opgave har sin egen underopgave: Indsæt en bindestreg korrekt i ord. Vi løser også denne delopgave i tre trin – som du kan se, gentages de på mange niveauer.
Lad os overveje mere detaljeret det første trin: hvilket problem programmet løser. Her modellerer vi oftest et program som en funktion, der tager noget input og producerer noget output. I matematik beskrives en funktion normalt som et ordnet sæt af par. For eksempel beskrives kvadreringsfunktionen for naturlige tal som mængden {<0,0>, <1,1>, <2,4>, <3,9>, …}. Domænet for en sådan funktion er mængden af de første elementer i hvert par, det vil sige de naturlige tal. For at definere en funktion skal vi angive dens omfang og formel.
Men funktioner i matematik er ikke det samme som funktioner i programmeringssprog. Matematikken er meget nemmere. Da jeg ikke har tid til komplekse eksempler, lad os overveje et simpelt: en funktion i C eller en statisk metode i Java, der returnerer den største fælles divisor af to heltal. I specifikationen af denne metode vil vi skrive: beregner GCD(M,N) for argumenter M и NHvor GCD(M,N) - en funktion, hvis domæne er sættet af par af heltal, og returværdien er det største heltal, der er deleligt med M и N. Hvordan forholder denne model sig til virkeligheden? Modellen opererer på heltal, mens vi i C eller Java har en 32-bit int. Denne model giver os mulighed for at afgøre, om algoritmen er korrekt GCD, men det forhindrer ikke overløbsfejl. Dette ville kræve en mere kompleks model, som der ikke er tid til.
Lad os tale om begrænsningerne ved en funktion som model. Nogle programmer (såsom operativsystemer) returnerer ikke bare en bestemt værdi for visse argumenter, de kan køre kontinuerligt. Derudover er funktionen som model ikke velegnet til det andet trin: planlægning af, hvordan problemet skal løses. Hurtig sortering og boblesortering beregner den samme funktion, men de er helt forskellige algoritmer. For at beskrive, hvordan målet med programmet nås, bruger jeg derfor en anden model, lad os kalde det standardadfærdsmodellen. Programmet i det er repræsenteret som et sæt af alle tilladte adfærd, som hver igen er en sekvens af tilstande, og tilstanden er tildelingen af værdier til variabler.
Lad os se, hvordan det andet trin for Euclid-algoritmen ville se ud. Vi skal beregne GCD(M, N). Vi initialiserer M som xOg N som y, træk derefter den mindste af disse variable gentagne gange fra de større, indtil de er ens. For eksempel hvis M = 12Og N = 18, kan vi beskrive følgende adfærd:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
Og hvis M = 0 и N = 0? Nul er deleligt med alle tal, så der er ingen største divisor i dette tilfælde. I denne situation skal vi gå tilbage til det første trin og spørge: skal vi virkelig beregne GCD for ikke-positive tal? Hvis dette ikke er nødvendigt, skal du blot ændre specifikationen.
Her bør vi lave en lille digression om produktivitet. Det måles ofte i antallet af kodelinjer skrevet om dagen. Men dit arbejde er meget mere nyttigt, hvis du slipper af med et vist antal linjer, fordi du har mindre plads til fejl. Og den nemmeste måde at slippe af med koden er ved første trin. Det er helt muligt, at du bare ikke har brug for alle de klokker og fløjter, du forsøger at implementere. Den hurtigste måde at forenkle et program og spare tid på er ikke at gøre ting, der ikke burde gøres. Det andet trin er det næstmest tidsbesparende potentiale. Hvis du måler produktivitet i form af skrevne linjer, vil det få dig til at tænke på, hvordan du udfører en opgave mindre produktiv, fordi du kan løse det samme problem med mindre kode. Jeg kan ikke give nøjagtige statistikker her, for jeg har ingen måde at tælle antallet af linjer, som jeg ikke skrev, fordi jeg brugte tid på specifikationen, det vil sige på det første og andet trin. Og forsøget kan heller ikke sættes op her, for i forsøget har vi ikke ret til at gennemføre det første trin, opgaven er forudbestemt.
Det er let at overse mange vanskeligheder i uformelle specifikationer. Der er ikke noget svært ved at skrive strenge specifikationer for funktioner, jeg vil ikke diskutere dette. I stedet vil vi tale om at skrive stærke specifikationer for standardadfærd. Der er et teorem, der siger, at ethvert sæt adfærd kan beskrives ved hjælp af sikkerhedsegenskaben (sikkerhed) og overlevelsesegenskaber (livlighed). Sikkerhed betyder, at intet dårligt vil ske, programmet vil ikke give et forkert svar. Overlevelsesevne betyder, at der før eller siden vil ske noget godt, det vil sige, at programmet før eller siden giver det rigtige svar. Som regel er sikkerhed en vigtigere indikator, her opstår der oftest fejl. For at spare tid vil jeg derfor ikke tale om overlevelsesevne, selvom det selvfølgelig også er vigtigt.
Vi opnår sikkerhed ved først at foreskrive et sæt af mulige begyndelsestilstande. Og for det andet, relationer med alle mulige næste stater for hver stat. Lad os opføre os som videnskabsmænd og definere tilstande matematisk. Sættet af begyndelsestilstande er beskrevet af en formel, for eksempel i tilfælde af Euklids algoritme: (x = M) ∧ (y = N). For visse værdier M и N der er kun én begyndelsestilstand. Forholdet til den næste tilstand beskrives med en formel, hvor variablerne i den næste tilstand skrives med et primtal, og variablerne i den aktuelle tilstand skrives uden et primtal. I tilfælde af Euklids algoritme vil vi beskæftige os med disjunktionen af to formler, hvoraf den ene x er den største værdi, og i den anden - y:
I det første tilfælde er den nye værdi af y lig med den tidligere værdi af y, og vi får den nye værdi af x ved at trække den mindre variabel fra den større. I det andet tilfælde gør vi det modsatte.
Lad os gå tilbage til Euklids algoritme. Lad os antage det igen M = 12, N = 18. Dette definerer en enkelt begyndelsestilstand, (x = 12) ∧ (y = 18). Vi sætter derefter disse værdier ind i formlen ovenfor og får:
Her er den eneste mulige løsning: x' = 18 - 12 ∧ y' = 12og vi får adfærden: [x = 12, y = 18]. På samme måde kan vi beskrive alle tilstande i vores adfærd: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
I sidste tilstand [x = 6, y = 6] begge dele af udtrykket vil være falsk, så det har ingen næste tilstand. Så vi har en komplet specifikation af det andet trin - som du kan se, er dette ganske almindelig matematik, som i ingeniører og videnskabsmænd, og ikke mærkeligt, som i datalogi.
Disse to formler kan kombineres til én formel for tidslogik. Hun er elegant og nem at forklare, men der er ikke tid til hende nu. Vi har måske kun brug for tidsmæssig logik for livlighedsejendommen, det er ikke nødvendigt for sikkerhed. Jeg bryder mig ikke som sådan om tidslogik, det er ikke helt almindelig matematik, men i tilfælde af livlighed er det et nødvendigt onde.
I Euklids algoritme, for hver værdi x и y har unikke værdier x' и y', som gør forholdet til den næste tilstand sand. Med andre ord er Euklids algoritme deterministisk. For at modellere en ikke-deterministisk algoritme skal den nuværende tilstand have flere mulige fremtidige tilstande, og at hver ikke-primede variabelværdi har flere primede variabelværdier, således at relationen til den næste tilstand er sand. Det er nemt at gøre, men jeg vil ikke give eksempler nu.
For at lave et arbejdsredskab har du brug for formel matematik. Hvordan gør man specifikationen formel? For at gøre dette har vi brug for et formelt sprog, f.eks. . Specifikationen af Euclid-algoritmen ville se sådan ud på dette sprog:
Et lighedstegnsymbol med en trekant betyder, at værdien til venstre for tegnet er defineret til at være lig med værdien til højre for tegnet. I det væsentlige er specifikationen en definition, i vores tilfælde to definitioner. Til specifikationen i TLA+ skal du tilføje deklarationer og noget syntaks, som i sliden ovenfor. I ASCII ville det se sådan ud:
Som du kan se, intet kompliceret. Specifikationen for TLA+ kan testes, dvs. omgå al mulig adfærd i en lille model. I vores tilfælde vil denne model være visse værdier M и N. Dette er en meget effektiv og enkel verifikationsmetode, der er fuldstændig automatisk. Det er også muligt at skrive formelle sandhedsbeviser og kontrollere dem mekanisk, men det tager meget tid, så næsten ingen gør dette.
Den største ulempe ved TLA+ er, at det er matematik, og programmører og dataloger er bange for matematik. Umiddelbart lyder det som en joke, men desværre mener jeg det i fuld alvor. Min kollega fortalte mig lige, hvordan han forsøgte at forklare TLA+ til flere udviklere. Så snart formlerne dukkede op på skærmen, blev de straks glasagtige øjne. Så hvis TLA+ skræmmer dig, kan du bruge , det er en slags legetøjsprogrammeringssprog. Et udtryk i PlusCal kan være et hvilket som helst TLA+-udtryk, det vil sige i det store og hele ethvert matematisk udtryk. Derudover har PlusCal en syntaks for ikke-deterministiske algoritmer. Fordi PlusCal kan skrive ethvert TLA+-udtryk, er PlusCal meget mere udtryksfuldt end noget rigtigt programmeringssprog. Dernæst er PlusCal kompileret til en letlæselig TLA+-specifikation. Dette betyder selvfølgelig ikke, at den komplekse PlusCal-specifikation bliver til en simpel en på TLA + - bare korrespondancen mellem dem er indlysende, der vil ikke være nogen yderligere kompleksitet. Endelig kan denne specifikation verificeres af TLA+ værktøjer. Alt i alt kan PlusCal hjælpe med at overvinde matematikfobi og er let at forstå selv for programmører og dataloger. Tidligere udgav jeg algoritmer på det i nogen tid (ca. 10 år).
Måske vil nogen indvende, at TLA + og PlusCal er matematik, og matematik virker kun på opfundne eksempler. I praksis har du brug for et rigtigt sprog med typer, procedurer, objekter og så videre. Det er forkert. Her er hvad Chris Newcomb, der arbejdede hos Amazon, skriver: "Vi har brugt TLA+ på ti store projekter, og i hvert tilfælde har brugen af det gjort en væsentlig forskel for udviklingen, fordi vi var i stand til at fange farlige fejl, før vi ramte produktionen, og fordi det gav os den indsigt og selvtillid, vi havde brug for lav aggressive præstationsoptimeringer uden at påvirke programmets sandhed". Man kan ofte høre, at ved brug af formelle metoder får vi ineffektiv kode – i praksis er alt det modsatte. Derudover er der en opfattelse af, at ledere ikke kan overbevises om behovet for formelle metoder, selvom programmører er overbeviste om deres anvendelighed. Og Newcomb skriver: "Ledere presser nu hårdt på for at skrive specifikationer til TLA + og afsætter specifikt tid til dette". Så når ledere ser, at TLA+ virker, accepterer de det gerne. Chris Newcomb skrev dette for omkring seks måneder siden (oktober 2014), men nu, så vidt jeg ved, bruges TLA+ i 14 projekter, ikke 10. Et andet eksempel vedrører designet af XBox 360. En praktikant kom til Charles Thacker og skrev specifikation for hukommelsessystemet. Takket være denne specifikation blev der fundet en fejl, som ellers ville forsvinde ubemærket, og på grund af hvilken hver XBox 360 ville gå ned efter fire timers brug. IBM-ingeniører bekræftede, at deres test ikke ville have fundet denne fejl.
Du kan læse mere om TLA + på internettet, men lad os nu tale om uformelle specifikationer. Vi skal sjældent skrive programmer, der udregner mindste fælles divisor og lignende. Meget oftere skriver vi programmer som det smukke printerværktøj, jeg skrev til TLA+. Efter den enkleste behandling vil TLA +-koden se sådan ud:
Men i ovenstående eksempel ønskede brugeren højst sandsynligt, at konjunktion- og lighedstegnene skulle justeres. Så den korrekte formatering ville se mere sådan ud:
Overvej et andet eksempel:
Her var justeringen af ligheds-, additions- og multiplikationstegnene i kilden tværtimod tilfældig, så den enkleste behandling er ganske nok. Generelt er der ingen nøjagtig matematisk definition af korrekt formatering, fordi "korrekt" i dette tilfælde betyder "hvad brugeren ønsker", og dette kan ikke bestemmes matematisk.
Det ser ud til, at hvis vi ikke har en definition af sandhed, så er specifikationen ubrugelig. Men det er det ikke. Bare fordi vi ikke ved, hvad et program skal gøre, betyder det ikke, at vi ikke behøver at tænke over, hvordan det fungerer – tværtimod skal vi lægge endnu mere kræfter i det. Specifikationen er især vigtig her. Det er umuligt at bestemme det optimale program til struktureret udskrivning, men det betyder ikke, at vi slet ikke skal tage det, og at skrive kode som en strøm af bevidsthed er ikke en god ting. Til sidst skrev jeg en specifikation af seks regler med definitioner i form af kommentarer i en java-fil. Her er et eksempel på en af reglerne: a left-comment token is LeftComment aligned with its covering token. Denne regel er skrevet på, skal vi sige, matematisk engelsk: LeftComment aligned, left-comment и covering token - termer med definitioner. Sådan beskriver matematikere matematik: De skriver definitioner af begreber og ud fra dem regler. Fordelen ved en sådan specifikation er, at seks regler er meget nemmere at forstå og fejlfinde end 850 linjer kode. Jeg må sige, at det ikke var let at skrive disse regler, det tog ret lang tid at fejlsøge dem. Specielt til dette formål skrev jeg en kode, der rapporterede, hvilken regel der blev brugt. Takket være det faktum, at jeg testede disse seks regler på flere eksempler, behøvede jeg ikke at fejlsøge 850 linjer kode, og fejl viste sig at være ret nemme at finde. Java har gode værktøjer til dette. Hvis jeg bare havde skrevet koden, ville det have taget mig meget længere tid, og formateringen ville have været af dårligere kvalitet.
Hvorfor kunne en formel specifikation ikke bruges? På den ene side er den korrekte udførelse ikke så vigtig her. Strukturelle udskrifter er bundet til ikke at behage nogen, så jeg behøvede ikke at få det til at fungere rigtigt i alle de mærkelige situationer. Endnu vigtigere er det faktum, at jeg ikke havde tilstrækkeligt værktøj. TLA+ modelcheckeren er ubrugelig her, så jeg bliver nødt til manuelt at skrive eksemplerne.
Ovenstående specifikation har funktioner, der er fælles for alle specifikationer. Det er højere niveau end koden. Det kan implementeres på ethvert sprog. Alle værktøjer eller metoder er ubrugelige til at skrive det. Intet programmeringskursus vil hjælpe dig med at skrive denne specifikation. Og der er ingen værktøjer, der kan gøre denne specifikation unødvendig, medmindre du selvfølgelig skriver et sprog specifikt til at skrive strukturerede printprogrammer i TLA+. Endelig siger denne specifikation ikke noget om præcis hvordan vi vil skrive koden, den angiver kun hvad denne kode gør. Vi skriver specifikationen for at hjælpe os med at tænke problemet igennem, før vi begynder at tænke på koden.
Men denne specifikation har også funktioner, der adskiller den fra andre specifikationer. 95 % af andre specifikationer er væsentligt kortere og enklere:
Yderligere er denne specifikation et sæt regler. Som regel er dette et tegn på dårlig specifikation. Det er ret svært at forstå konsekvenserne af et sæt regler, hvorfor jeg skulle bruge meget tid på at fejlsøge dem. Men i dette tilfælde kunne jeg ikke finde en bedre måde.
Det er værd at sige et par ord om programmer, der kører kontinuerligt. Som regel arbejder de parallelt, for eksempel operativsystemer eller distribuerede systemer. Meget få mennesker kan forstå dem mentalt eller på papiret, og jeg er ikke en af dem, selvom jeg engang var i stand til det. Derfor har vi brug for værktøjer, der vil tjekke vores arbejde - for eksempel TLA + eller PlusCal.
Hvorfor var det nødvendigt at skrive en specifikation, hvis jeg allerede vidste, hvad koden præcis skulle gøre? Faktisk troede jeg bare, at jeg vidste det. Derudover behøver en udenforstående med en specifikation ikke længere at komme ind i koden for at forstå, hvad han præcis gør. Jeg har en regel: der skal ikke være generelle regler. Der er en undtagelse til denne regel, selvfølgelig, det er den eneste generelle regel, jeg følger: specifikationen af, hvad koden gør, skal fortælle folk alt, hvad de behøver at vide, når de bruger koden.
Så hvad er det præcist, programmører skal vide om tænkning? Til at begynde med, det samme som alle andre: hvis du ikke skriver, så ser det kun ud til, at du tænker. Du skal også tænke før du koder, hvilket betyder at du skal skrive før du koder. Specifikationen er, hvad vi skriver, før vi begynder at kode. En specifikation er nødvendig for enhver kode, der kan bruges eller ændres af enhver. Og denne "nogen" er måske selv forfatteren af koden en måned efter den blev skrevet. En specifikation er nødvendig for store programmer og systemer, for klasser, for metoder og nogle gange endda for komplekse sektioner af en enkelt metode. Hvad skal der præcist skrives om koden? Du skal beskrive, hvad den gør, det vil sige, hvad der kan være nyttigt for enhver person, der bruger denne kode. Nogle gange kan det også være nødvendigt at specificere, hvordan koden opfylder sit formål. Hvis vi gennemgik denne metode i løbet af algoritmer, så kalder vi det en algoritme. Hvis det er noget mere specielt og nyt, så kalder vi det design på højt niveau. Der er ingen formel forskel her: begge er en abstrakt model af et program.
Hvordan præcist skal du skrive en kodespecifikation? Det vigtigste: det skal være et niveau højere end selve koden. Den skal beskrive tilstande og adfærd. Det skal være så strengt, som opgaven kræver. Hvis du skriver en specifikation for, hvordan en opgave skal implementeres, kan du skrive den i pseudokode eller med PlusCal. Du skal lære at skrive specifikationer på formelle specifikationer. Dette vil give dig de nødvendige færdigheder, der også vil hjælpe dig med uformelle. Hvordan lærer man at skrive formelle specifikationer? Da vi lærte at programmere, skrev vi programmer og fejlede dem derefter. Det er det samme her: skriv specifikationerne, tjek det med modelcheckeren, og ret fejlene. TLA+ er muligvis ikke det bedste sprog til en formel specifikation, og et andet sprog vil sandsynligvis være bedre til dine specifikke behov. Fordelen ved TLA+ er, at det lærer matematisk tænkning meget godt.
Hvordan forbinder man specifikation og kode? Ved hjælp af kommentarer, der forbinder matematiske begreber og deres implementering. Hvis du arbejder med grafer, vil du på programniveau have arrays af noder og arrays af links. Derfor skal du skrive præcis, hvordan grafen er implementeret af disse programmeringsstrukturer.
Det skal bemærkes, at intet af ovenstående gælder for selve processen med at skrive kode. Når du skriver koden, altså udfører det tredje trin, skal du også tænke og gennemtænke programmet. Hvis en delopgave viser sig at være kompleks eller ikke-indlysende, skal du skrive en specifikation for den. Men jeg taler ikke om selve koden her. Du kan bruge et hvilket som helst programmeringssprog, enhver metode, det handler ikke om dem. Intet af ovenstående eliminerer heller behovet for at teste og fejlfinde kode. Selvom den abstrakte model er skrevet korrekt, kan der være fejl i dens implementering.
At skrive specifikationer er et ekstra trin i kodningsprocessen. Takket være det kan mange fejl fanges med mindre indsats - det ved vi fra erfaringen fra programmører fra Amazon. Med specifikationer bliver kvaliteten af programmer højere. Så hvorfor går vi så ofte uden dem? Fordi det er svært at skrive. Og at skrive er svært, for her skal du tænke, og det er også svært at tænke. Det er altid nemmere at lade som om, hvad du tænker. Her kan du tegne en analogi med løb – jo mindre du løber, jo langsommere løber du. Du skal træne dine muskler og øve dig i at skrive. Brug for øvelse.
Specifikationen kan være forkert. Du kan have lavet en fejl et sted, eller kravene kan have ændret sig, eller der skal muligvis foretages en forbedring. Enhver kode, som nogen bruger, skal ændres, så før eller siden vil specifikationen ikke længere matche programmet. Ideelt set skal du i dette tilfælde skrive en ny specifikation og fuldstændigt omskrive koden. Vi ved godt, at ingen gør det. I praksis patcher vi koden og opdaterer eventuelt specifikationen. Hvis dette er bundet til at ske før eller siden, hvorfor så overhovedet skrive specifikationer? For det første, for den person, der vil redigere din kode, vil hvert ekstra ord i specifikationen være guld værd, og denne person kan meget vel være dig selv. Jeg udskælder ofte mig selv for ikke at have nok specifikationer, når jeg redigerer min kode. Og jeg skriver flere specifikationer end kode. Når du redigerer koden, skal specifikationen derfor altid opdateres. For det andet, med hver revision, bliver koden værre, den bliver mere og mere vanskelig at læse og vedligeholde. Dette er en stigning i entropi. Men hvis du ikke starter med en spec, så vil hver linje du skriver være en redigering, og koden vil være uhåndterlig og svær at læse fra starten.
Som sagt , ingen kamp blev vundet efter plan, og ingen kamp blev vundet uden en plan. Og han vidste en ting eller to om kampe. Der er en opfattelse af, at det er spild af tid at skrive specifikationer. Nogle gange er det sandt, og opgaven er så enkel, at der ikke er noget at tænke igennem. Men du skal altid huske, at når du får besked på ikke at skrive specifikationer, får du besked på ikke at tænke. Og du bør tænke over det hver gang. At gennemtænke opgaven garanterer ikke, at du ikke laver fejl. Som vi ved, var der ingen, der opfandt tryllestaven, og programmering er en vanskelig opgave. Men hvis du ikke tænker problemet igennem, vil du med garanti begå fejl.
Du kan læse mere om TLA + og PlusCal på en særlig hjemmeside, du kan gå dertil fra min hjemmeside . Det var alt for mig, tak for din opmærksomhed.
Bemærk venligst, at dette er en oversættelse. Når du skriver kommentarer, så husk, at forfatteren ikke vil læse dem. Hvis du virkelig vil chatte med forfatteren, så vil han være til Hydra 2019-konferencen, som afholdes 11.-12. juli 2019 i St. Petersborg. Billetter kan købes .
Kilde: www.habr.com