Dit is een vertaalartikel . Maar eerst een korte inleiding. Hoe ontstaan zombie's? Iedereen komt wel eens in een situatie waarin je een vriend of collega naar jouw niveau wilt tillen, maar het lukt niet. En met 'het lukt niet' ligt het niet zozeer aan jou, maar aan hem: aan de ene kant staan een normaal salaris, taken, enzovoorts, en aan de andere kant de noodzaak om na te denken. Denken is vervelend en pijnlijk. Hij geeft snel op en blijft gewoon code schrijven, zonder zijn hersenen in te schakelen. Kun je je voorstellen hoeveel moeite het kost om de barrière van aangeleerde machteloosheid te overwinnen, en dan doe je het gewoon niet. Zo ontstaan zombie's die misschien te genezen zijn, maar waar volgens velen niemand zich mee bezig zal houden.
Toen ik zag dat (ja-ja, diezelfde man uit de boeken) en geen lezing gaf, maar een vragen-en-antwoorden-sessie, was ik een beetje op mijn hoede. Voor de duidelijkheid, Leslie is een wereldberoemde wetenschapper, auteur van grondleggende werken op het gebied van gedistribueerde computing, en je kunt hem misschien kennen van de letters La in het woord LaTeX — "Lamport TeX". Een tweede zorgwekkende factor is zijn eis: iedereen die komt, moet (volledig gratis) van tevoren een paar van zijn lezingen beluisteren, minimaal één vraag verzinnen en pas dan komen. Ik besloot te kijken wat Lamport te vertellen heeft — en het is geweldig! Dit is precies dat ding, een magische link-pil voor het genezen van zombiedom. Ik waarschuw je: de tekst kan veel weerstand oproepen bij liefhebbers van superflexibele methodologieën en niet-liefhebbers van het testen van wat geschreven is.
Na de hogebrokatie begint eigenlijk de vertaling van het seminar. Veel leesplezier!
Voor elke taak die je ook aanpakt, moet je altijd drie stappen doorlopen:
- bepalen welk doel je wilt bereiken;
- beslissen hoe je jouw doel gaat bereiken;
- aan je doel komen.
Dit geldt ook voor programmeren. Wanneer we code schrijven, moeten we:
- bepalen wat het programma moet doen;
- vaststellen hoe het zijn taak moet uitvoeren;
- de bijbehorende code schrijven.
De laatste stap is natuurlijk heel belangrijk, maar daar ga ik vandaag niet over spreken. In plaats daarvan zullen we de eerste twee bespreken. Deze uitvoert elke programmeur voordat hij gaat werken. Je gaat niet schrijven als je niet hebt besloten wat je precies gaat schrijven: een browser of een database. Een duidelijk idee van het doel moet aanwezig zijn. En je moet zorgvuldig nadenken over wat het programma precies zal doen, en niet zomaar wat op papier zetten in de hoop dat de code zichzelf in een browser verandert.
Hoe verloopt deze voorbereidende overdenking van de code? Hoeveel moeite moeten we hieraan besteden? Dit hangt af van hoe complex het probleem is dat we proberen op te lossen. Stel dat we een fouttolerant gedistribueerd systeem willen schrijven. In dit geval moeten we alles goed doordachten voordat we aan de code beginnen. Maar als we gewoon een gehele variabele met 1 moeten verhogen? Op het eerste gezicht lijkt dit triviaal en is er geen nadenken nodig, maar dan herinneren we ons dat er een overloop kan optreden. Daarom moet je, om te begrijpen of het een eenvoudig of complex probleem is, in eerste instantie nadenken.
Als je mogelijke oplossingen voor een probleem van tevoren overdenkt, kun je fouten vermijden. Maar om dat te doen, moet je denken helder zijn. Om dat te bereiken, moet je je gedachten opschrijven. Ik hou erg van de uitspraak van Dick Hinton: 'Wanneer je schrijft, toont de natuur je hoe slordig je denken is'. Als je niet schrijft, heb je alleen maar de indruk dat je nadenkt. En je moet je gedachten opschrijven in de vorm van specificaties.
Specificaties vervullen veel functies, vooral in grote projecten. Maar ik zal alleen over één daarvan spreken: ze helpen ons om helder te denken. Helder denken is erg belangrijk en behoorlijk moeilijk, dus we hebben hier elke ondersteuning nodig. In welke taal moeten we specificaties schrijven? Dit is altijd de eerste vraag voor programmeurs: in welke taal gaan we schrijven? Er is geen enkel juist antwoord op deze vraag: de problemen die we oplossen zijn te divers. Voor sommige mensen is TLA+ nuttig - dit is de specificatietaal die ik heb ontwikkeld. Voor anderen is het handiger om Chinees te gebruiken. Het hangt allemaal van de situatie af.
Een belangrijker vraag is: hoe kunnen we duidelijker denken? Antwoord: we moeten denken als wetenschappers. Dit is een denkwijze die zich in de afgelopen 500 jaar goed heeft bewezen. In de wetenschap bouwen we wiskundige modellen van de werkelijkheid. Astronomie was waarschijnlijk de eerste wetenschap in de strikte zin van het woord. In het wiskundige model dat in de astronomie wordt gebruikt, worden hemellichamen gepresenteerd als punten met massa, positie en momentum, hoewel ze in werkelijkheid extreem complexe objecten zijn met bergen en oceanen, getijden en stromingen. Dit model, net als elk ander, is gemaakt om specifieke problemen op te lossen. Het is perfect om te bepalen waar we de telescoop moeten richten als we een planeet willen vinden. Maar als je het weer op deze planeet wilt voorspellen, is dit model niet geschikt.
Wiskunde stelt ons in staat om de eigenschappen van het model te bepalen. En de wetenschap laat zien hoe deze eigenschappen zich verhouden tot de werkelijkheid. Laten we het hebben over onze wetenschap, computerwetenschappen. De werkelijkheid waarmee we werken, zijn de allerhande rekensystemen: processors, gameconsoles, computers die programma's uitvoeren, enzovoort. Ik zal het hebben over het uitvoeren van programma's op een computer, maar in wezen zijn al deze conclusies toepasbaar op elk rekensysteem. In onze wetenschap gebruiken we veel verschillende modellen: de Turingmachine, gedeeltelijk geordende verzamelingen van gebeurtenissen en nog veel meer.
Wat is een programma? Dit is elke code die op zichzelf kan worden beschouwd. Stel dat we een browser moeten schrijven. We voeren drie taken uit: we ontwerpen de weergave van het programma voor de gebruiker, vervolgens schrijven we een hoge-level schema van het programma, en tenslotte schrijven we de code. Terwijl we de code schrijven, realiseren we ons dat we een middel voor tekstopmaak moeten schrijven. Hier moeten we opnieuw drie taken oplossen: bepalen welke tekst dit middel zal retourneren; een algoritme voor opmaak kiezen; de code schrijven. Deze taak heeft een subtaak: het correct invoegen van koppeltekens in woorden. Deze subtaak lossen we ook in drie stappen op – zoals we zien, komen ze op veel niveaus terug.
Laten we de eerste stap wat gedetailleerder bekijken: welk probleem lost het programma op. Hier modelleren we het programma vaak als een functie die bepaalde invoer ontvangt en bepaalde uitvoer genereert. In de wiskunde wordt een functie meestal beschreven als een geordende verzameling van paren. Bijvoorbeeld, de functie die getallen kwadrateert voor natuurlijke getallen wordt beschreven als de verzameling {, , , , …}. Het domein van zo'n functie is de verzameling van de eerste elementen van elk paar, dat zijn de natuurlijke getallen. Om een functie te definiëren, moeten we het domein en de formule opgeven.
Maar functies in de wiskunde zijn niet hetzelfde als functies in programmeertalen. Wiskunde is aanzienlijk eenvoudiger. Aangezien ik geen tijd heb voor complexe voorbeelden, laten we een eenvoudig voorbeeld bekijken: een functie in de taal 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 de argumenten M en N, waar GCD(M,N) — een functie waarvan het domein de verzameling van paren gehele getallen is, en de geretourneerde waarde is het grootste gehele getal dat deelbaar is door M en N. Hoe verhoudt dit model zich tot de realiteit? Het model werkt met gehele getallen, terwijl we in C of Java 32-bits hebben. intDit model stelt ons in staat om te bepalen of het algoritme GCD, correct is, maar het voorkomt geen overflow-fouten. Daarvoor zou een complexer model nodig zijn, waar geen tijd voor is.
Laten we het hebben over de beperkingen van de functie als model. Het werk van sommige programma's (bijvoorbeeld besturingssystemen) komt niet alleen neer op het retourneren van een bepaalde waarde voor bepaalde argumenten, ze kunnen continu draaien. Bovendien is het functie als model niet geschikt voor de tweede stap: het plannen van de manier om het probleem op te lossen. Snelle sorteeralgoritmes en bubble sort berekenen dezelfde functie, maar zijn totaal verschillende algoritmes. Daarom gebruik ik een ander model voor het beschrijven van de manier om de doelstellingen van het programma te bereiken, laten we dit de standaard gedragsmodel noemen. In dit model wordt het programma voorgesteld als een verzameling van alle mogelijke gedragingen, waarbij elk gedrag op zijn beurt een reeks toestanden is, en een toestand is een toewijzing van waarden aan variabelen.
Laten we bekijken hoe de tweede stap van het Euclidische algoritme eruit zal zien. We moeten berekenen GCD(M, N). We initialiseren M hoe x, met behulp van 1 bit, gelijk aan 0, N hoe y, en trekken dan het kleinere van deze variabelen af van de grotere, totdat ze gelijk zijn. Bijvoorbeeld, als M = 12, met behulp van 1 bit, gelijk aan 0, N = 18, kunnen we het volgende gedrag beschrijven:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
En als M = 0 en N = 0? Ноль делится на все числа, поэтому наибольшего делителя в этом случае нет. В этой ситуации нам нужно вернуться к первому шагу и спросить: действительно ли нам нужно вычислять НОД для неположительных чисел? Если в этом нет необходимости, то нужно просто изменить спецификацию.
Hier is het goed om een kleine zijstap te maken over productiviteit. Dit wordt vaak gemeten aan het aantal geschreven regels code per dag. Maar je werk is veel nuttiger als je een bepaalde hoeveelheid regels kwijt bent, omdat je dan minder ruimte hebt voor bugs. En het is het gemakkelijkste om code kwijt te raken in de eerste stap. Het is heel goed mogelijk dat je al die ingewikkeldheden die je probeert te implementeren, gewoon niet nodig hebt. De snelste manier om een programma te vereenvoudigen en tijd te besparen, is door dingen niet te doen die je beter niet kunt doen. De tweede stap is de tweede grootste mogelijkheid om tijd te besparen. Als je productiviteit meet aan de hand van het aantal geschreven regels, dan zal overdenken hoe je een taak uitvoert je minder productief maken, omdat je dezelfde taak met minder code kunt oplossen. Ik kan hier geen exacte statistieken geven, omdat ik geen manier heb om het aantal regels te tellen die ik niet heb geschreven omdat ik tijd heb besteed aan specificaties, dat wil zeggen aan de eerste en tweede stappen. En een experiment uitvoeren is ook niet mogelijk, want in een experiment hebben we niet het recht om de eerste stap uit te voeren; de opdracht is van tevoren bepaald.
In informele specificaties is het gemakkelijk om veel problemen over het hoofd te zien. Er is niets ingewikkelds aan het schrijven van strikte specificaties voor functies, daar ga ik niet verder op in. In plaats daarvan zullen we het hebben over het schrijven van strikte specificaties voor standaard gedragsmodellen. Er is een stelling die stelt dat elke verzameling gedragingen kan worden beschreven met behulp van de beveiligingsfunctie (safety) en de levensvatbaarheidsfunctie (liveness)Veiligheid betekent dat er niets slechts zal gebeuren, het programma geen verkeerde antwoorden zal geven. Duurzaamheid betekent dat er vroeg of laat iets goeds zal gebeuren, dat wil zeggen, het programma zal vroeg of laat het juiste antwoord geven. Over het algemeen is veiligheid een belangrijkere maatstaf, fouten komen meestal hier voor. Daarom zal ik het over duurzaamheid niet hebben, hoewel het natuurlijk ook belangrijk is.
We behalen veiligheid door, ten eerste, talloze mogelijke begintoestanden te beschrijven. En, ten tweede, de relaties met alle mogelijke volgende toestanden voor elke toestand. Laten we ons als wetenschappers gedragen en de toestanden wiskundig definiëren. De verzameling begintoestanden wordt beschreven met een formule, bijvoorbeeld in het geval van het algoritme van Euclides: (x = M) ∧ (y = N). Voor bepaalde waarden M en N is er slechts één begintoestand. De relatie met de volgende toestand wordt beschreven met een formule waarin de variabelen van de volgende toestand met een streepje worden geschreven, en de huidige toestand zonder streepje. In het geval van het algoritme van Euclides zullen we te maken krijgen met de disjunctie van twee formules, waarbij de ene x de grootste waarde is en de andere y:
In het eerste geval is de nieuwe waarde van y gelijk aan de oude waarde van y, en de nieuwe waarde van x krijgen we door de kleinere van de grotere variabele af te trekken. In het tweede geval doen we het omgekeerde.
Laten we terugkeren naar het algoritme van Euclides. Laten we opnieuw aannemen dat M = 12, N = 18. Dit definieert de enige begintoestand, (x = 12) ∧ (y = 18). Vervolgens substitueren we deze waarden in de bovenstaande formule en krijgen we:
Hier is de enige mogelijke oplossing: x' = 18 - 12 ∧ y' = 12, en we krijgen het gedrag: [x = 12, y = 18]. Evenzo kunnen we alle toestanden in ons gedrag beschrijven: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
In de laatste toestand [x = 6, y = 6] zullen beide delen van de uitdrukking onwaar zijn, wat betekent dat er geen volgende toestand is. Dus, we hebben de volledige specificatie van de tweede stap — zoals we zien, is dit heel gewone wiskunde, zoals bij ingenieurs en wetenschappers, en niet vreemd, zoals in de informatica.
Deze twee formules kunnen worden samengevoegd tot één temporele logica formule. Het is elegant en eenvoudig uit te leggen, maar daar is nu geen tijd voor. Temporele logica kan alleen nodig zijn voor de eigenschap van levendigheid; voor veiligheid is het niet nodig. Temporele logica in zijn geheel bevalt niet, het is niet helemaal gewone wiskunde, maar in het geval van levendigheid is het een noodzakelijk kwaad.
In het algoritme van Euclides is er voor elke waarde x en y een unieke waarde x' en y', die de relatie met de volgende toestand waarmaakt. Met andere woorden, het algoritme van Euclides is deterministisch. Om een niet-deterministisch algoritme te modelleren, moet de huidige toestand meerdere mogelijke toekomstige toestanden hebben, en elke waarde van de variabele zonder streepje moet meerdere waarden hebben van de variabele met streepje, waarvoor de relatie met de volgende toestand waar is. Dit is niet moeilijk te doen, maar ik zal nu geen voorbeelden geven.
Om een werkend hulpmiddel te maken, is formele wiskunde nodig. Hoe maken we een formele specificatie? Hiervoor hebben we een formele taal nodig, bijvoorbeeld . De specificatie van het algoritme van Euclides zou eruitzien als volgt in deze taal:
Het symbool van het gelijkteken met een driehoek betekent dat de waarde links van het teken is gedefinieerd als gelijk aan de waarde rechts van het teken. In wezen is een specificatie een definitie, in ons geval twee definities. Bij de specificatie in TLA+ moeten we verklaringen en een bepaalde syntaxis toevoegen, zoals op de bovenstaande dia. In ASCII zou het er als volgt uitzien:
Zoals we zien, is er niets ingewikkelds aan. De specificatie in TLA+ kan worden gecontroleerd, dat wil zeggen, alle mogelijke gedragingen in een klein model doorlopen. In ons geval zullen deze waarden zijn M en N. Dit is een zeer efficiënte en eenvoudige manier van verificatie die volledig automatisch wordt uitgevoerd. Bovendien kunnen formele bewijzen van waarheidsgetrouwhheid worden geschreven en mechanisch worden gecontroleerd, maar daarvoor is veel tijd nodig, daarom doet bijna niemand dat.
Het grootste nadeel van TLA+ is dat het wiskunde is, en programmeurs en computerwetenschappers bang zijn voor wiskunde. Op het eerste gezicht klinkt dit als een grap, maar helaas spreek ik dit heel serieus. Mijn collega vertelde me net hoe hij het geprobeerd heeft uit te leggen aan een aantal ontwikkelaars. Zodra er formules op het scherm verschenen, kregen ze ogen als glazen schotels. Dus als TLA+ beangstigend is, kan men gebruiken , dit is een soort speelgoed programmeertaal. Een expressie in PlusCal kan elke expressie in TLA+ zijn, dat wil zeggen, in feite elke wiskundige expressie. Bovendien heeft PlusCal syntaxis voor niet-deterministische algoritmen. Omdat je in PlusCal elke expressie van TLA+ kunt opschrijven, is het aanzienlijk expressiever dan elke echte programmeertaal. Vervolgens wordt PlusCal gecompileerd naar een gemakkelijk leesbare specificatie van TLA+. Dit betekent natuurlijk niet dat een complexe specificatie van PlusCal zal veranderen in een eenvoudige op TLA+ — de overeenkomst tussen hen is duidelijk, er komt geen extra complexiteit bij. Tenslotte kan deze specificatie worden gecontroleerd met TLA+ tools. Kortom, PlusCal kan helpen om de angst voor wiskunde te overwinnen, het is gemakkelijk te begrijpen voor zelfs programmeurs en computerwetenschappers. In het verleden heb ik ongeveer 10 jaar lang algoritmes in PlusCal gepubliceerd.
Misschien weerlegt iemand dat TLA+ en PlusCal wiskunde zijn, en wiskunde werkt alleen met verzonnen voorbeelden. In de praktijk hebben we echter een echte taal nodig met types, procedures, objecten, enzovoort. Dat is niet zo. Dit is wat Chris Newcomb schrijft, die bij Amazon heeft gewerkt: «We hebben TLA+ gebruikt in tien grote projecten, en in elk geval heeft het gebruik ervan een aanzienlijke bijdrage geleverd aan de ontwikkeling, omdat we gevaarlijke bugs konden opsporen voordat ze in productie kwamen, en omdat het ons het begrip en de zekerheid gaf die nodig zijn voor agressieve prestatieoptimalisaties zonder de juistheid van het programma aan te tasten». Vaak hoort men dat het gebruik van formele methoden resulteert in inefficiënte code — in de praktijk is het echter precies het tegenovergestelde. Bovendien bestaat de algemene opvatting dat het onmogelijk is om managers te overtuigen van de noodzaak van formele methoden, zelfs als programmeurs overtuigd zijn van hun nut. En Newcomb schrijft: Managers are increasingly encouraging the writing of specifications in TLA+, and are specifically allocating time for it.So when managers see that TLA+ works, they happily accept it. Chris Newcomb wrote this about six months ago (in October 2014); as far as I know, TLA+ is now used in 14 projects, not 10. Another example relates to the design of the Xbox 360. A intern came to Charles Ticker and wrote a specification for the memory system. Thanks to this specification, a bug was found that would otherwise have gone unnoticed, causing every Xbox 360 to crash after four hours of use. Engineers at IBM confirmed that their tests would not have detected this bug.
You can read more about TLA+ on the internet, but now let's talk about informal specifications. We rarely have to write programs that calculate the greatest common divisor and the like. More often, we write programs like the pretty-printer tool that I wrote for TLA+. After the simplest processing, the TLA+ code would look like this:
But in the given example, the user likely wanted the conjunction and equality signs to be aligned. So the correct formatting would look more like this:
Let's consider another example:
Here, on the contrary, the alignment of the equality, addition, and multiplication signs in the source was random, so the simplest processing is quite sufficient. In general, there is no precise mathematical definition of correct formatting because 'correct' in this case means 'what the user wants,' and this cannot be defined mathematically.
It might seem that if we have no definition of truth, the specification is useless. But that's not the case. If we don't know exactly what the program should do, it doesn't mean we shouldn't think through its operation—in fact, we should put even more effort into it. The specification is particularly important here. It is impossible to define the optimal program for pretty-printing, but that doesn't mean we should avoid tackling it; writing code as a stream of consciousness is not the way. In the end, I wrote a specification consisting of six rules with definitions. in the form of comments. in het Java-bestand. Hier is een voorbeeld van een van de regels: een left-comment token is LeftComment uitgelijnd met zijn dekkende token. Deze regel is geschreven in, laten we zeggen, wiskundig Engels: LeftComment uitgelijnd, left-comment en dekkende token — termen met definities. Dit is hoe wiskundigen wiskunde beschrijven: ze schrijven definities van termen en op basis daarvan - regels. Het voordeel van zo'n specificatie is dat het begrijpen en debuggen van zes regels veel eenvoudiger is dan 850 regels code. Het moet gezegd worden dat het schrijven van deze regels niet eenvoudig was; het kostte behoorlijk wat tijd om ze te debuggen. Speciaal voor dit doel schreef ik code die aangaf welke regel precies werd gebruikt. Doordat ik deze zes regels op verschillende voorbeelden testte, hoefde ik geen 850 regels code te debuggen en was het relatief eenvoudig om bugs te vinden. In Java zijn er uitstekende tools hiervoor. Als ik gewoon code had geschreven, had het me aanzienlijk meer tijd gekost en zou de opmaak van slechtere kwaliteit zijn geweest.
Waarom kon er geen formele specificatie worden gebruikt? Enerzijds is de correctheid hier niet zo belangrijk. Structuurtabellen zullen onvermijdelijk iemand niet bevallen, dus ik hoefde niet te zorgen voor correcte werking in alle ongewone situaties. Nog belangrijker is het feit dat ik niet de juiste tools had. Een hulpmiddel voor het controleren van modellen TLA+ is hier nutteloos, dus ik zou voorbeelden handmatig moeten schrijven.
De gegeven specificatie heeft kenmerken die gemeenschappelijk zijn voor alle specificaties. Het is van een hoger niveau dan code. Het kan in elke taal worden geïmplementeerd. Voor het schrijven ervan zijn geen hulpmiddelen of methoden nuttig. Geen enkele programmeercursus zal je helpen deze specificatie te schrijven. En er zijn geen tools die deze specificatie overbodig zouden maken, tenzij je een taal schrijft die speciaal is ontworpen voor het schrijven van programmatuur voor structuurtabellen in TLA+. Ten slotte zegt deze specificatie niets over hoe we de code precies gaan schrijven; het geeft alleen aan wat deze code doet. We schrijven de specificatie om ons te helpen het probleem te overdenken voordat we over de code gaan nadenken.
Maar deze specificatie heeft ook kenmerken die het onderscheiden van andere specificaties. 95% van de andere specificaties is aanzienlijk korter en eenvoudiger:
Verder is deze specificatie een set van regels. Over het algemeen is dit een teken van een slechte specificatie. De gevolgen van een set regels begrijpen is vrij moeilijk, en daarom heb ik veel tijd besteed aan het debuggen ervan. Desondanks was er in dit geval geen betere manier voor mij te vinden.
Het is de moeite waard om een paar woorden te zeggen over programma's die continu werken. Over het algemeen werken ze parallel, zoals besturingssystemen of gedistribueerde systemen. Slechts enkelen kunnen deze begrijpen, zowel in hun hoofd als op papier, en ik behoor daar niet toe, hoewel ik dat ooit wel kon. Daarom zijn er hulpmiddelen nodig die ons werk controleren — zoals TLA+ of PlusCal.
Waarom moest ik een specificatie schrijven als ik al wist wat de code moest doen? In werkelijkheid leek het alleen maar alsof ik dat wist. Bovendien, met een specificatie heeft een buitenstaander niet meer de noodzaak om in de code te duiken om te begrijpen wat hij doet. Ik heb een regel: er zouden geen algemene regels moeten zijn. Dit heeft natuurlijk een uitzondering, het is de enige algemene regel die ik volg: de specificatie van wat de code doet, moet mensen alles vertellen wat ze moeten weten bij het gebruik van deze code.
Wat moeten programmeurs weten over denken? Eerst en vooral, hetzelfde als iedereen: als je niet schrijft, lijkt het alleen maar alsof je denkt. Daarnaast moet je nadenken voordat je codeert, wat betekent dat je eerst moet schrijven voordat je begint met coderen. Een specificatie is wat we schrijven voordat we beginnen met coderen. Een specificatie is nodig voor elke code die door iemand kan worden gebruikt of gewijzigd. En die 'iemand' kan de auteur van de code zelf zijn, een maand na het schrijven ervan. Een specificatie is 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? Je moet beschrijven wat het doet, dat wil zeggen wat nuttig kan zijn voor iedereen die deze code gebruikt. Soms kan het ook nodig zijn om aan te geven hoe de code zijn doel bereikt. Als we die methode in de algoritmescursus hebben behandeld, noemen we dit een algoritme. Als het iets meer specifieks en nieuws is, noemen we dit hoog-niveau ontwerp. Er is geen formeel verschil: zowel het als het andere is een abstract model van een programma.
Hoe moet je een specificatie voor code schrijven? Het belangrijkste: het moet een niveau boven de code zelf zijn. Het moet toestanden en gedrag beschrijven. Het moet zo streng zijn als de taak vereist. Als je een specificatie schrijft voor de implementatiemethode van een taak, kan deze worden geschreven in pseudocode of met PlusCal. Leren om specificaties te schrijven, moet beginnen met formele specificaties. Dit geeft je de nodige vaardigheden die ook nuttig zijn voor informele specificaties. Maar hoe leer je formele specificaties schrijven? Toen we programmeerden, schreven we programma's en debugden ze vervolgens. Hetzelfde geldt hier: je moet een specificatie schrijven, deze controleren met behulp van een modelchecker en eventuele fouten corrigeren. TLA+ is misschien niet de beste taal voor formele specificaties, en voor jouw specifieke behoeften is waarschijnlijk een andere taal geschikter. Het voordeel van TLA+ is dat het uitstekend mathematisch denken aanleert.
Hoe verbind je specificaties met code? Door middel van opmerkingen die wiskundige concepten en hun implementatie koppelen. Als je met grafen werkt, heb je op het programmamacroniveau arrays van knooppunten en arrays van verbindingen. Daarom moet je schrijven hoe precies de grafiek door deze programmeerstructuren wordt geïmplementeerd.
Het is belangrijk op te merken dat niets van het bovenstaande betrekking heeft op het daadwerkelijke proces van coderen. Wanneer je code schrijft, dat wil zeggen de derde stap uitvoert, moet je ook nadenken en de programma's goed doordenken. Als een deeltaak gecompliceerd of onduidelijk blijkt, moet je er een specificatie voor schrijven. Maar over de code zelf heb ik het hier niet. Je kunt elke programmeertaal gebruiken, elke methodologie, daar gaat het niet om. Bovendien geeft niets van het bovenstaande je vrijstelling van de noodzaak om code te testen en debuggen. Zelfs als het abstracte model juist is geschreven, kunnen er bugs in de implementatie zitten.
Het schrijven van specificaties is een extra stap in het proces van coderen. Hiermee kunnen veel fouten met minder moeite worden opgespoord - dit weten we uit de ervaring van programmeurs bij Amazon. Met specificaties wordt de kwaliteit van programmatuur hoger. Waarom komen we dan zo vaak zonder ze toe? Omdat schrijven moeilijk is. En schrijven is moeilijk omdat je moet nadenken, en nadenken is ook moeilijk. Het is altijd gemakkelijker om te doen alsof je denkt. Hier kan je een analogie met hardlopen maken: hoe minder je rent, hoe langzamer je rent. Je moet je spieren trainen en oefenen met schrijven. Oefening baart kunst.
De specificatie kan onjuist zijn. U heeft misschien ergens een fout gemaakt, of de vereisten zijn veranderd, of het is noodzakelijk geweest om verbeteringen aan te brengen. Elke code die iemand gebruikt, moet worden aangepast, dus vroeg of laat zal de specificatie niet meer overeenkomen met het programma. Idealiter zou je in dit geval een nieuwe specificatie moeten schrijven en de code volledig opnieuw moeten schrijven. We weten allemaal dat dat bijna nooit gebeurt. In de praktijk patchen we de code en werken we wellicht de specificatie bij. Als dit onvermijdelijk vroeg of laat gebeurt, waarom zou je dan überhaupt specificaties schrijven? Ten eerste, voor de persoon die uw code moet aanpassen, is elk extra woord in de specificatie van onschatbare waarde, en die persoon zou heel goed uzelf kunnen zijn. Ik berisp mezelf vaak vanwege een onvoldoende specificatie wanneer ik mijn code aanpas. En ik schrijf meer specificaties dan code. Daarom moet u altijd de specificatie bijwerken wanneer u de code aanpast. Ten tweede, met elke aanpassing wordt de code slechter, het wordt steeds moeilijker te lezen en te onderhouden. Dit is een toename van entropie. Maar als u niet met een specificatie begint, zal elke geschreven regel een aanpassing zijn, en zal de code vanaf het begin omvangrijk en moeilijk leesbaar zijn.
Zoals gezegd , is er geen enkele strijd gewonnen volgens plan, en geen enkele strijd is gewonnen zonder plan. En hij wist iets over oorlogen. Er is een mening dat het schrijven van specificaties een verspilling van tijd is. Soms is dat inderdaad zo, en is de taak zo eenvoudig dat het niet echt nodig is om erover na te denken. Maar men moet altijd in gedachten houden dat wanneer iemand u adviseert geen specificaties te schrijven, dit betekent dat men u adviseert niet na te denken. En daar moet je elke keer over nadenken. Het doordenken van een taak garandeert niet dat u geen fouten maakt. Zoals we weten, is er geen toverstokje uitgevonden, en programmeren is een ingewikkelde bezigheid. Maar als u de taak niet doordenkt, maakt u gegarandeerd fouten.
Meer over TLA+ en PlusCal kunt u lezen op een speciale website, die toegankelijk is via mijn homepage . Dat is alles van mijn kant, bedankt voor uw aandacht.
Ter herinnering, dit is een vertaling. Wanneer je opmerkingen schrijft, onthoud dan dat de auteur deze niet zal lezen. Als je echt met de auteur wilt communiceren, zal hij aanwezig zijn op de Hydra 2019-conferentie die op 11-12 juli 2019 in Sint-Petersburg plaatsvindt. Tickets zijn verkrijgbaar. .
Bron: habr.com
