Dit is een vertaalartikel . Maar daarvoor is er een korte introductie. Hoe worden zombies gevormd? Iedereen heeft wel eens een situatie meegemaakt waarin hij of zij een vriend of collega op zijn niveau wil brengen, maar dat lukt niet. Bovendien 'werkt het niet' niet zozeer voor jou, maar voor hem: aan de ene kant van de schaal is er een normaal salaris, taken, enzovoort, en aan de andere kant is er de noodzaak om na te denken. Denken is onaangenaam en pijnlijk. Hij geeft het snel op en gaat door met het schrijven van code zonder zijn hersenen te gebruiken. Je beseft hoeveel moeite het kost om de barrière van aangeleerde hulpeloosheid te overwinnen, maar je doet het gewoon niet. Dit is hoe zombies worden gevormd, die mogelijk lijken te genezen, maar het lijkt erop dat niemand dit zal doen.
Toen ik dat zag (ja, diezelfde vriend uit de schoolboeken) en geen rapport geeft, maar een vraag-en-antwoordsessie, was ik een beetje op mijn hoede. Voor het geval dat Leslie een wereldberoemde wetenschapper is, de auteur van baanbrekende werken op het gebied van gedistribueerd computergebruik, en je kent hem misschien ook onder de letters La in LaTeX - "Lamport TeX". De tweede alarmerende factor is zijn eis: iedereen die komt, moet vooraf (geheel gratis) naar een paar van zijn rapporten luisteren, daar minimaal één vraag over bedenken, en dan pas komen. Ik besloot te kijken wat Lamport daar uitzond - en het is geweldig! Dit is precies dat ding, een magische linkpil voor de behandeling van zombies. Ik waarschuw je: de tekst kan degenen die van super-agile-methodologieën houden en die niet graag testen wat ze hebben geschreven ernstig verbranden.
Na de habrokat begint daadwerkelijk de vertaling van het seminar. Veel plezier met lezen!
Welke taak je ook op je neemt, je moet altijd drie stappen doorlopen:
- bepaal welk doel je wilt bereiken;
- beslissen hoe u uw doel precies gaat bereiken;
- bereik je doel.
Dit geldt ook voor programmeren. Als we code schrijven, hebben we het volgende nodig:
- beslissen wat het programma precies moet doen;
- bepalen hoe zij haar taak precies moet uitvoeren;
- schrijf de juiste code.
De laatste stap is natuurlijk heel belangrijk, maar daar ga ik het vandaag niet over hebben. In plaats daarvan zullen we de eerste twee bespreken. Elke programmeur voert ze uit voordat hij aan het werk gaat. Je gaat niet aan de slag om te schrijven tenzij je hebt besloten wat je schrijft: een browser of een database. Er moet een bepaald idee van het doel aanwezig zijn. En je denkt zeker na over wat het programma precies zal doen, en schrijft het niet lukraak in de hoop dat de code zelf op de een of andere manier in een browser zal veranderen.
Hoe gebeurt dit voordenken over code precies? Hoeveel moeite moeten we hierin steken? Het hangt allemaal af van hoe complex het probleem dat we oplossen. Laten we zeggen dat we een fouttolerant gedistribueerd systeem willen schrijven. In dit geval moeten we goed nadenken voordat we aan de slag gaan met coderen. Wat als we een integer-variabele gewoon met 1 moeten verhogen? Op het eerste gezicht is alles hier triviaal en is er geen nadenken nodig, maar dan herinneren we ons dat er een overloop kan optreden. Daarom moet u, zelfs om te begrijpen of een probleem eenvoudig of complex is, eerst nadenken.
Als je vooraf nadenkt over mogelijke oplossingen voor een probleem, kun je fouten voorkomen. Maar dit vereist dat uw denken helder is. Om dit te bereiken, moet je je gedachten opschrijven. Ik hou van het citaat van Dick Guindon: “Als je schrijft, laat de natuur je zien hoe slordig je denken is.” Als je niet schrijft, denk je alleen maar dat je denkt. En u moet uw gedachten opschrijven in de vorm van specificaties.
Specificaties hebben vele functies, vooral bij grote projecten. Maar ik zal het slechts over één ervan hebben: ze helpen ons helder na te denken. Helder denken is erg belangrijk en behoorlijk moeilijk, dus we hebben hier hulp nodig. In welke taal moeten we specificaties schrijven? Over het algemeen is dit altijd de eerste vraag voor programmeurs: in welke taal gaan we schrijven? Er is niet één juist antwoord: de problemen die we oplossen zijn te divers. Voor sommige mensen is TLA+ een specificatietaal die ik heb ontwikkeld. Voor anderen is het handiger om Chinees te gebruiken. Het hangt allemaal af van de situatie.
De belangrijkste vraag is: hoe kunnen we tot helderder denken komen? Antwoord: We moeten denken als wetenschappers. Dit is een manier van denken die de afgelopen 500 jaar goed heeft gewerkt. In de wetenschap bouwen we wiskundige modellen van de werkelijkheid. Astronomie was misschien wel de eerste wetenschap in de strikte zin van het woord. In het wiskundige model dat in de astronomie wordt gebruikt, verschijnen hemellichamen als punten met massa, positie en momentum, hoewel het in werkelijkheid uiterst complexe objecten zijn met bergen en oceanen, eb en vloed. Dit model is, net als elk ander model, gemaakt om bepaalde problemen op te lossen. Het is geweldig om te bepalen waar je een telescoop op moet richten als je een planeet wilt vinden. Maar als je het weer op deze planeet wilt voorspellen, zal dit model niet werken.
Wiskunde stelt ons in staat de eigenschappen van een model te bepalen. En de wetenschap laat zien hoe deze eigenschappen zich verhouden tot de werkelijkheid. Laten we het hebben over onze wetenschap, informatica. De realiteit waarmee we werken bestaat uit computersystemen van veel verschillende typen: processors, gameconsoles, computers waarop programma's draaien, enzovoort. Ik zal het hebben over het uitvoeren van een programma op een computer, maar over het algemeen zijn al deze conclusies van toepassing op elk computersysteem. In onze wetenschap gebruiken we veel verschillende modellen: de Turing-machine, gedeeltelijk geordende reeksen gebeurtenissen en vele andere.
Wat is het programma? Dit is elke code die op zichzelf kan worden beschouwd. Laten we zeggen dat we een browser moeten schrijven. We voeren drie taken uit: ontwerp de gebruikerspresentatie van het programma, schrijf vervolgens het diagram op hoog niveau van het programma en schrijf ten slotte de code. Terwijl we de code schrijven, realiseren we ons dat we een tekstformatter moeten schrijven. Ook hier moeten we drie problemen oplossen: bepalen welke tekst deze tool zal retourneren; selecteer een algoritme voor opmaak; code schrijven. Deze taak heeft zijn eigen subtaak: koppeltekens correct invoegen in woorden. We lossen deze deeltaak ook in drie stappen op - zoals we zien worden ze op veel niveaus herhaald.
Laten we de eerste stap eens nader bekijken: welk probleem het programma oplost. Hier modelleren we een programma meestal als een functie die enige invoer nodig heeft en enige uitvoer geeft. In de wiskunde wordt een functie gewoonlijk beschreven als een geordende reeks paren. De kwadratuurfunctie voor natuurlijke getallen wordt bijvoorbeeld beschreven als de verzameling {<0,0>, <1,1>, <2,4>, <3,9>, …}. Het definitiedomein van een dergelijke functie is de verzameling van de eerste elementen van elk paar, dat wil zeggen natuurlijke getallen. Om een functie te definiëren, moeten we het domein en de formule ervan specificeren.
Maar functies in de wiskunde zijn niet hetzelfde als functies in programmeertalen. De wiskunde is veel eenvoudiger. Omdat ik geen tijd heb voor complexe voorbeelden, laten we een eenvoudig voorbeeld bekijken: een functie in C of een statische methode in Java die de grootste gemene deler van twee gehele getallen retourneert. In de specificatie van deze methode schrijven we: berekent GCD(M,N) voor argumenten M и NWaar GCD(M,N) - een functie waarvan het domein een reeks paren gehele getallen is, en de retourwaarde het grootste gehele getal is dat wordt gedeeld door M и N. Hoe verhoudt de werkelijkheid zich tot dit model? Het model werkt met gehele getallen, en in C of Java hebben we 32-bits int. Met dit model kunnen we beslissen of het algoritme correct is GCD, maar het voorkomt geen overloopfouten. Hiervoor is een complexer model nodig, waarvoor geen tijd bestaat.
Laten we het hebben over de beperkingen van de functie als model. Sommige programma's (zoals besturingssystemen) retourneren niet alleen een specifieke waarde voor bepaalde argumenten; ze kunnen continu worden uitgevoerd. Bovendien is de functie als model slecht geschikt voor de tweede stap: het plannen van de oplossing van het probleem. Quicksort en bubble sort berekenen dezelfde functie, maar het zijn totaal verschillende algoritmen. Om de manier te beschrijven waarop het doel van het programma kan worden bereikt, gebruik ik daarom een ander model, laten we het het standaardgedragsmodel noemen. Het programma wordt daarin weergegeven als een verzameling van alle geldige gedragingen, die elk op hun beurt een reeks toestanden zijn, en een toestand de toewijzing van waarden aan variabelen is.
Laten we eens kijken hoe de tweede stap voor het Euclidische algoritme eruit zou zien. We moeten berekenen GCD(M, N). Wij initialiseren M hoe xEn N hoe y, trek vervolgens herhaaldelijk de kleinste van deze variabelen af van de grotere totdat ze gelijk zijn. Bijvoorbeeld als M = 12En N = 18, kunnen we het volgende gedrag beschrijven:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
En als M = 0 и N = 0? Nul is deelbaar door alle getallen, dus er is in dit geval geen grootste deler. In deze situatie moeten we teruggaan naar de eerste stap en ons afvragen: moeten we GCD echt berekenen voor niet-positieve getallen? Als dit niet nodig is, hoeft u alleen maar de specificatie te wijzigen.
Een korte uitweiding over de productiviteit is hier op zijn plaats. Het wordt vaak gemeten in het aantal regels code dat per dag wordt geschreven. Maar je werk is veel nuttiger als je een bepaald aantal regels verwijdert, omdat je minder ruimte hebt voor bugs. En de gemakkelijkste manier om van code af te komen is in de eerste stap. Het is mogelijk dat u eenvoudigweg niet alle toeters en bellen nodig heeft die u probeert te implementeren. De snelste manier om een programma te vereenvoudigen en tijd te besparen, is door geen dingen te doen die niet gedaan zouden moeten worden. De tweede stap heeft het op een na hoogste tijdbesparende potentieel. Als je de productiviteit meet in termen van geschreven regels, dan zul je nadenken over hoe je een taak moet voltooien minder productief, omdat je hetzelfde probleem met minder code kunt oplossen. Ik kan hier geen exacte statistieken geven, omdat ik geen manier heb om het aantal regels te tellen dat ik niet heb geschreven vanwege de tijd die ik aan de specificatie heb besteed, dat wil zeggen aan de eerste en tweede stap. En ook hier kunnen we geen experiment doen, omdat we bij een experiment niet het recht hebben om de eerste stap te voltooien; de taak wordt vooraf bepaald.
Het is gemakkelijk om veel problemen bij informele specificaties over het hoofd te zien. Er is niets moeilijks aan het schrijven van strikte specificaties voor functies; ik zal hier niet op ingaan. In plaats daarvan zullen we het hebben over het schrijven van sterke specificaties voor standaardgedrag. Er is een stelling die stelt dat elke reeks gedragingen kan worden beschreven met behulp van de beveiligingseigenschap (veiligheid) en overlevingseigenschappen (levendigheid). Veiligheid betekent dat er niets ergs zal gebeuren, het programma zal niet het verkeerde antwoord geven. Overlevingsvermogen betekent dat er vroeg of laat iets goeds zal gebeuren, d.w.z. dat het programma vroeg of laat het juiste antwoord zal geven. In de regel is beveiliging een belangrijkere indicator; hier komen het vaakst fouten voor. Om tijd te besparen zal ik daarom niet praten over de overlevingskansen, hoewel dit natuurlijk ook belangrijk is.
Veiligheid bereiken we door eerst een reeks mogelijke begintoestanden te specificeren. En ten tweede de relaties met alle mogelijke volgende staten voor elke staat. Laten we ons gedragen als wetenschappers en toestanden wiskundig definiëren. De reeks begintoestanden wordt beschreven door de formule, bijvoorbeeld in het geval van het Euclidische algoritme: (x = M) ∧ (y = N). Voor bepaalde waarden M и N er is slechts één begintoestand. De relatie met de volgende staat wordt beschreven door een formule waarin de variabelen van de volgende staat met een priemgetal worden geschreven, en de variabelen van de huidige staat zonder priemgetal. In het geval van het Euclidische algoritme zullen we te maken hebben met de disjunctie van twee formules, waarvan er één x is de grootste waarde, en in de tweede - y:
In het eerste geval is de nieuwe waarde van y gelijk aan de vorige waarde van y, en krijgen we de nieuwe waarde van x door de kleinere variabele van de grotere af te trekken. In het tweede geval doen we het tegenovergestelde.
Laten we terugkeren naar het Euclidische algoritme. Stel dat nog eens voor M = 12, N = 18. Dit definieert een enkele initiële toestand, (x = 12) ∧ (y = 18). Vervolgens pluggen we deze waarden in de bovenstaande formule en krijgen:
Dit is de enige mogelijke oplossing: x' = 18 - 12 ∧ y' = 12, en we krijgen het gedrag: [x = 12, y = 18]. Op dezelfde manier kunnen we alle toestanden in ons gedrag beschrijven: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
In laatste staat [x = 6, y = 6] beide delen van de uitdrukking zullen onwaar zijn en daarom heeft deze geen volgende status. We hebben dus een volledige specificatie van de tweede stap - zoals we zien is dit een vrij gewone wiskunde, zoals die van ingenieurs en wetenschappers, en niet vreemd, zoals in de informatica.
Deze twee formules kunnen worden gecombineerd tot één formule van temporele logica. Het is elegant en gemakkelijk uit te leggen, maar daar is nu geen tijd voor. Misschien hebben we temporele logica alleen nodig voor de eigenschap van levendigheid; voor veiligheid is ze niet nodig. Ik houd niet van temporele logica als zodanig, het is geen gewone wiskunde, maar in het geval van levendigheid is het een noodzakelijk kwaad.
In het Euclidische algoritme voor elke waarde x и y er zijn unieke waarden x' и y', waardoor de relatie met de volgende toestand waar wordt. Met andere woorden: het Euclidische algoritme is deterministisch. Om een niet-deterministisch algoritme te modelleren, moet de huidige toestand meerdere mogelijke toekomstige toestanden hebben, en moet elke waarde van de niet-geprimeerde variabele meerdere waarden van de geprimeerde variabele hebben, zodat de relatie met de volgende toestand waar is. Dit is niet moeilijk om te doen, maar ik zal nu geen voorbeelden geven.
Om een werkinstrument te maken heb je formele wiskunde nodig. Hoe maak je een specificatie formeel? Om dit te doen hebben we een formele taal nodig, b.v. . De specificatie van het Euclidische algoritme in deze taal zal er als volgt uitzien:
Het gelijktekensymbool met een driehoek betekent dat wordt bepaald dat de waarde links van het teken gelijk is aan de waarde rechts van het teken. In essentie is een specificatie een definitie, in ons geval twee definities. Aan de specificatie in TLA+ moet je declaraties en wat syntaxis toevoegen, zoals in de dia hierboven. In ASCII zou het er als volgt uitzien:
Zoals je kunt zien, niets ingewikkelds. De specificatie op TLA+ kan worden geverifieerd, dat wil zeggen dat het mogelijk is om al het mogelijke gedrag in een klein model te omzeilen. In ons geval zal dit model bepaalde waarden zijn M и N. Dit is een zeer effectieve en eenvoudige verificatiemethode die volledig automatisch verloopt. Bovendien is het mogelijk om formele bewijzen van de waarheid te schrijven en deze mechanisch te controleren, maar dit kost veel tijd, dus bijna niemand doet dit.
Het grootste nadeel van TLA+ is dat het wiskunde is en dat programmeurs en computerwetenschappers bang zijn voor wiskunde. Op het eerste gezicht klinkt dit als een grap, maar helaas zeg ik dit in alle ernst. Een collega van mij vertelde me net hoe hij TLA+ aan verschillende ontwikkelaars probeerde uit te leggen. Zodra de formules op het scherm verschenen, werden hun ogen onmiddellijk glazig. Dus als TLA+ eng is, kun je het gebruiken , is een soort speelgoedprogrammeertaal. Een expressie in PlusCal kan elke TLA+-expressie zijn, dat wil zeggen, in principe elke wiskundige expressie. Bovendien heeft PlusCal syntaxis voor niet-deterministische algoritmen. Omdat PlusCal elke TLA+-expressie kan schrijven, is het aanzienlijk expressiever dan welke echte programmeertaal dan ook. Vervolgens wordt PlusCal gecompileerd tot een gemakkelijk leesbare TLA+ specificatie. Dit betekent uiteraard niet dat de complexe PlusCal-specificatie op TLA+ een eenvoudige zal worden - alleen dat de overeenkomst daartussen duidelijk is, er zal geen extra complexiteit verschijnen. Ten slotte kan deze specificatie worden geverifieerd met behulp van TLA+-tools. Over het algemeen kan PlusCal helpen een wiskundefobie te overwinnen; het is zelfs voor programmeurs en computerwetenschappers gemakkelijk te begrijpen. Ik heb er in het verleden al een tijdje (ongeveer 10 jaar) algoritmen op gepubliceerd.
Misschien zal iemand tegenwerpen dat TLA+ en PlusCal wiskunde zijn, en dat wiskunde alleen werkt met verzonnen voorbeelden. In de praktijk heb je een echte taal nodig met typen, procedures, objecten, enzovoort. Dit is fout. Dit is wat Chris Newcomb, die bij Amazon werkte, schrijft: “We hebben TLA+ gebruikt bij tien grote projecten, en in alle gevallen maakte het gebruik ervan een aanzienlijk verschil voor de ontwikkeling, omdat we gevaarlijke bugs konden onderscheppen voordat ze in productie gingen, en omdat het ons het inzicht en vertrouwen gaf dat we nodig hadden om agressieve oplossingen te ontwikkelen. prestatie-optimalisaties zonder de waarheid van het programma te beïnvloeden". Je hoort vaak dat we bij het gebruik van formele methoden inefficiënte code krijgen - in de praktijk is alles precies het tegenovergestelde. Bovendien bestaat de perceptie dat managers niet overtuigd kunnen worden van de noodzaak van formele methoden, ook al zijn programmeurs overtuigd van het nut ervan. En Newcomb schrijft: “Managers doen er nu alles aan om specificaties in TLA+ te schrijven en maken daar specifiek tijd voor vrij”. Dus als managers zien dat TLA+ werkt, omarmen ze het. Chris Newcomb schreef dit ongeveer zes maanden geleden (oktober 2014), maar voor zover ik weet wordt TLA+ nu in 14 projecten gebruikt, niet in 10. Een ander voorbeeld heeft betrekking op het ontwerp van de XBox 360. Er kwam een stagiair bij Charles Thacker en schreef specificaties voor het geheugensysteem. Dankzij deze specificatie werd een bug gevonden die anders onopgemerkt zou zijn gebleven en ervoor zou zorgen dat elke XBox 360 na vier uur gebruik crasht. Ingenieurs van IBM bevestigden dat hun tests deze bug niet zouden hebben gedetecteerd.
U kunt meer lezen over TLA+ op internet, maar laten we het nu hebben over informele specificaties. We hoeven zelden programma's te schrijven die de kleinste gemene deler en dergelijke berekenen. Veel vaker schrijven we programma's zoals de mooie printertool die ik voor TLA+ schreef. Na de eenvoudigste verwerking zou de TLA+-code er als volgt uitzien:
Maar in het bovenstaande voorbeeld wilde de gebruiker hoogstwaarschijnlijk dat de conjunctie en het isgelijkteken op één lijn lagen. De juiste opmaak zou er dus ongeveer zo uitzien:
Laten we een ander voorbeeld bekijken:
Hier was de uitlijning van gelijktekens, optelling en vermenigvuldiging in de bron daarentegen willekeurig, dus de eenvoudigste verwerking is voldoende. Over het algemeen bestaat er geen exacte wiskundige definitie van correcte opmaak, omdat 'correct' in dit geval betekent 'wat de gebruiker wil', en dit kan niet wiskundig worden bepaald.
Het lijkt erop dat als we geen definitie van waarheid hebben, de specificatie nutteloos is. Maar dat is niet waar. Het feit dat we niet weten wat een programma zou moeten doen, betekent niet dat we niet hoeven na te denken over hoe het zou moeten werken; integendeel, we zouden er zelfs nog meer moeite aan moeten besteden. Vooral de specificatie is hier belangrijk. Het is onmogelijk om het optimale programma voor gestructureerd afdrukken te bepalen, maar dit betekent niet dat we het helemaal niet moeten ondernemen, en het schrijven van code als een stroom van bewustzijn is niet het geval. Uiteindelijk heb ik een specificatie geschreven van zes regels met definities in de vorm van commentaar in een Java-bestand. Hier is een voorbeeld van een van de regels: a left-comment token is LeftComment aligned with its covering token. Deze regel is geschreven in, laten we zeggen, wiskundig Engels: LeftComment aligned, left-comment и covering token — termen met definities. Dit is hoe wiskundigen wiskunde beschrijven: ze schrijven definities van termen en creëren op basis daarvan regels. Het voordeel van deze specificatie is dat zes regels veel gemakkelijker te begrijpen en te debuggen zijn dan 850 regels code. Ik moet zeggen dat het schrijven van deze regels niet eenvoudig was; het kostte behoorlijk wat tijd om ze te debuggen. Ik heb speciaal voor dit doel code geschreven die me vertelde welke regel werd gebruikt. Omdat ik deze zes regels met een paar voorbeelden heb getest, hoefde ik geen 850 regels code te debuggen en waren de bugs vrij eenvoudig te vinden. Java heeft hiervoor geweldige tools. Als ik zojuist de code had geschreven, zou het veel langer hebben geduurd en zou de opmaak van mindere kwaliteit zijn geweest.
Waarom kon er geen formele specificatie worden gebruikt? Enerzijds is een correcte uitvoering hier niet zo belangrijk. Een gestructureerde afdruk zal voor sommigen ongetwijfeld onbevredigend zijn, dus ik hoefde het niet in alle ongebruikelijke situaties correct te laten werken. Nog belangrijker is het feit dat ik niet over het juiste gereedschap beschikte. De TLA+-modelcontrole is hier nutteloos, dus ik zou de voorbeelden met de hand moeten schrijven.
De gegeven specificatie heeft kenmerken die alle specificaties gemeen hebben. Het is een hoger niveau dan code. Het kan in elke taal worden geïmplementeerd. Er zijn geen tools of methoden om het te schrijven. Geen enkele programmeercursus zal u helpen bij het schrijven van deze specificatie. En er zijn geen tools die deze specificatie overbodig kunnen maken, tenzij je natuurlijk een taal schrijft die specifiek is voor het schrijven van gestructureerde afdrukprogramma's in TLA+. Ten slotte zegt deze specificatie niets over hoe we de code precies gaan schrijven, maar alleen wat de code doet. We schrijven een specificatie om ons te helpen het probleem te overdenken voordat we over de code gaan nadenken.
Maar deze specificatie heeft ook kenmerken die hem onderscheiden van andere specificaties. 95% van de andere specificaties zijn veel korter en eenvoudiger:
Verder is deze specificatie een reeks regels. Dit is meestal een teken van slechte specificatie. Het begrijpen van de gevolgen van een reeks regels is behoorlijk moeilijk, en daarom moest ik veel tijd besteden aan het debuggen ervan. In dit geval kon ik echter geen betere manier vinden.
Het is de moeite waard een paar woorden te zeggen over programma's die continu draaien. Meestal werken ze parallel, zoals besturingssystemen of gedistribueerde systemen. Er zijn maar heel weinig mensen die ze in hun hoofd of op papier kunnen begrijpen, en ik ben daar niet een van, hoewel ik dat ooit wel heb kunnen doen. Daarom hebben we tools nodig die ons werk controleren, bijvoorbeeld TLA+ of PlusCal.
Waarom moest ik een specificatie schrijven als ik al wist wat de code moest doen? Eigenlijk dacht ik alleen maar dat ik het wist. Bovendien hoeft een buitenstaander, als er een specificatie is opgesteld, niet langer in de code te kijken om te begrijpen wat deze precies doet. Ik heb een regel: er mogen geen algemene regels zijn. Er is natuurlijk een uitzondering op deze regel, dit is de enige algemene regel die ik volg: de specificatie van wat de code doet, moet mensen alles vertellen wat ze moeten weten als ze die code gebruiken.
Wat moeten programmeurs precies weten over denken? Om te beginnen hetzelfde als voor iedereen: als je niet schrijft, dan lijkt het alleen maar dat je denkt. Je moet ook nadenken voordat je codeert, wat betekent dat je moet schrijven voordat je codeert. Een specificatie is wat we schrijven voordat we beginnen met coderen. Voor elke code die door iedereen kan worden gebruikt of gewijzigd, is een specificatie nodig. En deze ‘iemand’ kan een maand nadat deze is geschreven de auteur van de code blijken te zijn. Er is een specificatie nodig voor grote programma's en systemen, voor klassen, voor methoden en soms zelfs voor complexe delen van een enkele methode. Wat moet je precies over de code schrijven? U moet beschrijven wat het doet, dat wil zeggen iets dat nuttig kan zijn voor iedereen die deze code gebruikt. Soms kan het ook nodig zijn om aan te geven hoe de code precies zijn doel bereikt. Als we deze methode in de cursus algoritmen hebben doorlopen, noemen we het een algoritme. Als het iets gespecialiseerders en nieuws is, dan noemen we het design op hoog niveau. Er is hier geen formeel verschil: beide zijn abstracte modellen van het programma.
Hoe moet je een codespecificatie precies schrijven? Het belangrijkste: het moet een niveau hoger zijn dan de code zelf. Het moet toestanden en gedragingen beschrijven. Het moet zo streng zijn als de taak vereist. Als u een specificatie schrijft over hoe een taak moet worden geïmplementeerd, dan kan deze in pseudocode worden geschreven of met PlusCal. U moet leren specificaties te schrijven met behulp van formele specificaties. Dit geeft je de nodige vaardigheden die ook zullen helpen bij informele vaardigheden. Hoe kun je formele specificaties leren schrijven? Toen we leerden programmeren, schreven we programma's en debuggen ze vervolgens. Hetzelfde hier: u moet een specificatie schrijven, deze controleren met een modelchecker en de fouten herstellen. TLA+ is mogelijk niet de beste taal voor een formele specificatie, en een andere taal is waarschijnlijk beter geschikt voor uw specifieke behoeften. Het mooie van TLA+ is dat het uitstekend werk levert bij het aanleren van wiskundig denken.
Hoe specificatie en code koppelen? Gebruik van commentaar dat wiskundige concepten en hun implementatie met elkaar verbindt. Als je met grafieken werkt, heb je op programmaniveau arrays van knooppunten en arrays van links. Je moet dus schrijven hoe de grafiek precies wordt geïmplementeerd door deze programmeerstructuren.
Opgemerkt moet worden dat geen van het bovenstaande van toepassing is op het proces van het schrijven van code zelf. Wanneer u code schrijft, dat wil zeggen de derde stap uitvoert, moet u ook over het programma nadenken en nadenken. Als een deeltaak complex of niet voor de hand liggend blijkt te zijn, moet je er een specificatie voor schrijven. Maar ik heb het hier niet over de code zelf. Je kunt elke programmeertaal en elke methodologie gebruiken, dit gaat niet over hen. Bovendien elimineert geen van de bovenstaande de noodzaak om uw code te testen en fouten op te sporen. Zelfs als het abstracte model correct is geschreven, kunnen er fouten optreden in de implementatie ervan.
Het schrijven van specificaties is een extra stap in het codeerproces. Dankzij dit kunnen veel fouten met minder moeite worden onderschept - dit weten we uit de ervaring van programmeurs van Amazon. Met specificaties wordt de kwaliteit van programma’s hoger. Waarom gaan we dan zo vaak zonder? Omdat schrijven moeilijk is. Maar schrijven is moeilijk, omdat je hiervoor moet nadenken, en denken is ook moeilijk. Het is altijd gemakkelijker om te doen alsof je nadenkt. Hier kan een analogie worden getrokken met hardlopen: hoe minder je rent, hoe langzamer je rent. Je moet je spieren trainen en oefenen met schrijven. Het vergt oefening.
De specificatie is mogelijk onjuist. Het kan zijn dat u ergens een fout heeft gemaakt, dat de eisen zijn veranderd of dat er een verbetering nodig is. Elke code die iemand gebruikt, moet worden gewijzigd, zodat vroeg of laat de specificatie niet langer overeenkomt met het programma. Idealiter moet u in dit geval een nieuwe specificatie schrijven en de code volledig herschrijven. Wij weten heel goed dat niemand dit doet. In de praktijk patchen we de code en updaten we eventueel de specificatie. Als dit vroeg of laat toch zal gebeuren, waarom zouden we dan überhaupt specificaties schrijven? Ten eerste zal voor de persoon die uw code gaat bewerken elk extra woord in de specificatie goud waard zijn, en deze persoon zou wel eens uzelf kunnen zijn. Ik schop mezelf vaak omdat ik niet specifiek genoeg ben als ik mijn code bewerk. En ik schrijf meer specificaties dan code. Daarom moet de specificatie altijd worden bijgewerkt als u de code bewerkt. Ten tweede wordt de code bij elke bewerking slechter en moeilijker te lezen en te onderhouden. Dit is een toename van de entropie. Maar als je niet met een specificatie begint, zal elke regel die je schrijft een bewerking zijn, en zal de code vanaf het begin omvangrijk en moeilijk te lezen zijn.
Zoals gezegd , geen enkele strijd werd gewonnen volgens een plan, en geen enkele strijd werd gewonnen zonder een plan. En hij wist iets van veldslagen. Er is een mening dat het schrijven van specificaties tijdverspilling is. Soms is dit waar, en is de taak zo eenvoudig dat het geen zin heeft erover na te denken. Maar u moet altijd onthouden dat wanneer u wordt geadviseerd geen specificaties te schrijven, dit betekent dat u ook wordt geadviseerd niet na te denken. En daar moet je elke keer over nadenken. Het doordenken van een taak garandeert niet dat je geen fouten zult maken. Zoals we weten heeft niemand een toverstaf uitgevonden en is programmeren een moeilijke taak. Maar als je niet goed nadenkt, maak je gegarandeerd fouten.
Meer over TLA+ en PlusCal kun je lezen op een speciale website, je kunt daar naartoe gaan vanaf mijn homepagina . Dat is alles voor mij, bedankt voor uw aandacht.
Houd er rekening mee dat dit een vertaling is. Wanneer u opmerkingen schrijft, houd er dan rekening mee dat de auteur deze niet zal lezen. Als je echt met de auteur wilt praten, zal hij op de Hydra 2019-conferentie zijn, die van 11 tot en met 12 juli 2019 in St. Petersburg wordt gehouden. Er kunnen kaartjes worden gekocht .
Bron: www.habr.com