Denne artikkelen er en oversettelse . Men før henne en liten introduksjon. Hvordan dannes zombier? Alle kom i en situasjon der de ønsker å trekke en venn eller kollega opp til sitt nivå, men det går ikke. Og det er ikke så mye med deg som med ham at "det går ikke": på den ene siden av skalaen er en normal lønn, oppgaver og så videre, og på den andre, behovet for å tenke. Å tenke er ubehagelig og smertefullt. Han gir raskt opp og fortsetter å skrive kode uten å skru på hjernen i det hele tatt. Du forestiller deg hvor mye innsats det tar å overvinne barrieren av lært hjelpeløshet, og du gjør det bare ikke. Dette er hvordan zombier dannes, som, det ser ut til, kan kureres, men det ser ut til at ingen vil gjøre det.
Da jeg så det (ja, samme kamerat fra lærebøkene) og lager ikke en rapport, men en spørsmål-og-svar-sesjon, jeg var litt på vakt. Bare i tilfelle, Leslie er en verdensberømt vitenskapsmann, forfatteren av grunnleggende verk innen distribuert databehandling, og du kan også kjenne ham med bokstavene La i ordet LaTeX - "Lamport TeX". Den andre alarmerende faktoren er kravet hans: alle som kommer må (helt gratis) lytte til et par av rapportene hans på forhånd, komme med minst ett spørsmål om dem, og først da komme. Jeg bestemte meg for å se hva Lamport sendte der – og det er flott! Det er akkurat den tingen, den magiske lenkepillen for å kurere zombier. Jeg advarer deg: fra teksten kan elskere av superfleksible metoder og de som ikke liker å teste det som skrives, brenne ut.
Etter habrokat begynner faktisk oversettelsen av seminaret. Liker å lese!
Uansett hvilken oppgave du tar på deg, må du alltid gå gjennom tre trinn:
- bestemme hvilket mål du vil oppnå;
- bestemme hvordan du vil nå målet ditt;
- komme til målet ditt.
Dette gjelder også programmering. Når vi skriver kode, må vi:
- bestemme hva programmet skal gjøre;
- bestemme hvordan den skal utføre oppgaven sin;
- skriv den tilsvarende koden.
Det siste trinnet er selvfølgelig veldig viktig, men jeg skal ikke snakke om det i dag. I stedet skal vi diskutere de to første. Hver programmerer utfører dem før de begynner å jobbe. Du setter deg ikke ned for å skrive med mindre du har bestemt deg for om du skal skrive en nettleser eller en database. En viss ide om målet må være tilstede. Og du tenker definitivt over hva programmet vil gjøre, og ikke skriv på en eller annen måte i håp om at koden på en eller annen måte blir til en nettleser.
Hvordan skjer denne forhåndstenkningen for koden? Hvor mye innsats bør vi legge i dette? Alt avhenger av hvor komplekst problemet vi løser. Anta at vi ønsker å skrive et feiltolerant distribuert system. I dette tilfellet bør vi tenke nøye gjennom ting før vi setter oss ned for å kode. Hva om vi bare trenger å øke en heltallsvariabel med 1? Ved første øyekast er alt trivielt her, og ingen tanke er nødvendig, men så husker vi at et overløp kan oppstå. Derfor, selv for å forstå om et problem er enkelt eller komplekst, må du først tenke.
Hvis du tenker på mulige løsninger på problemet på forhånd, kan du unngå feil. Men dette krever at tankegangen din er klar. For å oppnå dette må du skrive ned tankene dine. Jeg liker virkelig Dick Guindon-sitatet: "Når du skriver, viser naturen deg hvor slurvete du tenker." Hvis du ikke skriver, tenker du bare at du tenker. Og du må skrive ned tankene dine i form av spesifikasjoner.
Spesifikasjoner utfører mange funksjoner, spesielt i store prosjekter. Men jeg vil bare snakke om én av dem: de hjelper oss å tenke klart. Å tenke klart er veldig viktig og ganske vanskelig, så her trenger vi hjelp. Hvilket språk skal vi skrive spesifikasjoner på? Generelt er dette alltid det første spørsmålet for programmerere: hvilket språk skal vi skrive på. Det er ingen riktig svar på det: problemene vi løser er for forskjellige. For noen er TLA+ et spesifikasjonsspråk jeg har utviklet. For andre er det mer praktisk å bruke kinesisk. Alt avhenger av situasjonen.
Viktigere er et annet spørsmål: hvordan oppnå klarere tenkning? Svar: Vi må tenke som forskere. Dette er en måte å tenke på som har bevist seg de siste 500 årene. I naturfag bygger vi matematiske modeller av virkeligheten. Astronomi var kanskje den første vitenskapen i ordets strenge forstand. I den matematiske modellen som brukes i astronomi, vises himmellegemer som punkter med masse, posisjon og fart, selv om de i virkeligheten er ekstremt komplekse objekter med fjell og hav, tidevann og tidevann. Denne modellen, som alle andre, ble laget for å løse visse problemer. Det er flott for å finne ut hvor du skal peke teleskopet ditt hvis du trenger å finne en planet. Men hvis du vil forutsi været på denne planeten, vil ikke denne modellen fungere.
Matematikk lar oss bestemme egenskapene til modellen. Og vitenskapen viser hvordan disse egenskapene forholder seg til virkeligheten. La oss snakke om vår vitenskap, informatikk. Virkeligheten vi jobber med er datasystemer av ulike slag: prosessorer, spillkonsoller, datamaskiner, kjøring av programmer og så videre. Jeg vil snakke om å kjøre et program på en datamaskin, men i det store og hele gjelder alle disse konklusjonene for ethvert datasystem. I vår vitenskap bruker vi mange forskjellige modeller: Turing-maskinen, delvis bestilte sett med arrangementer og mange andre.
Hva er et program? Dette er en hvilken som helst kode som kan vurderes uavhengig. Anta at vi må skrive en nettleser. Vi utfører tre oppgaver: Vi designer brukerens syn på programmet, deretter skriver vi høynivådiagrammet til programmet, og til slutt skriver vi koden. Når vi skriver koden, innser vi at vi må skrive en tekstformater. Her må vi igjen løse tre problemer: bestemme hvilken tekst dette verktøyet vil returnere; velg en algoritme for formatering; skrive kode. Denne oppgaven har sin egen underoppgave: legg inn en bindestrek riktig i ord. Vi løser også denne deloppgaven i tre trinn – som du ser, gjentas de på mange nivåer.
La oss vurdere det første trinnet mer detaljert: hvilket problem programmet løser. Her modellerer vi oftest et program som en funksjon som tar litt input og produserer noe output. I matematikk er en funksjon vanligvis beskrevet som et ordnet sett med par. For eksempel beskrives kvadreringsfunksjonen for naturlige tall som settet {<0,0>, <1,1>, <2,4>, <3,9>, …}. Domenet til en slik funksjon er settet av de første elementene i hvert par, det vil si de naturlige tallene. For å definere en funksjon, må vi spesifisere dens omfang og formel.
Men funksjoner i matematikk er ikke det samme som funksjoner i programmeringsspråk. Matematikken er mye enklere. Siden jeg ikke har tid til komplekse eksempler, la oss vurdere et enkelt: en funksjon i C eller en statisk metode i Java som returnerer den største felles divisor av to heltall. I spesifikasjonen av denne metoden vil vi skrive: beregner GCD(M,N) for argumenter M и NDer GCD(M,N) - en funksjon hvis domene er settet av par med heltall, og returverdien er det største heltall som er delelig med M и N. Hvordan forholder denne modellen seg til virkeligheten? Modellen opererer på heltall, mens vi i C eller Java har en 32-bit int. Denne modellen lar oss bestemme om algoritmen er riktig GCD, men det forhindrer ikke overløpsfeil. Dette vil kreve en mer kompleks modell, som det ikke er tid til.
La oss snakke om begrensningene til en funksjon som modell. Noen programmer (som operativsystemer) returnerer ikke bare en viss verdi for visse argumenter, de kan kjøre kontinuerlig. I tillegg er funksjonen som modell ikke godt egnet for det andre trinnet: planlegging av hvordan problemet skal løses. Rask sortering og boblesortering beregner samme funksjon, men de er helt forskjellige algoritmer. Derfor, for å beskrive hvordan målet med programmet oppnås, bruker jeg en annen modell, la oss kalle den standard atferdsmodellen. Programmet i det er representert som et sett med all tillatt oppførsel, som hver i sin tur er en sekvens av tilstander, og tilstanden er tilordningen av verdier til variabler.
La oss se hvordan det andre trinnet for Euclid-algoritmen vil se ut. Vi må beregne GCD(M, N). Vi initialiserer M som xOg N som y, så trekk gjentatte ganger den minste av disse variablene fra de større til de er like. For eksempel hvis M = 12Og N = 18, kan vi beskrive følgende oppførsel:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
Og hvis M = 0 и N = 0? Null er delelig med alle tall, så det er ingen største divisor i dette tilfellet. I denne situasjonen må vi gå tilbake til det første trinnet og spørre: trenger vi virkelig å beregne GCD for ikke-positive tall? Hvis dette ikke er nødvendig, trenger du bare å endre spesifikasjonen.
Her bør vi gjøre en liten digresjon om produktivitet. Det måles ofte i antall linjer med kode skrevet per dag. Men arbeidet ditt er mye mer nyttig hvis du blir kvitt et visst antall linjer, fordi du har mindre plass til feil. Og den enkleste måten å bli kvitt koden på er ved første trinn. Det er fullt mulig at du bare ikke trenger alle klokkene og fløytene du prøver å implementere. Den raskeste måten å forenkle et program og spare tid på er å ikke gjøre ting som ikke bør gjøres. Det andre trinnet er det nest mest tidsbesparende potensialet. Hvis du måler produktivitet i form av linjer skrevet, vil det å tenke på hvordan du utfører en oppgave gjøre deg mindre produktiv, fordi du kan løse det samme problemet med mindre kode. Jeg kan ikke gi nøyaktig statistikk her, fordi jeg ikke har noen måte å telle antall linjer som jeg ikke skrev på grunn av det faktum at jeg brukte tid på spesifikasjonen, det vil si på det første og andre trinnet. Og forsøket kan heller ikke settes opp her, for i forsøket har vi ikke rett til å gjennomføre det første trinnet, oppgaven er forhåndsbestemt.
Det er lett å overse mange vanskeligheter i uformelle spesifikasjoner. Det er ikke noe vanskelig å skrive strenge spesifikasjoner for funksjoner, jeg vil ikke diskutere dette. I stedet skal vi snakke om å skrive sterke spesifikasjoner for standard atferd. Det er et teorem som sier at ethvert sett med atferd kan beskrives ved hjelp av sikkerhetsegenskapen (sikkerhet) og overlevelsesegenskaper (livlighet). Sikkerhet betyr at ingenting vondt vil skje, programmet vil ikke gi feil svar. Overlevelse betyr at det før eller siden vil skje noe godt, det vil si at programmet vil gi riktig svar før eller siden. Som regel er sikkerhet en viktigere indikator, feil oppstår oftest her. Derfor, for å spare tid, vil jeg ikke snakke om overlevelsesevne, selv om det selvfølgelig også er viktig.
Vi oppnår sikkerhet ved først å foreskrive settet med mulige starttilstander. Og for det andre, forhold til alle mulige neste stater for hver stat. La oss oppføre oss som forskere og definere tilstander matematisk. Settet med begynnelsestilstander er beskrevet av en formel, for eksempel når det gjelder Euklid-algoritmen: (x = M) ∧ (y = N). For visse verdier M и N det er bare én starttilstand. Forholdet til den neste tilstanden er beskrevet av en formel der variablene til den neste tilstanden skrives med et primtall, og variablene til den nåværende tilstanden skrives uten primtall. Når det gjelder Euklids algoritme, vil vi behandle disjunksjonen av to formler, hvorav den ene x er den største verdien, og i den andre - y:
I det første tilfellet er den nye verdien av y lik den forrige verdien av y, og vi får den nye verdien av x ved å trekke den minste variabelen fra den større variabelen. I det andre tilfellet gjør vi det motsatte.
La oss gå tilbake til Euklids algoritme. La oss anta det igjen M = 12, N = 18. Dette definerer en enkelt starttilstand, (x = 12) ∧ (y = 18). Vi kobler deretter disse verdiene inn i formelen ovenfor og får:
Her er den eneste mulige løsningen: x' = 18 - 12 ∧ y' = 12og vi får oppførselen: [x = 12, y = 18]. På samme måte kan vi beskrive alle tilstandene i oppførselen vår: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
I siste tilstand [x = 6, y = 6] begge deler av uttrykket vil være usann, så det har ingen neste tilstand. Så vi har en fullstendig spesifikasjon av det andre trinnet - som du kan se, er dette ganske vanlig matematikk, som i ingeniører og vitenskapsmenn, og ikke rart, som i informatikk.
Disse to formlene kan kombineres til én formel for tidslogikk. Hun er elegant og lett å forklare, men det er ikke tid til henne nå. Vi trenger kanskje tidsmessig logikk bare for livlighetsegenskapen, den er ikke nødvendig for sikkerhet. Jeg liker ikke tidslogikk som sådan, det er ikke helt vanlig matematikk, men når det gjelder livlighet er det et nødvendig onde.
I Euklids algoritme, for hver verdi x и y har unike verdier x' и y', som gjør forholdet til neste tilstand sann. Euklids algoritme er med andre ord deterministisk. For å modellere en ikke-deterministisk algoritme, må den nåværende tilstanden ha flere mulige fremtidige tilstander, og at hver ikke-primede variabelverdi har flere primede variabelverdier slik at forholdet til neste tilstand er sann. Dette er enkelt å gjøre, men jeg skal ikke gi eksempler nå.
For å lage et arbeidsverktøy trenger du formell matematikk. Hvordan gjøre spesifikasjonen formell? For å gjøre dette trenger vi et formelt språk, for eksempel . Spesifikasjonen til Euclid-algoritmen vil se slik ut på dette språket:
Et likhetstegnsymbol med en trekant betyr at verdien til venstre for tegnet er definert til å være lik verdien til høyre for tegnet. I hovedsak er spesifikasjonen en definisjon, i vårt tilfelle to definisjoner. Til spesifikasjonen i TLA+ må du legge til deklarasjoner og litt syntaks, som i lysbildet ovenfor. I ASCII vil det se slik ut:
Som du kan se, ingenting komplisert. Spesifikasjonen for TLA+ kan testes, dvs. omgå all mulig atferd i en liten modell. I vårt tilfelle vil denne modellen være visse verdier M и N. Dette er en veldig effektiv og enkel verifiseringsmetode som er helt automatisk. Det er også mulig å skrive formelle sannhetsbevis og kontrollere dem mekanisk, men dette tar mye tid, så nesten ingen gjør dette.
Den største ulempen med TLA+ er at det er matematikk, og programmerere og datavitere er redde for matematikk. Ved første øyekast høres dette ut som en spøk, men dessverre mener jeg det på fullt alvor. Min kollega fortalte meg bare hvordan han prøvde å forklare TLA+ til flere utviklere. Så snart formlene dukket opp på skjermen, ble de umiddelbart glassaktige øyne. Så hvis TLA+ skremmer deg, kan du bruke , det er et slags programmeringsspråk for leker. Et uttrykk i PlusCal kan være et hvilket som helst TLA+-uttrykk, det vil si i det store og hele et hvilket som helst matematisk uttrykk. I tillegg har PlusCal en syntaks for ikke-deterministiske algoritmer. Fordi PlusCal kan skrive et hvilket som helst TLA+-uttrykk, er PlusCal mye mer uttrykksfullt enn noe ekte programmeringsspråk. Deretter er PlusCal kompilert til en lett lesbar TLA+-spesifikasjon. Dette betyr selvfølgelig ikke at den komplekse PlusCal-spesifikasjonen blir til en enkel på TLA + - bare korrespondansen mellom dem er åpenbar, det vil ikke være noen ekstra kompleksitet. Til slutt kan denne spesifikasjonen verifiseres av TLA+-verktøy. Alt i alt kan PlusCal hjelpe med å overvinne matematikkfobi og er lett å forstå selv for programmerere og datavitere. Tidligere publiserte jeg algoritmer på den i noen tid (omtrent 10 år).
Kanskje noen vil innvende at TLA + og PlusCal er matematikk, og matematikk fungerer kun på oppfunne eksempler. I praksis trenger du et ekte språk med typer, prosedyrer, objekter og så videre. Dette er feil. Her er hva Chris Newcomb, som jobbet hos Amazon, skriver: "Vi har brukt TLA+ på ti store prosjekter, og i hvert tilfelle har det gjort en betydelig forskjell for utviklingen fordi vi klarte å fange opp farlige feil før vi traff produksjonen, og fordi det ga oss innsikten og selvtilliten vi trengte for å gjøre aggressiv ytelse optimaliseringer uten å påvirke sannheten til programmet". Man kan ofte høre at ved bruk av formelle metoder får vi ineffektiv kode – i praksis er alt akkurat det motsatte. I tillegg er det en oppfatning om at ledere ikke kan overbevises om behovet for formelle metoder, selv om programmerere er overbevist om deres nytteverdi. Og Newcomb skriver: "Ledere presser nå hardt på å skrive spesifikasjoner for TLA +, og spesifikt tildele tid til dette". Så når ledere ser at TLA+ fungerer, aksepterer de det gjerne. Chris Newcomb skrev dette for omtrent et halvt år siden (oktober 2014), men nå, så vidt jeg vet, brukes TLA+ i 14 prosjekter, ikke 10. Et annet eksempel gjelder utformingen av XBox 360. En praktikant kom til Charles Thacker og skrev spesifikasjon for minnesystemet. Takket være denne spesifikasjonen ble det funnet en feil som ellers ville gå ubemerket hen, og på grunn av denne ville hver Xbox 360 krasje etter fire timers bruk. IBM-ingeniører bekreftet at testene deres ikke ville ha funnet denne feilen.
Du kan lese mer om TLA + på Internett, men la oss nå snakke om uformelle spesifikasjoner. Vi må sjelden skrive programmer som regner ut minste felles divisor og lignende. Mye oftere skriver vi programmer som pretty-printer-verktøyet jeg skrev for TLA+. Etter den enkleste behandlingen vil TLA +-koden se slik ut:
Men i eksemplet ovenfor ønsket brukeren mest sannsynlig at konjunksjons- og likhetstegnet skulle være justert. Så riktig formatering vil se mer slik ut:
Tenk på et annet eksempel:
Her, tvert imot, var justeringen av likhets-, addisjons- og multiplikasjonstegnene i kilden tilfeldig, så den enkleste behandlingen er nok. Generelt er det ingen eksakt matematisk definisjon av korrekt formatering, fordi "riktig" i dette tilfellet betyr "hva brukeren vil ha", og dette kan ikke bestemmes matematisk.
Det ser ut til at hvis vi ikke har en definisjon av sannhet, så er spesifikasjonen ubrukelig. Men det er det ikke. Bare fordi vi ikke vet hva et program skal gjøre, betyr ikke det at vi ikke trenger å tenke på hvordan det fungerer – tvert imot, vi må legge enda mer innsats i det. Spesifikasjonen er spesielt viktig her. Det er umulig å bestemme det optimale programmet for strukturert utskrift, men dette betyr ikke at vi ikke skal ta det i det hele tatt, og å skrive kode som en bevissthetsstrøm er ikke bra. Til slutt skrev jeg en spesifikasjon av seks regler med definisjoner i form av kommentarer i en java-fil. Her er et eksempel på en av reglene: a left-comment token is LeftComment aligned with its covering token. Denne regelen er skrevet på, skal vi si, matematisk engelsk: LeftComment aligned, left-comment и covering token - termer med definisjoner. Slik beskriver matematikere matematikk: de skriver definisjoner av begreper og, basert på dem, regler. Fordelen med en slik spesifikasjon er at seks regler er mye lettere å forstå og feilsøke enn 850 linjer med kode. Jeg må si at det ikke var lett å skrive disse reglene, det tok ganske mye tid å feilsøke dem. Spesielt for dette formålet skrev jeg en kode som rapporterte hvilken regel som ble brukt. Takket være det faktum at jeg testet disse seks reglene på flere eksempler, trengte jeg ikke å feilsøke 850 linjer med kode, og feil viste seg å være ganske enkle å finne. Java har gode verktøy for dette. Hvis jeg bare hadde skrevet koden, ville det tatt mye lengre tid, og formateringen ville vært av dårligere kvalitet.
Hvorfor kunne ikke en formell spesifikasjon brukes? På den ene siden er riktig utførelse ikke så viktig her. Strukturelle utskrifter vil garantert ikke glede noen, så jeg trengte ikke å få den til å fungere riktig i alle de rare situasjonene. Enda viktigere er det faktum at jeg ikke hadde tilstrekkelig verktøy. TLA+-modellkontrollen er ubrukelig her, så jeg må skrive eksemplene manuelt.
Ovennevnte spesifikasjon har funksjoner som er felles for alle spesifikasjoner. Det er høyere nivå enn koden. Det kan implementeres på alle språk. Alle verktøy eller metoder er ubrukelige for å skrive det. Ingen programmeringskurs vil hjelpe deg med å skrive denne spesifikasjonen. Og det er ingen verktøy som kan gjøre denne spesifikasjonen unødvendig, med mindre du selvfølgelig skriver et språk spesifikt for å skrive strukturerte utskriftsprogrammer i TLA+. Til slutt, denne spesifikasjonen sier ikke noe om nøyaktig hvordan vi skal skrive koden, den sier bare hva denne koden gjør. Vi skriver spesifikasjonen for å hjelpe oss å tenke gjennom problemet før vi begynner å tenke på koden.
Men denne spesifikasjonen har også funksjoner som skiller den fra andre spesifikasjoner. 95 % av andre spesifikasjoner er betydelig kortere og enklere:
Videre er denne spesifikasjonen et sett med regler. Som regel er dette et tegn på dårlig spesifikasjon. Å forstå konsekvensene av et sett med regler er ganske vanskelig, og det er derfor jeg måtte bruke mye tid på å feilsøke dem. Men i dette tilfellet kunne jeg ikke finne en bedre måte.
Det er verdt å si noen ord om programmer som kjører kontinuerlig. Som regel jobber de parallelt, for eksempel operativsystemer eller distribuerte systemer. Svært få mennesker kan forstå dem mentalt eller på papiret, og jeg er ikke en av dem, selv om jeg en gang klarte det. Derfor trenger vi verktøy som vil sjekke arbeidet vårt - for eksempel TLA + eller PlusCal.
Hvorfor var det nødvendig å skrive en spesifikasjon hvis jeg allerede visste hva nøyaktig koden skulle gjøre? Faktisk trodde jeg bare at jeg visste det. I tillegg, med en spesifikasjon, trenger ikke lenger en utenforstående å komme inn i koden for å forstå nøyaktig hva han gjør. Jeg har en regel: det skal ikke være noen generelle regler. Det er et unntak fra denne regelen, selvfølgelig, det er den eneste generelle regelen jeg følger: spesifikasjonen av hva koden gjør skal fortelle folk alt de trenger å vite når de bruker koden.
Så hva trenger programmerere å vite om tenkning? For det første, det samme som alle andre: hvis du ikke skriver, så virker det bare for deg at du tenker. Du må også tenke før du koder, noe som betyr at du må skrive før du koder. Spesifikasjonen er det vi skriver før vi begynner å kode. En spesifikasjon er nødvendig for enhver kode som kan brukes eller endres av hvem som helst. Og denne "noen" kan være forfatteren av koden selv en måned etter at den ble skrevet. En spesifikasjon er nødvendig for store programmer og systemer, for klasser, for metoder, og noen ganger til og med for komplekse deler av en enkelt metode. Hva skal egentlig skrives om koden? Du må beskrive hva den gjør, det vil si hva som kan være nyttig for enhver person som bruker denne koden. Noen ganger kan det også være nødvendig å spesifisere hvordan koden oppnår formålet. Hvis vi gikk gjennom denne metoden i løpet av algoritmer, kaller vi det en algoritme. Hvis det er noe mer spesielt og nytt, så kaller vi det design på høyt nivå. Det er ingen formell forskjell her: begge er en abstrakt modell av et program.
Hvordan skal du skrive en kodespesifikasjon? Det viktigste: den skal være ett nivå høyere enn selve koden. Den skal beskrive tilstander og atferd. Det bør være så strengt som oppgaven krever. Hvis du skriver en spesifikasjon for hvordan en oppgave skal implementeres, kan du skrive den i pseudokode eller med PlusCal. Du må lære å skrive spesifikasjoner på formelle spesifikasjoner. Dette vil gi deg de nødvendige ferdighetene som vil hjelpe deg også med uformelle. Hvordan lærer du å skrive formelle spesifikasjoner? Da vi lærte å programmere, skrev vi programmer og feilsøkte dem deretter. Det er det samme her: skriv spesifikasjonen, sjekk den med modellsjekkeren og fiks feilene. TLA+ er kanskje ikke det beste språket for en formell spesifikasjon, og et annet språk er sannsynligvis bedre for dine spesifikke behov. Fordelen med TLA+ er at den lærer matematisk tenkning veldig bra.
Hvordan koble sammen spesifikasjon og kode? Ved hjelp av kommentarer som kobler matematiske begreper og deres implementering. Hvis du jobber med grafer, vil du på programnivå ha arrays av noder og arrays av lenker. Derfor må du skrive nøyaktig hvordan grafen implementeres av disse programmeringsstrukturene.
Det skal bemerkes at ingen av de ovennevnte gjelder selve prosessen med å skrive kode. Når du skriver koden, det vil si at du utfører det tredje trinnet, må du også tenke og tenke gjennom programmet. Hvis en deloppgave viser seg å være kompleks eller ikke-åpenbar, må du skrive en spesifikasjon for den. Men jeg snakker ikke om selve koden her. Du kan bruke hvilket som helst programmeringsspråk, hvilken som helst metodikk, det handler ikke om dem. Ingen av de ovennevnte eliminerer heller behovet for å teste og feilsøke kode. Selv om den abstrakte modellen er skrevet riktig, kan det være feil i implementeringen.
Å skrive spesifikasjoner er et ekstra trinn i kodeprosessen. Takket være det kan mange feil fanges opp med mindre innsats - vi vet dette fra erfaringene til programmerere fra Amazon. Med spesifikasjoner blir kvaliteten på programmene høyere. Så hvorfor går vi så ofte uten dem? For det er vanskelig å skrive. Og skriving er vanskelig, for for dette må du tenke, og å tenke er også vanskelig. Det er alltid lettere å late som du tenker. Her kan du trekke en analogi med løping – jo mindre du løper, jo saktere løper du. Du må trene musklene og trene å skrive. Trenger øvelse.
Spesifikasjonen kan være feil. Du kan ha gjort en feil et sted, eller kravene kan ha endret seg, eller en forbedring må kanskje gjøres. Enhver kode som noen bruker må endres, så før eller siden vil spesifikasjonen ikke lenger samsvare med programmet. Ideelt sett må du i dette tilfellet skrive en ny spesifikasjon og skrive om koden fullstendig. Vi vet godt at ingen gjør det. I praksis lapper vi koden og oppdaterer eventuelt spesifikasjonen. Hvis dette er bundet til å skje før eller siden, hvorfor skrive spesifikasjoner i det hele tatt? For det første, for personen som skal redigere koden din, vil hvert ekstra ord i spesifikasjonen være gull verdt, og denne personen kan godt være deg. Jeg bespotter meg selv for ikke å få nok spesifikasjoner når jeg redigerer koden min. Og jeg skriver flere spesifikasjoner enn kode. Derfor, når du redigerer koden, må spesifikasjonen alltid oppdateres. For det andre, med hver revisjon, blir koden verre, den blir mer og mer vanskelig å lese og vedlikeholde. Dette er en økning i entropi. Men hvis du ikke starter med en spesifikasjon, vil hver linje du skriver være en redigering, og koden vil være uhåndterlig og vanskelig å lese fra starten av.
Som sagt , ingen kamp ble vunnet etter plan, og ingen kamp ble vunnet uten en plan. Og han visste en ting eller to om kamper. Det er en oppfatning at å skrive spesifikasjoner er bortkastet tid. Noen ganger er dette sant, og oppgaven er så enkel at det ikke er noe å tenke gjennom den. Men du bør alltid huske at når du får beskjed om å ikke skrive spesifikasjoner, får du beskjed om å ikke tenke. Og du bør tenke på det hver gang. Å tenke gjennom oppgaven garanterer ikke at du ikke gjør feil. Som vi vet var det ingen som fant opp tryllestaven, og programmering er en vanskelig oppgave. Men hvis du ikke tenker gjennom problemet, vil du garantert gjøre feil.
Du kan lese mer om TLA + og PlusCal på en spesiell nettside, du kan gå dit fra min hjemmeside . Det var alt for meg, takk for oppmerksomheten.
Vær oppmerksom på at dette er en oversettelse. Når du skriver kommentarer, husk at forfatteren ikke vil lese dem. Hvis du virkelig ønsker å chatte med forfatteren, så vil han være på Hydra 2019-konferansen, som arrangeres 11.-12. juli 2019 i St. Petersburg. Billetter kan kjøpes .
Kilde: www.habr.com