Denne artikel er en oversættelse . Men før det, en kort introduktion. Hvordan bliver zombies til? Alle har været i en situation, hvor man ønsker at løfte en ven eller kollega op til sit eget niveau, men det lykkes ikke. Og det er ikke så meget dit problem som hans: på den ene side står en god løn, opgaver og så videre, mens den anden side kræver, at man tænker. At tænke er ubehageligt og smertefuldt. Han giver hurtigt op og fortsætter med at skrive kode uden at bruge sin hjerne. Kan du forestille dig, hvor meget energi det kræver at overvinde barrieren af indlært hjælpeløshed, og derfor gør man det bare ikke. Sådan bliver der dannet zombies, som tilsyneladende kan helbredes, men ingen tager sig egentlig af det.
Da jeg så, at (ja, ja, den samme fyr fra lærebøgerne) og ikke holdt et foredrag, men en spørgsmål-svar session, blev jeg lidt bekymret. For en sikkerheds skyld, Leslie er en verdenskendt forsker, forfatter til grundlæggende værker inden for distribueret computing, og du kender ham måske fra bogstaverne La i ordet LaTeX — "Lamport TeX". Den anden bekymrende faktor er hans krav: alle, der kommer, skal (helt gratis) på forhånd have lyttet til et par af hans foredrag, finde på mindst ét spørgsmål til dem, og kun så komme. Jeg besluttede at se, hvad Lәмпорт prædiker — og det er fantastisk! Det er præcis den ting, det magiske link-piller til behandling af zombietilstand. Jeg advarer: tekstens indhold kan virke noget provokerende for tilhængere af super fleksible metoder og dem, der ikke bryder sig om at teste deres skrivearbejde.
Efter housetweetet begynder selve oversættelsen af seminaret. God læsning!
Uanset hvilken opgave du påtager dig, skal du altid gennemgå tre trin:
- bestemme, hvilket mål du ønsker at opnå;
- beslutte, hvordan du vil nå dit mål;
- nå dit mål.
Dette gælder også programmering. Når vi skriver kode, er det nødvendigt at:
- bestemme, hvad programmet præcist skal gøre;
- definere, hvordan det skal udføre sin opgave;
- skrive den relevante kode.
Det sidste skridt er naturligvis meget vigtigt, men jeg vil ikke tale om det i dag. I stedet vil vi diskutere de første to. Disse udføres af hver programmør, før de går i gang med arbejdet. Man sætter sig ikke ned for at skrive, hvis man ikke har besluttet, hvad man præcist skriver: en browser eller en database. En klar forståelse af målet skal være til stede. Og man overvejer absolut, hvad programmet præcist vil gøre, snarere end blot at skrive tilfældigt i håbet om, at koden selv vil blive til en browser.
Hvordan foregår denne forudgående overvejelse af koden egentlig? Hvor meget indsats skal vi investere i det? Det afhænger af, hvor kompleks et problem vi løser. Lad os antage, at vi ønsker at skrive et fejlrobust distribueret system. I så fald bør vi overveje alt grundigt, før vi sætter os ned for at kode. Men hvis vi bare skal øge en heltalvariabel med 1? Ved første øjekast virker dette trivielt, og der er ikke behov for overvejelser, men så husker vi, at vi kan få et overløb. Derfor, for at forstå, om problemet er simpelt eller komplekst, er det først nødvendigt at tænke.
Ved at overveje mulige løsninger på et problem på forhånd kan man undgå fejl. Men for dette er det nødvendigt, at ens tankegang er klar. For at opnå dette skal man nedskrive sine tanker. Jeg kan meget godt lide citatet fra Dick Hindle: "Når du skriver, viser naturen dig, hvor rodet dit tænkning er." Hvis du ikke skriver, så synes du blot, at du tænker. Og man skal nedskrive sine tanker 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 enhver støtte. Hvilket sprog skal vi bruge til at skrive specifikationerne? Dette er generelt altid det første spørgsmål for programmører: hvilket sprog vil vi skrive på. Der er ikke et enkelt rigtigt svar på det: problemerne, vi løser, er alt for forskellige. For nogle er TLA+ nyttigt — et specifikationssprog, som jeg har udviklet. For andre er det lettere at bruge kinesisk. Det afhænger af situationen.
Et mere vigtigt spørgsmål er: hvordan opnår vi klarere tænkning? Svaret er: vi må tænke som videnskabsfolk. Dette er en tænkemåde, der har vist sig effektiv i de sidste 500 år. Inden for videnskab bygger vi matematiske modeller af virkeligheden. Astronomi var måske den første videnskab i strengt forstand. I den matematiske model, der anvendes i astronomi, repræsenteres himmellegemer som punkter med masse, position og momentum, selvom de i virkeligheden er ekstremt komplekse objekter med bjerge og oceaner, tidevandsbevægelser osv. Denne model, ligesom enhver anden, er skabt til at løse specifikke opgaver. Den fungerer glimrende til at afgøre, hvor teleskopet skal rettes, hvis man skal finde en planet. Men hvis du ønsker at forudsige vejret på denne planet, er denne model ikke tilstrækkelig.
Matematik hjælper os med at bestemme modellens egenskaber. Og videnskab viser, hvordan disse egenskaber relaterer til virkeligheden. Lad os tale om vores videnskab, computer science. Den virkelighed, vi arbejder med, er beregningssystemer af forskellige typer: processorer, spilkonsoller, computere, der kører programmer osv. Jeg vil tale om at køre et program på en computer, men i det store hele gælder alle disse konklusioner for enhver beregningssystem. I vores videnskab anvender vi mange forskellige modeller: Turing-maskinen, delvist ordnede sæt af hændelser og mange andre.
Hvad er et program? Det er enhver kode, der kan betragtes selvstændigt. Lad os antage, at vi skal skrive en browser. Vi udfører tre opgaver: designe programmets præsentation for brugeren, derefter skrive et overordnet programdiagram og til sidst skrive koden. Under skrivningen af koden indser vi, at vi har brug for at skrive et værktøj til tekstformatering. Her skal vi igen løse tre opgaver: definere, hvilken tekst dette værktøj skal returnere; vælge en algoritme til formatering; skrive koden. Denne opgave har en delopgave: korrekt indsætte bindestreger i ord. Denne delopgave løser vi også i tre trin — som vi ser, gentages de på mange niveauer.
Lad os se nærmere på det første skridt: hvilken opgave programmet løser. Her modellerer vi oftest et program som en funktion, der modtager visse inddata og genererer nogle uddata. I matematik beskrives en funktion typisk som et ordnet sæt af par. For eksempel beskrives funktionen for kvadrering af naturlige tal som sættet {, , , , ...}. Funktionsområdet for en sådan funktion er mængden af de første elementer i hvert par, det vil sige naturlige tal. For at definere en funktion skal vi angive dens definitionsmængde og formel.
Men funktioner i matematik er ikke det samme som funktioner i programmeringssprog. Matematik er betydeligt enklere. Da jeg ikke har tid til komplekse eksempler, lad os tage et simpelt: en funktion i C eller en statisk metode i Java, der returnerer den største fælles divisor (GCD) af to heltal. I specifikationen for denne metode skriver vi: beregner GCD(M,N) for argumenter M og N, hvor GCD(M,N) — en funktion, hvis definitionsmængde er mængden af par af heltal, og hvis returværdi er det største heltal, der deler M og N. Hvordan relaterer denne model sig til virkeligheden? Modellen arbejder med heltal, mens vi i C eller Java har 32-bit int. Denne model gør det muligt for os at afgøre, om algoritmen er korrekt GCD, men den forhindrer ikke overflow-fejl. For dette ville en mere kompleks model være nødvendig, men der er ikke tid til det.
Lad os tale om begrænsningerne ved funktionen som model. Nogle programmers (f.eks. operativsystemers) arbejde reduceres ikke blot til at returnere en bestemt værdi for bestemte argumenter; de kan køre kontinuerligt. Desuden er funktionen som model dårligt egnet til det andet skridt: planlægning af, hvordan opgaven skal løses. Quick sort og bubble sort beregner den samme funktion, men det er helt forskellige algoritmer. Derfor bruger jeg en anden model til at beskrive, hvordan programmet når sit mål, som vi kalder den standard adfærdsmodel. I denne model præsenteres programmet som mængden af alle tilladte adfærd, hvor hver af disse igen er en sekvens af tilstande, og en tilstand er tildelingen af værdier til variabler.
Lad os se på, hvordan det andet trin i Euklids algoritme vil se ud. Vi skal beregne GCD(M, N). Vi initialiserer M hvordan x, og N hvordan y, og trækker derefter den mindste af disse variabler fra den større, indtil de er ens. For eksempel, hvis M = 12, og N = 18, kan vi beskrive den følgende adfærd:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
Og hvis M = 0 og N = 0? Ноль делится на все числа, поэтому наибольшего делителя в этом случае нет. В этой ситуации нам нужно вернуться к первому шагу и спросить: действительно ли нам нужно вычислять НОД для неположительных чисел? Если в этом нет необходимости, то нужно просто изменить спецификацию.
Her skal jeg lave en kort bemærkning om produktivitet. Den måles ofte i antal linjer kode skrevet om dagen. Men dit arbejde er langt mere værdifuldt, hvis du har skåret ned på et bestemt antal linjer, fordi du så har færre muligheder for fejl. Og det er nemmest at fjerne kode i det første trin. Det er meget muligt, at du slet ikke har brug for alt det halløj, du forsøger at implementere. Den hurtigste måde at forenkle programmet og spare tid på er at undlade at gøre ting, som ikke er værd at gøre. Det andet trin er det næsthøjeste i potentialet for tidsbesparelser. Hvis du måler produktivitet i antal skrevne linjer, så vil overvejelse om, hvordan opgaven skal udføres, gøre dig mindre produktiv, da du kan løse den samme opgave med mindre kode. Jeg kan ikke give dig nøjagtig statistik her, fordi jeg ikke har en metode til at tælle det antal linjer, jeg ikke har skrevet, takket være at jeg brugte tid på specifikationen, altså på de første to trin. Og et eksperiment kan heller ikke udføres her, fordi vi i et eksperiment ikke har ret til at udføre første trin, da opgaven er fastlagt på forhånd.
I uformelle specifikationer er det let at overse mange vanskeligheder. Der er ikke noget svært ved at skrive strenge specifikationer for funktioner, og det vil jeg ikke diskutere. I stedet vil vi tale om at skrive strenge specifikationer for standard adfærdsmønstre. Der er en sætning, der siger, at enhver mængde adfærd kan beskrives ved hjælp af sikkerhedsegenskaber (safety) og livsduelighedsegenskaber (liveness). Sikkerhed betyder, at intet dårligt vil ske, programmet vil ikke give et forkert svar. Levetid betyder, at der før eller senere vil ske noget godt, nemlig at programmet før eller senere vil give det rigtige svar. Som regel er sikkerhed en vigtigere indikator, fejl opstår oftest her. Derfor vil jeg for at spare tid ikke tale om levetid, selvom det selvfølgelig også er vigtigt.
Vi opnår sikkerhed ved at beskrive, for det første, mange mulige starttilstande. Og for det andet, relationer til alle mulige følgende tilstande for hver tilstand. Vi vil opføre os som forskere og definere tilstande matematik. Sættet af starttilstande beskrives med en formel, for eksempel i tilfælde af Euklids algoritme: (x = M) ∧ (y = N). For bestemte værdier M og N er der kun én starttilstand. Forholdet til den følgende tilstand beskrives med en formel, hvor variablerne for den følgende tilstand skrives med en streg, og den aktuelle tilstand uden streg. I tilfælde af Euklids algoritme vil vi have med disjunktion af to formler at gøre, hvor den ene x er den største værdi, og den anden er y:
I det første tilfælde er den nye værdi y lig med den tidligere værdi y, og den nye værdi x får vi ved at trække den mindre variabel fra den større. I det andet tilfælde gør vi det modsatte.
Lad os vende tilbage til Euklids algoritme. Antag igen, at M = 12, N = 18. Dette definerer den eneste starttilstand, (x = 12) ∧ (y = 18). Derefter indsætter vi disse værdier i formlen ovenfor og får:
Her er den eneste mulige løsning: x' = 18 - 12 ∧ y' = 12, og vi får en adfærd: [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 den sidste tilstand [x = 6, y = 6] vil begge dele af udtrykket være falske, derfor har den ikke en næste tilstand. Så vi har en fuldstændig specifikation af det andet trin – som vi ser, er dette ret almindelig matematik, som hos ingeniører og forskere, og ikke underlig, som i computer science.
Disse to formler kan samles i én formel for tidslogik. Den er elegant og let at forklare, men der er ikke tid til det nu. Tidslogik kan være nødvendig for livs-egenskaber, men for sikkerhed er den ikke nødvendig. Tidslogik i sig selv er ikke populært; det er ikke helt almindelig matematik, men i forbindelse med liv er det et nødvendigt onde.
I Euklids algoritme for hver værdi x og y er der unikke værdier x' og y', som gør forholdet med den næste tilstand sandt. Med andre ord er Euklids algoritme determineret. For at modellere en ikke-determineret algoritme skal den nuværende tilstand have flere mulige fremtidige tilstande, og hver værdi af variablen uden streg skal have flere værdier af variablen med streg, hvor forholdet med den næste tilstand er sandt. Det er ikke svært at gøre, men jeg vil ikke give eksempler lige nu.
For at lave et fungerende værktøj er der brug for formel matematik. Hvordan laver man en formel specifikation? Til det har vi brug for et formelt sprog, for eksempel . Specifikationen af Euklids algoritme ville se således ud på dette sprog:
Symbolet for lighedstegn med en trekant betyder, at værdien til venstre for lighedstegnet er defineret som lig med værdien til højre for lighedstegnet. I essensen er en specifikation en definition; i vores tilfælde to definitioner. Til specifikationen i TLA+ skal der tilføjes erklæringer og en vis syntaks, som vist på diassene ovenfor. I ASCII ville det se sådan ud:
Som vi kan se, er der ikke noget kompliceret. Specifikationen i TLA+ kan verificeres, dvs. man kan gennemgå alle mulige adfærd i en lille model. I vores tilfælde vil denne model være de bestemte værdier M og N. Dette er en meget effektiv og enkel måde at verificere på, som helt udføres automatisk. Derudover kan man skrive formelle beviser for sandhed og verificere dem mekanisk, men det kræver meget tid, så næsten ingen gør det.
Den største ulempe ved TLA+ er, at det er matematik, og programmører samt computer science-folk er bange for matematik. Ved første øjekast lyder det som en vittighed, men desværre mener jeg det helt alvorligt. En kollega fortalte mig netop, hvordan han forsøgte at forklare TLA+ til nogle udviklere. Så snart formlerne dukkede op på skærmen, fik de straks glasagtige øjne. Så hvis TLA+ er skræmmende, kan man bruge , som er en slags legetøjs programmeringssprog. Et udtryk i PlusCal kan være et hvilket som helst TLA+-udtryk, det vil sige, stort set et hvilket som helst matematisk udtryk. Derudover har PlusCal en syntaks til ikke-deterministiske algoritmer. Fordi man kan skrive et hvilket som helst TLA+-udtryk i PlusCal, er det betydeligt mere udtryksfuldt end ethvert virkeligt programmeringssprog. PlusCal kompileres til en letlæselig specifikation i TLA+. Det betyder ikke, at en kompliceret PlusCal-specifikation bliver enkel i TLA+ — bare at der er en åbenlys overensstemmelse mellem dem, uden ekstra kompleksitet. Endelig kan denne specification kontrolleres med TLA+-værktøjer. Generelt kan PlusCal hjælpe med at overvinde matematikfobien, det er let at forstå, selv for programmører og computer science-folk. Tidligere publicerede jeg algoritmer på det i omkring 10 år.
Måske vil nogen indvende, at TLA+ og PlusCal er matematik, og at matematik kun fungerer på opfundne eksempler. I praksis er der dog brug for et reelt sprog med typer, procedurer, objekter osv. Det er ikke tilfældet. Her er, hvad Chris Newcomb, som arbejdede hos Amazon, skriver: «Vi har brugt TLA+ i ti store projekter, og i hvert tilfælde har dets anvendelse haft en betydelig indflydelse på udviklingen, fordi vi kunne fange farlige fejl, inden de nåede produktion, og fordi det gav os den forståelse og selvsikkerhed, der var nødvendig for aggressive optimeringer af ydeevnen uden at påvirke programmets korrekthed». Man hører ofte, at brugen af formelle metoder resulterer i ineffektiv kode — i praksis er det helt omvendt. Derudover er der en almen opfattelse af, at man ikke kan overbevise ledere om nødvendigheden af formelle metoder, selvom programmører er overbevist om deres nytteværdi. Og Newcomb skriver: «Ledere opfordrer nu på alle måder til at skrive specifikationer i TLA+, og de giver endda tid til det.». Så når lederne ser, at TLA+ fungerer, tager de det gladeligt til sig. Chris Newcomb skrev dette for omkring seks måneder siden (i oktober 2014), og nu, så vidt jeg ved, anvendes TLA+ i 14 projekter, snarere end 10. Et andet eksempel relaterer sig til designet af Xbox 360. En praktikant kom til Charles Tecker og skrev en specifikation for hukommelsessystemet. Takket være denne specifikation blev en fejl opdaget, som ellers ville være gået ubemærket hen, og som ville have fået hver Xbox 360 til at gå ned efter fire timers brug. Ingeniører fra IBM bekræftede, at deres tests ikke ville have opdaget denne fejl.
Mere detaljeret om TLA+ kan du læse om på internettet, men lad os nu tale om uformelle specifikationer. Vi skriver sjældent programmer, der beregner den mindste fælles divisor og lignende. Langt oftere skriver vi programmer som en strukturel formatteringsværktøj (pretty-printer), som jeg har skrevet til TLA+. Efter den enkleste behandling ville koden for TLA+ se således ud:
Men i det angivne eksempel ville brugeren sandsynligvis have ønsket, at konjunktioner og lighedstegn var justeret. Så den korrekte formatering ville se mere sådan ud:
Lad os overveje et andet eksempel:
Herimod var justeringen af lighedstegn, plus- og gangeting i kilden tilfældig, så den enkleste behandling er fuldt tilstrækkelig. Generelt findes der ikke en nøjagtig matematisk definition af korrekt formatering, fordi "korrekt" i dette tilfælde betyder "sådan som brugeren ønsker det", hvilket ikke kan defineres matematisk.
Det virker som om, at hvis vi ikke har en definition af sandhed, så er specifikationen ubrugelig. Men det er ikke tilfældet. Hvis vi ikke ved, hvad programmet præcist skal gøre, betyder det ikke, at vi ikke skal tænke over, hvordan det skal fungere — tværtimod, vi bør investere endnu mere tid i det. Specifikationen er her særlig vigtig. Det er umuligt at definere det optimale program til strukturel formattering, men det betyder ikke, at vi ikke skal forsøge at lave det overhovedet, og at skrive koden som en strøm af bevidsthed — det er ikke sagen. I sidste ende skrev jeg en specifikation med seks regler med definitioner i form af kommentarer i Java-filen. Her er et eksempel på en af reglerne: et left-comment-token er LeftComment, som er justeret med sit dækket token. Denne regel er skrevet på, lad os sige, matematisk engelsk: LeftComment justeret, left-comment og dækket token — termer med definitioner. Dette er, hvordan matematikere beskriver matematik: de skriver definitioner af termer og baserer regler på dem. Fordelen ved en sådan specifikation er, at det er meget lettere at forstå og debugge seks regler end 850 linjer kode. Jeg må sige, at det var en udfordring at skrive disse regler; det tog ret lang tid at debugge dem. Specifikt til dette formål skrev jeg kode, der informerede mig om, hvilken regel der anvendtes. Takket være at jeg testede disse seks regler med flere eksempler, havde jeg ikke brug for at debugge 850 linjer kode, og fejlene var ret nemme at finde. Der findes fremragende værktøjer til dette i Java. Hvis jeg bare havde skrevet koden, ville det tage betydeligt længere tid, og formateringen ville være af dårligere kvalitet.
Hvorfor kunne man ikke bruge en formel specifikation? På den ene side er korrektheden her ikke så vigtig. Den strukturelle udskrift vil helt sikkert ikke glæde alle, så jeg havde ikke brug for at sikre, at den fungerede korrekt i alle usædvanlige situationer. Endnu vigtigere er det, at jeg ikke havde ordentlige værktøjer. TLA+ modelverifikationen er her ubrugelig, så jeg skulle have skrevet eksempler manuelt.
Den givne specifikation har træk, der er fælles for alle specifikationer. Den er på et højere niveau end koden. Den kan implementeres på ethvert sprog. Det er ubrugeligt at anvende værktøjer eller metoder til at skrive den. Ingen programmeringskurser vil hjælpe dig med at skrive denne specifikation. Og der findes ingen værktøjer, der kunne gøre denne specifikation overflødig, medmindre du selvfølgelig skriver et sprog specifikt til strukturudskrivningsprogrammering på TLA+. Endelig siger denne specifikation intet om, hvordan vi præcist vil skrive koden; den angiver kun, hvad denne kode gør. Vi skriver specifikationen for at hjælpe os med at overveje problemet, før vi begynder at tænke på koden.
Men denne specifikation har også nogle særlige træk, der adskiller den fra andre specifikationer. 95% af andre specifikationer er betydeligt kortere og enklere:
Derudover er denne specifikation et sæt regler. Som regel er dette et tegn på en dårlig specifikation. At forstå konsekvenserne af et sæt regler er ret vanskeligt, og derfor har jeg brugt meget tid på at debugge dem. Ikke desto mindre kunne jeg ikke finde en bedre måde i dette tilfælde.
Det er værd at sige et par ord om programmer, der kører kontinuerligt. Som regel kører de parallelt, som for eksempel operativsystemer eller distribuerede systemer. Meget få kan forstå dem i tankerne eller på papir, og jeg regner mig ikke blandt dem, selvom jeg engang kunne. Derfor er der behov for værktøjer, der kan kontrollere vores arbejde - for eksempel TLA+ eller PlusCal.
Hvorfor skulle jeg skrive en specifikation, når jeg allerede vidste, hvad koden skulle gøre? Faktisk troede jeg kun, at jeg vidste det. Derudover, med en specifikation, behøver en udenforstående ikke at døje med koden for at forstå, hvad den gør. Jeg har en regel: der bør ikke være nogen generelle regler. Denne regel har selvfølgelig en undtagelse; det er den eneste generelle regel, jeg følger: specifikationen for, hvad koden gør, skal informere folk om alt, hvad de behøver at vide, når de bruger denne kode.
Så hvad skal programmører vide om tankegang? For det første det samme som alle andre: hvis du ikke skriver, så tror du blot, at du tænker. Derudover skal du tænke, før du koder, hvilket betyder, at du skal skrive, før du koder. Specifikation er det, vi skriver, inden vi begynder at kode. En specifikation er nødvendig for enhver kode, der kan bruges eller ændres af nogen. Og dette "nogen" kan være koden forfatter selv en måned efter dens skrivning. Specifikation er nødvendig for store programmer og systemer, for klasser, for metoder og nogle gange endda for komplekse dele af en enkelt metode. Hvad skal man specifikt skrive om koden? Man skal beskrive, hvad den gør, altså hvad der kan være nyttigt for enhver, der bruger denne kode. Nogle gange kan det også være nødvendigt at angive, hvordan koden når sit mål. Hvis vi har gennemgået denne metode i algoritmekurset, kalder vi det en algoritme. Hvis det er noget mere specielt og nyt, kalder vi det højniveau design. Der er ingen formel forskel her: begge er abstrakte modeller af programmet.
Hvordan skal man egentlig skrive en kode-specifikation? Hovedpunkten: den skal være et niveau højere end selve koden. Den skal beskrive tilstande og adfærd. Den skal være så streng, som opgaven kræver. Hvis du skriver en specifikation for en opgaves implementeringsmetode, kan den skrives i pseudokode eller med PlusCal. Man skal lære at skrive specifikationer på formelle specifikationer. Dette vil give dig de nødvendige færdigheder, som også vil hjælpe med de uformelle. Men hvordan lærer man at skrive formelle specifikationer? Da vi lærte programmering, skrev vi programmer og fejlfandt dem. Det samme gælder her: man skal skrive en specifikation, kontrollere den med et model-checking værktøj og rette fejlene. TLA+ er muligvis ikke det bedste sprog til formel specifikation, og til dine specifikke behov vil sandsynligvis et andet sprog være bedre egnet. Fordelen ved TLA+ er, at det fremragende lærer matematisk tænkning.
Hvordan forbinder man specifikationen med koden? Gennem kommentarer, der forbinder matematiske begreber med deres implementering. Hvis du arbejder med grafer, vil du på programniveau have arrays af noder og arrays af forbindelser. Derfor skal du skrive, hvordan grafen konkret implementeres med disse programmeringsstrukturer.
Det skal bemærkes, at intet af det ovenstående vedrører selve processen med at skrive kode. Når du skriver kode, det vil sige udfører det tredje trin, skal du også tænke og planlægge programmet. Hvis en delopgave viser sig at være kompleks eller ikke helt klar, skal du lave en specifikation for den. Men jeg taler ikke om selve koden her. Du kan bruge ethvert programmeringssprog, enhver metode; det handler ikke om dem. Desuden fritager intet af det ovenstående for nødvendigheden af at teste og debugge koden. Selv hvis den abstrakte model er skrevet korrekt, kan der være fejl i dens implementering.
Skrivning af specifikationer er et tillægstrin i kode-skrivningsprocessen. Gennem dette kan mange fejl fanges med mindre indsats — dette ved vi fra erfaringer fra programmører hos Amazon. Med specifikationer bliver kvaliteten af programmer højere. Så hvorfor klarer vi os så ofte uden dem? Fordi det er svært at skrive. Og det er svært at skrive, fordi det kræver tankegang, og at tænke er også svært. Det er altid nemmere at lade som om, man tænker. Her kan man lave en parallel til løb — jo mindre du løber, jo langsommere løber du. Du skal træne dine muskler og øve dig i at skrive. Øvelse er nødvendig.
Specifikationen kan være ukorrekt. Du kan have lavet en fejl et sted, eller kravene kan have ændret sig, eller det kan have vist sig nødvendigt at lave forbedringer. Al kode, som nogen bruger, skal ændres, så på et eller andet tidspunkt vil specifikationen ikke længere stemme overens med programmet. I ideelle tilfælde bør man skrive en ny specifikation og fuldstændig omskrive koden. Vi ved alle, at det sjældent sker. I praksis patcher vi koden og opdaterer muligvis specifikationen. Hvis dette nødvendigvis sker før eller siden, hvorfor skrive specifikationer overhovedet? For det første vil hvert eneste overflødige ord i specifikationen være guld værd for den person, der skal rette din kode, og denne person kan sagtens være dig selv. Jeg bebrejder ofte mig selv for utilstrækkelige specifikationer, når jeg retter min kode. Jeg skriver faktisk flere specifikationer end kode. Derfor skal specifikationen altid opdateres, når du retter koden. For det andet bliver koden værre med hver rettelse, den bliver sværere at læse og vedligeholde. Det er en stigning i entropi. Men hvis du ikke starter med en specifikation, vil hver enkelt linje skrevet være en rettelse, og koden vil fra starten være klodset og svær at læse.
Som sagt , ingen kamp er vundet efter planen, og ingen kamp er vundet uden plan. Og han vidste noget om kampe. Der er en opfattelse af, at det er spild af tid at skrive specifikationer. Nogle gange er det faktisk tilfældet, og opgaven er så simpel, at der ikke er noget at tænke over. Men man skal altid huske, at når du rådes til ikke at skrive specifikationer, så rådes du til ikke at tænke. Og det er noget, man altid bør overveje. At tænke opgaven igennem garanterer ikke, at du ikke vil lave fejl. Som vi ved, er der ikke opfundet nogen tryllestav, og programmering er en kompleks opgave. Men hvis du ikke tænker over opgaven, garanterer du, at du vil lave fejl.
Du kan læse mere om TLA+ og PlusCal på den specielle hjemmeside, som du kan tilgå fra min hjemmeside . Det var alt fra mig, tak for opmærksomheden.
Jeg minder om, at dette er en oversættelse. Når du skriver kommentarer - husk, at forfatteren ikke vil læse dem. Hvis du virkelig ønsker at kommunikere med forfatteren, vil han være til stede på konferencen Hydra 2019, som finder sted den 11.-12. juli 2019 i Sankt Petersborg. Billetter kan købes .
Kilde: habr.com
