Tämä artikkeli on käännös . Mutta ennen häntä pieni esittely. Miten zombit muodostuvat? Jokainen on joutunut tilanteeseen, jossa he haluavat vetää ystävän tai kollegan omalle tasolleen, mutta se ei onnistu. Eikä se "ei onnistu" niinkään sinussa kuin hänessä: toisella puolella on normaali palkka, tehtävät ja niin edelleen, ja toisaalta tarve ajatella. Ajattelu on epämiellyttävää ja tuskallista. Hän luovuttaa nopeasti ja jatkaa koodin kirjoittamista kytkemättä aivojaan lainkaan päälle. Kuvittelet, kuinka paljon vaivaa vaatii opitun avuttomuuden esteen ylittäminen, etkä vain tee sitä. Näin muodostuu zombeja, jotka näyttävät olevan parannettavissa, mutta näyttää siltä, että kukaan ei tee sitä.
Kun näin sen (kyllä, sama toveri oppikirjoista) ja ei tee raporttia, vaan kysymys-vastaus-istunnon, olin hieman varovainen. Varmuuden vuoksi Leslie on maailmankuulu tiedemies, hajautetun laskennan perusteosten kirjoittaja, ja voit myös tuntea hänet La-kirjaimista sanassa LaTeX - “Lamport TeX”. Toinen hälyttävä tekijä on hänen vaatimuksensa: jokaisen saapuvan täytyy (täysin ilmaiseksi) kuunnella pari hänen raporttiaan etukäteen, keksiä niistä vähintään yksi kysymys ja vasta sitten tulla. Päätin nähdä, mitä Lamport lähettää siellä - ja se on hienoa! Se on juuri se asia, maaginen linkkipilleri zombien parantamiseen. Varoitan: tekstin perusteella superjoustavien menetelmien ystävät ja ne, jotka eivät halua testata kirjoitettua, voivat polttaa huomattavasti.
Habrokatin jälkeen alkaa itse asiassa seminaarin kääntäminen. Nauti lukemisesta!
Mitä tahansa tehtävää otatkin vastaan, sinun tulee aina käydä läpi kolme vaihetta:
- päätä, minkä tavoitteen haluat saavuttaa;
- päättää, kuinka saavutat tavoitteesi;
- tule tavoitteeseesi.
Tämä koskee myös ohjelmointia. Kun kirjoitamme koodia, meidän on:
- päättää, mitä ohjelman pitäisi tehdä;
- määrittää, kuinka sen tulee suorittaa tehtävänsä;
- kirjoita vastaava koodi.
Viimeinen vaihe on tietysti erittäin tärkeä, mutta en puhu siitä tänään. Sen sijaan keskustelemme kahdesta ensimmäisestä. Jokainen ohjelmoija suorittaa ne ennen työn aloittamista. Et istu alas kirjoittamaan, ellet ole päättänyt, kirjoitatko selaimella vai tietokantaan. Tietty käsitys tavoitteesta täytyy olla läsnä. Ja mietit ehdottomasti, mitä ohjelma tarkalleen tekee, äläkä kirjoita jotenkin siinä toivossa, että koodi muuttuu jotenkin selaimeksi.
Miten tämä koodin ennakko-ajattelu oikein tapahtuu? Kuinka paljon meidän pitäisi panostaa tähän? Kaikki riippuu siitä, kuinka monimutkaista ongelmaa ratkaisemme. Oletetaan, että haluamme kirjoittaa vikasietoisen hajautetun järjestelmän. Tässä tapauksessa meidän tulisi miettiä asioita huolellisesti ennen kuin alamme koodaamaan. Entä jos meidän täytyy vain kasvattaa kokonaislukumuuttujaa yhdellä? Ensi silmäyksellä täällä kaikki on triviaalia, eikä ajattelua tarvita, mutta sitten muistamme, että ylivuoto voi tapahtua. Siksi jopa ymmärtääksesi, onko ongelma yksinkertainen vai monimutkainen, sinun on ensin mietittävä.
Jos mietit mahdollisia ratkaisuja ongelmaan etukäteen, voit välttää virheet. Mutta tämä vaatii, että ajatuksesi on selkeä. Tämän saavuttamiseksi sinun on kirjoitettava ajatuksesi muistiin. Pidän todella Dick Guindonin lainauksesta: "Kun kirjoitat, luonto näyttää, kuinka huolimaton ajattelusi on." Jos et kirjoita, luulet vain ajattelevasi. Ja sinun on kirjoitettava ajatuksesi muistiin eritelmien muodossa.
Tekniset tiedot suorittavat monia toimintoja, erityisesti suurissa projekteissa. Mutta puhun vain yhdestä niistä: ne auttavat meitä ajattelemaan selkeästi. Selkeä ajattelu on erittäin tärkeää ja melko vaikeaa, joten tässä tarvitsemme apua. Millä kielellä tekniset tiedot pitäisi kirjoittaa? Tämä on yleensä aina ohjelmoijien ensimmäinen kysymys: millä kielellä kirjoitamme. Siihen ei ole yhtä oikeaa vastausta: ratkaisemamme ongelmat ovat liian erilaisia. Joillekin TLA+ on kehittämäni määrittelykieli. Toisille on kätevämpää käyttää kiinaa. Kaikki riippuu tilanteesta.
Tärkeämpi on toinen kysymys: kuinka saada aikaan selkeämpi ajattelu? Vastaus: Meidän täytyy ajatella kuin tiedemiehet. Tämä on ajattelutapa, joka on osoittautunut viimeisten 500 vuoden aikana. Tieteessä rakennamme matemaattisia todellisuuden malleja. Tähtitiede oli ehkä ensimmäinen tiede sanan suppeassa merkityksessä. Tähtitieteessä käytetyssä matemaattisessa mallissa taivaankappaleet esiintyvät pisteinä, joilla on massa, sijainti ja liikemäärä, vaikka todellisuudessa ne ovat erittäin monimutkaisia esineitä, joilla on vuoria ja valtameriä, vuorovesi- ja vuorovesi. Tämä malli, kuten kaikki muutkin, luotiin tiettyjen ongelmien ratkaisemiseksi. Sen avulla voit selvittää, mihin kohdistaa kaukoputkesi, jos sinun on löydettävä planeetta. Mutta jos haluat ennustaa tämän planeetan sään, tämä malli ei toimi.
Matematiikka antaa meille mahdollisuuden määrittää mallin ominaisuudet. Ja tiede osoittaa, kuinka nämä ominaisuudet liittyvät todellisuuteen. Puhutaanpa tieteestämme, tietojenkäsittelytieteestämme. Todellisuus, jonka parissa työskentelemme, on erilaisia laskentajärjestelmiä: prosessorit, pelikonsolit, tietokoneet, ohjelmien suorittaminen ja niin edelleen. Puhun ohjelman suorittamisesta tietokoneella, mutta yleisesti ottaen kaikki nämä johtopäätökset koskevat kaikkia tietokonejärjestelmiä. Tieteessämme käytämme monia erilaisia malleja: Turingin konetta, osittain tilattuja tapahtumasarjoja ja monia muita.
Mikä on ohjelma? Tämä on mikä tahansa koodi, jota voidaan tarkastella itsenäisesti. Oletetaan, että meidän on kirjoitettava selain. Suoritamme kolme tehtävää: suunnittelemme käyttäjän näkemyksen ohjelmasta, kirjoitamme sitten ohjelman korkean tason kaavion ja lopuksi kirjoitamme koodin. Kun kirjoitamme koodia, ymmärrämme, että meidän on kirjoitettava tekstinmuotoilija. Tässä meidän on jälleen ratkaistava kolme ongelmaa: määritetään minkä tekstin tämä työkalu palauttaa; valitse muotoilun algoritmi; kirjoittaa koodia. Tällä tehtävällä on oma osatehtävänsä: lisää yhdysviiva oikein sanoihin. Ratkaisemme myös tämän alitehtävän kolmessa vaiheessa - kuten näet, ne toistuvat monella tasolla.
Tarkastellaan tarkemmin ensimmäistä vaihetta: minkä ongelman ohjelma ratkaisee. Tässä mallinnetaan useimmiten ohjelmaa funktiona, joka ottaa jonkin syötteen ja tuottaa jonkin verran tulosta. Matematiikassa funktiota kuvataan yleensä järjestetyksi parijoukoksi. Esimerkiksi luonnollisten lukujen neliöintifunktio kuvataan joukkona {<0,0>, <1,1>, <2,4>, <3,9>, …}. Tällaisen funktion toimialue on kunkin parin ensimmäisten alkioiden, toisin sanoen luonnollisten lukujen, joukko. Funktion määrittelemiseksi meidän on määritettävä sen laajuus ja kaava.
Mutta funktiot matematiikassa eivät ole samoja kuin funktiot ohjelmointikielissä. Matematiikka on paljon helpompaa. Koska minulla ei ole aikaa monimutkaisille esimerkeille, harkitaan yksinkertaista: funktiota C:ssä tai staattista menetelmää Javassa, joka palauttaa kahden kokonaisluvun suurimman yhteisen jakajan. Tämän menetelmän määrittelyssä kirjoitamme: laskee GCD(M,N) argumentteja varten M и NMissä GCD(M,N) - funktio, jonka toimialue on kokonaislukuparien joukko ja palautusarvo on suurin kokonaisluku, joka on jaollinen M и N. Miten tämä malli liittyy todellisuuteen? Malli toimii kokonaisluvuilla, kun taas C:ssä tai Javassa meillä on 32-bittinen int. Tämän mallin avulla voimme päättää, onko algoritmi oikea GCD, mutta se ei estä ylivuotovirheitä. Tämä vaatisi monimutkaisempaa mallia, jolle ei ole aikaa.
Puhutaanpa funktion rajoituksista mallina. Jotkut ohjelmat (kuten käyttöjärjestelmät) eivät vain palauta tiettyä arvoa tietyille argumenteille, vaan ne voivat toimia jatkuvasti. Lisäksi toiminto mallina ei sovellu hyvin toiseen vaiheeseen: ongelman ratkaisun suunnitteluun. Pikalajittelu ja kuplalajittelu laskevat saman funktion, mutta ne ovat täysin erilaisia algoritmeja. Siksi kuvaamaan, kuinka ohjelman tavoite saavutetaan, käytän eri mallia, kutsutaan sitä normaaliksi käyttäytymismalliksi. Siinä oleva ohjelma esitetään joukona kaikkia sallittuja käyttäytymismalleja, joista jokainen on puolestaan tilasarja, ja tila on arvojen määrittäminen muuttujille.
Katsotaanpa, miltä Euclid-algoritmin toinen vaihe näyttäisi. Meidän on laskettava GCD(M, N). Alustamme M как xJa N как y, vähennä sitten toistuvasti pienempi näistä muuttujista suuremmasta, kunnes ne ovat yhtä suuret. Esimerkiksi jos M = 12Ja N = 18, voimme kuvata seuraavan käyttäytymisen:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
Ja jos M = 0 и N = 0? Nolla on jaollinen kaikilla luvuilla, joten tässä tapauksessa ei ole suurinta jakajaa. Tässä tilanteessa meidän on palattava ensimmäiseen vaiheeseen ja kysyttävä: tarvitseeko meidän todella laskea GCD ei-positiivisille luvuille? Jos tämä ei ole välttämätöntä, sinun tarvitsee vain muuttaa määrityksiä.
Tässä meidän pitäisi tehdä pieni poikkeama tuottavuudesta. Se mitataan usein päivässä kirjoitettujen koodirivien lukumääränä. Mutta työsi on paljon hyödyllisempää, jos pääset eroon tietystä määrästä rivejä, koska sinulla on vähemmän tilaa bugeille. Ja helpoin tapa päästä eroon koodista on ensimmäinen askel. On täysin mahdollista, että et vain tarvitse kaikkia kelloja ja pillejä, joita yrität toteuttaa. Nopein tapa yksinkertaistaa ohjelmaa ja säästää aikaa on olla tekemättä asioita, joita ei pitäisi tehdä. Toinen vaihe on toiseksi eniten aikaa säästävä potentiaali. Jos mittaat tuottavuutta kirjoitetuilla riveillä, ajattelu siitä, miten tehtävä suoritetaan, saa sinut vähemmän tuottava, koska voit ratkaista saman ongelman vähemmällä koodilla. En voi antaa tarkkoja tilastoja täällä, koska minulla ei ole tapaa laskea niiden rivien määrää, joita en kirjoittanut, koska vietin aikaa määrittelyyn, eli ensimmäiseen ja toiseen vaiheeseen. Eikä kokeilua voi asettaa tännekään, koska kokeilussa meillä ei ole oikeutta suorittaa ensimmäistä vaihetta, tehtävä on ennalta määrätty.
Epävirallisissa eritelmissä on helppo jättää huomiotta monet vaikeudet. Ei ole mitään vaikeaa kirjoittaa tiukkoja eritelmiä funktioille, en käsittele tätä. Sen sijaan puhumme vahvojen standardien määrittelyjen kirjoittamisesta. On olemassa lause, joka sanoo, että mikä tahansa käyttäytymisjoukko voidaan kuvata suojausominaisuuden avulla (turvallisuus) ja selviytymisominaisuudet (eloisuus). Turvallisuus tarkoittaa, että mitään pahaa ei tapahdu, ohjelma ei anna väärää vastausta. Selviytyvyys tarkoittaa, että ennemmin tai myöhemmin tapahtuu jotain hyvää, eli ohjelma antaa oikean vastauksen ennemmin tai myöhemmin. Pääsääntöisesti turvallisuus on tärkeämpi indikaattori, virheitä tapahtuu useimmiten täällä. Siksi ajan säästämiseksi en puhu selviytyvyydestä, vaikka se on tietysti myös tärkeää.
Saavutamme turvallisuuden määräämällä ensin joukko mahdollisia alkutiloja. Ja toiseksi suhteet kaikkiin mahdollisiin seuraaviin tiloihin kussakin osavaltiossa. Toimitaan kuin tiedemiehet ja määritellään tilat matemaattisesti. Alkutilojen joukko kuvataan kaavalla, esimerkiksi Euklides-algoritmin tapauksessa: (x = M) ∧ (y = N). Tietyille arvoille M и N on vain yksi alkutila. Suhdetta seuraavaan tilaan kuvataan kaavalla, jossa seuraavan tilan muuttujat kirjoitetaan alkuluvulla ja nykyisen tilan muuttujat ilman alkulukua. Eukleideen algoritmin tapauksessa käsittelemme kahden kaavan disjunktiota, joista toisessa x on suurin arvo, ja toisessa - y:
Ensimmäisessä tapauksessa y:n uusi arvo on yhtä suuri kuin y:n edellinen arvo ja x:n uusi arvo saadaan vähentämällä pienempi muuttuja suuremmasta. Toisessa tapauksessa teemme päinvastoin.
Palataan Eukleideen algoritmiin. Oletetaanpa taas niin M = 12, N = 18. Tämä määrittää yhden alkutilan, (x = 12) ∧ (y = 18). Yhdistämme sitten nämä arvot yllä olevaan kaavaan ja saamme:
Tässä on ainoa mahdollinen ratkaisu: x' = 18 - 12 ∧ y' = 12ja saamme käyttäytymisen: [x = 12, y = 18]. Samalla tavalla voimme kuvata kaikki käyttäytymisemme tilat: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
Viimeisessä tilassa [x = 6, y = 6] molemmat lausekkeen osat ovat epätosi, joten sillä ei ole seuraavaa tilaa. Joten meillä on täydellinen erittely toisesta vaiheesta - kuten näet, tämä on aivan tavallista matematiikkaa, kuten insinööreissä ja tiedemiehissä, eikä outoa, kuten tietojenkäsittelytieteessä.
Nämä kaksi kaavaa voidaan yhdistää yhdeksi ajallisen logiikan kaavaksi. Hän on tyylikäs ja helppo selittää, mutta nyt ei ole aikaa hänelle. Saatamme tarvita ajallista logiikkaa vain eloisuudelle, sitä ei tarvita turvallisuuden vuoksi. En pidä ajallisesta logiikasta sinänsä, se ei ole aivan tavallista matematiikkaa, mutta elävyyden tapauksessa se on välttämätön paha.
Euklidesin algoritmissa jokaiselle arvolle x и y on ainutlaatuisia arvoja x' и y', jotka tekevät suhteen seuraavaan tilaan tosi. Toisin sanoen Eukleideen algoritmi on deterministinen. Epädeterministisen algoritmin mallintamiseksi nykyisellä tilalla on oltava useita mahdollisia tulevaisuuden tiloja ja jokaisella alustamattomalla muuttujan arvolla on useita esikäsiteltyjä muuttujan arvoja siten, että suhde seuraavaan tilaan on tosi. Tämä on helppo tehdä, mutta en nyt anna esimerkkejä.
Työvälineen tekemiseen tarvitaan muodollista matematiikkaa. Kuinka tehdä määrittelystä muodollinen? Tätä varten tarvitsemme muodollisen kielen, esim. . Euklidisen algoritmin määrittely näyttäisi tältä tällä kielellä:
Kolmiolla varustettu yhtäläisyysmerkkisymboli tarkoittaa, että merkin vasemmalla puolella oleva arvo määritellään yhtä suureksi kuin merkin oikealla puolella oleva arvo. Pohjimmiltaan spesifikaatio on määritelmä, meidän tapauksessamme kaksi määritelmää. TLA+:n määrityksiin sinun on lisättävä ilmoitukset ja syntaksi, kuten yllä olevassa diassa. ASCII:ssa se näyttäisi tältä:
Kuten näette, ei mitään monimutkaista. TLA+:n spesifikaatiota voidaan testata, eli ohittaa kaikki mahdolliset käyttäytymiset pienessä mallissa. Meidän tapauksessamme tämä malli on tiettyjä arvoja M и N. Tämä on erittäin tehokas ja yksinkertainen tarkistusmenetelmä, joka on täysin automaattinen. On myös mahdollista kirjoittaa muodollisia totuustodistuksia ja tarkistaa ne mekaanisesti, mutta tämä vie paljon aikaa, joten melkein kukaan ei tee sitä.
TLA+:n suurin haittapuoli on, että se on matematiikkaa, ja ohjelmoijat ja tietojenkäsittelytieteilijät pelkäävät matematiikkaa. Ensi silmäyksellä tämä kuulostaa vitsiltä, mutta valitettavasti tarkoitan sitä täysin vakavasti. Kollegani kertoi juuri minulle, kuinka hän yritti selittää TLA+:n useille kehittäjille. Heti kun kaavat ilmestyivät näytölle, niistä tuli välittömästi lasimaisia silmiä. Joten jos TLA+ pelottaa sinua, voit käyttää , se on eräänlainen leluohjelmointikieli. PlusCalin lauseke voi olla mikä tahansa TLA+-lauseke, eli yleisesti ottaen mikä tahansa matemaattinen lauseke. Lisäksi PlusCalissa on syntaksi ei-deterministisille algoritmeille. Koska PlusCal voi kirjoittaa mitä tahansa TLA+ -lauseketta, PlusCal on paljon ilmaisuvoimaisempi kuin mikään oikea ohjelmointikieli. Seuraavaksi PlusCal kootaan helposti luettavaksi TLA+ -spesifikaatioksi. Tämä ei tietenkään tarkoita, että monimutkainen PlusCal-spesifikaatio muuttuisi yksinkertaiseksi TLA +:ssa - vain niiden välinen vastaavuus on ilmeinen, lisämonimutkaisuutta ei synny. Lopuksi tämä määritys voidaan tarkistaa TLA+ -työkaluilla. Kaiken kaikkiaan PlusCal voi auttaa voittamaan matematiikan pelon, ja se on helppo ymmärtää jopa ohjelmoijille ja tietojenkäsittelytieteilijöille. Aiemmin julkaisin sille algoritmeja jonkin aikaa (noin 10 vuotta).
Ehkä joku vastustaa sitä, että TLA + ja PlusCal ovat matematiikkaa ja matematiikka toimii vain keksityillä esimerkeillä. Käytännössä tarvitset oikean kielen, jossa on tyyppejä, menettelyjä, objekteja ja niin edelleen. Tämä on väärin. Tässä on mitä Amazonilla työskennellyt Chris Newcomb kirjoittaa: "Olemme käyttäneet TLA+:aa kymmenessä suuressa projektissa, ja jokaisessa tapauksessa sen käyttö on vaikuttanut merkittävästi kehitykseen, koska pystyimme havaitsemaan vaarallisia bugeja ennen tuotantoon pääsyä ja koska se antoi meille tarvittavan näkemyksen ja itseluottamuksen. tehdä aggressiivisia suorituskyvyn optimointeja vaikuttamatta ohjelman totuuteen". Usein kuulee, että muodollisia menetelmiä käytettäessä saamme tehotonta koodia - käytännössä kaikki on juuri päinvastoin. Lisäksi ollaan sitä mieltä, että johtajat eivät voi olla vakuuttuneita muodollisten menetelmien tarpeesta, vaikka ohjelmoijat olisivat vakuuttuneita niiden hyödyllisyydestä. Ja Newcomb kirjoittaa: "Esimiehet ponnistelevat nyt kovasti kirjoittaakseen TLA+:n spesifikaatioita ja varatakseen tähän erityisesti aikaa". Joten kun esimiehet näkevät TLA+:n toimivan, he ottavat sen mielellään vastaan. Chris Newcomb kirjoitti tämän noin kuusi kuukautta sitten (lokakuu 2014), mutta nyt tietääkseni TLA+:aa käytetään 14 projektissa, ei 10:ssä. Toinen esimerkki liittyy XBox 360:n suunnitteluun. Harjoittelija tuli Charles Thackerin luo ja kirjoitti muistijärjestelmän tekniset tiedot. Tämän spesifikaation ansiosta löydettiin bugi, joka muuten jäisi huomaamatta ja jonka takia jokainen XBox 360 kaatui neljän tunnin käytön jälkeen. IBM:n insinöörit vahvistivat, että heidän testinsä eivät olisi löytäneet tätä vikaa.
Voit lukea lisää TLA +:sta Internetistä, mutta nyt puhutaan epävirallisista eritelmistä. Harvoin joudumme kirjoittamaan ohjelmia, jotka laskevat vähiten yhteisen jakajan ja vastaavaa. Kirjoitamme paljon useammin ohjelmia, kuten TLA+:lle kirjoittamani kaunis-tulostintyökalu. Yksinkertaisimman käsittelyn jälkeen TLA + -koodi näyttäisi tältä:
Mutta yllä olevassa esimerkissä käyttäjä todennäköisimmin halusi konjunktion ja yhtäläisyysmerkit olevan kohdakkain. Joten oikea muotoilu näyttäisi enemmän tältä:
Mieti toista esimerkkiä:
Päinvastoin, yhtälö-, yhteen- ja kertolaskumerkkien kohdistus lähteessä oli satunnainen, joten yksinkertaisin käsittely riittää. Yleisesti ottaen oikealle muotoilulle ei ole tarkkaa matemaattista määritelmää, koska "oikea" tarkoittaa tässä tapauksessa "mitä käyttäjä haluaa", eikä sitä voida matemaattisesti määrittää.
Vaikuttaa siltä, että jos meillä ei ole totuuden määritelmää, määrittely on hyödytön. Mutta se ei ole. Se, että emme tiedä, mitä ohjelman pitäisi tehdä, ei tarkoita, ettei meidän tarvitse miettiä, miten se toimii – päinvastoin, meidän on panostettava siihen vielä enemmän. Erittely on erityisen tärkeä tässä. On mahdotonta määrittää optimaalista ohjelmaa strukturoidulle tulostamiselle, mutta tämä ei tarkoita, että meidän ei pitäisi ottaa sitä ollenkaan, ja koodin kirjoittaminen tietoisuuden virtana ei ole hyvä asia. Lopuksi kirjoitin kuuden säännön määrittelyn määritelmineen kommenttien muodossa java-tiedostossa. Tässä on esimerkki yhdestä säännöstä: a left-comment token is LeftComment aligned with its covering token. Tämä sääntö on kirjoitettu matemaattisella englanniksi: LeftComment aligned, left-comment и covering token - termit määritelmillä. Näin matemaatikot kuvaavat matematiikkaa: he kirjoittavat termien määritelmiä ja niiden perusteella sääntöjä. Tällaisen määrittelyn etuna on, että kuusi sääntöä on paljon helpompi ymmärtää ja korjata kuin 850 koodiriviä. Minun on sanottava, että näiden sääntöjen kirjoittaminen ei ollut helppoa, niiden virheenkorjaus vei melko paljon aikaa. Erityisesti tätä tarkoitusta varten kirjoitin koodin, joka raportoi mitä sääntöä käytettiin. Koska testasin näitä kuutta sääntöä useissa esimerkeissä, minun ei tarvinnut debugoida 850 koodiriviä, ja vikoja oli melko helppo löytää. Javalla on tähän loistavat työkalut. Jos olisin vain kirjoittanut koodin, se olisi kestänyt paljon kauemmin ja muotoilu olisi ollut huonompaa.
Miksi muodollista määrittelyä ei voitu käyttää? Toisaalta oikea toteutus ei ole tässä liian tärkeä. Rakenteelliset tulosteet eivät välttämättä miellytä ketään, joten minun ei tarvinnut saada niitä toimimaan oikein kaikissa kummallisissa tilanteissa. Vielä tärkeämpää on se, että minulla ei ollut riittäviä työkaluja. TLA+ mallintarkistus on hyödytön tässä, joten minun pitäisi kirjoittaa esimerkit manuaalisesti.
Yllä olevassa spesifikaatiossa on kaikille eritelmille yhteisiä ominaisuuksia. Se on korkeampi taso kuin koodi. Se voidaan toteuttaa millä tahansa kielellä. Kaikki työkalut tai menetelmät ovat hyödyttömiä sen kirjoittamiseen. Mikään ohjelmointikurssi ei auta sinua kirjoittamaan tätä eritelmää. Eikä ole olemassa työkaluja, jotka tekisivät tästä määrityksestä tarpeettoman, ellet tietenkään kirjoita kieltä, joka on tarkoitettu strukturoitujen tulostusohjelmien kirjoittamiseen TLA+:ssa. Lopuksi, tämä määritys ei kerro mitään tarkalleen siitä, kuinka kirjoitamme koodin, se kertoo vain, mitä koodi tekee. Kirjoitamme spesifikaation auttaaksemme meitä miettimään ongelmaa ennen kuin alamme miettiä koodia.
Mutta tällä spesifikaatiolla on myös ominaisuuksia, jotka erottavat sen muista eritelmistä. 95 % muista tiedoista on huomattavasti lyhyempiä ja yksinkertaisempia:
Lisäksi tämä eritelmä on joukko sääntöjä. Yleensä tämä on merkki huonosta spesifikaatiosta. Sääntöjoukon seurausten ymmärtäminen on melko vaikeaa, minkä vuoksi minun piti viettää paljon aikaa niiden virheenkorjaukseen. Tässä tapauksessa en kuitenkaan löytänyt parempaa tapaa.
On syytä sanoa muutama sana ohjelmista, jotka toimivat jatkuvasti. Yleensä ne toimivat rinnakkain esimerkiksi käyttöjärjestelmien tai hajautettujen järjestelmien kanssa. Hyvin harvat ihmiset voivat ymmärtää niitä henkisesti tai paperilla, enkä ole yksi heistä, vaikka joskus pystyin siihen. Siksi tarvitsemme työkaluja, jotka tarkistavat työmme - esimerkiksi TLA + tai PlusCal.
Miksi piti kirjoittaa spesifikaatio, jos tiesin jo, mitä koodin pitäisi tarkalleen tehdä? Itse asiassa luulin vain tietäväni sen. Lisäksi erittelyn myötä ulkopuolisen ei enää tarvitse päästä koodiin ymmärtääkseen, mitä hän tarkalleen tekee. Minulla on sääntö: yleisiä sääntöjä ei pitäisi olla. Tähän sääntöön on tietysti poikkeus, se on ainoa yleinen sääntö, jota noudatan: koodin toiminnan määrittelyn pitäisi kertoa ihmisille kaikki, mitä he tarvitsevat koodia käyttäessään.
Mitä ohjelmoijien tarkalleen ottaen pitää tietää ajattelusta? Ensinnäkin sama kuin kaikki muutkin: jos et kirjoita, sinusta vain näyttää siltä, että ajattelet. Sinun on myös mietittävä ennen koodaamista, mikä tarkoittaa, että sinun on kirjoitettava ennen koodaamista. Määrittely on se, mitä kirjoitamme ennen koodauksen aloittamista. Jokaiselle koodille, jota kuka tahansa voi käyttää tai muokata, tarvitaan erittely. Ja tämä "joku" voi olla itse koodin kirjoittaja kuukausi sen kirjoittamisen jälkeen. Erittely tarvitaan suurille ohjelmille ja järjestelmille, luokille, menetelmille ja joskus jopa yhden menetelmän monimutkaisille osille. Mitä koodista oikein pitäisi kirjoittaa? Sinun on kuvattava, mitä se tekee, eli mikä voi olla hyödyllistä kenelle tahansa tätä koodia käyttävälle henkilölle. Joskus voi myös olla tarpeen määrittää, kuinka koodi saavuttaa tarkoituksensa. Jos kävimme läpi tämän menetelmän algoritmien aikana, kutsumme sitä algoritmiksi. Jos se on jotain erikoisempaa ja uutta, niin kutsumme sitä korkean tason suunnitteluksi. Tässä ei ole muodollista eroa: molemmat ovat ohjelman abstrakteja malleja.
Kuinka tarkalleen pitäisi kirjoittaa koodimääritys? Tärkeintä: sen tulisi olla yksi taso korkeampi kuin itse koodi. Sen pitäisi kuvata tiloja ja käyttäytymistä. Sen tulee olla niin tiukka kuin tehtävä vaatii. Jos kirjoitat määritystä siitä, miten tehtävä tulee toteuttaa, voit kirjoittaa sen pseudokoodilla tai PlusCalilla. Sinun on opittava kirjoittamaan eritelmiä muodollisiin eritelmiin. Tämä antaa sinulle tarvittavat taidot, jotka auttavat sinua myös epävirallisissa taidoissa. Kuinka opit kirjoittamaan muodollisia määritelmiä? Kun opimme ohjelmoimaan, kirjoitimme ohjelmia ja sitten debuggimme niitä. Se on sama täällä: kirjoita tekniset tiedot, tarkista se mallintarkistuksella ja korjaa virheet. TLA+ ei ehkä ole paras kieli muodollisille määrityksille, ja toinen kieli on todennäköisesti parempi erityistarpeisiisi. TLA+:n etuna on, että se opettaa erittäin hyvin matemaattista ajattelua.
Kuinka linkitän tiedot ja koodi? Matemaattisia käsitteitä ja niiden toteutusta yhdistävien kommenttien avulla. Jos työskentelet kaavioiden kanssa, sinulla on ohjelmatasolla solmu- ja linkkijoukkoja. Siksi sinun on kirjoitettava tarkasti, kuinka nämä ohjelmointirakenteet toteuttavat kaavion.
On huomattava, että mikään yllä olevista ei koske varsinaista koodin kirjoitusprosessia. Kun kirjoitat koodia, eli suoritat kolmannen vaiheen, sinun on myös mietittävä ja mietittävä ohjelma. Jos osatehtävä osoittautuu monimutkaiseksi tai epäselväksi, sinun on kirjoitettava sille spesifikaatio. Mutta en puhu itse koodista tässä. Voit käyttää mitä tahansa ohjelmointikieltä, mitä tahansa menetelmää, kyse ei ole niistä. Mikään yllä olevista ei myöskään poista tarvetta testata ja korjata koodia. Vaikka abstrakti malli on kirjoitettu oikein, sen toteutuksessa voi olla virheitä.
Teknisten tietojen kirjoittaminen on lisävaihe koodausprosessissa. Sen ansiosta monet virheet voidaan havaita pienemmällä vaivalla - tiedämme tämän Amazonin ohjelmoijien kokemuksesta. Eritelmien myötä ohjelmien laatu paranee. Miksi sitten niin usein pärjätään ilman niitä? Koska kirjoittaminen on vaikeaa. Ja kirjoittaminen on vaikeaa, koska tätä varten sinun on ajateltava, ja ajatteleminen on myös vaikeaa. On aina helpompi teeskennellä mitä ajattelee. Tässä voit vetää analogian juoksun kanssa - mitä vähemmän juokset, sitä hitaammin juokset. Sinun täytyy harjoitella lihaksiasi ja harjoitella kirjoittamista. Vaatii harjoittelua.
Erittely voi olla virheellinen. Olet saattanut tehdä virheen jossain, vaatimukset ovat saattaneet muuttua tai parannuksia on ehkä tehtävä. Kaikki kenen tahansa käyttämät koodit on vaihdettava, joten ennemmin tai myöhemmin määritykset eivät enää vastaa ohjelmaa. Ihannetapauksessa tässä tapauksessa sinun on kirjoitettava uusi spesifikaatio ja kirjoitettava koodi kokonaan uudelleen. Tiedämme hyvin, ettei kukaan tee niin. Käytännössä korjaamme koodin ja mahdollisesti päivitämme spesifikaatiota. Jos tämä tapahtuu ennemmin tai myöhemmin, miksi sitten ylipäätään kirjoittaa teknisiä tietoja? Ensinnäkin henkilölle, joka muokkaa koodiasi, jokainen ylimääräinen sana määrittelyssä on kullan arvoinen, ja tämä henkilö voi hyvinkin olla sinä itse. Sanon usein itseäni siitä, etten saa tarpeeksi tarkkoja tietoja muokatessani koodiani. Ja kirjoitan enemmän teknisiä tietoja kuin koodia. Siksi koodia muokatessa määrittely on aina päivitettävä. Toiseksi koodi huononee jokaisen version myötä, sen lukeminen ja ylläpito on yhä vaikeampaa. Tämä on entropian kasvua. Mutta jos et aloita tiedolla, jokainen kirjoittamasi rivi on muokkaus, ja koodi on raskas ja vaikea lukea alusta alkaen.
Kuten sanottu , mitään taistelua ei voitettu suunnitelmalla, eikä taistelua voitettu ilman suunnitelmaa. Ja hän tiesi yhden tai kaksi taisteluista. On olemassa mielipide, että eritelmien kirjoittaminen on ajanhukkaa. Joskus tämä on totta, ja tehtävä on niin yksinkertainen, ettei sitä tarvitse miettiä. Mutta sinun tulee aina muistaa, että kun sinua kehotetaan olemaan kirjoittamatta eritelmiä, sinua kehotetaan olemaan ajattelematta. Ja sitä kannattaa miettiä joka kerta. Tehtävän harkitseminen ei takaa, että et tee virheitä. Kuten tiedämme, kukaan ei keksinyt taikasauvaa, ja ohjelmointi on vaikea tehtävä. Mutta jos et ajattele ongelmaa läpi, teet varmasti virheitä.
Voit lukea lisää TLA +:sta ja PlusCalista erityiseltä verkkosivustolta, voit mennä sinne kotisivultani . Siinä kaikki minulle, kiitos huomiosta.
Huomaa, että tämä on käännös. Kun kirjoitat kommentteja, muista, että kirjoittaja ei lue niitä. Jos todella haluat jutella kirjoittajan kanssa, niin hän on Hydra 2019 -konferenssissa, joka pidetään 11.-12 Pietarissa. Lippuja voi ostaa .
Lähde: will.com