Ez a cikk fordítás . De előtte egy kis bemutatkozás. Hogyan keletkeznek a zombik? Mindenki került olyan helyzetbe, hogy fel akarja húzni egy barátját vagy kollégáját a saját szintjére, de ez nem megy. És nem is annyira veled, mint inkább vele, hogy „nem megy”: a skála egyik oldalán a normális fizetés, a feladatok és így tovább, a másikon pedig a gondolkodás szükségessége. A gondolkodás kellemetlen és fájdalmas. Gyorsan feladja, és anélkül folytatja a kódírást, hogy egyáltalán nem kapcsolja be az agyát. Elképzeled, mennyi erőfeszítést igényel a tanult tehetetlenség gátjának leküzdése, és egyszerűen nem teszed meg. Így keletkeznek a zombik, amiket, úgy tűnik, meg lehet gyógyítani, de úgy tűnik, senki sem fogja megtenni.
Amikor azt láttam (igen, ugyanaz az elvtárs a tankönyvekből) és nem riportot készít, hanem kérdezz-feleletet, kicsit óvatos voltam. Minden esetre Leslie világhírű tudós, az elosztott számítástechnika alapvető alkotásainak szerzője, akit a LaTeX - „Lamport TeX” szó La betűiről is ismerhetünk. A második riasztó tényező az ő követelménye: mindenkinek, aki jön, (teljesen ingyenesen) előre meg kell hallgatnia pár beszámolóját, legalább egy kérdést feltenni azokra, és csak azután jöjjön. Úgy döntöttem, megnézem, mit sugároz ott Lamport – és ez nagyszerű! Pontosan ez a varázslatos link-pirula a zombik gyógyítására. Figyelmeztetlek: a szövegből kifejezetten kiéghetnek a szuperrugalmas módszertanok kedvelői és azok, akik nem szeretik tesztelni a leírtakat.
A habrokat után tulajdonképpen kezdődik a szeminárium fordítása. Élvezd az olvasást!
Bármilyen feladatot is vállal, mindig három lépésen kell keresztülmennie:
- döntse el, milyen célt szeretne elérni;
- döntse el, hogyan éri el célját;
- érj el a célodhoz.
Ez vonatkozik a programozásra is. Amikor kódot írunk, a következőkre van szükségünk:
- döntse el, mit tegyen a program;
- meghatározza, hogyan kell ellátnia feladatát;
- írja be a megfelelő kódot.
Az utolsó lépés természetesen nagyon fontos, de ma nem erről beszélek. Ehelyett az első kettőt fogjuk megvitatni. Minden programozó elvégzi ezeket a munka megkezdése előtt. Csak akkor ül le írni, ha eldöntötte, hogy böngészőt vagy adatbázist ír. Egy bizonyos elképzelésnek jelen kell lennie a célról. És feltétlenül gondolja át, hogy pontosan mit fog csinálni a program, és ne írjon valahogy abban a reményben, hogy a kód valahogy böngészővé válik.
Pontosan hogyan történik ez a kód-előregondolás? Mennyi erőfeszítést kell tennünk ebbe? Minden attól függ, mennyire összetett a megoldandó probléma. Tegyük fel, hogy egy hibatűrő elosztott rendszert akarunk írni. Ebben az esetben alaposan át kell gondolnunk a dolgokat, mielőtt leülnénk kódolni. Mi van, ha egy egész változót csak 1-gyel kell növelnünk? Első pillantásra itt minden triviális, és nem kell gondolkodni, de aztán eszünkbe jut, hogy túlcsordulhat. Ezért még annak megértéséhez is, hogy egy probléma egyszerű vagy összetett, először gondolkodnia kell.
Ha előre átgondolja a probléma lehetséges megoldásait, elkerülheti a hibákat. De ehhez világosnak kell lennie a gondolkodásodnak. Ennek eléréséhez le kell írnia gondolatait. Nagyon szeretem Dick Guindon idézetét: „Amikor írsz, a természet megmutatja, milyen hanyag a gondolkodásod.” Ha nem írsz, akkor csak azt hiszed, hogy gondolkodsz. És le kell írnia gondolatait specifikációk formájában.
A specifikációk számos funkciót látnak el, különösen nagy projekteknél. De ezek közül csak az egyikről beszélek: segítenek tisztán gondolkodni. A világos gondolkodás nagyon fontos és meglehetősen nehéz, ezért itt minden segítségre van szükségünk. Milyen nyelven írjuk a specifikációkat? Általában mindig ez az első kérdés a programozóknak: milyen nyelven fogunk írni. Nincs rá egyetlen helyes válasz: a megoldandó problémák túl sokfélék. Egyesek számára a TLA+ egy általam fejlesztett specifikációs nyelv. Mások számára kényelmesebb a kínai használata. Minden a helyzettől függ.
Még fontosabb egy másik kérdés: hogyan lehet tisztább gondolkodást elérni? Válasz: Tudósként kell gondolkodnunk. Ez egy olyan gondolkodásmód, amely az elmúlt 500 évben bevált. A tudományban a valóság matematikai modelljeit építjük fel. A csillagászat volt talán az első tudomány a szó szoros értelmében. A csillagászatban használt matematikai modellben az égitestek tömeggel, helyzettel és lendülettel rendelkező pontokként jelennek meg, bár a valóságban rendkívül összetett objektumok hegyekkel és óceánokkal, árapályokkal és árapályokkal. Ezt a modellt, mint bármely mást, bizonyos problémák megoldására hozták létre. Kiválóan alkalmas annak meghatározására, hogy hová irányítsa a távcsövet, ha bolygót kell találnia. De ha meg akarja jósolni az időjárást ezen a bolygón, ez a modell nem fog működni.
A matematika lehetővé teszi a modell tulajdonságainak meghatározását. A tudomány pedig megmutatja, hogyan viszonyulnak ezek a tulajdonságok a valósághoz. Beszéljünk a tudományunkról, az informatikáról. A valóság, amellyel dolgozunk, a különféle számítástechnikai rendszerek: processzorok, játékkonzolok, számítógépek, programok végrehajtása stb. Egy program számítógépen való futtatásáról fogok beszélni, de nagyjából ezek a következtetések minden számítástechnikai rendszerre vonatkoznak. Tudományunkban sok különböző modellt használunk: a Turing-gépet, részben rendezett eseményhalmazokat és még sok mást.
Mi az a program? Ez bármilyen kód, amely önállóan tekinthető. Tegyük fel, hogy írnunk kell egy böngészőt. Három feladatot végzünk el: megtervezzük a program felhasználói nézetét, majd megírjuk a program magas szintű diagramját, végül megírjuk a kódot. Ahogy írjuk a kódot, rájövünk, hogy szövegformázót kell írnunk. Itt ismét három problémát kell megoldanunk: határozzuk meg, hogy ez az eszköz milyen szöveget ad vissza; válasszon egy algoritmust a formázáshoz; kódot írni. Ennek a feladatnak megvan a maga részfeladata: helyesen illesszen be egy kötőjelet a szavakba. Ezt a részfeladatot is három lépésben oldjuk meg - mint látható, ezek sok szinten ismétlődnek.
Nézzük részletesebben az első lépést: milyen problémát old meg a program. Itt a programot leggyakrabban függvényként modellezzük, amely némi bemenetet vesz fel, és valamilyen kimenetet termel. A matematikában egy függvényt általában párok rendezett halmazaként írnak le. Például a természetes számok négyzetesítési függvénye a következő halmazként van leírva: {<0,0>, <1,1>, <2,4>, <3,9>, …}. Egy ilyen függvény tartománya az egyes párok első elemeinek halmaza, vagyis a természetes számok. Egy függvény meghatározásához meg kell adnunk a hatókörét és a képletet.
De a függvények a matematikában nem ugyanazok, mint a programozási nyelvek függvényei. A matek sokkal könnyebb. Mivel nincs időm bonyolult példákra, tekintsünk egy egyszerűt: egy függvényt C-ben vagy egy statikus metódust Java-ban, amely két egész szám legnagyobb közös osztóját adja vissza. Ennek a módszernek a specifikációjában ezt írjuk: kiszámítja GCD(M,N) érvekre M и NAhol GCD(M,N) - egy függvény, amelynek tartománya egész számpárok halmaza, és a visszatérési értéke a legnagyobb egész szám, amely osztható M и N. Hogyan viszonyul ez a modell a valósághoz? A modell egész számokkal működik, míg C-ben vagy Java-ban van egy 32 bites int. Ez a modell lehetővé teszi számunkra annak eldöntését, hogy az algoritmus helyes-e GCD, de nem akadályozza meg a túlcsordulási hibákat. Ehhez bonyolultabb modellre lenne szükség, amire nincs idő.
Beszéljünk a függvény mint modell korlátairól. Egyes programok (például operációs rendszerek) nem csak egy bizonyos értéket adnak vissza bizonyos argumentumokhoz, hanem folyamatosan futhatnak. Ráadásul a modell mint funkció nem alkalmas a második lépésre: a probléma megoldásának megtervezésére. A gyors rendezés és a buborékos rendezés ugyanazt a függvényt számítja ki, de ezek teljesen különböző algoritmusok. Ezért a program céljának elérésének leírására egy másik modellt használok, nevezzük standard viselkedési modellnek. A benne lévő program az összes megengedett viselkedés halmazaként van ábrázolva, amelyek mindegyike állapotok sorozata, az állapot pedig értékek hozzárendelése a változókhoz.
Nézzük meg, hogyan néz ki az Euklidész algoritmus második lépése. Számolnunk kell GCD(M, N). Inicializáljuk M mint xÉs N mint y, majd ismételten vonja ki e változók közül a kisebbet a nagyobbból, amíg egyenlőek nem lesznek. Például ha M = 12És N = 18, a következő viselkedést írhatjuk le:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
A hacsak M = 0 и N = 0? A nulla minden számmal osztható, így ebben az esetben nincs legnagyobb osztó. Ebben a helyzetben vissza kell térnünk az első lépéshez, és meg kell kérdeznünk: valóban ki kell számítanunk a GCD-t nem pozitív számokra? Ha ez nem szükséges, akkor csak módosítani kell a specifikációt.
Itt egy kis kitérőt kell tennünk a termelékenységet illetően. Ezt gyakran a naponta írt kódsorok számában mérik. De a munkád sokkal hasznosabb, ha bizonyos számú sortól megszabadulsz, mert kevesebb helyed van a hibáknak. És a legegyszerűbb módja annak, hogy az első lépésben megszabaduljon a kódtól. Teljesen lehetséges, hogy nincs szüksége az összes csengőre és sípra, amelyet megvalósítani próbál. A program egyszerűsítésének és időmegtakarításának leggyorsabb módja az, ha nem teszünk olyan dolgokat, amelyeket nem kellene megtenni. A második lépés a második legnagyobb időmegtakarítási lehetőség. Ha a termelékenységet a megírt sorokban méri, akkor a feladat elvégzésének átgondolása készteti kevésbé produktív, mert ugyanazt a problémát kevesebb kóddal is meg tudod oldani. Pontos statisztikát itt nem tudok közölni, mert nem tudom megszámolni, hogy hány sort nem írtam le, mert időt fordítottam a specifikációra, vagyis az első és a második lépésre. A kísérletet pedig itt sem lehet beállítani, mert a kísérletben nincs jogunk az első lépés elvégzésére, a feladat előre meghatározott.
Könnyű figyelmen kívül hagyni az informális specifikációk sok nehézségét. Nincs semmi nehéz a függvények szigorú specifikációinak megírásában, ezt nem tárgyalom. Ehelyett arról fogunk beszélni, hogy szigorú előírásokat írjunk a szabványos viselkedésekre. Van egy tétel, amely azt mondja, hogy a viselkedés bármely halmaza leírható a biztonsági tulajdonság segítségével (biztonság) és a túlélési tulajdonságok (élénkség). A biztonság azt jelenti, hogy semmi rossz nem fog történni, a program nem ad helytelen választ. A túlélés azt jelenti, hogy előbb-utóbb valami jó történik, vagyis a program előbb-utóbb megadja a helyes választ. Általában a biztonság fontosabb mutató, a hibák leggyakrabban itt fordulnak elő. Ezért az időmegtakarítás érdekében nem beszélek a túlélésről, bár ez is fontos.
A biztonságot úgy érjük el, hogy először felírjuk a lehetséges kezdeti állapotok halmazát. Másodszor pedig kapcsolatok az egyes állapotok összes lehetséges következő állapotával. Tegyünk úgy, mint a tudósok, és határozzuk meg az állapotokat matematikailag. A kezdeti állapotok halmazát egy képlet írja le, például az Euklidész algoritmus esetében: (x = M) ∧ (y = N). Bizonyos értékekre M и N csak egy kezdeti állapot van. A következő állapothoz való viszonyt egy képlet írja le, amelyben a következő állapot változóit prímszámmal, az aktuális állapot változóit prímszám nélkül írjuk. Az eukleidészi algoritmus esetében két képlet diszjunkciójával fogunk foglalkozni, amelyek közül az egyikben x a legnagyobb érték, a másodikban pedig - y:
Az első esetben y új értéke megegyezik y korábbi értékével, és az x új értékét úgy kapjuk meg, hogy a kisebb változót kivonjuk a nagyobbból. A második esetben az ellenkezőjét csináljuk.
Térjünk vissza Eukleidész algoritmusához. Tételezzük fel még egyszer M = 12, N = 18. Ez egyetlen kezdeti állapotot határoz meg, (x = 12) ∧ (y = 18). Ezután beillesztjük ezeket az értékeket a fenti képletbe, és megkapjuk:
Íme az egyetlen lehetséges megoldás: x' = 18 - 12 ∧ y' = 12és megkapjuk a viselkedést: [x = 12, y = 18]. Hasonlóképpen leírhatjuk viselkedésünk összes állapotát: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
Utolsó állapotban [x = 6, y = 6] a kifejezés mindkét része hamis lesz, így nincs következő állapota. Tehát van egy teljes specifikációnk a második lépésről - amint látja, ez teljesen hétköznapi matematika, mint a mérnököknél és a tudósoknál, és nem furcsa, mint a számítástechnikában.
Ez a két képlet kombinálható az időbeli logika egyetlen képletévé. Elegáns és könnyen elmagyarázható, de most nincs rá idő. Időbeli logikára csak az elevenség miatt lehet szükségünk, a biztonság miatt nem. Nem szeretem az időbeli logikát, mint olyat, nem egészen hétköznapi matematika, de az elevenségnél szükségszerű rossz.
Euklidész algoritmusában minden értékre x и y egyedi értékekkel bírnak x' и y', amelyek igazzá teszik a kapcsolatot a következő állapottal. Más szóval, Eukleidész algoritmusa determinisztikus. Egy nem-determinisztikus algoritmus modellezéséhez az aktuális állapotnak több lehetséges jövőbeli állapottal kell rendelkeznie, és minden előíratlan változó értéknek több primer változóértéke kell, hogy a következő állapothoz való viszony igaz legyen. Ezt könnyű megtenni, de most nem mondok példákat.
Egy munkaeszköz elkészítéséhez formális matematikára van szükség. Hogyan lehet formálissá tenni a specifikációt? Ehhez szükségünk van egy formális nyelvre, pl. . Az Euklidész algoritmus specifikációja a következőképpen nézne ki ezen a nyelven:
A háromszöggel ellátott egyenlőségjel szimbólum azt jelenti, hogy a jeltől balra lévő érték egyenlő a jeltől jobbra lévő értékkel. A specifikáció lényegében definíció, esetünkben két definíció. A TLA+ specifikációjához hozzá kell adnia deklarációkat és némi szintaxist, ahogy a fenti dián is látható. ASCII-ben így nézne ki:
Mint látható, semmi bonyolult. A TLA+ specifikációja tesztelhető, azaz egy kis modellben minden lehetséges viselkedés megkerülhető. A mi esetünkben ez a modell bizonyos értékeket jelent M и N. Ez egy nagyon hatékony és egyszerű ellenőrzési módszer, amely teljesen automatikus. Formális igazságbizonyítást is lehet írni és mechanikusan ellenőrizni, de ez sok időt vesz igénybe, így ezt szinte senki sem csinálja.
A TLA+ fő hátránya, hogy matematikai, a programozók és informatikusok pedig félnek a matematikától. Első pillantásra ez viccnek tűnik, de sajnos komolyan mondom. A kollégám éppen azt mesélte, hogyan próbálta több fejlesztőnek elmagyarázni a TLA+-t. Amint a képletek megjelentek a képernyőn, azonnal üveges szemek lettek. Tehát ha a TLA+ megijeszt, használhatja , ez egyfajta játékprogramozási nyelv. Egy kifejezés a PlusCalben bármilyen TLA+ kifejezés lehet, vagyis nagyjából bármilyen matematikai kifejezés. Ezenkívül a PlusCal rendelkezik egy szintaxissal a nem determinisztikus algoritmusokhoz. Mivel a PlusCal bármilyen TLA+ kifejezést írhat, a PlusCal sokkal kifejezőbb, mint bármely valódi programozási nyelv. Ezután a PlusCal egy könnyen olvasható TLA+ specifikációba kerül. Ez természetesen nem jelenti azt, hogy a komplex PlusCal specifikáció egyszerűvé válik a TLA +-on - csak a köztük lévő megfelelés nyilvánvaló, nem lesz további bonyolultság. Végül ez a specifikáció ellenőrizhető a TLA+ eszközökkel. Összességében a PlusCal segíthet leküzdeni a matematikai fóbiát, és még a programozók és informatikusok számára is könnyen érthető. Régebben egy ideig (kb. 10 évig) publikáltam rajta algoritmusokat.
Talán valaki kifogásolja, hogy a TLA + és a PlusCal matematika, és a matematika csak kitalált példákon működik. A gyakorlatban szükség van egy valódi nyelvre típusokkal, eljárásokkal, objektumokkal stb. Ez rossz. Chris Newcomb, aki az Amazonnál dolgozott, ezt írja: „Tíz nagy projektben használtuk a TLA+-t, és minden esetben jelentős változást hozott a fejlesztésben, mivel veszélyes hibákat tudtunk elkapni, mielőtt elkezdtük volna a gyártást, és mert ez megadta nekünk a szükséges betekintést és önbizalmat. agresszív teljesítményoptimalizálást hajt végre anélkül, hogy befolyásolná a program valódiságát". Gyakran hallani, hogy formális módszerek használatakor nem hatékony kódot kapunk - a gyakorlatban minden pont fordítva van. Emellett van olyan vélemény, hogy a menedzsereket nem lehet meggyőzni a formális módszerek szükségességéről, még akkor sem, ha a programozók meg vannak győződve azok hasznosságáról. És Newcomb ezt írja: „A menedzserek most keményen igyekeznek megírni a TLA+ specifikációit, és kifejezetten erre fordítanak időt.”. Így amikor a vezetők látják, hogy a TLA+ működik, örömmel fogadják. Chris Newcomb ezt körülbelül hat hónapja írta (2014 októberében), de most, amennyire én tudom, a TLA+-t 14 projektben használják, nem 10-ben. Egy másik példa az XBox 360 tervezése. Egy gyakornok Charles Thackerhez jött, és specifikációt írt a memóriarendszerhez. Ennek a specifikációnak köszönhetően egy olyan hibát találtak, amely egyébként észrevétlen maradna, és ami miatt négy óra használat után minden XBox 360 összeomlik. Az IBM mérnökei megerősítették, hogy tesztjeik nem találták volna ezt a hibát.
A TLA +-ról többet olvashat az interneten, de most beszéljünk az informális specifikációkról. Ritkán kell olyan programokat írnunk, amelyek kiszámítják a legkisebb közös osztót és hasonlókat. Sokkal gyakrabban írunk olyan programokat, mint a szép nyomtató eszköz, amit a TLA+-hoz írtam. A legegyszerűbb feldolgozás után a TLA + kód így néz ki:
De a fenti példában a felhasználó nagy valószínűséggel azt akarta, hogy a kötőszó és az egyenlőségjelek igazodjanak. Tehát a helyes formázás inkább így nézne ki:
Vegyünk egy másik példát:
Itt éppen ellenkezőleg, az egyenlőségi, összeadási és szorzási jelek igazítása a forrásban véletlenszerű volt, így a legegyszerűbb feldolgozás is elég. Általánosságban elmondható, hogy a helyes formázásnak nincs pontos matematikai meghatározása, mert a "helyes" ebben az esetben azt jelenti, hogy "amit a felhasználó akar", és ez matematikailag nem határozható meg.
Úgy tűnik, hogy ha nincs definíciónk az igazságra, akkor a specifikáció haszontalan. De nem az. Csak azért, mert nem tudjuk, mit kell tennie egy programnak, nem jelenti azt, hogy nem kell gondolkodnunk a működésén – éppen ellenkezőleg, még több erőfeszítést kell tennünk rá. A specifikáció itt különösen fontos. Lehetetlen meghatározni az optimális programot a strukturált nyomtatáshoz, de ez nem jelenti azt, hogy egyáltalán ne vegyük, és a kód írása, mint tudatfolyam nem jó dolog. Végül hat szabály specifikációját írtam definíciókkal megjegyzések formájában egy java fájlban. Íme egy példa az egyik szabályra: a left-comment token is LeftComment aligned with its covering token. Ez a szabály, mondjuk úgy, matematikai angolul van írva: LeftComment aligned, left-comment и covering token - kifejezések definíciókkal. A matematikusok így írják le a matematikát: terminus-definíciókat és ezek alapján szabályokat írnak. Egy ilyen specifikáció előnye, hogy hat szabályt sokkal könnyebb megérteni és hibakeresni, mint 850 kódsort. Azt kell mondanom, hogy ezeket a szabályokat nem volt könnyű megírni, elég sok időbe telt a hibakeresésük. Különösen erre a célra írtam egy kódot, amely közölte, hogy melyik szabályt használtam. Köszönhetően annak, hogy ezt a hat szabályt több példán is teszteltem, nem kellett 850 sornyi kódot hibakeresnem, és a hibákat meglehetősen könnyű megtalálni. A Java remek eszközökkel rendelkezik ehhez. Ha csak a kódot írtam volna, sokkal tovább tartott volna, és a formázás is gyengébb minőségű lett volna.
Miért nem lehetett formális specifikációt használni? Egyrészt itt nem túl fontos a helyes végrehajtás. A szerkezeti nyomatok senkinek nem fognak tetszeni, így nem kellett minden furcsa helyzetben megfelelően működni. Még ennél is fontosabb, hogy nem voltak megfelelő eszközök. A TLA+ modellellenőrző itt használhatatlan, ezért kézzel kellene megírnom a példákat.
A fenti specifikáció minden specifikációra közös jellemzőkkel rendelkezik. Ez magasabb szintű, mint a kód. Bármilyen nyelven megvalósítható. Minden eszköz vagy módszer használhatatlan az íráshoz. Egyetlen programozási tanfolyam sem segít megírni ezt a specifikációt. És nincsenek olyan eszközök, amelyek szükségtelenné tennék ezt a specifikációt, hacsak természetesen nem írunk egy nyelvet kifejezetten strukturált nyomtatási programok írásához TLA+-ban. Végül ez a specifikáció nem mond semmit arról, hogy pontosan hogyan fogjuk megírni a kódot, csak azt, hogy ez a kód mit csinál. A specifikációt azért írjuk meg, hogy segítsen átgondolni a problémát, mielőtt elkezdenénk gondolkodni a kódon.
De ennek a specifikációnak vannak olyan jellemzői is, amelyek megkülönböztetik a többi specifikációtól. A többi specifikáció 95%-a lényegesen rövidebb és egyszerűbb:
Ezenkívül ez a specifikáció egy szabályrendszer. Általában ez a rossz specifikáció jele. Egy szabályrendszer következményeit meglehetősen nehéz megérteni, ezért is kellett sok időt töltenem a hibakereséssel. Ebben az esetben azonban nem találtam jobb megoldást.
A folyamatosan futó programokról érdemes néhány szót ejteni. Általában párhuzamosan működnek, például operációs rendszerekkel vagy elosztott rendszerekkel. Nagyon kevesen értik meg őket gondolatban vagy papíron, és én nem tartozom közéjük, bár egyszer képes voltam rá. Ezért szükségünk van olyan eszközökre, amelyek ellenőrizni fogják a munkánkat - például TLA + vagy PlusCal.
Miért kellett specifikációt írni, ha már tudtam, hogy pontosan mit kell csinálnia a kódnak? Valójában csak azt hittem, ismerem. Ráadásul egy specifikációval a kívülállónak már nem kell belemennie a kódba, hogy megértse, mit is csinál pontosan. Van egy szabályom: ne legyenek általános szabályok. Ez alól természetesen van egy kivétel, ez az egyetlen általános szabály, amit követek: a kód működésének specifikációja mindent elmond az embereknek, amit a kód használatakor tudniuk kell.
Tehát mit kell pontosan tudniuk a programozóknak a gondolkodásról? Kezdetnek ugyanaz, mint mindenki más: ha nem írsz, akkor csak úgy tűnik neked, hogy gondolkodsz. Ezenkívül gondolkodnia kell, mielőtt kódol, ami azt jelenti, hogy írnia kell, mielőtt kódol. A specifikáció az, amit a kódolás megkezdése előtt írunk. Minden, bárki által használható vagy módosítható kódhoz specifikáció szükséges. És ez a "valaki" egy hónappal a megírása után maga lehet a kód szerzője. Specifikációra van szükség nagy programokhoz és rendszerekhez, osztályokhoz, metódusokhoz, sőt néha egyetlen metódus összetett szakaszaihoz is. Mit kell pontosan írni a kódra? Le kell írnia, hogy mit csinál, vagyis mi lehet hasznos bármely személy számára, aki ezt a kódot használja. Néha azt is meg kell adni, hogy a kód hogyan éri el a célját. Ha ezt a módszert algoritmusok során végigvittük, akkor algoritmusnak nevezzük. Ha valami különlegesebb és újszerű, akkor azt magas szintű dizájnnak nevezzük. Itt nincs formai különbség: mindkettő egy program absztrakt modellje.
Pontosan hogyan kell kódspecifikációt írni? A legfontosabb dolog: egy szinttel magasabbnak kell lennie, mint maga a kód. Le kell írnia az állapotokat és a viselkedéseket. Olyan szigorúnak kell lennie, amennyire a feladat megköveteli. Ha specifikációt ír egy feladat megvalósításához, akkor azt pszeudokóddal vagy PlusCal-al is megírhatja. Meg kell tanulnod, hogyan írj specifikációkat a formális specifikációkra. Ez megadja azokat a szükséges készségeket, amelyek az informálisaknál is segítséget nyújtanak. Hogyan lehet megtanulni formális előírásokat írni? Amikor megtanultunk programozni, programokat írtunk, majd hibakeresést végeztünk. Itt is ugyanaz: írd meg a specifikációt, ellenőrizd a modellellenőrzővel, és javítsd ki a hibákat. Előfordulhat, hogy a TLA+ nem a legjobb nyelv egy formális specifikációhoz, és egy másik nyelv valószínűleg jobban megfelel az Ön speciális igényeinek. A TLA+ előnye, hogy nagyon jól tanítja a matematikai gondolkodást.
Hogyan lehet összekapcsolni a specifikációt és a kódot? A matematikai fogalmakat és azok megvalósítását összekapcsoló megjegyzések segítségével. Ha grafikonokkal dolgozik, akkor programszinten csomópontok és hivatkozások tömbjei lesznek. Ezért pontosan meg kell írni, hogyan valósítják meg a gráfot ezek a programozási struktúrák.
Meg kell jegyezni, hogy a fentiek egyike sem vonatkozik a kódírás tényleges folyamatára. Amikor megírod a kódot, vagyis végrehajtod a harmadik lépést, akkor is át kell gondolnod és végig kell gondolnod a programot. Ha egy részfeladat összetettnek vagy nem nyilvánvalónak bizonyul, akkor specifikációt kell írnia hozzá. De itt nem magáról a kódról beszélek. Bármilyen programozási nyelvet, módszertant használhatsz, nem róluk van szó. Ezenkívül a fentiek egyike sem szünteti meg a kód tesztelésének és hibakeresésének szükségességét. Még akkor is, ha az absztrakt modell helyesen van megírva, előfordulhatnak hibák a megvalósításában.
A specifikációk írása egy további lépés a kódolási folyamatban. Ennek köszönhetően sok hibát kevesebb erőfeszítéssel el lehet fogni – tudjuk ezt az Amazon programozóinak tapasztalataiból. A specifikációkkal a programok minősége magasabb lesz. Akkor miért megyünk olyan gyakran nélkülük? Mert írni nehéz. Írni pedig nehéz, mert ehhez gondolkodni kell, és a gondolkodás is nehéz. Mindig könnyebb úgy tenni, mintha azt gondolnád. Itt egy hasonlatot vonhatunk le a futással - minél kevesebbet futsz, annál lassabban futsz. Edzened kell az izmaidat és gyakorolnod kell az írást. Gyakorlat kell.
A specifikáció hibás lehet. Lehet, hogy valahol hibát követett el, vagy megváltoztak a követelmények, esetleg fejlesztésre van szükség. Bármilyen kódot, amit bárki használ, meg kell változtatni, így előbb-utóbb a specifikáció már nem fog megegyezni a programmal. Ideális esetben ebben az esetben új specifikációt kell írnia, és teljesen át kell írnia a kódot. Nagyon jól tudjuk, hogy ezt senki sem csinálja. A gyakorlatban javítjuk a kódot, és esetleg frissítjük a specifikációt. Ha ez előbb-utóbb megtörténik, akkor miért kell egyáltalán specifikációkat írni? Először is, annak a személynek, aki szerkeszti a kódját, a specifikációban szereplő minden extra szó aranyat ér, és ez a személy lehet, hogy te magad vagy. Gyakran szidalmazom magam, amiért nem kapok elég specifikációt a kód szerkesztésekor. És több specifikációt írok, mint kódot. Ezért a kód szerkesztésekor a specifikációt mindig frissíteni kell. Másodszor, minden átdolgozással a kód rosszabbodik, egyre nehezebb lesz elolvasni és karbantartani. Ez az entrópia növekedése. De ha nem specifikációval kezded, akkor minden beírt sor szerkesztés lesz, a kód pedig nehézkes és nehezen olvasható lesz az elejétől fogva.
Ahogy mondták , egyetlen csatát sem nyert meg terv, és egyetlen csatát sem nyertek meg terv nélkül. És tudott egy-két dolgot a csatákról. Van egy vélemény, hogy a specifikációk írása időpocsékolás. Néha ez igaz, és a feladat olyan egyszerű, hogy nincs mit végiggondolni. De mindig emlékezned kell arra, hogy amikor azt mondják, hogy ne írj specifikációkat, akkor azt mondják, hogy ne gondolkodj. És minden alkalommal gondolnia kell rá. A feladat átgondolása nem garantálja, hogy nem fog hibázni. Mint tudjuk, a varázspálcát senki sem találta fel, a programozás pedig nehéz feladat. De ha nem gondolja végig a problémát, garantáltan hibázik.
A TLA+-ról és a PlusCalról bővebben egy speciális weboldalon olvashatsz, oda a kezdőlapomról érhetsz el . Számomra ennyi, köszönöm a figyelmet.
Kérjük, vegye figyelembe, hogy ez egy fordítás. Amikor megjegyzéseket ír, ne feledje, hogy a szerző nem fogja elolvasni őket. Ha igazán szeretne beszélgetni a szerzővel, akkor ott lesz a Hydra 2019 konferencián, amelyet 11. július 12-2019-én rendeznek meg Szentpéterváron. Jegyek vásárolhatók .
Forrás: will.com