Nkan yii jẹ itumọ . Sugbon niwaju rẹ kekere kan ifihan. Bawo ni a ṣe ṣẹda awọn Ebora? Gbogbo eniyan wa sinu ipo kan nibiti wọn fẹ lati fa ọrẹ tabi alabaṣiṣẹpọ soke si ipele wọn, ṣugbọn ko ṣiṣẹ. Ati pe kii ṣe pupọ pẹlu rẹ bi pẹlu rẹ pe "ko ṣiṣẹ jade": ni apa kan ti iwọn naa jẹ owo-ori deede, awọn iṣẹ-ṣiṣe, ati bẹbẹ lọ, ati lori ekeji, o nilo lati ronu. Lerongba jẹ unpleasant ati irora. O yara fi silẹ ati tẹsiwaju lati kọ koodu laisi titan ọpọlọ rẹ rara. O wo iye akitiyan ti o gba lati bori idena ti ailagbara ti ẹkọ, ati pe o kan ko ṣe. Eyi ni bii awọn Ebora ṣe ṣẹda, eyiti, o dabi pe o le mu larada, ṣugbọn o dabi pe ko si ẹnikan ti yoo ṣe.
Nigbati mo ri pe (bẹẹni, ẹlẹgbẹ kanna lati awọn iwe-ẹkọ) ati pe ko ṣe ijabọ kan, ṣugbọn igba ibeere ati idahun, Mo ṣọra diẹ. O kan ni ọran, Leslie jẹ onimọ-jinlẹ olokiki agbaye, onkọwe ti awọn iṣẹ ipilẹ ni iširo pinpin, ati pe o tun le mọ ọ nipasẹ awọn lẹta La ninu ọrọ LaTeX - “Lamport TeX”. Okunfa ibanilẹru keji ni ibeere rẹ: gbogbo eniyan ti o wa gbọdọ (ni ọfẹ ọfẹ) tẹtisi awọn ijabọ meji ni ilosiwaju, wa pẹlu o kere ju ibeere kan lori wọn, ati lẹhinna wa nikan. Mo pinnu lati wo kini Lamport n ṣe ikede nibẹ - ati pe o dara! Ohun naa gan-an ni, oogun ọna asopọ idan lati ṣe iwosan awọn Ebora. Mo kilọ fun ọ: lati inu ọrọ naa, awọn ololufẹ ti awọn ilana ti o ni irọrun pupọ ati awọn ti ko nifẹ lati ṣe idanwo ohun ti a kọ le jo jade ni pataki.
Lẹhin habrokat, ni otitọ, itumọ ti apejọ naa bẹrẹ. Gbadun kika!
Eyikeyi iṣẹ-ṣiṣe ti o ba ṣe, o nilo nigbagbogbo lati lọ nipasẹ awọn igbesẹ mẹta:
- pinnu kini ibi-afẹde ti o fẹ lati ṣaṣeyọri;
- pinnu bi o ṣe le ṣaṣeyọri ibi-afẹde rẹ;
- wa si ibi-afẹde rẹ.
Eyi tun kan siseto. Nigbati a ba kọ koodu, a nilo lati:
- pinnu ohun ti eto yẹ ki o ṣe;
- pinnu bi o ṣe yẹ ki o ṣe iṣẹ rẹ;
- kọ awọn ti o baamu koodu.
Igbesẹ ikẹhin, dajudaju, ṣe pataki pupọ, ṣugbọn Emi kii yoo sọrọ nipa rẹ loni. Kàkà bẹ́ẹ̀, a máa jíròrò méjì àkọ́kọ́. Gbogbo pirogirama ṣe wọn ṣaaju ki o to bẹrẹ iṣẹ. Iwọ ko joko lati kọ ayafi ti o ba ti pinnu boya o n kọ ẹrọ aṣawakiri tabi data data kan. Ero kan ti ibi-afẹde naa gbọdọ wa. Ati pe o dajudaju kini ohun ti eto naa yoo ṣe ni pato, ati maṣe kọ bakan ni ireti pe koodu naa yoo yipada bakan sinu ẹrọ aṣawakiri kan.
Bawo ni pato koodu yi ṣaaju-ero ṣẹlẹ? Báwo ló ṣe yẹ ká sapá tó nínú èyí? Gbogbo rẹ da lori bii iṣoro ti o nira ti a n yanju. Sawon a fẹ lati kọ kan ẹbi-ọlọdun eto pin. Ni idi eyi, o yẹ ki a ronu awọn nkan daradara ṣaaju ki a to joko si koodu. Ti a ba kan nilo lati ṣafikun oniyipada odidi nipasẹ 1? Ni wiwo akọkọ, ohun gbogbo jẹ ohun kekere nibi, ko si si ero ti a nilo, ṣugbọn lẹhinna a ranti pe iṣan omi le waye. Nitorinaa, paapaa lati ni oye boya iṣoro kan rọrun tabi eka, o nilo akọkọ lati ronu.
Ti o ba ronu nipa awọn ojutu ti o ṣeeṣe si iṣoro naa ni ilosiwaju, o le yago fun awọn aṣiṣe. Ṣùgbọ́n èyí ń béèrè pé kí ìrònú rẹ ṣe kedere. Lati ṣe aṣeyọri eyi, o nilo lati kọ awọn ero rẹ silẹ. Mo fẹran agbasọ Dick Guindon gaan: “Nigbati o ba kọ, ẹda n fihan ọ bi ironu rẹ ṣe rọ.” Ti o ko ba kọ, iwọ nikan ro pe o nro. Ati pe o nilo lati kọ awọn ero rẹ silẹ ni irisi awọn pato.
Awọn pato ṣe ọpọlọpọ awọn iṣẹ, paapaa ni awọn iṣẹ akanṣe nla. Ṣugbọn emi yoo sọrọ nipa ọkan ninu wọn nikan: wọn ṣe iranlọwọ fun wa lati ronu kedere. Ironu kedere jẹ pataki pupọ ati pe o nira pupọ, nitorinaa a nilo iranlọwọ eyikeyi. Ede wo ni o yẹ ki a kọ awọn pato ni pato? Ni gbogbogbo, eyi nigbagbogbo jẹ ibeere akọkọ fun awọn olupilẹṣẹ: ede wo ni a yoo kọ sinu. Ko si idahun kan ti o pe: awọn iṣoro ti a yanju ni o yatọ pupọ. Fun diẹ ninu, TLA+ jẹ ede sipesifikesonu ti Mo ni idagbasoke. Fun awọn miiran, o rọrun diẹ sii lati lo Kannada. Ohun gbogbo da lori ipo naa.
Pataki julọ ni ibeere miiran: bawo ni a ṣe le ṣaṣeyọri ironu ti o han gbangba? Idahun: A gbọdọ ronu bi awọn onimọ-jinlẹ. Eyi jẹ ọna ironu ti o ti fi ara rẹ han ni awọn ọdun 500 sẹhin. Ni imọ-jinlẹ, a kọ awọn awoṣe mathematiki ti otito. Aworawo jẹ boya imọ-jinlẹ akọkọ ni ori ti o muna ti ọrọ naa. Ninu awoṣe mathematiki ti a lo ninu imọ-jinlẹ, awọn ara ọrun han bi awọn aaye pẹlu ibi-ipo, ipo ati ipa, botilẹjẹpe ni otitọ wọn jẹ awọn nkan ti o ni eka pupọ pẹlu awọn oke-nla ati awọn okun, awọn okun ati awọn ṣiṣan. Awoṣe yii, bii eyikeyi miiran, ni a ṣẹda lati yanju awọn iṣoro kan. O jẹ nla fun ṣiṣe ipinnu ibiti o le tọka si ẹrọ imutobi ti o ba nilo lati wa aye kan. Ṣugbọn ti o ba fẹ ṣe asọtẹlẹ oju ojo lori aye yii, awoṣe yii kii yoo ṣiṣẹ.
Iṣiro gba wa laaye lati pinnu awọn ohun-ini ti awoṣe. Ati pe imọ-jinlẹ fihan bi awọn ohun-ini wọnyi ṣe ni ibatan si otitọ. Jẹ ki a sọrọ nipa imọ-jinlẹ wa, imọ-ẹrọ kọnputa. Otitọ pẹlu eyiti a n ṣiṣẹ ni awọn ọna ṣiṣe iṣiro ti awọn oriṣiriṣi oriṣiriṣi: awọn ero isise, awọn afaworanhan ere, awọn kọnputa, awọn eto ṣiṣe, ati bẹbẹ lọ. Emi yoo sọrọ nipa ṣiṣe eto kan lori kọnputa, ṣugbọn lapapọ, gbogbo awọn ipinnu wọnyi lo si eyikeyi eto iširo. Ninu imọ-jinlẹ wa, a lo ọpọlọpọ awọn awoṣe oriṣiriṣi: ẹrọ Turing, awọn eto iṣẹlẹ ti a paṣẹ ni apakan, ati ọpọlọpọ awọn miiran.
Kini eto kan? Eyi jẹ koodu eyikeyi ti o le gbero ni ominira. Ṣebi a nilo lati kọ ẹrọ aṣawakiri kan. A ṣe awọn iṣẹ-ṣiṣe mẹta: a ṣe apẹrẹ wiwo olumulo ti eto naa, lẹhinna a kọ apẹrẹ ipele giga ti eto naa, ati nikẹhin a kọ koodu naa. Bi a ṣe n kọ koodu naa, a mọ pe a nilo lati kọ ọna kika ọrọ kan. Nibi a tun nilo lati yanju awọn iṣoro mẹta: pinnu kini ọrọ ti ọpa yii yoo pada; yan algorithm kan fun kika; kọ koodu. Iṣẹ-ṣiṣe yii ni iṣẹ-ṣiṣe ti ara rẹ: fi ami-ọrọ sii ni deede sinu awọn ọrọ. A tun yanju iṣẹ-ṣiṣe kekere yii ni awọn igbesẹ mẹta - bi o ti le rii, wọn tun ṣe ni awọn ipele pupọ.
Jẹ ki a ronu ni awọn alaye diẹ sii ni igbesẹ akọkọ: kini iṣoro ti eto naa yanju. Nibi, a nigbagbogbo ṣe apẹẹrẹ eto kan bi iṣẹ kan ti o gba diẹ ninu awọn titẹ sii ati ṣe agbejade diẹ ninu awọn iṣelọpọ. Ni mathimatiki, iṣẹ kan ni a maa n ṣe apejuwe bi akojọpọ awọn orisii ti a paṣẹ. Fun apẹẹrẹ, iṣẹ onigun fun awọn nọmba adayeba jẹ apejuwe bi ṣeto {<0,0>, <1,1>, <2,4>, <3,9>, …}. Awọn aaye ti iru iṣẹ kan jẹ ṣeto ti awọn eroja akọkọ ti bata kọọkan, iyẹn ni, awọn nọmba adayeba. Lati ṣalaye iṣẹ kan, a nilo lati pato iwọn ati agbekalẹ rẹ.
Ṣugbọn awọn iṣẹ ni mathimatiki kii ṣe kanna bi awọn iṣẹ ni awọn ede siseto. Iṣiro jẹ rọrun pupọ. Niwọn igba ti Emi ko ni akoko fun awọn apẹẹrẹ idiju, jẹ ki a gbero ọkan ti o rọrun: iṣẹ kan ni C tabi ọna aimi ni Java ti o da ipinpapọ wọpọ nla ti awọn odidi meji pada. Ni sipesifikesonu ti ọna yii, a yoo kọ: ṣe iṣiro GCD(M,N) fun awọn ariyanjiyan M и Nnibo GCD(M,N) - iṣẹ kan ti agbegbe rẹ jẹ ṣeto awọn orisii odidi, ati iye ipadabọ jẹ odidi ti o tobi julọ ti o pin nipasẹ M и N. Bawo ni awoṣe yii ṣe ni ibatan si otitọ? Awọn awoṣe nṣiṣẹ lori odidi, nigba ti ni C tabi Java a ni a 32-bit int. Awoṣe yii gba wa laaye lati pinnu boya algorithm jẹ deede GCD, ṣugbọn kii yoo ṣe idiwọ awọn aṣiṣe aponsedanu. Eyi yoo nilo awoṣe eka diẹ sii, eyiti ko si akoko.
Jẹ ki a sọrọ nipa awọn idiwọn ti iṣẹ kan bi awoṣe. Diẹ ninu awọn eto (gẹgẹbi awọn ọna ṣiṣe) kii ṣe da pada iye kan fun awọn ariyanjiyan kan, wọn le ṣiṣe ni igbagbogbo. Ni afikun, iṣẹ bi awoṣe ko dara fun igbesẹ keji: ṣiṣero bi o ṣe le yanju iṣoro naa. Too too ati bubble too ṣe iṣiro iṣẹ kanna, ṣugbọn wọn jẹ awọn algoridimu ti o yatọ patapata. Nitorinaa, lati ṣapejuwe bi ibi-afẹde ti eto naa ṣe waye, Mo lo awoṣe ti o yatọ, jẹ ki a pe ni awoṣe ihuwasi boṣewa. Eto ti o wa ninu rẹ jẹ aṣoju bi ṣeto ti gbogbo awọn ihuwasi iyọọda, ọkọọkan eyiti, lapapọ, jẹ ọkọọkan ti awọn ipinlẹ, ati pe ipinlẹ jẹ ipinfunni ti awọn iye si awọn oniyipada.
Jẹ ki a wo kini igbesẹ keji fun algorithm Euclid yoo dabi. A nilo lati ṣe iṣiro GCD(M, N). A bẹrẹ M bi o x, ati N bi o y, lẹhinna leralera yọkuro diẹ ninu awọn oniyipada wọnyi lati tobi titi ti wọn yoo fi dọgba. Fun apẹẹrẹ, ti o ba M = 12, ati N = 18, a le ṣe apejuwe iwa wọnyi:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
Ati ti o ba M = 0 и N = 0? Odo jẹ pipin nipasẹ gbogbo awọn nọmba, nitorinaa ko si ipinya nla julọ ninu ọran yii. Ni ipo yii, a nilo lati pada si igbesẹ akọkọ ki a beere: ṣe a nilo gaan lati ṣe iṣiro GCD fun awọn nọmba ti kii ṣe rere? Ti eyi ko ba wulo, lẹhinna o kan nilo lati yi sipesifikesonu naa pada.
Nibi a yẹ ki o ṣe kekere digression nipa ise sise. Nigbagbogbo wọn wọn ni nọmba awọn laini koodu ti a kọ fun ọjọ kan. Ṣugbọn iṣẹ rẹ jẹ iwulo diẹ sii ti o ba yọ nọmba kan ti awọn laini kuro, nitori pe o ni yara diẹ fun awọn idun. Ati ọna ti o rọrun julọ lati yọ koodu naa kuro ni ipele akọkọ. O ṣee ṣe patapata pe o kan ko nilo gbogbo awọn agogo ati awọn whistles ti o n gbiyanju lati ṣe. Ọna ti o yara ju lati jẹ ki eto rọrun ati fi akoko pamọ ni lati ma ṣe awọn nkan ti ko yẹ ki o ṣe. Igbesẹ keji jẹ agbara fifipamọ akoko pupọ julọ. Ti o ba ṣe iwọn iṣelọpọ ni awọn ofin ti awọn laini ti a kọ, lẹhinna ronu nipa bi o ṣe le ṣe iṣẹ-ṣiṣe kan yoo jẹ ki o jẹ kere productive, nitori ti o le yanju awọn kanna isoro pẹlu kere koodu. Emi ko le fun awọn iṣiro deede nibi, nitori Emi ko ni ọna lati ka iye awọn ila ti Emi ko kọ nitori otitọ pe Mo lo akoko lori sipesifikesonu, iyẹn, ni awọn igbesẹ akọkọ ati keji. Ati pe a ko le ṣeto idanwo naa nibi boya, nitori ninu idanwo a ko ni ẹtọ lati pari igbesẹ akọkọ, iṣẹ-ṣiṣe ti pinnu tẹlẹ.
O rọrun lati gbojufo ọpọlọpọ awọn iṣoro ni awọn pato alaye. Ko si ohun ti o ṣoro ni kikọ awọn pato ti o muna fun awọn iṣẹ, Emi kii yoo jiroro eyi. Dipo, a yoo sọrọ nipa kikọ awọn pato ti o lagbara fun awọn ihuwasi boṣewa. Ilana kan wa ti o sọ pe eyikeyi eto awọn ihuwasi le ṣe apejuwe nipa lilo ohun-ini aabo (ailewu) ati survivability-ini (igbesi aye). Aabo tumọ si pe ko si ohun buburu ti yoo ṣẹlẹ, eto naa kii yoo fun idahun ti ko tọ. Iwalaaye tumọ si pe laipẹ tabi ya ohun ti o dara yoo ṣẹlẹ, ie eto naa yoo fun idahun ti o pe laipẹ tabi ya. Gẹgẹbi ofin, aabo jẹ itọkasi pataki diẹ sii, awọn aṣiṣe nigbagbogbo waye nibi. Nitorina, lati fi akoko pamọ, Emi kii yoo sọrọ nipa iwalaaye, biotilejepe o jẹ, dajudaju, tun ṣe pataki.
A ṣe aṣeyọri aabo nipasẹ ṣiṣe ilana, akọkọ, ṣeto ti awọn ipinlẹ ibẹrẹ ti o ṣeeṣe. Ati keji, awọn ibatan pẹlu gbogbo ṣee ṣe tókàn ipinle fun kọọkan ipinle. Jẹ ki a ṣe bi awọn onimọ-jinlẹ ati ṣalaye awọn ipinlẹ ni mathematiki. Eto ti awọn ipinlẹ akọkọ jẹ apejuwe nipasẹ agbekalẹ kan, fun apẹẹrẹ, ninu ọran ti Euclid algorithm: (x = M) ∧ (y = N). Fun awọn iye kan M и N ipo ibẹrẹ kan wa. Ibasepo pẹlu ipinle ti o tẹle ni a ṣe apejuwe nipasẹ agbekalẹ kan ninu eyiti awọn oniyipada ti ipinle ti o tẹle ti wa ni kikọ pẹlu alakoko, ati awọn oniyipada ti ipo ti o wa lọwọlọwọ ni a kọ laisi ipilẹ. Ninu ọran ti Euclid's algorithm, a yoo ṣe pẹlu isọpọ ti awọn agbekalẹ meji, ninu ọkan ninu eyiti x jẹ iye ti o tobi julọ, ati ni keji - y:
Ninu ọran akọkọ, iye tuntun ti y jẹ dogba si iye ti tẹlẹ ti y, ati pe a gba iye tuntun ti x nipa iyokuro oniyipada kekere lati oniyipada nla. Ninu ọran keji, a ṣe idakeji.
Jẹ ki a pada si algorithm Euclid. Jẹ ká ro lẹẹkansi pe M = 12, N = 18. Eyi ṣe asọye ipo ibẹrẹ kan, (x = 12) ∧ (y = 18). Lẹhinna a pulọọgi awọn iye wọnyẹn sinu agbekalẹ loke ati gba:
Eyi ni ojutu ti o ṣeeṣe nikan: x' = 18 - 12 ∧ y' = 12ati pe a gba iwa naa: [x = 12, y = 18]. Bakanna, a le ṣe apejuwe gbogbo awọn ipinlẹ ninu ihuwasi wa: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
Ni kẹhin ipinle [x = 6, y = 6] awọn ẹya mejeeji ti ikosile yoo jẹ eke, nitorina ko ni ipo atẹle. Nitorinaa, a ni sipesifikesonu pipe ti igbesẹ keji - bi o ti le rii, eyi jẹ mathimatiki lasan, bii ninu awọn ẹlẹrọ ati awọn onimọ-jinlẹ, kii ṣe ajeji, bii imọ-ẹrọ kọnputa.
Awọn agbekalẹ meji wọnyi le ṣe idapo sinu agbekalẹ kan ti ọgbọn igba. Arabinrin jẹ yangan ati rọrun lati ṣalaye, ṣugbọn ko si akoko fun u ni bayi. A le nilo ọgbọn igba diẹ fun ohun-ini igbesi aye, ko nilo fun aabo. Emi ko fẹ awọn kannaa igba akoko bi iru, o ni ko oyimbo lasan mathimatiki, sugbon ni irú ti liveliness o jẹ kan pataki ibi.
Ni Euclid's algorithm, fun iye kọọkan x и y ni oto iye x' и y', eyiti o jẹ ki ibatan pẹlu ipinlẹ atẹle jẹ otitọ. Ni awọn ọrọ miiran, algorithm Euclid jẹ ipinnu. Lati ṣe awoṣe algorithm ti kii ṣe ipinnu, ipo lọwọlọwọ nilo lati ni ọpọlọpọ awọn ipinlẹ ọjọ iwaju ti o ṣeeṣe, ati pe iye oniyipada kọọkan ti ko ni ipilẹ ni awọn iye oniyipada alakoko lọpọlọpọ gẹgẹbi ibatan si ipinlẹ atẹle jẹ otitọ. Eyi rọrun lati ṣe, ṣugbọn Emi kii yoo fun apẹẹrẹ ni bayi.
Lati ṣe ohun elo ti n ṣiṣẹ, o nilo mathematiki laiṣe. Bawo ni lati ṣe sipesifikesonu lodo? Lati ṣe eyi, a nilo ede deede, fun apẹẹrẹ, . Sipesifikesonu ti algorithm Euclid yoo dabi eyi ni ede yii:
Aami ami dogba pẹlu onigun mẹta tumọ si pe iye si apa osi ti ami naa jẹ asọye lati dogba si iye si apa ọtun ti ami naa. Ni pataki, sipesifikesonu jẹ asọye, ninu ọran wa awọn asọye meji. Si sipesifikesonu ni TLA+, o nilo lati ṣafikun awọn ikede ati diẹ ninu sintasi, bi ninu ifaworanhan loke. Ni ASCII yoo dabi eyi:
Bi o ti le ri, ko si ohun idiju. Sipesifikesonu fun TLA + le ṣe idanwo, ie fori gbogbo awọn ihuwasi ti o ṣeeṣe ni awoṣe kekere kan. Ninu ọran wa, awoṣe yii yoo jẹ awọn iye kan M и N. Eyi jẹ ọna ṣiṣe ti o munadoko pupọ ati irọrun ti o jẹ adaṣe patapata. O tun ṣee ṣe lati kọ awọn ẹri otitọ deede ati ṣayẹwo wọn ni ọna ẹrọ, ṣugbọn eyi gba akoko pupọ, nitorinaa o fẹrẹ pe ko si ẹnikan ti o ṣe eyi.
Alailanfani akọkọ ti TLA + ni pe o jẹ iṣiro, ati pe awọn pirogirama ati awọn onimọ-jinlẹ kọnputa bẹru ti iṣiro. Ni wiwo akọkọ, eyi dabi awada, ṣugbọn, laanu, Mo tumọ si ni gbogbo pataki. Ẹlẹgbẹ mi kan n sọ fun mi bi o ṣe gbiyanju lati ṣalaye TLA + si ọpọlọpọ awọn idagbasoke. Ni kete ti awọn agbekalẹ han loju iboju, wọn di oju gilasi lẹsẹkẹsẹ. Nitorina ti TLA+ ba dẹruba ọ, o le lo , o jẹ iru ede siseto nkan isere. Ọrọ ikosile ni PlusCal le jẹ eyikeyi ikosile TLA+, iyẹn ni, nipasẹ ati nla, eyikeyi ikosile mathematiki. Ni afikun, PlusCal ni sintasi kan fun awọn algoridimu ti kii ṣe ipinnu. Nitori PlusCal le kọ eyikeyi ọrọ TLA+, PlusCal jẹ ikosile pupọ diẹ sii ju ede siseto gidi eyikeyi. Nigbamii ti, PlusCal ti wa ni akojọpọ sinu irọrun kika TLA+ sipesifikesonu. Eyi ko tumọ si, nitorinaa, pe eka PlusCal sipesifikesonu yoo yipada si ọkan ti o rọrun lori TLA + - ifọrọranṣẹ laarin wọn han gbangba, kii yoo si idiju afikun. Nikẹhin, sipesifikesonu yii le jẹri nipasẹ awọn irinṣẹ TLA +. Ni gbogbo rẹ, PlusCal le ṣe iranlọwọ bori phobia math ati pe o rọrun lati ni oye paapaa fun awọn pirogirama ati awọn onimọ-jinlẹ kọnputa. Ni igba atijọ, Mo ṣe atẹjade awọn algoridimu lori rẹ fun igba diẹ (nipa ọdun 10).
Boya ẹnikan yoo tako pe TLA + ati PlusCal jẹ mathimatiki, ati pe mathimatiki ṣiṣẹ nikan lori awọn apẹẹrẹ ti a ṣẹda. Ni iṣe, o nilo ede gidi kan pẹlu awọn oriṣi, awọn ilana, awọn nkan, ati bẹbẹ lọ. Eyi jẹ aṣiṣe. Eyi ni ohun ti Chris Newcomb, ti o ṣiṣẹ ni Amazon, kowe: “A ti lo TLA + lori awọn iṣẹ akanṣe mẹwa mẹwa, ati ni ọran kọọkan, lilo rẹ ti ṣe iyatọ nla si idagbasoke nitori a ni anfani lati mu awọn idun ti o lewu ṣaaju ki a to kọlu iṣelọpọ, ati nitori pe o fun wa ni oye ati igboya ti a nilo lati ṣe awọn iṣapeye iṣẹ ibinu laisi ni ipa lori otitọ ti eto naa.". Nigbagbogbo o le gbọ pe nigba lilo awọn ọna iṣe, a gba koodu ailagbara - ni iṣe, ohun gbogbo jẹ idakeji. Ni afikun, ero kan wa pe awọn alakoso ko le ni idaniloju iwulo fun awọn ọna ti o ṣe deede, paapaa ti awọn olutọpa ba ni idaniloju iwulo wọn. Ati Newcomb kọ: "Awọn alakoso n titari ni bayi lati kọ awọn pato fun TLA +, ati ni pataki pin akoko fun eyi". Nitorinaa nigbati awọn alakoso rii pe TLA + n ṣiṣẹ, inu wọn dun lati gba. Chris Newcomb kowe eyi ni oṣu mẹfa sẹyin (Oṣu Kẹwa ọdun 2014), ṣugbọn ni bayi, bi mo ti mọ, TLA + ni a lo ninu awọn iṣẹ akanṣe 14, kii ṣe 10. Apeere miiran wa ninu apẹrẹ ti XBox 360. Akọṣẹ kan wa si Charles Thacker ati kowe sipesifikesonu fun eto iranti. Ṣeun si sipesifikesonu yii, a rii kokoro kan ti yoo jẹ bibẹẹkọ ko ṣe akiyesi, ati nitori eyiti gbogbo XBox 360 yoo kọlu lẹhin awọn wakati mẹrin ti lilo. Awọn onimọ-ẹrọ IBM jẹrisi pe awọn idanwo wọn kii yoo ti rii kokoro yii.
O le ka diẹ sii nipa TLA + lori Intanẹẹti, ṣugbọn ni bayi jẹ ki a sọrọ nipa awọn alaye ni pato. A ṣọwọn ni lati kọ awọn eto ti o ṣe iṣiro ipinya ti o kere julọ ati iru bẹ. Pupọ diẹ sii nigbagbogbo a kọ awọn eto bii ohun elo itẹwe lẹwa ti Mo kowe fun TLA +. Lẹhin ilana ti o rọrun julọ, koodu TLA + yoo dabi eyi:
Ṣugbọn ninu apẹẹrẹ ti o wa loke, o ṣeeṣe julọ olumulo fẹ asopọ ati awọn ami dogba lati wa ni ibamu. Nitorinaa ọna kika ti o tọ yoo dabi eyi diẹ sii:
Jẹ ki a gbero apẹẹrẹ miiran:
Nibi, ni ilodi si, titete awọn dọgba, afikun, ati awọn ami isodipupo ni orisun jẹ laileto, nitorinaa ilana ti o rọrun julọ jẹ to. Ni gbogbogbo, ko si asọye mathematiki gangan ti ọna kika to tọ, nitori “ti o tọ” ninu ọran yii tumọ si “ohun ti olumulo fẹ”, ati pe eyi ko le ṣe ipinnu ni mathematiki.
Yoo dabi pe ti a ko ba ni asọye ti otitọ, lẹhinna sipesifikesonu jẹ asan. Ṣugbọn kii ṣe. Nitoripe a ko mọ ohun ti eto kan yẹ ki o ṣe ko tumọ si pe a ko nilo lati ronu nipa bi o ṣe n ṣiṣẹ — ni ilodi si, a ni lati paapaa ni igbiyanju pupọ sii sinu rẹ. Sipesifikesonu jẹ pataki paapaa nibi. Ko ṣee ṣe lati pinnu eto ti o dara julọ fun titẹjade iṣeto, ṣugbọn eyi ko tumọ si pe ko yẹ ki a gba rara, ati koodu kikọ bi ṣiṣan ti aiji kii ṣe ohun ti o dara. Ni ipari, Mo kọ sipesifikesonu ti awọn ofin mẹfa pẹlu awọn asọye ni awọn fọọmu ti comments ninu faili java. Eyi ni apẹẹrẹ ti ọkan ninu awọn ofin: a left-comment token is LeftComment aligned with its covering token. Ofin yii ni a kọ sinu, ṣe a sọ, Gẹẹsi mathematiki: LeftComment aligned, left-comment и covering token - awọn ofin pẹlu awọn asọye. Eyi ni bi awọn oniṣiro ṣe ṣapejuwe mathimatiki: wọn kọ awọn asọye ti awọn ofin ati, da lori wọn, awọn ofin. Anfaani ti iru sipesifikesonu ni pe awọn ofin mẹfa rọrun pupọ lati ni oye ati yokokoro ju awọn laini koodu 850. Mo gbọdọ sọ pe kikọ awọn ofin wọnyi ko rọrun, o gba akoko pupọ pupọ lati ṣatunṣe wọn. Paapa fun idi eyi, Mo kọ koodu kan ti o royin iru ofin ti a lo. Ṣeun si otitọ pe Mo ṣe idanwo awọn ofin mẹfa wọnyi lori awọn apẹẹrẹ pupọ, Emi ko ni lati ṣatunṣe awọn laini koodu 850, ati pe awọn idun wa ni irọrun pupọ lati wa. Java ni awọn irinṣẹ nla fun eyi. Ti MO ba ti kọ koodu naa tẹlẹ, yoo ti gba mi pẹ pupọ, ati pe ọna kika naa yoo jẹ didara ko dara.
Kilode ti a ko le lo sipesifikesonu deede? Ni apa kan, ipaniyan ti o tọ ko ṣe pataki pupọ nibi. Awọn atẹjade igbekalẹ jẹ owun lati ko wu ẹnikẹni, nitorinaa Emi ko ni lati gba lati ṣiṣẹ ni deede ni gbogbo awọn ipo aibikita. Paapaa pataki julọ ni otitọ pe Emi ko ni awọn irinṣẹ to peye. Oluyẹwo awoṣe TLA + ko wulo nibi, nitorinaa Emi yoo ni lati kọ awọn apẹẹrẹ pẹlu ọwọ.
Sipesifikesonu ti o wa loke ni awọn ẹya ti o wọpọ si gbogbo awọn pato. O jẹ ipele ti o ga ju koodu naa lọ. O le ṣe imuse ni eyikeyi ede. Eyikeyi awọn irinṣẹ tabi awọn ọna ko wulo fun kikọ. Ko si eto siseto yoo ran ọ lọwọ lati kọ sipesifikesonu yii. Ati pe ko si awọn irinṣẹ ti o le jẹ ki sipesifikesonu ko ṣe pataki, ayafi ti, nitorinaa, o n kọ ede kan pataki fun kikọ awọn eto atẹjade eleto ni TLA+. Lakotan, sipesifikesonu yii ko sọ ohunkohun nipa gangan bi a ṣe le kọ koodu naa, o sọ ohun ti koodu yii ṣe. A kọ sipesifikesonu lati ṣe iranlọwọ fun wa lati ronu nipasẹ iṣoro naa ṣaaju ki a to bẹrẹ ironu nipa koodu naa.
Ṣugbọn sipesifikesonu yii tun ni awọn ẹya ti o ṣe iyatọ rẹ lati awọn pato miiran. 95% ti awọn alaye lẹkunrẹrẹ miiran jẹ kukuru pupọ ati rọrun:
Siwaju si, yi sipesifikesonu jẹ kan ti ṣeto ti awọn ofin. Bi ofin, eyi jẹ ami ti ko dara sipesifikesonu. Lílóye awọn abajade ti ṣeto awọn ofin jẹ ohun ti o nira, eyiti o jẹ idi ti MO ni lati lo akoko pupọ lati ṣatunṣe wọn. Sibẹsibẹ, ninu ọran yii, Emi ko le wa ọna ti o dara julọ.
O tọ lati sọ awọn ọrọ diẹ nipa awọn eto ti o nṣiṣẹ nigbagbogbo. Gẹgẹbi ofin, wọn ṣiṣẹ ni afiwe, fun apẹẹrẹ, awọn ọna ṣiṣe tabi awọn eto pinpin. Awọn eniyan diẹ ni o le loye wọn ni opolo tabi lori iwe, ati pe emi kii ṣe ọkan ninu wọn, botilẹjẹpe Mo ti le ṣe. Nitorinaa, a nilo awọn irinṣẹ ti yoo ṣayẹwo iṣẹ wa - fun apẹẹrẹ, TLA + tabi PlusCal.
Kini idi ti o ṣe pataki lati kọ sipesifikesonu ti MO ba ti mọ kini gangan koodu yẹ ki o ṣe? Ni otitọ, Mo kan ro pe mo mọ. Ni afikun, pẹlu sipesifikesonu kan, ode ko nilo lati wọle sinu koodu lati loye kini gangan ti o ṣe. Mo ni ofin kan: ko yẹ ki o jẹ awọn ofin gbogbogbo. Iyatọ kan wa si ofin yii, nitorinaa, o jẹ ofin gbogbogbo nikan ti Mo tẹle: sipesifikesonu ti ohun ti koodu ṣe yẹ ki o sọ fun eniyan ohun gbogbo ti wọn nilo lati mọ nigba lilo koodu naa.
Nitorinaa kini gangan awọn olupilẹṣẹ nilo lati mọ nipa ironu? Fun awọn ibẹrẹ, kanna bi gbogbo eniyan miiran: ti o ko ba kọ, lẹhinna o dabi fun ọ nikan pe o nro. Paapaa, o nilo lati ronu ṣaaju koodu, eyiti o tumọ si pe o nilo lati kọ ṣaaju koodu. Sipesifikesonu jẹ ohun ti a kọ ṣaaju ki a to bẹrẹ ifaminsi. A nilo sipesifikesonu fun eyikeyi koodu ti o le ṣee lo tabi yipada nipasẹ ẹnikẹni. Ati pe "ẹnikan" yii le jẹ onkọwe koodu funrararẹ ni oṣu kan lẹhin ti o ti kọ. A nilo sipesifikesonu fun awọn eto nla ati awọn ọna ṣiṣe, fun awọn kilasi, fun awọn ọna, ati nigbakan paapaa fun awọn apakan eka ti ọna kan. Kini pato yẹ ki o kọ nipa koodu naa? O nilo lati ṣe apejuwe ohun ti o ṣe, iyẹn ni, kini o le wulo fun eyikeyi eniyan ti o nlo koodu yii. Nigba miiran o tun le jẹ pataki lati pato bi koodu naa ṣe ṣe aṣeyọri idi rẹ. Ti a ba lọ nipasẹ ọna yii ni ọna ti awọn algoridimu, lẹhinna a pe ni algorithm kan. Ti o ba jẹ nkan pataki diẹ sii ati tuntun, lẹhinna a pe ni apẹrẹ ipele giga. Ko si iyato lodo nibi: mejeeji jẹ awoṣe aljẹẹri ti eto kan.
Bawo ni pato o yẹ ki o kọ sipesifikesonu koodu kan? Ohun akọkọ: o yẹ ki o jẹ ipele kan ti o ga ju koodu naa funrararẹ. O yẹ ki o ṣe apejuwe awọn ipo ati awọn iwa. O yẹ ki o jẹ ti o muna bi iṣẹ-ṣiṣe nbeere. Ti o ba n kọ sipesifikesonu kan fun bii iṣẹ-ṣiṣe kan yoo ṣe imuse, o le kọ sinu pseudocode tabi pẹlu PlusCal. O nilo lati kọ ẹkọ bi o ṣe le kọ awọn pato lori awọn alaye ni pato. Eyi yoo fun ọ ni awọn ọgbọn pataki ti yoo ṣe iranlọwọ fun ọ pẹlu awọn ti kii ṣe alaye bi daradara. Bawo ni o ṣe kọ ẹkọ lati kọ awọn pato pato? Nigba ti a kọ ẹkọ lati ṣe eto, a kọ awọn eto ati lẹhinna ṣe atunṣe wọn. O jẹ kanna nibi: kọ alaye naa, ṣayẹwo pẹlu oluṣayẹwo awoṣe, ati ṣatunṣe awọn idun. TLA+ le ma jẹ ede ti o dara julọ fun sipesifikesonu laiṣe, ati pe o ṣee ṣe ede miiran dara julọ fun awọn iwulo pato rẹ. Anfani ti TLA + ni pe o kọni ironu mathematiki daradara.
Bii o ṣe le sopọ sipesifikesonu ati koodu? Pẹlu iranlọwọ ti awọn asọye ti o so awọn imọran mathematiki ati imuse wọn. Ti o ba ṣiṣẹ pẹlu awọn aworan, lẹhinna ni ipele eto iwọ yoo ni awọn ọna ti awọn apa ati awọn ọna asopọ. Nitorinaa, o nilo lati kọ ni deede bii iwọn ti ṣe imuse nipasẹ awọn ẹya siseto wọnyi.
O yẹ ki o ṣe akiyesi pe ko si ọkan ninu awọn loke ti o kan ilana gangan ti koodu kikọ. Nigbati o ba kọ koodu naa, iyẹn ni, o ṣe igbesẹ kẹta, o tun nilo lati ronu ati ronu nipasẹ eto naa. Ti iṣẹ-ṣiṣe kekere kan ba jade lati jẹ eka tabi kii ṣe kedere, o nilo lati kọ sipesifikesonu kan fun. Ṣugbọn Emi ko sọrọ nipa koodu funrararẹ nibi. O le lo eyikeyi ede siseto, eyikeyi ilana, kii ṣe nipa wọn. Pẹlupẹlu, ko si ọkan ninu awọn loke ti o ṣe imukuro iwulo lati ṣe idanwo ati yokokoro koodu. Paapaa ti o ba jẹ pe awoṣe aljẹbrà ti kọ ni deede, awọn idun le wa ninu imuse rẹ.
Awọn pato kikọ jẹ igbesẹ afikun ninu ilana ifaminsi. O ṣeun si rẹ, ọpọlọpọ awọn aṣiṣe ni a le mu pẹlu igbiyanju diẹ - a mọ eyi lati iriri ti awọn olutọpa lati Amazon. Pẹlu awọn pato, didara awọn eto di ti o ga. Nítorí náà, èé ṣe tí a fi sábà máa ń lọ láìsí wọn? Nitori kikọ jẹ lile. Ati kikọ jẹ nira, nitori fun eyi o nilo lati ronu, ati ero tun nira. O rọrun nigbagbogbo lati dibọn ohun ti o ro. Nibi o le fa afiwe pẹlu ṣiṣiṣẹ - kere si ti o nṣiṣẹ, o lọra ti o nṣiṣẹ. O nilo lati kọ awọn iṣan rẹ ati adaṣe kikọ. Nilo adaṣe.
Sipesifikesonu le jẹ ti ko tọ. O le ti ṣe aṣiṣe ni ibikan, tabi awọn ibeere le ti yipada, tabi ilọsiwaju le nilo lati ṣe. Eyikeyi koodu ti ẹnikẹni nlo ni lati yipada, nitorinaa laipẹ tabi ya sipesifikesonu kii yoo baamu eto naa mọ. Bi o ṣe yẹ, ninu ọran yii, o nilo lati kọ sipesifikesonu tuntun kan ati atunkọ koodu naa patapata. A mọ daradara pe ko si ẹnikan ti o ṣe bẹ. Ni iṣe, a pa koodu naa ati o ṣee ṣe imudojuiwọn sipesifikesonu. Ti eyi ba jẹ dandan lati ṣẹlẹ laipẹ tabi ya, lẹhinna kilode ti kọ awọn pato rara? Ni akọkọ, fun eniyan ti yoo ṣatunkọ koodu rẹ, gbogbo ọrọ afikun ninu sipesifikesonu yoo tọsi iwuwo rẹ ni wura, ati pe eniyan yii le jẹ iwọ funrararẹ. Nigbagbogbo Mo maa n ba ara mi jẹ nitori pe ko gba alaye ti o to nigbati Mo n ṣatunkọ koodu mi. Ati pe Mo kọ awọn alaye diẹ sii ju koodu lọ. Nitorinaa, nigbati o ba ṣatunkọ koodu naa, sipesifikesonu nigbagbogbo nilo lati ni imudojuiwọn. Ni ẹẹkeji, pẹlu atunyẹwo kọọkan, koodu naa buru si, o di pupọ ati siwaju sii nira lati ka ati ṣetọju. Eyi jẹ ilosoke ninu entropy. Ṣugbọn ti o ko ba bẹrẹ pẹlu alaye lẹkunrẹrẹ, lẹhinna gbogbo laini ti o kọ yoo jẹ atunṣe, ati pe koodu naa yoo jẹ ailagbara ati lile lati ka lati ibẹrẹ.
Bi a ti sọ , ko si ogun ti a bori nipa ete, ko si si ogun ti a ṣẹgun laisi ero. Ati pe o mọ ohun kan tabi meji nipa awọn ogun. Nibẹ ni ohun ero ti kikọ ni pato ni a egbin ti akoko. Nigba miiran eyi jẹ otitọ, ati pe iṣẹ naa rọrun pupọ pe ko si nkankan lati ronu nipasẹ rẹ. Ṣugbọn o yẹ ki o ranti nigbagbogbo pe nigbati o ba sọ fun ọ pe ko kọ awọn pato, a sọ fun ọ lati ma ronu. Ati pe o yẹ ki o ronu nipa rẹ ni gbogbo igba. Ni ero nipasẹ iṣẹ-ṣiṣe ko ṣe idaniloju pe iwọ kii yoo ṣe awọn aṣiṣe. Gẹ́gẹ́ bí a ti mọ̀, kò sẹ́ni tí ó ṣẹ̀dá ọ̀pá idan, ati siseto jẹ iṣẹ-ṣiṣe ti o nira. Ṣugbọn ti o ko ba ronu nipasẹ iṣoro naa, o ni idaniloju lati ṣe awọn aṣiṣe.
O le ka diẹ sii nipa TLA + ati PlusCal lori oju opo wẹẹbu pataki kan, o le lọ sibẹ lati oju-iwe ile mi . Iyẹn ni gbogbo fun mi, o ṣeun fun akiyesi rẹ.
Jọwọ ṣe akiyesi pe eyi jẹ itumọ kan. Nigbati o ba kọ awọn asọye, ranti pe onkọwe kii yoo ka wọn. Ti o ba fẹ lati ba onkọwe sọrọ gaan, lẹhinna oun yoo wa ni apejọ Hydra 2019, eyiti yoo waye ni Oṣu Keje 11-12, 2019 ni St. Tiketi le ṣee ra .
orisun: www.habr.com