Dësen Artikel ass eng Iwwersetzung . Awer virun hirem eng kleng Aféierung. Wéi entstinn Zombien? Jiddereen ass an eng Situatioun komm wou se e Frënd oder Kolleg op hiren Niveau zéien wëllen, awer et klappt net. An et ass net sou vill mat Iech wéi mat him, datt "et net klappt": op enger Säit vun der Skala ass eng normal Pai, Aufgaben, an sou op, an op der anerer, de Besoin ze denken. Denken ass onsympathesch a schmerzhaf. Hie gëtt séier op a schreiwt weider Code ouni säi Gehir iwwerhaapt unzedréien. Dir stellt Iech vir wéi vill Effort et brauch fir d'Barrière vun der geléierter Hëlleflosegkeet ze iwwerwannen, an Dir maacht et einfach net. Dëst ass wéi Zombien geformt ginn, déi, et schéngt, geheelt kënne ginn, awer et schéngt datt keen et wäert maachen.
Wéi ech dat gesinn hunn (jo, dee selwechte Komerod aus de Léierbicher) a mécht kee Rapport, mee eng Fro-an-Äntwert Sëtzung, Ech war e bësse virsiichteg. Just am Fall, Leslie ass e weltberühmte Wëssenschaftler, den Auteur vu fundamentale Wierker am verdeelt Informatik, an Dir kënnt hien och duerch d'Bréiwer La am Wuert LaTeX kennen - "Lamport TeX". Den zweeten alarméierende Faktor ass seng Fuerderung: Jiddereen, dee kënnt, muss (absolut gratis) e puer vu senge Berichter am Viraus lauschteren, op d'mannst eng Fro doriwwer stellen, an eréischt dann kommen. Ech hu beschloss ze gesinn wat de Lamport do ausstrahlt - an et ass super! Et ass genau déi Saach, déi magesch Link-Pille fir Zombien ze heelen. Ech warnen Iech: Vum Text kënnen d'Liebhaber vu superflexibele Methodologien an déi, déi net gär testen wat geschriwwe steet, notamment ausbrennen.
No habrokat, tatsächlech, fänkt d'Iwwersetzung vum Seminar un. Genéisst d'Liesen!
Egal wéi eng Aufgab Dir maacht, musst Dir ëmmer dräi Schrëtt duerchgoen:
- entscheeden wat Zil Dir wëllt erreechen;
- entscheede wéi Dir Äert Zil erreechen wäert;
- kommt op Äert Zil.
Dëst gëllt och fir d'Programméierung. Wa mir Code schreiwen, musse mir:
- entscheeden wat de Programm soll maachen;
- bestëmmen, wéi et seng Aufgab Leeschtunge soll;
- schreiwen déi entspriechend Code.
De leschte Schrëtt ass natierlech ganz wichteg, awer ech wäert haut net driwwer schwätzen. Amplaz wäerte mir déi éischt zwee diskutéieren. All Programméierer mécht se virum Start ze schaffen. Dir sëtzt net fir ze schreiwen ausser Dir hutt decidéiert ob Dir e Browser oder eng Datebank schreift. Eng gewëssen Iddi vum Zil muss präsent sinn. An Dir denkt definitiv iwwer wat genau de Programm wäert maachen, a schreift net iergendwéi an der Hoffnung datt de Code iergendwéi an e Browser gëtt.
Wéi genee geschitt dëse Code Pre-Thinking? Wéi vill Efforte solle mir dofir leeën? Et hänkt alles dovun of wéi komplex de Problem mir léisen. Ugeholl mir wëllen e Feeler-tolerant verdeelt System schreiwen. An dësem Fall sollte mir d'Saache virsiichteg iwwerdenken ier mir eis sëtzen fir ze codéieren. Wat wa mir just eng ganz Zuel Variabel ëm 1 inkrementéiere mussen? Op den éischte Bléck ass alles trivial hei, a kee Gedanke brauch, awer dann erënnere mer datt en Iwwerschwemmung kann optrieden. Dofir, och fir ze verstoen ob e Problem einfach oder komplex ass, musst Dir als éischt denken.
Wann Dir iwwer méiglech Léisunge fir de Problem am Viraus denkt, kënnt Dir Feeler vermeiden. Awer dëst erfuerdert datt Äert Denken kloer ass. Fir dëst z'erreechen, musst Dir Är Gedanken opschreiwen. Ech hunn den Dick Guindon Zitat wierklech gär: "Wann Dir schreift, weist d'Natur Iech wéi schlëmm Äert Denken ass." Wann Dir net schreift, denkt Dir nëmmen datt Dir denkt. An Dir musst Är Gedanken a Form vu Spezifikatioune opschreiwen.
Spezifikatioune maachen vill Funktiounen, besonnesch a grousse Projeten. Mee ech wäert nëmmen iwwer ee vun hinnen schwätzen: si hëllefen eis kloer ze denken. Kloer denken ass ganz wichteg an zimlech schwéier, also hei brauche mir Hëllef. A wéi enger Sprooch solle mir Spezifikatioune schreiwen? Am Allgemengen ass dëst ëmmer déi éischt Fro fir Programméierer: a wéi enger Sprooch wäerte mir schreiwen. Et gëtt keng richteg Äntwert drop: d'Problemer déi mir léisen sinn ze divers. Fir e puer ass TLA + eng Spezifizéierungssprooch déi ech entwéckelt hunn. Fir anerer ass et méi praktesch Chinesesch ze benotzen. Alles hänkt vun der Situatioun of.
Méi wichteg ass eng aner Fro: wéi erreechen ech méi kloer Denken? Äntwert: Mir mussen denken wéi Wëssenschaftler. Dëst ass e Wee vum Denken, dee sech an de leschte 500 Joer bewisen huet. An der Wëssenschaft bauen mir mathematesch Modeller vun der Realitéit. Astronomie war vläicht déi éischt Wëssenschaft am strikte Sënn vum Wuert. Am mathematesche Modell, deen an der Astronomie benotzt gëtt, erschéngen Himmelskierper als Punkte mat Mass, Positioun a Dynamik, obwuel et a Wierklechkeet extrem komplex Objete mat Bierger an Ozeanen, Gezäiten a Gezäite sinn. Dëse Modell, wéi all aner, gouf geschaf fir verschidde Problemer ze léisen. Et ass super fir ze bestëmmen wou Dir den Teleskop soll weisen wann Dir e Planéit muss fannen. Awer wann Dir d'Wieder op dësem Planéit viraussoe wëllt, funktionnéiert dëse Modell net.
Mathematik erlaabt eis d'Eegeschafte vum Modell ze bestëmmen. An d'Wëssenschaft weist wéi dës Eegeschafte mat der Realitéit bezéien. Loosst eis iwwer eis Wëssenschaft schwätzen, Informatik. D'Realitéit mat där mir schaffen ass Rechensystemer vu verschiddenen Aarte: Prozessoren, Spillkonsolen, Computeren, Ausféierungsprogrammer, asw. Ech wäert schwätzen iwwer e Programm op engem Computer ze lafen, awer duerch a grouss, all dës Conclusiounen gëllen fir all Rechensystem. An eiser Wëssenschaft benotze mir vill verschidde Modeller: d'Turing Maschinn, deelweis bestallt Sets vun Eventer a vill anerer.
Wat ass e Programm? Dëst ass all Code deen onofhängeg ugesi ka ginn. Ugeholl mir mussen e Browser schreiwen. Mir maachen dräi Aufgaben: mir designen de Benotzer seng Vue op de Programm, da schreiwen mir den Héichniveau Diagramm vum Programm, a schliisslech schreiwen mir de Code. Wéi mir de Code schreiwen, mierken mir datt mir en Textformater musse schreiwen. Hei musse mir erëm dräi Problemer léisen: bestëmmen wat Text dëst Instrument wäert zréck; wielt en Algorithmus fir d'Formatéierung; schreiwen Code. Dës Aufgab huet seng eege Ënnertask: setzt en Bindestrecken korrekt a Wierder. Mir léisen dës Ënnertask och an dräi Schrëtt - wéi Dir gesitt, gi se op ville Niveauen widderholl.
Loosst eis den éischte Schrëtt méi detailléiert betruechten: wat fir e Problem de Programm léist. Hei modelléiere mir meeschtens e Programm als eng Funktioun déi e puer Input hëlt an e puer Output produzéiert. An der Mathematik gëtt eng Funktioun normalerweis als e bestallte Set vu Pairen beschriwwen. Zum Beispill gëtt d'Quadratfunktioun fir natierlech Zuelen als Set {<0,0>, <1,1>, <2,4>, <3,9>, …} beschriwwen. D'Domain vun esou enger Funktioun ass de Set vun den éischten Elementer vun all Pair, dat heescht déi natierlech Zuelen. Fir eng Funktioun ze definéieren, musse mir säin Ëmfang a Formel spezifizéieren.
Awer Funktiounen an der Mathematik sinn net d'selwecht wéi Funktiounen a Programméierungssproochen. Mathematik ass vill méi einfach. Well ech keng Zäit fir komplex Beispiller hunn, loosst eis eng einfach betruechten: eng Funktioun am C oder eng statesch Method am Java déi de gréisste gemeinsame Divisor vun zwee ganz Zuelen zréckkënnt. An der Spezifizéierung vun dëser Method wäerte mir schreiwen: berechent GCD(M,N) fir Argumenter M и Nwou GCD(M,N) - eng Funktioun där säin Domain de Set vu Pairen vun ganz Zuelen ass, an de Retourwäert ass dat gréisst Ganzt dat deelbar ass duerch M и N. Wéi ass dëse Modell mat der Realitéit verbonnen? De Modell funktionnéiert op ganz Zuelen, wärend am C oder Java mir en 32-Bit hunn int. Dëse Modell erlaabt eis ze entscheeden ob den Algorithmus richteg ass GCD, awer et wäert net Iwwerschwemmungsfehler verhënneren. Dat géif e méi komplexe Modell erfuerderen, fir dee keng Zäit gëtt.
Loosst eis iwwer d'Aschränkungen vun enger Funktioun als Modell schwätzen. E puer Programmer (wéi Betribssystemer) ginn net nëmmen e bestëmmte Wäert fir bestëmmten Argumenter zréck, si kënne kontinuéierlech lafen. Zousätzlech ass d'Funktioun als Modell net gutt fir den zweete Schrëtt: Planung wéi de Problem ze léisen. Quick Sort a Bubblesort berechnen déiselwecht Funktioun, awer si si komplett aner Algorithmen. Dofir, fir ze beschreiwen wéi d'Zil vum Programm erreecht gëtt, benotzen ech en anere Modell, loosst eis et de Standard Verhalensmodell nennen. De Programm an et ass als eng Rei vun all zulässlech Verhalen duergestallt, jiddereng vun deenen, ofwiesselnd, ass eng Sequenz vun Staaten, an de Staat ass d'Zeeche vu Wäerter ze Variablen.
Loosst eis kucken wéi den zweete Schrëtt fir den Euclid Algorithmus ausgesäit. Mir mussen ausrechnen GCD(M, N). Mir initialiséieren M wéi xan N wéi y, subtrahéiert dann ëmmer erëm déi kleng vun dëse Verännerlechen vun der grousser bis se gläich sinn. Zum Beispill, wann M = 12an N = 18, kënne mir folgend Verhalen beschreiwen:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
A wann et M = 0 и N = 0? Null ass deelbar vun all Zuelen, sou datt et kee gréissten Divisor an dësem Fall ass. An dëser Situatioun musse mer op den éischte Schrëtt zréckgoen a froen: musse mir wierklech GCD fir net-positiv Zuelen berechnen? Wann dat net néideg ass, da musst Dir just d'Spezifikatioun änneren.
Hei sollte mir e klengen Degressioun iwwer Produktivitéit maachen. Et gëtt dacks gemooss an der Unzuel vun de Zeilen vum Code pro Dag geschriwwe ginn. Awer Är Aarbecht ass vill méi nëtzlech wann Dir eng gewëssen Unzuel vun Zeilen läscht, well Dir manner Plaz fir Bugs hutt. An deen einfachste Wee fir de Code lass ze ginn ass um éischte Schrëtt. Et ass ganz méiglech datt Dir just net all d'Klacken a Pfeifen braucht, déi Dir probéiert ëmzesetzen. De schnellste Wee fir e Programm ze vereinfachen an Zäit ze spueren ass net Saachen ze maachen déi net solle gemaach ginn. Den zweete Schrëtt ass dat zweet meescht Zäitspuerend Potenzial. Wann Dir Produktivitéit moosst a punkto geschriwwene Linnen, dann ze denken wéi Dir eng Aufgab maache kënnt manner produktiv, well Dir de selwechte Problem mat manner Code léisen kann. Ech kann hei net genee Statistike ginn, well ech kee Wee hunn d'Zuel vun Zeilen ze zielen, déi ech net geschriwwen hunn wéinst der Tatsaach, datt ech Zäit op der Spezifizéierung verbruecht hunn, dat heescht op den éischten an zweete Schrëtt. An d'Experiment kann och hei net opgeriicht ginn, well mir am Experiment net d'Recht hunn den éischte Schrëtt ofzeschléissen, d'Aufgab ass virbestëmmt.
Et ass einfach vill Schwieregkeeten an informelle Spezifikatioune ze iwwersinn. Et gëtt näischt schwéier fir strikt Spezifikatioune fir Funktiounen ze schreiwen, ech wäert dat net diskutéieren. Amplaz schwätze mir iwwer d'Schreiwen vu staarke Spezifikatioune fir Standardverhalen. Et gëtt en Theorem dee seet datt all Set vu Behuelen ka beschriwwe ginn mat der Sécherheetseigenschaft (Sécherheet) an survivability Eegeschafte (Liveness). Sécherheet bedeit datt näischt Schlechtes geschitt, de Programm gëtt keng falsch Äntwert. D'Iwwerliewensbarkeet bedeit datt fréier oder spéider eppes Guddes geschitt, dh de Programm gëtt fréier oder spéider déi richteg Äntwert. Als Regel ass d'Sécherheet e méi wichtege Indikator, Feeler komme meeschtens hei. Dofir, fir Zäit ze spueren, wäert ech net iwwer Iwwerliewensfäegkeet schwätzen, obwuel et natierlech och wichteg ass.
Mir erreechen Sécherheet andeems mir als éischt de Set vu méiglechen initialen Zoustänn virschreiwe. An zweetens, Relatiounen mat all méiglech nächst Staaten fir all Staat. Loosst eis wéi Wëssenschaftler handelen a Staaten mathematesch definéieren. De Set vun initialen Zoustänn gëtt mat enger Formel beschriwwen, zum Beispill am Fall vum Euklideschen Algorithmus: (x = M) ∧ (y = N). Fir bestëmmte Wäerter M и N et gëtt nëmmen een initialen Zoustand. D'Relatioun mam nächste Staat gëtt duerch eng Formel beschriwwen, an där d'Variabelen vum nächste Staat mat engem Prime geschriwwe sinn, an d'Variabelen vum aktuelle Staat ouni Prime geschriwwe ginn. Am Fall vum Euklids Algorithmus wäerte mir mat der Disjunktioun vun zwou Formelen beschäftegen, an enger vun deenen x ass de gréisste Wäert, an am zweeten - y:
Am éischte Fall ass den neie Wäert vun y gläich wéi de fréiere Wäert vun y, a mir kréien den neie Wäert vun x andeems Dir déi kleng Variabel vun der méi grousser subtrahéiert. Am zweete Fall maache mir de Géigendeel.
Komme mer zréck op den Euklids Algorithmus. Loosst eis dat nach eng Kéier unhuelen M = 12, N = 18. Dëst definéiert een eenzegen initialen Zoustand, (x = 12) ∧ (y = 18). Mir pluggen dës Wäerter dann an d'Formel hei uewen a kréien:
Hei ass déi eenzeg méiglech Léisung: x' = 18 - 12 ∧ y' = 12a mir kréien d'Verhalen: [x = 12, y = 18]. Ähnlech kënne mir all Staaten an eisem Verhalen beschreiwen: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
Am leschte Staat [x = 6, y = 6] béid Deeler vum Ausdrock wäert falsch sinn, sou datt et keen nächste Staat huet. Also, mir hunn eng komplett Spezifizéierung vun der zweeter Schrëtt - wéi Dir gesitt kann, dat ass ganz normal Mathematik, wéi an Ingenieuren a Wëssenschaftler, an net komesch, wéi an Informatik.
Dës zwou Formelen kënnen an eng Formel vun der temporärer Logik kombinéiert ginn. Si ass elegant an einfach ze erklären, awer et gëtt keng Zäit fir hatt elo. Mir brauche vläicht temporär Logik nëmme fir d'Liewensqualitéit, et ass net néideg fir Sécherheet. Ech hunn d'temporal Logik als solch net gär, et ass net ganz normal Mathematik, awer am Fall vun der Liveliness ass et en noutwendegt Béis.
Am Algorithmus vum Euklid, fir all Wäert x и y hunn eenzegaarteg Wäerter x' и y', déi d'Relatioun mam nächste Staat richteg maachen. An anere Wierder, dem Euklid säin Algorithmus ass deterministesch. Fir en net-deterministesche Algorithmus ze modelléieren, muss den aktuellen Zoustand multiple méiglech zukünfteg Zoustänn hunn, an datt all onpriméiert Variabelwäert multiple priméiert Variabelwäerter huet, sou datt d'Relatioun zum nächste Staat richteg ass. Dëst ass einfach ze maachen, awer ech ginn elo keng Beispiller.
Fir en Aarbechtsinstrument ze maachen, braucht Dir formell Mathematik. Wéi d'Spezifikatioun formell ze maachen? Fir dëst ze maachen brauche mir eng formell Sprooch, z.B. . D'Spezifikatioun vum Euclid Algorithmus géif an dëser Sprooch esou ausgesinn:
E Gläichzeechen Symbol mat engem Dräieck bedeit datt de Wäert lénks vum Schëld definéiert ass wéi de Wäert riets vum Schëld. Am Wesentlechen ass d'Spezifikatioun eng Definitioun, an eisem Fall zwou Definitiounen. Zu der Spezifizéierung an TLA + musst Dir Deklaratiounen an e puer Syntax addéieren, wéi an der Rutsch uewen. An ASCII géif et esou ausgesinn:
Wéi Dir kënnt gesinn, näischt komplizéiert. D'Spezifikatioun fir TLA + kann getest ginn, dh all méiglech Verhalen an engem klenge Modell ëmgoen. An eisem Fall wäert dëse Modell bestëmmte Wäerter sinn M и N. Dëst ass eng ganz effizient an einfach Verifizéierungsmethod déi komplett automatesch ass. Et ass och méiglech formell Wourecht Beweiser ze schreiwen an se mechanesch kontrolléieren, mä dat hëlt vill Zäit, also bal keen mécht dat.
Den Haaptnodeel vun TLA + ass datt et Mathematik ass, a Programméierer a Computerwëssenschaftler hunn Angscht virun der Mathematik. Op den éischte Bléck kléngt dat no engem Witz, mee leider mengen ech et ganz Eescht. Mäi Kolleg huet mir just gesot wéi hien probéiert TLA + zu verschiddenen Entwéckler z'erklären. Soubal d'Formelen um Bildschierm erschéngen, goufen se direkt glasg Aen. Also wann TLA + Iech Angscht mécht, kënnt Dir benotzen , et ass eng Zort Spillsaach Programméiersprooch. En Ausdrock am PlusCal kann all TLA + Ausdrock sinn, dat ass, duerch a grouss, all mathemateschen Ausdrock. Zousätzlech huet PlusCal eng Syntax fir net-deterministesch Algorithmen. Well PlusCal all TLA + Ausdrock schreiwen kann, ass PlusCal vill méi expressiv wéi all richteg Programméierungssprooch. Als nächst gëtt PlusCal an eng liicht liesbar TLA + Spezifizéierung zesummegesat. Dëst bedeit natierlech net datt déi komplex PlusCal Spezifizéierung zu engem einfachen op TLA + gëtt - just d'Korrespondenz tëscht hinnen ass offensichtlech, et gëtt keng zousätzlech Komplexitéit. Schlussendlech kann dës Spezifizéierung duerch TLA + Tools verifizéiert ginn. Alles an allem kann PlusCal hëllefen mathematesch Phobie ze iwwerwannen an ass einfach ze verstoen och fir Programméierer a Computerwëssenschaftler. An der Vergaangenheet hunn ech Algorithmen drop publizéiert fir eng Zäit (ongeféier 10 Joer).
Vläicht wäert iergendeen Objet datt TLA + a PlusCal Mathematik sinn, a Mathematik funktionnéiert nëmmen op erfonnten Beispiller. An der Praxis braucht Dir eng richteg Sprooch mat Typen, Prozeduren, Objeten, asw. Dëst ass falsch. Hei ass wat de Chris Newcomb, deen bei Amazon geschafft huet, schreift: "Mir hunn TLA + op zéng gréisser Projete benotzt, an all Fall, d'Benotzung huet e wesentlechen Ënnerscheed zu der Entwécklung gemaach, well mir fäeg sinn geféierlech Bugs ze fangen ier mer d'Produktioun erreecht hunn, a well et eis den Asiicht an d'Vertraue ginn huet, déi mir gebraucht hunn aggressiv Leeschtungsoptimisatiounen maachen ouni d'Wahrheet vum Programm ze beaflossen". Dir kënnt dacks héieren datt wann Dir formell Methoden benotzt, mir ineffiziente Code kréien - an der Praxis ass alles genau de Géigendeel. Zousätzlech gëtt et eng Meenung datt d'Manager net vun der Bedierfnes fir formell Methoden iwwerzeegt kënne ginn, och wann d'Programméierer vun hirer Nëtzlechkeet iwwerzeegt sinn. An Newcomb schreift: "D'Manager drécken elo schwéier fir Spezifikatioune fir TLA + ze schreiwen, a speziell Zäit dofir ze verdeelen". Also wann d'Manager gesinn datt TLA + funktionnéiert, si si frou et ze akzeptéieren. De Chris Newcomb huet dat viru ronn sechs Méint (Oktober 2014) geschriwwen, awer elo, souwäit ech weess, gëtt TLA+ a 14 Projete benotzt, net 10. En anert Beispill ass am Design vun der XBox 360. Eng Stagiaire koum bei de Charles Thacker an geschriwwen Spezifizéierung fir d'Erënnerung System. Dank dëser Spezifizéierung gouf e Käfer fonnt, deen soss onnotéiert géif goen, a wéinst deem all Xbox 360 no véier Stonne Gebrauch erofgefall ass. IBM Ingenieuren hunn bestätegt datt hir Tester dëse Feeler net fonnt hunn.
Dir kënnt méi iwwer TLA + um Internet liesen, awer loosst eis elo iwwer informelle Spezifikatioune schwätzen. Mir mussen selten Programmer schreiwen déi de mannsten gemeinsamen Divisor an dergläiche berechent. Vill méi dacks schreiwen mir Programmer wéi de schéine Printer-Tool, deen ech fir TLA+ geschriwwen hunn. No der einfachster Veraarbechtung géif den TLA + Code esou ausgesinn:
Awer am uewe genannte Beispill wollt de Benotzer héchstwahrscheinlech datt d'Konjunktioun an d'Gläichzeechen ausgeriicht sinn. Also déi richteg Formatéierung géif méi esou ausgesinn:
Betruecht en anert Beispill:
Hei, am Géigendeel, war d'Ausrichtung vun de Gleich-, Zousatz- a Multiplikatiounszeechen an der Quell zoufälleg, sou datt déi einfachst Veraarbechtung ganz genuch ass. Am Allgemengen gëtt et keng exakt mathematesch Definitioun vu richteger Formatéierung, well "korrekt" an dësem Fall heescht "wat de Benotzer wëll", an dëst kann net mathematesch bestëmmt ginn.
Et géif schéngen datt wa mir keng Definitioun vu Wahrheet hunn, dann ass d'Spezifikatioun nëtzlos. Mä et ass net. Just well mir net wësse wat e Programm soll maachen, heescht net datt mir net mussen iwwerdenken wéi et funktionnéiert - am Géigendeel, mir mussen nach méi Effort dran maachen. D'Spezifikatioun ass besonnesch wichteg hei. Et ass onméiglech den optimale Programm fir strukturéiert Dréckerei ze bestëmmen, awer dat heescht net datt mir et guer net sollten huelen, a Code als Bewosstsinn ze schreiwen ass net gutt. Um Enn hunn ech eng Spezifizéierung vu sechs Regele mat Definitioune geschriwwen a Form vu Kommentaren an enger Java Datei. Hei ass e Beispill vun enger vun de Regelen: a left-comment token is LeftComment aligned with its covering token. Dës Regel ass geschriwwen op, wäerte mir soen, mathematesch Englesch: LeftComment aligned, left-comment и covering token - Begrëffer mat Definitiounen. Esou beschreiwen Mathematiker Mathematik: Si schreiwen Definitioune vu Begrëffer a baséiert op hinnen Regelen. De Virdeel vun esou enger Spezifizéierung ass datt sechs Regele vill méi einfach ze verstoen an ze debuggen wéi 850 Zeilen Code. Ech muss soen datt d'Schreiwen vun dëse Regelen net einfach war, et huet zimmlech vill Zäit gedauert fir se ze debuggen. Besonnesch fir dësen Zweck hunn ech e Code geschriwwen, dee gemellt huet wéi eng Regel benotzt gouf. Dank der Tatsaach, datt ech dës sechs Reegelen op e puer Beispiller getest hunn, hunn ech net 850 Zeilen Code ze debuggen, a Käfere ware ganz einfach ze fannen. Java huet super Tools fir dëst. Wann ech just de Code geschriwwen hätt, hätt et vill méi laang gedauert, an d'Formatéierung wier vu méi schlechter Qualitéit gewiescht.
Firwat konnt net eng formell Spezifizéierung benotzt ginn? Engersäits ass déi richteg Ausféierung hei net ze wichteg. Strukturell Ofdréck si gebonnen fir keen ze gefalen, also hunn ech et net missen an all komeschen Situatiounen richteg funktionnéieren. Nach méi wichteg ass de Fakt datt ech net adäquat Tools haten. Den TLA + Modellchecker ass nëtzlos hei, also muss ech d'Beispiller manuell schreiwen.
Déi uewe Spezifizéierung huet Features, déi fir all Spezifikatioune gemeinsam sinn. Et ass méi héich wéi de Code. Et kann an all Sprooch ëmgesat ginn. All Tools oder Methode sinn nëtzlos fir et ze schreiwen. Kee Programméierungscours hëlleft Iech dës Spezifizéierung ze schreiwen. An et gi keng Tools déi dës Spezifizéierung onnéideg maache kënnen, ausser Dir schreift natierlech eng Sprooch speziell fir strukturéiert Printprogrammer an TLA+ ze schreiwen. Schlussendlech seet dës Spezifizéierung näischt iwwer genau wéi mir de Code schreiwen, et seet nëmmen wat dëse Code mécht. Mir schreiwen d'Spezifikatioun fir eis ze hëllefen duerch de Problem ze denken ier mir un de Code denken.
Awer dës Spezifizéierung huet och Features déi se vun anere Spezifikatioune ënnerscheeden. 95% vun anere Spezifikatioune si wesentlech méi kuerz a méi einfach:
Weider ass dës Spezifizéierung eng Rei vu Regelen. Als Regel, ass dëst en Zeeche vun enger schlechter Spezifizéierung. D'Konsequenze vun enger Rei vu Regelen ze verstoen ass zimmlech schwéier, dofir hunn ech vill Zäit misse verbréngen fir se ze Debuggéieren. Wéi och ëmmer, an dësem Fall konnt ech kee bessere Wee fannen.
Et ass derwäert e puer Wierder ze soen iwwer Programmer déi kontinuéierlech lafen. Als Regel, schaffen se parallel, zum Beispill, Betribssystemer oder verdeelt Systemer. Ganz wéineg Leit kënnen se geeschteg oder op Pabeier verstoen, an ech sinn net ee vun hinnen, obwuel ech et eemol konnt maachen. Dofir brauche mir Tools déi eis Aarbecht iwwerpréiwen - zum Beispill TLA + oder PlusCal.
Firwat war et néideg eng Spezifizéierung ze schreiwen wann ech scho wosst wat genau de Code soll maachen? Tatsächlech, Ech geduecht just ech wosst et. Zousätzlech, mat enger Spezifizéierung, brauch en Outsider net méi an de Code ze kommen fir ze verstoen wat hien genau mécht. Ech hunn eng Regel: et soll keng allgemeng Regele ginn. Et gëtt eng Ausnam zu dëser Regel, natierlech, et ass déi eenzeg allgemeng Regel déi ech verfollegen: d'Spezifikatioun vun deem wat de Code mécht, soll de Leit alles soen wat se wësse mussen wann se de Code benotzen.
Also wat genau musse Programméierer iwwer Denken wëssen? Fir Ufänger, d'selwecht wéi all déi aner: Wann Dir net schreift, da schéngt et Iech nëmmen datt Dir denkt. Och musst Dir denken ier Dir codéiert, dat heescht datt Dir musst schreiwen ier Dir codéiert. D'Spezifikatioun ass dat wat mir schreiwen ier mer ufänken ze codéieren. Eng Spezifizéierung ass néideg fir all Code dee vu jidderee benotzt oder geännert ka ginn. An dësen "een" kann den Auteur vum Code selwer e Mount nodeems et geschriwwe gouf. Eng Spezifizéierung ass néideg fir grouss Programmer a Systemer, fir Klassen, fir Methoden, an heiansdo souguer fir komplex Sektioune vun enger eenzeger Method. Wat genau soll iwwer de Code geschriwwe ginn? Dir musst beschreiwen wat et mécht, dat ass, wat kann nëtzlech sinn fir all Persoun déi dëse Code benotzt. Heiansdo kann et och néideg sinn ze spezifizéieren wéi de Code säin Zweck erfëllt. Wa mir dës Method am Laf vun Algorithmen duerchgaange sinn, da nenne mir et en Algorithmus. Wann et eppes méi Besonnesches an Neies ass, da nenne mir et High-Level Design. Et gëtt keen formellen Ënnerscheed hei: béid sinn en abstrakte Modell vun engem Programm.
Wéi genau sollt Dir eng Code Spezifizéierung schreiwen? Den Haapt Saach: et soll een Niveau méi héich sinn wéi de Code selwer. Et soll Staaten a Behuelen beschreiwen. Et soll esou strikt sinn wéi d'Aufgab erfuerdert. Wann Dir eng Spezifizéierung schreift fir wéi eng Aufgab ëmgesat gëtt, kënnt Dir et a Pseudocode oder mat PlusCal schreiwen. Dir musst léieren wéi Dir Spezifikatioune op formell Spezifikatioune schreift. Dëst gëtt Iech déi néideg Fäegkeeten, déi Iech och mat informelle hëllefen. Wéi léiert Dir formell Spezifikatioune ze schreiwen? Wa mir geléiert hunn ze programméieren, hu mir Programmer geschriwwen an se dann debugged. Et ass d'selwecht hei: schreift d'Spezifikatioun, kontrolléiert et mam Modellchecker, a fixéiert d'Bugs. TLA + ass vläicht net déi bescht Sprooch fir eng formell Spezifizéierung, an eng aner Sprooch ass méiglecherweis besser fir Är spezifesch Besoinen. De Virdeel vun TLA + ass datt et mathematescht Denken ganz gutt léiert.
Wéi verbënnt Spezifizéierung a Code? Mat Hëllef vu Kommentaren déi mathematesch Konzepter an hir Ëmsetzung verbannen. Wann Dir mat Grafike schafft, da sidd Dir um Programmniveau Arrays vun Noden an Arrays vu Linken. Dofir musst Dir genau schreiwen wéi d'Grafik vun dëse Programméierungsstrukturen ëmgesat gëtt.
Et sollt bemierkt datt keng vun den uewe genannte fir den eigentleche Prozess vum Code schreiwen. Wann Dir de Code schreift, dat heescht, Dir maacht den drëtte Schrëtt, musst Dir och iwwer de Programm denken an denken. Wann eng Ënnertask komplex oder net offensichtlech ass, musst Dir eng Spezifizéierung dofir schreiwen. Mee ech schwätzen net iwwer de Code selwer hei. Dir kënnt all Programméierungssprooch benotzen, all Methodik, et geet net ëm si. Och kee vun den uewe genannte eliminéiert de Besoin fir Code ze testen an ze debuggen. Och wann den abstrakte Modell richteg geschriwwe gëtt, kënnen et Bugs a senger Ëmsetzung sinn.
Spezifikatioune schreiwen ass en zousätzleche Schrëtt am Kodéierungsprozess. Dank et kënne vill Feeler mat manner Effort erfaasst ginn - mir wëssen dat aus der Erfahrung vun de Programméierer vun Amazon. Mat Spezifikatioune gëtt d'Qualitéit vu Programmer méi héich. Also firwat gi mir dann sou dacks ouni si? Well schreiwen ass schwéier. A schreiwen ass schwéier, well dofir musst Dir denken, an denken ass och schwéier. Et ass ëmmer méi einfach ze maachen wéi Dir denkt. Hei kënnt Dir eng Analogie mam Lafen zéien - wat Dir manner laaft, wat Dir méi lues laaft. Dir musst Är Muskelen trainéieren a schreiwen. Brauchen Praxis.
D'Spezifikatioun kann falsch sinn. Dir hutt vläicht iergendwou e Feeler gemaach, oder d'Ufuerderunge kënne geännert hunn, oder eng Verbesserung muss gemaach ginn. All Code dee jidderee benotzt muss geännert ginn, sou datt fréier oder spéider d'Spezifikatioun net méi mam Programm passt. Idealfall, an dësem Fall musst Dir eng nei Spezifizéierung schreiwen an de Code komplett nei schreiwen. Mir wëssen ganz gutt, datt keen dat mécht. An der Praxis patche mir de Code a aktualiséieren eventuell d'Spezifikatioun. Wann dat gebonnen ass desto oder spéider ze geschéien, firwat dann iwwerhaapt Spezifikatioune schreiwen? Als éischt, fir déi Persoun déi Äre Code ännere wäert, all extra Wuert an der Spezifizéierung wäert säi Gewiicht am Gold wäert sinn, an dës Persoun kann Iech selwer sinn. Ech berouegen mech dacks fir net genuch Spezifizéierung ze kréien wann ech mäi Code änneren. An ech schreiwen méi Spezifikatioune wéi Code. Dofir, wann Dir de Code ännert, muss d'Spezifikatioun ëmmer aktualiséiert ginn. Zweetens, mat all Versioun gëtt de Code verschlechtert, et gëtt ëmmer méi schwéier ze liesen an z'erhalen. Dëst ass eng Erhéijung vun der Entropie. Awer wann Dir net mat enger Spezifizéierung ufänkt, da wäert all Zeil déi Dir schreift eng Ännerung sinn, an de Code wäert onbestänneg a schwéier vun Ufank un ze liesen.
Wéi gesot , keng Schluecht gouf vum Plang gewonnen, a keng Schluecht gouf ouni Plang gewonnen. An hie wousst eng Saach oder zwee iwwer Schluechte. Et gëtt eng Meenung datt d'Spezifikatioune schreiwen eng Zäitverschwendung ass. Heiansdo ass dat richteg, an d'Aufgab ass sou einfach datt et näischt ass ze iwwerdenken. Awer Dir sollt ëmmer drun erënneren datt wann Dir gesot hutt keng Spezifikatioune ze schreiwen, Dir sidd gesot net ze denken. An Dir sollt all Kéier driwwer nodenken. Denken duerch d'Aufgab garantéiert net datt Dir keng Feeler maacht. Wéi mir wëssen, huet keen den Zauberwand erfonnt, a Programméiere ass eng schwiereg Aufgab. Awer wann Dir de Problem net duerchdenkt, sidd Dir garantéiert Feeler ze maachen.
Dir kënnt méi iwwer TLA + a PlusCal op enger spezieller Websäit liesen, Dir kënnt do vu menger Homepage goen . Dat ass alles fir mech, Merci fir Är Opmierksamkeet.
Maacht weg datt dëst eng Iwwersetzung ass. Wann Dir Kommentaren schreift, denkt drun datt den Auteur se net liest. Wann Dir wierklech mam Auteur wëllt chatten, da wäert hien op der Hydra 2019 Konferenz sinn, déi 11-12 Juli 2019 zu St. Tickete kënne kaaft ginn .
Source: will.com