Hii ni makala ya tafsiri . Lakini kabla ya hapo kuna utangulizi mfupi. Riddick hutengenezwaje? Kila mtu amejikuta katika hali ambayo anataka kuleta rafiki au mwenzake hadi kiwango chake, lakini haifanyi kazi. Zaidi ya hayo, "haifanyiki" sio sana kwako, lakini kwa ajili yake: kwa upande mmoja wa kiwango kuna mshahara wa kawaida, kazi, na kadhalika, na kwa upande mwingine ni haja ya kufikiri. Kufikiria sio kupendeza na kuumiza. Haraka anakata tamaa na kuendelea kuandika msimbo bila kutumia ubongo wake kabisa. Unatambua ni juhudi ngapi inachukua ili kushinda kizuizi cha kutokuwa na uwezo wa kujifunza, na hufanyi hivyo. Hivi ndivyo Riddick hutengenezwa, ambayo inaonekana kuwa inawezekana kutibu, lakini inaonekana kwamba hakuna mtu atafanya hivyo.
Nilipoona hivyo (ndio, rafiki huyo huyo kutoka kwa vitabu vya kiada) na sitoi ripoti, lakini kipindi cha maswali na majibu, nilikuwa na wasiwasi kidogo. Ikiwezekana, Leslie ni mwanasayansi mashuhuri ulimwenguni, mwandishi wa kazi za semina katika kompyuta iliyosambazwa, na unaweza pia kumjua kwa herufi La in LaTeX - "Lamport TeX". Jambo la pili la kutisha ni hitaji lake: kila mtu anayekuja lazima (bila malipo kabisa) asikilize ripoti zake kadhaa mapema, aje na angalau swali moja juu yao, na kisha aje. Niliamua kuona kile ambacho Lamport alikuwa akitangaza hapo - na ni nzuri! Hiki ndicho kitu hasa, kidonge cha kiungo cha uchawi cha kutibu Riddick. Ninakuonya: maandishi yanaweza kuwachoma sana wale wanaopenda mbinu za kisasa na ambao hawapendi kujaribu kile wameandika.
Baada ya habrokat, tafsiri ya semina huanza. Furahia kusoma!
Kazi yoyote unayochukua, kila wakati unahitaji kupitia hatua tatu:
- amua ni lengo gani unataka kufikia;
- amua jinsi utafikia lengo lako;
- kufikia lengo lako.
Hii inatumika pia kwa programu. Tunapoandika nambari, tunahitaji:
- kuamua nini hasa mpango unapaswa kufanya;
- kuamua hasa jinsi inapaswa kufanya kazi yake;
- andika msimbo unaofaa.
Hatua ya mwisho, bila shaka, ni muhimu sana, lakini sitaizungumzia leo. Badala yake, tutajadili mbili za kwanza. Kila programu huzifanya kabla ya kuanza kufanya kazi. Huketi chini kuandika isipokuwa umeamua unachoandika: kivinjari au hifadhidata. Wazo fulani la lengo lazima liwepo. Na hakika unafikiri juu ya nini hasa mpango huo utafanya, na usiandike bila mpangilio kwa matumaini kwamba msimbo yenyewe utageuka kuwa kivinjari.
Je, mawazo haya ya awali ya kanuni hutokea vipi hasa? Je, tunapaswa kuweka juhudi kiasi gani katika hili? Yote inategemea jinsi shida tunayosuluhisha ni ngumu. Wacha tuseme tunataka kuandika mfumo uliosambazwa unaostahimili makosa. Katika hali hii, tunapaswa kufikiria mambo kwa makini kabla ya kukaa chini ya kanuni. Je, ikiwa tunahitaji tu kuongeza kigezo kamili kwa 1? Kwa mtazamo wa kwanza, kila kitu hapa ni kidogo na hakuna mawazo inahitajika, lakini basi tunakumbuka kwamba kufurika kunaweza kutokea. Kwa hivyo, hata ili kuelewa ikiwa shida ni rahisi au ngumu, kwanza unahitaji kufikiria.
Ikiwa unafikiri kwa njia ya ufumbuzi iwezekanavyo kwa tatizo mapema, unaweza kuepuka makosa. Lakini hii inahitaji mawazo yako kuwa wazi. Ili kufikia hili, unahitaji kuandika mawazo yako. Ninapenda nukuu ya Dick Guindon: "Unapoandika, asili hukuonyesha jinsi mawazo yako yalivyo duni." Usipoandika unafikiri tu unawaza. Na unahitaji kuandika mawazo yako kwa namna ya vipimo.
Vipimo hutumikia kazi nyingi, haswa katika miradi mikubwa. Lakini nitazungumza tu juu ya mmoja wao: wanatusaidia kufikiria wazi. Kufikiria kwa uwazi ni muhimu sana na ni ngumu sana, kwa hivyo tunahitaji msaada wowote hapa. Je, tunapaswa kuandika vipimo kwa lugha gani? Kwa ujumla, hili ni swali la kwanza kwa waandaaji wa programu: tutaandika kwa lugha gani? Hakuna jibu moja sahihi: matatizo tunayosuluhisha ni tofauti sana. Kwa watu wengine, TLA+ ni lugha maalum niliyotengeneza. Kwa wengine, ni rahisi zaidi kutumia Kichina. Yote inategemea hali.
Swali muhimu zaidi ni: tunawezaje kufikia mawazo yaliyo wazi zaidi? Jibu: Ni lazima tufikiri kama wanasayansi. Hii ni njia ya kufikiri ambayo imefanya kazi vizuri zaidi ya miaka 500 iliyopita. Katika sayansi tunaunda mifano ya hesabu ya ukweli. Astronomy labda ilikuwa sayansi ya kwanza kwa maana kali ya neno hilo. Katika modeli ya hisabati inayotumiwa katika unajimu, miili ya mbinguni huonekana kama alama zenye misa, msimamo na kasi, ingawa kwa kweli ni vitu ngumu sana na milima na bahari, ebbs na mtiririko. Mfano huu, kama nyingine yoyote, iliundwa kutatua matatizo fulani. Ni vizuri kuamua mahali pa kuelekeza darubini ikiwa unataka kupata sayari. Lakini ikiwa unataka kutabiri hali ya hewa kwenye sayari hii, mtindo huu hautafanya kazi.
Hisabati inaruhusu sisi kuamua sifa za mfano. Na sayansi inaonyesha jinsi mali hizi zinavyohusiana na ukweli. Wacha tuzungumze juu ya sayansi yetu, sayansi ya kompyuta. Ukweli tunaofanya nao kazi ni mifumo ya kompyuta ya aina nyingi tofauti: vichakataji, vidhibiti vya mchezo, kompyuta zinazoendesha programu, na kadhalika. Nitazungumzia juu ya kutekeleza programu kwenye kompyuta, lakini, kwa kiasi kikubwa, hitimisho hizi zote zinatumika kwa mfumo wowote wa kompyuta. Katika sayansi yetu tunatumia miundo mingi tofauti: Mashine ya Turing, seti za matukio zilizopangwa kwa kiasi, na nyingine nyingi.
Mpango ni nini? Hii ni kanuni yoyote ambayo inaweza kuchukuliwa peke yake. Wacha tuseme tunahitaji kuandika kivinjari. Tunafanya kazi tatu: tengeneza uwasilishaji wa mtumiaji wa programu, kisha uandike mchoro wa kiwango cha juu cha programu, na hatimaye uandike msimbo. Tunapoandika msimbo, tunatambua kwamba tunahitaji kuandika fomati ya maandishi. Hapa tena tunahitaji kutatua matatizo matatu: kuamua ni maandishi gani chombo hiki kitarudi; chagua algorithm ya muundo; kuandika kanuni. Jukumu hili lina kazi yake ndogo: kuingiza vistari katika maneno kwa usahihi. Pia tunatatua jukumu hili dogo katika hatua tatu - kama tunavyoona, linarudiwa katika viwango vingi.
Hebu tuchunguze kwa undani hatua ya kwanza: ni tatizo gani ambalo programu hutatua. Hapa mara nyingi tunatoa mfano wa programu kama chaguo la kukokotoa ambalo huchukua pembejeo fulani na kutoa matokeo fulani. Katika hisabati, kipengele cha kukokotoa kwa kawaida hufafanuliwa kama seti ya jozi zilizopangwa. Kwa mfano, kipengele cha kukokotoa cha kukokotoa cha nambari asili kinafafanuliwa kama seti {<0,0>, <1,1>, <2,4>, <3,9>, β¦}. Kikoa cha ufafanuzi wa kazi hiyo ni seti ya vipengele vya kwanza vya kila jozi, yaani, nambari za asili. Ili kufafanua chaguo za kukokotoa, tunahitaji kutaja kikoa chake na fomula.
Lakini kazi katika hisabati si sawa na kazi katika lugha za programu. Hisabati ni rahisi zaidi. Kwa kuwa sina wakati wa mifano changamano, hebu tuzingatie moja rahisi: chaguo za kukokotoa katika C au njia tuli katika Java ambayo inarudisha kigawanyiko kikuu cha kawaida cha nambari mbili kamili. Katika vipimo vya njia hii tutaandika: mahesabu GCD(M,N) kwa hoja M ΠΈ NAmbapo GCD(M,N) - chaguo la kukokotoa ambalo kikoa chake ni seti ya jozi za nambari kamili, na thamani ya kurudi ni nambari kamili zaidi ambayo imegawanywa na M ΠΈ N. Je, ukweli unalinganishwaje na mfano huu? Mfano hufanya kazi na nambari kamili, na katika C au Java tuna 32-bit int. Muundo huu unaturuhusu kuamua ikiwa algorithm ni sahihi GCD, lakini haitazuia makosa ya kufurika. Hii itahitaji mfano ngumu zaidi, ambao hakuna wakati.
Wacha tuzungumze juu ya mapungufu ya kazi kama mfano. Baadhi ya programu (kama vile mifumo ya uendeshaji) hazirudishi tu thamani maalum kwa hoja fulani; zinaweza kufanya kazi mfululizo. Kwa kuongeza, kazi kama mfano haifai kwa hatua ya pili: kupanga jinsi ya kutatua tatizo. Upangaji wa Quicksort na Bubble hukusanya utendaji sawa, lakini ni algoriti tofauti kabisa. Kwa hiyo, kuelezea njia ya kufikia lengo la programu, ninatumia mfano mwingine, hebu tuite mfano wa kawaida wa tabia. Mpango huo unawakilishwa ndani yake kama seti ya tabia zote halali, ambayo kila moja, kwa upande wake, ni mlolongo wa majimbo, na hali ni mgawo wa maadili kwa vigezo.
Wacha tuone hatua ya pili ya algorithm ya Euclidean ingeonekanaje. Tunahitaji kuhesabu GCD(M, N). Tunaanzisha M kama xNa N kama y, kisha toa mara kwa mara ndogo kati ya vigeu hivi kutoka kubwa hadi ziwe sawa. Kwa mfano, ikiwa M = 12Na N = 18, tunaweza kuelezea tabia ifuatayo:
[x = 12, y = 18] β [x = 12, y = 6] β [x = 6, y = 6]
Na kama M = 0 ΠΈ N = 0? Sufuri inaweza kugawanywa kwa nambari zote, kwa hivyo hakuna kigawanyiko kikubwa zaidi katika kesi hii. Katika hali hii, tunahitaji kurejea hatua ya kwanza na kuuliza: ni kweli tunahitaji kuhesabu GCD kwa nambari zisizo chanya? Ikiwa hii sio lazima, basi unahitaji tu kubadilisha vipimo.
Upungufu mfupi wa tija unafaa hapa. Mara nyingi hupimwa kwa idadi ya mistari ya msimbo iliyoandikwa kwa siku. Lakini kazi yako ni muhimu zaidi ikiwa utaondoa idadi fulani ya mistari, kwa sababu una nafasi ndogo ya mende. Na njia rahisi zaidi ya kuondoa nambari iko katika hatua ya kwanza. Inawezekana kwamba hauitaji kengele na filimbi zote unazojaribu kutekeleza. Njia ya haraka sana ya kurahisisha programu na kuokoa muda ni kutofanya mambo ambayo hayafai kufanywa. Hatua ya pili ina uwezo wa pili wa kuokoa muda. Ikiwa unapima tija kwa suala la mistari iliyoandikwa, basi kufikiria jinsi ya kukamilisha kazi itakufanya tija kidogo, kwa sababu unaweza kutatua shida sawa na nambari ndogo. Siwezi kutoa takwimu halisi hapa, kwa sababu sina njia ya kuhesabu idadi ya mistari ambayo sikuandika kutokana na muda niliotumia kwenye vipimo, yaani, kwa hatua ya kwanza na ya pili. Na hatuwezi kufanya jaribio hapa pia, kwa sababu katika jaribio hatuna haki ya kukamilisha hatua ya kwanza; kazi imedhamiriwa mapema.
Ni rahisi kupuuza shida nyingi katika uainishaji usio rasmi. Hakuna chochote kigumu juu ya kuandika maelezo madhubuti ya kazi; Sitajadili hili. Badala yake, tutazungumza juu ya kuandika vipimo vikali vya tabia za kawaida. Kuna nadharia inayosema kwamba seti yoyote ya tabia inaweza kuelezewa kwa kutumia mali ya usalama (usalama) na sifa za kuishi (uhai). Usalama unamaanisha kuwa hakuna kitu kibaya kitatokea, mpango hautatoa jibu lisilofaa. Kunusurika kunamaanisha kuwa mapema au baadaye kitu kizuri kitatokea, i.e. programu mapema au baadaye itatoa jibu sahihi. Kama sheria, usalama ni kiashiria muhimu zaidi; makosa mara nyingi hutokea hapa. Kwa hivyo, ili kuokoa wakati, sitazungumza juu ya kuishi, ingawa, kwa kweli, ni muhimu pia.
Tunapata usalama kwa kubainisha kwanza seti ya hali zinazowezekana za awali. Na pili, uhusiano na majimbo yote yanayofuata kwa kila jimbo. Wacha tuishi kama wanasayansi na tufafanue majimbo kihisabati. Seti ya majimbo ya awali inaelezewa na formula, kwa mfano, katika kesi ya algorithm ya Euclidean: (x = M) β§ (y = N). Kwa maadili fulani M ΠΈ N kuna hali moja tu ya awali. Uhusiano na hali inayofuata inaelezewa na fomula ambayo vigezo vya hali inayofuata vimeandikwa na mkuu, na vigezo vya hali ya sasa vimeandikwa bila mkuu. Kwa upande wa algorithm ya Euclidean, tutakuwa tunashughulikia mgawanyiko wa fomula mbili, katika moja ambayo x ni thamani kubwa zaidi, na katika pili - y:
Katika kesi ya kwanza, thamani mpya ya y ni sawa na thamani ya awali ya y, na tunapata thamani mpya ya x kwa kutoa tofauti ndogo kutoka kwa kubwa zaidi. Katika kesi ya pili, tunafanya kinyume.
Wacha turudi kwenye algorithm ya Euclidean. Tuseme hivyo tena M = 12, N = 18. Hii inafafanua hali moja ya awali, (x = 12) β§ (y = 18). Kisha tunaunganisha maadili haya kwenye fomula hapo juu na kupata:
Hapa ndio suluhisho pekee linalowezekana: x' = 18 - 12 β§ y' = 12, na tunapata tabia: [x = 12, y = 18]. Kwa njia hiyo hiyo, tunaweza kuelezea majimbo yote katika tabia zetu: [x = 12, y = 18] β [x = 12, y = 6] β [x = 6, y = 6].
Katika hali ya mwisho [x = 6, y = 6] sehemu zote mbili za usemi zitakuwa za uwongo, kwa hivyo hazina hali inayofuata. Kwa hivyo, tunayo maelezo kamili ya hatua ya pili - kama tunavyoona, hii ni hesabu ya kawaida, kama ile ya wahandisi na wanasayansi, na sio ya kushangaza, kama katika sayansi ya kompyuta.
Fomula hizi mbili zinaweza kuunganishwa katika fomula moja ya mantiki ya muda. Ni ya kifahari na rahisi kuelezea, lakini hakuna wakati kwa sasa. Tunaweza kuhitaji mantiki ya muda tu kwa mali ya uchangamfu; kwa usalama haihitajiki. Sipendi mantiki ya muda kama hiyo, sio hisabati ya kawaida, lakini kwa hali ya uchangamfu ni uovu wa lazima.
Katika algorithm ya Euclidean kwa kila thamani x ΠΈ y kuna maadili ya kipekee x' ΠΈ y', ambayo hufanya uhusiano na hali inayofuata kuwa kweli. Kwa maneno mengine, algorithm ya Euclidean ni ya kuamua. Ili kuiga algoriti isiyobainishwa, hali ya sasa lazima iwe na hali nyingi zinazowezekana za siku zijazo, na kila thamani ya kigezo kisichobainishwa lazima iwe na thamani nyingi za kigezo kilichowekwa ili uhusiano na hali inayofuata uwe kweli. Hii sio ngumu kufanya, lakini sitatoa mifano sasa.
Ili kutengeneza chombo cha kufanya kazi, unahitaji hisabati rasmi. Jinsi ya kufanya vipimo rasmi? Ili kufanya hivyo tutahitaji lugha rasmi, k.m. . Uainishaji wa algorithm ya Euclidean katika lugha hii itaonekana kama hii:
Ishara ya ishara sawa na pembetatu ina maana kwamba thamani ya kushoto ya ishara imedhamiriwa kuwa sawa na thamani ya kulia ya ishara. Kwa asili, maelezo ni ufafanuzi, kwa upande wetu ufafanuzi mbili. Kwa maelezo katika TLA+ unahitaji kuongeza matamko na syntax, kama ilivyo kwenye slaidi hapo juu. Katika ASCII ingeonekana kama hii:
Kama unaweza kuona, hakuna kitu ngumu. Ufafanuzi kwenye TLA + unaweza kuthibitishwa, yaani, inawezekana kupuuza tabia zote zinazowezekana katika mfano mdogo. Kwa upande wetu, mfano huu utakuwa maadili fulani M ΠΈ N. Hii ni njia nzuri sana na rahisi ya uthibitishaji ambayo ni kiotomatiki kabisa. Kwa kuongeza, inawezekana kuandika uthibitisho rasmi wa ukweli na kuwaangalia kwa mitambo, lakini hii inachukua muda mwingi, hivyo karibu hakuna mtu anayefanya hivi.
Hasara kuu ya TLA + ni kwamba ni hisabati, na waandaaji wa programu na wanasayansi wa kompyuta wanaogopa hisabati. Kwa mtazamo wa kwanza hii inaonekana kama utani, lakini, kwa bahati mbaya, nasema hivi kwa uzito wote. Mwenzangu alikuwa akiniambia tu jinsi alijaribu kuelezea TLA+ kwa watengenezaji kadhaa. Mara tu fomula zilipoonekana kwenye skrini, macho yao mara moja yakawa ya glasi. Kwa hivyo ikiwa TLA+ inatisha, unaweza kutumia , ni aina ya lugha ya programu ya kuchezea. Usemi katika PlusCal unaweza kuwa usemi wowote wa TLA+, yaani, kimsingi usemi wowote wa kihesabu. Zaidi ya hayo, PlusCal ina syntax ya algoriti zisizoamua. Kwa sababu PlusCal inaweza kuandika usemi wowote wa TLA+, inajieleza zaidi kuliko lugha yoyote halisi ya programu. Ifuatayo, PlusCal inakusanywa katika vipimo vya TLA+ ambavyo ni rahisi kusoma. Hii haimaanishi, bila shaka, kwamba vipimo vya PlusCal tata vitageuka kuwa rahisi kwenye TLA + - tu kwamba mawasiliano kati yao ni dhahiri, hakuna utata wa ziada utaonekana. Hatimaye, maelezo haya yanaweza kuthibitishwa kwa kutumia zana za TLA+. Kwa ujumla, PlusCal inaweza kusaidia kushinda phobia ya hisabati; ni rahisi kuelewa hata kwa watengeneza programu na wanasayansi wa kompyuta. Nilichapisha algorithms juu yake kwa muda (karibu miaka 10) hapo awali.
Labda mtu atapinga kwamba TLA+ na PlusCal ni hisabati, na hisabati inafanya kazi tu na mifano iliyoundwa. Katika mazoezi, unahitaji lugha halisi na aina, taratibu, vitu, na kadhalika. Hii si sahihi. Hivi ndivyo Chris Newcomb, ambaye alifanya kazi huko Amazon, anaandika: "Tumetumia TLA+ kwenye miradi kumi kubwa, na kwa kila hali utumiaji wake ulifanya mabadiliko makubwa kwa maendeleo kwa sababu tuliweza kupata mende hatari kabla hawajaanza uzalishaji, na kwa sababu ilitupa ufahamu na ujasiri tuliohitaji kufanya fujo. uboreshaji wa utendaji bila kuathiri ukweli wa programu". Mara nyingi unaweza kusikia kwamba wakati wa kutumia njia rasmi tunapata msimbo usiofaa - kwa mazoezi, kila kitu ni kinyume chake. Kwa kuongezea, kuna maoni kwamba wasimamizi hawawezi kusadikishwa juu ya hitaji la mbinu rasmi, hata kama watayarishaji wa programu wanasadikishwa juu ya manufaa yao. Na Newcomb anaandika: "Wasimamizi sasa wanasukuma kwa kila njia iwezekanayo kuandika maelezo katika TLA+, na wanatenga wakati mahsusi kwa hili". Kwa hivyo wasimamizi wanapoona kuwa TLA+ inafanya kazi, wanaikumbatia. Chris Newcomb aliandika hivi kuhusu miezi sita iliyopita (Oktoba 2014), lakini sasa, nijuavyo, TLA+ inatumika katika miradi 14, sio 10. Mfano mwingine unahusiana na muundo wa XBox 360. Mfanyikazi wa ndani alikuja kwa Charles Thacker na aliandika maelezo ya mfumo wa kumbukumbu. Shukrani kwa vipimo hivi, hitilafu ilipatikana ambayo isingetambuliwa na ingesababisha kila XBox 360 kuanguka baada ya saa nne za matumizi. Wahandisi kutoka IBM walithibitisha kuwa majaribio yao yasingegundua hitilafu hii.
Unaweza kusoma zaidi kuhusu TLA+ kwenye mtandao, lakini sasa hebu tuzungumze kuhusu vipimo visivyo rasmi. Ni mara chache tunapaswa kuandika programu zinazohesabu kigawanyaji cha kawaida zaidi na kadhalika. Mara nyingi zaidi tunaandika programu kama zana nzuri ya kuchapisha niliyoandika kwa TLA+. Baada ya usindikaji rahisi zaidi, nambari ya TLA+ ingeonekana kama hii:
Lakini katika mfano hapo juu, mtumiaji uwezekano mkubwa alitaka muunganisho na ishara sawa zilinganishwe. Kwa hivyo umbizo sahihi lingeonekana zaidi kama hii:
Fikiria mfano mwingine:
Hapa, kinyume chake, upatanishi wa ishara sawa, kuongeza na kuzidisha katika chanzo ilikuwa nasibu, hivyo usindikaji rahisi ni wa kutosha kabisa. Kwa ujumla, hakuna ufafanuzi kamili wa hisabati wa uundaji sahihi, kwa sababu "sahihi" katika kesi hii inamaanisha "kile mtumiaji anataka," na hii haiwezi kuamua hisabati.
Inaweza kuonekana kuwa ikiwa hatuna ufafanuzi wa ukweli, basi maelezo hayana maana. Lakini hiyo si kweli. Kwa sababu tu hatujui ni nini programu inapaswa kufanya haimaanishi kuwa hatuhitaji kufikiria jinsi inavyopaswa kufanya kaziβkinyume chake, tunapaswa kutumia juhudi zaidi kuishughulikia. Uainishaji ni muhimu sana hapa. Haiwezekani kuamua mpango bora wa uchapishaji uliopangwa, lakini hii haimaanishi kwamba hatupaswi kuifanya hata kidogo, na kuandika nambari kama mkondo wa fahamu sio hivyo. Niliishia kuandika maelezo ya sheria sita na ufafanuzi kwa namna ya maoni katika faili ya Java. Hapa kuna mfano wa moja ya sheria: a left-comment token is LeftComment aligned with its covering token. Sheria hii imeandikwa, wacha tuseme, Kiingereza cha hisabati: LeftComment aligned, left-comment ΠΈ covering token - masharti na ufafanuzi. Hivi ndivyo wanahisabati wanavyoelezea hisabati: wanaandika ufafanuzi wa maneno na, kwa kuzingatia wao, huunda sheria. Faida ya vipimo hivi ni kwamba sheria sita ni rahisi zaidi kuelewa na kutatua hitilafu kuliko mistari 850 ya msimbo. Lazima niseme kwamba kuandika sheria hizi haikuwa rahisi; ilichukua muda mwingi sana kuzitatua. Niliandika nambari mahsusi kwa kusudi hili ambalo liliniambia ni sheria gani inatumika. Kwa sababu nilijaribu sheria hizi sita na mifano michache, sikulazimika kurekebisha mistari 850 ya nambari, na mende zilikuwa rahisi kupata. Java ina zana nzuri za hii. Ikiwa ningeandika msimbo tu, ingenichukua muda mrefu zaidi na umbizo lingekuwa la ubora duni.
Kwa nini ubainishaji rasmi haukuweza kutumika? Kwa upande mmoja, utekelezaji sahihi sio muhimu sana hapa. Uchapishaji uliopangwa hautawaridhisha wengine, kwa hivyo sikulazimika kuifanya ifanye kazi kwa usahihi katika hali zote zisizo za kawaida. Hata muhimu zaidi ni ukweli kwamba sikuwa na zana za kutosha. Kikagua mfano wa TLA+ haina maana hapa, kwa hivyo ningelazimika kuandika mifano kwa mkono.
Vipimo vilivyotolewa vina sifa zinazofanana kwa vipimo vyote. Ni kiwango cha juu kuliko kanuni. Inaweza kutekelezwa katika lugha yoyote. Hakuna zana au njia za kuiandika. Hakuna kozi ya programu itakusaidia kuandika maelezo haya. Na hakuna zana zinazoweza kufanya ubainishaji huu usiwe wa lazima, isipokuwa bila shaka unaandika lugha mahususi kwa ajili ya kuandika programu za kuchapisha zilizopangwa katika TLA+. Hatimaye, maelezo haya hayasemi chochote kuhusu jinsi tutakavyoandika msimbo, inasema tu kile kanuni hufanya. Tunaandika vipimo ili kutusaidia kutafakari tatizo kabla ya kuanza kufikiria kuhusu msimbo.
Lakini maelezo haya pia yana sifa zinazoitofautisha na vipimo vingine. 95% ya vipimo vingine ni fupi zaidi na rahisi zaidi:
Zaidi ya hayo, uainishaji huu ni seti ya sheria. Kawaida hii ni ishara ya uainishaji duni. Kuelewa matokeo ya seti ya sheria ni ngumu sana, ndiyo sababu ilinibidi kutumia muda mwingi kuzitatua. Walakini, katika kesi hii sikuweza kupata njia bora.
Inafaa kusema maneno machache kuhusu programu zinazoendelea. Kwa kawaida zinafanya kazi sambamba, kama vile mifumo ya uendeshaji au mifumo iliyosambazwa. Ni watu wachache sana wanaoweza kuyaelewa akilini mwao au kwenye karatasi, na mimi si mmoja wao, ingawa siku moja niliweza kuifanya. Kwa hiyo, tunahitaji zana ambazo zitaangalia kazi yetu - kwa mfano, TLA + au PlusCal.
Kwa nini nilihitaji kuandika maelezo ikiwa tayari nilijua kanuni inapaswa kufanya nini? Kwa kweli, nilifikiri tu nilijua. Kwa kuongezea, ikiwa na vipimo vilivyowekwa, mtu wa nje hahitaji tena kuangalia ndani ya nambari ili kuelewa ni nini hasa inafanya. Nina sheria: haipaswi kuwa na sheria za jumla. Kuna ubaguzi kwa sheria hii kwa kweli, hii ndio sheria pekee ya jumla ninayofuata: maelezo ya kile kanuni hufanya inapaswa kuwaambia watu kila kitu wanachohitaji kujua wakati wa kutumia nambari hiyo.
Kwa hivyo waandaaji wa programu wanahitaji kujua nini juu ya kufikiria? Kuanza, sawa na kwa kila mtu: ikiwa hutaandika, basi inaonekana kwako tu kuwa unafikiri. Pia, unahitaji kufikiria kabla ya kuweka msimbo, ambayo inamaanisha unahitaji kuandika kabla ya kuweka msimbo. Uainishaji ni kile tunachoandika kabla ya kuanza kusimba. Ubainishaji unahitajika kwa msimbo wowote unaoweza kutumiwa au kubadilishwa na mtu yeyote. Na "mtu" huyu anaweza kugeuka kuwa mwandishi wa kanuni mwezi baada ya kuandikwa. Uainishaji unahitajika kwa programu kubwa na mifumo, kwa madarasa, kwa njia, na wakati mwingine hata kwa sehemu ngumu za njia moja. Ni nini hasa unapaswa kuandika kuhusu kanuni? Unahitaji kuelezea kile kinachofanya, yaani, kitu ambacho kinaweza kuwa muhimu kwa mtu yeyote anayetumia nambari hii. Wakati mwingine inaweza pia kuwa muhimu kutaja jinsi kanuni inafikia lengo lake. Ikiwa tulipitia njia hii katika kozi ya algorithms, basi tunaiita algorithm. Ikiwa ni kitu maalum zaidi na kipya, basi tunaiita muundo wa hali ya juu. Hakuna tofauti rasmi hapa: zote mbili ni mifano dhahania ya programu.
Je, unapaswa kuandika vipi msimbo maalum? Jambo kuu: inapaswa kuwa ngazi moja ya juu kuliko kanuni yenyewe. Ni lazima ielezee hali na tabia. Inapaswa kuwa kali kama kazi inavyohitaji. Ikiwa unaandika maelezo ya jinsi ya kutekeleza kazi, basi inaweza kuandikwa kwa pseudocode au kutumia PlusCal. Unahitaji kujifunza kuandika vipimo kwa kutumia vipimo rasmi. Hii itakupa ujuzi muhimu ambao utasaidia pia kwa wale wasio rasmi. Unawezaje kujifunza kuandika vipimo rasmi? Tulipojifunza kupanga, tuliandika programu na kisha kuzitatua. Jambo lile lile hapa: unahitaji kuandika vipimo, angalia na kiangalia mfano, na urekebishe makosa. TLA+ inaweza isiwe lugha bora zaidi kwa ubainifu rasmi, na lugha nyingine inaweza kufaa zaidi kwa mahitaji yako mahususi. Jambo kuu kuhusu TLA+ ni kwamba inafanya kazi nzuri ya kufundisha kufikiri hisabati.
Jinsi ya kuunganisha vipimo na nambari? Kwa kutumia maoni yanayounganisha dhana za hisabati na utekelezaji wake. Ikiwa unafanya kazi na grafu, basi katika ngazi ya programu utakuwa na safu za nodes na safu za viungo. Kwa hivyo unahitaji kuandika jinsi grafu inatekelezwa na miundo hii ya programu.
Ikumbukwe kwamba hakuna yoyote ya hapo juu inatumika kwa mchakato wa kuandika kanuni yenyewe. Unapoandika msimbo, yaani, fanya hatua ya tatu, unahitaji pia kufikiri na kufikiri kupitia programu. Ikiwa kazi ndogo itageuka kuwa ngumu au si dhahiri, unahitaji kuandika maelezo yake. Lakini sizungumzii kanuni yenyewe hapa. Unaweza kutumia lugha yoyote ya programu, mbinu yoyote, hii sio juu yao. Pia, hakuna kati ya zilizo hapo juu inayoondoa hitaji la kujaribu na kurekebisha msimbo wako. Hata kama mfano wa kufikirika umeandikwa kwa usahihi, kunaweza kuwa na mende katika utekelezaji wake.
Uainishaji wa uandishi ni hatua ya ziada katika mchakato wa kuweka msimbo. Shukrani kwa hilo, makosa mengi yanaweza kupatikana kwa bidii kidogo - tunajua hili kutokana na uzoefu wa watengeneza programu kutoka Amazon. Kwa vipimo, ubora wa programu unakuwa wa juu. Kwa hivyo kwa nini basi mara nyingi tunaenda bila wao? Kwa sababu kuandika ni ngumu. Lakini kuandika ni vigumu, kwa sababu kwa hili unahitaji kufikiri, na kufikiri pia ni vigumu. Daima ni rahisi kujifanya unafikiri. Mfano unaweza kuchorwa hapa kwa kukimbia - kadri unavyokimbia kidogo, ndivyo unavyokimbia polepole. Unahitaji kufundisha misuli yako na kufanya mazoezi ya kuandika. Inachukua mazoezi.
Vipimo vinaweza kuwa si sahihi. Huenda umefanya makosa mahali fulani, au mahitaji yamebadilika, au uboreshaji unaweza kuhitajika kufanywa. Nambari yoyote ambayo mtu yeyote hutumia lazima ibadilishwe, kwa hivyo mapema au baadaye maelezo hayatalingana na programu. Kwa hakika, katika kesi hii, unahitaji kuandika vipimo vipya na kuandika upya kabisa msimbo. Tunajua vizuri kwamba hakuna mtu anayefanya hivi. Kwa mazoezi, tunaweka kiraka msimbo na labda kusasisha vipimo. Ikiwa hii italazimika kutokea mapema au baadaye, basi kwa nini uandike maelezo hata kidogo? Kwanza, kwa mtu ambaye atahariri msimbo wako, kila neno la ziada katika vipimo litastahili uzito wake katika dhahabu, na mtu huyu anaweza kuwa wewe. Mara nyingi mimi hujipiga teke kwa kutokuwa mahususi vya kutosha ninapohariri nambari yangu. Na mimi kuandika specifikationer zaidi ya kanuni. Kwa hivyo, unapohariri msimbo, vipimo vinahitaji kusasishwa kila wakati. Pili, kwa kila hariri msimbo unakuwa mbaya zaidi, inakuwa ngumu zaidi kusoma na kudumisha. Hii ni ongezeko la entropy. Lakini usipoanza na vipimo, basi kila mstari utakaoandika utakuwa hariri, na msimbo utakuwa mwingi na mgumu kusoma tangu mwanzo.
Kama ilivyosemwa , hakuna pigano lililoshindikana kulingana na mpango, na hakuna pigano lililoshindwa bila mpango. Na alijua kitu kuhusu vita. Kuna maoni kwamba kuandika vipimo ni kupoteza muda. Wakati mwingine hii ni kweli, na kazi ni rahisi sana kwamba hakuna maana katika kuifikiria. Lakini unapaswa kukumbuka daima kwamba unaposhauriwa usiandike vipimo, ina maana kwamba unashauriwa usifikiri. Na unapaswa kufikiria juu ya hili kila wakati. Kufikiri kwa njia ya kazi hakuhakikishi kwamba hutafanya makosa. Kama tunavyojua, hakuna mtu aliyegundua wand ya uchawi, na programu ni kazi ngumu. Lakini ikiwa hutafikiria kupitia kazi hiyo, umehakikishiwa kufanya makosa.
Unaweza kusoma zaidi kuhusu TLA+ na PlusCal kwenye tovuti maalum, unaweza kwenda huko kutoka kwa ukurasa wangu wa nyumbani . Ni kwa ajili yangu tu, asante kwa umakini wako.
Tafadhali kumbuka kuwa hii ni tafsiri. Unapoandika maoni, kumbuka kwamba mwandishi hatayasoma. Ikiwa ungependa kuzungumza na mwandishi, atakuwa kwenye mkutano wa Hydra 2019, ambao utafanyika Julai 11-12, 2019 huko St. Tikiti zinaweza kununuliwa .
Chanzo: mapenzi.com