Սա թարգմանական հոդված է . Բայց մինչ այդ կա մի կարճ նախաբան. Ինչպե՞ս են ձևավորվում զոմբիները: Բոլորն էլ հայտնվել են մի իրավիճակում, երբ ցանկանում են ընկերոջը կամ գործընկերոջը հասցնել իրենց մակարդակին, բայց դա չի ստացվում: Ընդ որում, «չի ստացվում» ոչ այնքան ձեզ, որքան նրա համար. սանդղակի մի կողմում նորմալ աշխատավարձն է, առաջադրանքները և այլն, իսկ մյուս կողմում՝ մտածելու անհրաժեշտությունը։ Մտածելը տհաճ է և ցավոտ։ Նա արագ հանձնվում է և շարունակում է կոդ գրել՝ ընդհանրապես չօգտագործելով ուղեղը։ Դուք հասկանում եք, թե որքան ջանք է պահանջվում հաղթահարել սովորած անօգնականության արգելքը, և դուք պարզապես չեք անում դա: Ահա թե ինչպես են ձևավորվում զոմբիները, որոնք, թվում է, հնարավոր է բուժել, բայց թվում է, թե ոչ ոք դա չի անի։
Երբ ես տեսա դա (այո, այդ նույն ընկերը դասագրքերից) և ոչ թե հաշվետվություն է տալիս, այլ հարցուպատասխան, ես մի փոքր զգուշացա։ Համենայն դեպս, Լեսլին աշխարհահռչակ գիտնական է, բաշխված հաշվողականության հիմնական աշխատանքների հեղինակ, և դուք կարող եք նրան ճանաչել LaTeX-ի La տառերով՝ «Lamport TeX»: Երկրորդ տագնապալի գործոնը նրա պահանջն է՝ յուրաքանչյուրը, ով գալիս է, պետք է (բոլորովին անվճար) նախօրոք լսի իր զեկույցներից մի երկուսը, գոնե մեկ հարց տա դրանց մասին և նոր միայն գա։ Ես որոշեցի տեսնել, թե ինչ է հեռարձակում Լամպորտը այնտեղ, և դա հիանալի է: Սա հենց այն բանն է, որը կախարդական կապի հաբ է զոմբիների բուժման համար: Ես զգուշացնում եմ ձեզ. տեքստը կարող է լրջորեն այրել նրանց, ովքեր սիրում են գերարագ մեթոդաբանությունները և ովքեր չեն սիրում փորձարկել իրենց գրածը:
Հաբրոկատից հետո փաստորեն սկսվում է սեմինարի թարգմանությունը։ Վայելե՛ք կարդալը:
Ինչ խնդիր էլ որ վերցնեք, միշտ պետք է անցնեք երեք քայլ.
- որոշեք, թե ինչ նպատակ եք ուզում հասնել;
- որոշեք, թե կոնկրետ ինչպես կհասնեք ձեր նպատակին.
- հասնել ձեր նպատակին.
Սա վերաբերում է նաև ծրագրավորմանը։ Կոդ գրելիս մեզ անհրաժեշտ է.
- որոշել, թե կոնկրետ ինչ պետք է անի ծրագիրը.
- հստակ որոշել, թե ինչպես պետք է կատարի իր խնդիրը.
- գրեք համապատասխան կոդը:
Վերջին քայլը, իհարկե, շատ կարևոր է, բայց ես դրա մասին այսօր չեմ խոսի։ Փոխարենը, մենք կքննարկենք առաջին երկուսը: Յուրաքանչյուր ծրագրավորող դրանք կատարում է նախքան աշխատանքը սկսելը: Դուք չեք նստում գրելու, քանի դեռ չեք որոշել, թե ինչ եք գրում՝ բրաուզեր կամ տվյալների բազա: Նպատակի որոշակի պատկերացում պետք է լինի: Եվ դուք հաստատ մտածում եք, թե կոնկրետ ինչ է անելու ծրագիրը, և մի գրեք այն պատահականորեն, հույս ունենալով, որ կոդը ինքնին ինչ-որ կերպ կվերածվի բրաուզերի:
Ինչպե՞ս է տեղի ունենում կոդի մասին նախապես մտածելը: Որքա՞ն ջանք պետք է գործադրենք դրա համար: Ամեն ինչ կախված է նրանից, թե որքան բարդ խնդիր ենք մենք լուծում։ Ենթադրենք, ուզում ենք գրել սխալների հանդուրժող բաշխված համակարգ: Այս դեպքում, նախքան կոդավորմանը նստելը, մենք պետք է լավ մտածենք: Իսկ եթե մեզ պարզապես անհրաժեշտ լինի մեծացնել ամբողջ փոփոխականը 1-ով: Առաջին հայացքից այստեղ ամեն ինչ չնչին է, և մտածելու կարիք չկա, բայց հետո հիշում ենք, որ կարող է տեղի ունենալ հեղեղում։ Հետևաբար, նույնիսկ որպեսզի հասկանաք՝ խնդիրը պարզ է, թե բարդ, նախ պետք է մտածել։
Եթե նախօրոք մտածեք խնդրի հնարավոր լուծումների մասին, կարող եք խուսափել սխալներից: Բայց սա պահանջում է, որ ձեր մտածողությունը հստակ լինի: Դրան հասնելու համար դուք պետք է գրեք ձեր մտքերը: Ես սիրում եմ Դիկ Գինդոնի մեջբերումը. «Երբ գրում ես, բնությունը ցույց է տալիս, թե որքան անփույթ է քո մտածողությունը»: Եթե չես գրում, միայն մտածում ես, որ մտածում ես։ Եվ դուք պետք է գրեք ձեր մտքերը բնութագրերի տեսքով:
Տեխնիկական բնութագրերը կատարում են բազմաթիվ գործառույթներ, հատկապես խոշոր նախագծերում: Բայց ես կխոսեմ միայն դրանցից մեկի մասին. դրանք օգնում են մեզ հստակ մտածել: Հստակ մտածելը շատ կարևոր է և բավականին դժվար, ուստի այստեղ մեզ անհրաժեշտ է ցանկացած օգնություն: Ի՞նչ լեզվով գրենք բնութագրերը: Ընդհանրապես ծրագրավորողների համար սա միշտ առաջին հարցն է՝ ի՞նչ լեզվով ենք գրելու։ Չկա մեկ ճիշտ պատասխան. այն խնդիրները, որոնք մենք լուծում ենք, չափազանց բազմազան են: Որոշ մարդկանց համար TLA+-ը իմ մշակած հստակեցման լեզու է: Մյուսների համար ավելի հարմար է չինարեն օգտագործելը։ Ամեն ինչ կախված է իրավիճակից։
Ավելի կարևոր հարցն այն է, թե ինչպե՞ս կարող ենք հասնել ավելի հստակ մտածողության: Պատասխան. Մենք պետք է մտածենք գիտնականների նման։ Սա մտածելակերպ է, որը լավ է աշխատել վերջին 500 տարիների ընթացքում: Գիտության մեջ մենք կառուցում ենք իրականության մաթեմատիկական մոդելներ։ Աստղագիտությունը թերեւս առաջին գիտությունն էր բառի խիստ իմաստով։ Աստղագիտության մեջ օգտագործվող մաթեմատիկական մոդելում երկնային մարմինները հայտնվում են որպես զանգվածով, դիրքով և իմպուլսով կետեր, թեև իրականում դրանք չափազանց բարդ օբյեկտներ են լեռներով և օվկիանոսներով, մակընթացություններով և հոսքերով: Այս մոդելը, ինչպես ցանկացած այլ, ստեղծվել է որոշակի խնդիրներ լուծելու համար։ Դա հիանալի է որոշելու համար, թե որտեղ պետք է ուղղել աստղադիտակը, եթե ցանկանում եք մոլորակ գտնել: Բայց եթե ցանկանում եք կանխատեսել եղանակը այս մոլորակի վրա, ապա այս մոդելը չի աշխատի։
Մաթեմատիկան թույլ է տալիս որոշել մոդելի հատկությունները։ Իսկ գիտությունը ցույց է տալիս, թե ինչպես են այդ հատկությունները առնչվում իրականությանը: Անդրադառնանք մեր գիտությանը, համակարգչային գիտությանը։ Իրականությունը, որի հետ մենք աշխատում ենք, տարբեր տեսակի հաշվողական համակարգեր են՝ պրոցեսորներ, խաղային կոնսուլներ, ծրագրեր գործարկող համակարգիչներ և այլն: Ես կխոսեմ համակարգչով ծրագիր իրականացնելու մասին, բայց, մեծ հաշվով, այս բոլոր եզրակացությունները վերաբերում են ցանկացած հաշվողական համակարգի։ Մեր գիտության մեջ մենք օգտագործում ենք բազմաթիվ տարբեր մոդելներ՝ Թյուրինգի մեքենա, իրադարձությունների մասնակի պատվիրված հավաքածուներ և շատ ուրիշներ:
Ինչ է ծրագիրը: Սա ցանկացած ծածկագիր է, որը կարելի է ինքնուրույն դիտարկել: Ենթադրենք, մենք պետք է գրենք բրաուզեր: Մենք կատարում ենք երեք առաջադրանք՝ նախագծում ենք ծրագրի օգտատիրոջ ներկայացումը, այնուհետև գրում ենք ծրագրի բարձր մակարդակի դիագրամը և վերջում գրում ենք կոդը։ Երբ մենք գրում ենք կոդը, մենք հասկանում ենք, որ պետք է գրել տեքստի ձևաչափ: Այստեղ մենք կրկին պետք է լուծենք երեք խնդիր. որոշել, թե ինչ տեքստ է վերադարձնելու այս գործիքը; ընտրեք ալգորիթմ ֆորմատավորման համար; գրել կոդը. Այս առաջադրանքն ունի իր ենթաառաջադրանքը՝ բառերի մեջ գծիկները ճիշտ մտցնել: Մենք նաև լուծում ենք այս ենթաառաջադրանքը երեք քայլով. ինչպես տեսնում ենք, դրանք կրկնվում են բազմաթիվ մակարդակներում:
Եկեք մանրամասն նայենք առաջին քայլին՝ ինչ խնդիր է լուծում ծրագիրը: Այստեղ մենք ամենից հաճախ մոդելավորում ենք ծրագիր որպես ֆունկցիա, որը որոշակի մուտք է վերցնում և տալիս որոշակի ելք: Մաթեմատիկայում ֆունկցիան սովորաբար նկարագրվում է որպես զույգերի դասավորված բազմություն։ Օրինակ, բնական թվերի քառակուսի ֆունկցիան նկարագրվում է որպես {<0,0>, <1,1>, <2,4>, <3,9>, …} բազմությունը: Նման ֆունկցիայի սահմանման տիրույթը յուրաքանչյուր զույգի առաջին տարրերի, այսինքն՝ բնական թվերի բազմությունն է։ Ֆունկցիան սահմանելու համար մենք պետք է նշենք դրա տիրույթը և բանաձևը:
Բայց մաթեմատիկայի ֆունկցիաները նույնը չեն, ինչ ֆունկցիաները ծրագրավորման լեզուներում: Մաթեմատիկան շատ ավելի պարզ է. Քանի որ ես ժամանակ չունեմ բարդ օրինակների համար, եկեք դիտարկենք մի պարզ մեկը՝ ֆունկցիա C-ում կամ ստատիկ մեթոդ Java-ում, որը վերադարձնում է երկու ամբողջ թվերի ամենամեծ ընդհանուր բաժանարարը: Այս մեթոդի հստակեցման մեջ մենք կգրենք՝ հաշվարկում GCD(M,N) փաստարկների համար M и NՈրտեղ GCD(M,N) - ֆունկցիա, որի տիրույթը ամբողջ թվերի զույգերի բազմություն է, իսկ վերադարձի արժեքը ամենամեծ ամբողջ թիվն է, որը բաժանվում է M и N. Ինչպե՞ս է իրականությունը համեմատվում այս մոդելի հետ: Մոդելը գործում է ամբողջ թվերով, իսկ C-ում կամ Java-ում մենք ունենք 32-բիթանոց int. Այս մոդելը թույլ է տալիս որոշել, թե արդյոք ալգորիթմը ճիշտ է GCD, բայց դա չի կանխի արտահոսքի սխալները: Սա կպահանջի ավելի բարդ մոդել, որի համար ժամանակ չկա։
Եկեք խոսենք ֆունկցիայի սահմանափակումների մասին՝ որպես մոդել։ Որոշ ծրագրեր (օրինակ՝ օպերացիոն համակարգերը) ոչ միայն որոշակի արգումենտների համար որոշակի արժեք են վերադարձնում, այլ կարող են շարունակաբար աշխատել: Բացի այդ, որպես մոդելի գործառույթը վատ է համապատասխանում երկրորդ քայլին. պլանավորել, թե ինչպես լուծել խնդիրը: Quicksort-ը և bubble sort-ը հաշվարկում են նույն ֆունկցիան, բայց դրանք բոլորովին տարբեր ալգորիթմներ են: Հետևաբար, ծրագրի նպատակին հասնելու ճանապարհը նկարագրելու համար ես օգտագործում եմ մեկ այլ մոդել, եկեք այն անվանենք ստանդարտ վարքային մոդել։ Ծրագիրը դրանում ներկայացված է որպես բոլոր վավեր վարքագծի մի շարք, որոնցից յուրաքանչյուրն իր հերթին վիճակների հաջորդականություն է, իսկ վիճակը փոփոխականներին արժեքների նշանակումն է:
Տեսնենք, թե ինչպիսին կլինի Էվկլիդեսյան ալգորիթմի երկրորդ քայլը: Մենք պետք է հաշվարկենք GCD(M, N). Մենք նախաստորագրում ենք M ինչպես xԻսկ N ինչպես y, ապա մի քանի անգամ հանեք այս փոփոխականներից փոքրը մեծից մինչև դրանք հավասարվեն: Օրինակ, եթե M = 12Իսկ N = 18, մենք կարող ենք նկարագրել հետևյալ վարքագիծը.
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
Եվ եթե M = 0 и N = 0? Զրոն բաժանվում է բոլոր թվերի վրա, ուստի այս դեպքում ամենամեծ բաժանարար չկա: Այս իրավիճակում մենք պետք է վերադառնանք առաջին քայլին և հարցնենք՝ իսկապե՞ս պետք է հաշվարկել GCD-ն ոչ դրական թվերի համար: Եթե դա անհրաժեշտ չէ, ապա դուք պարզապես պետք է փոխեք ճշգրտումը:
Այստեղ անհրաժեշտ է կարճ շեղում արտադրողականության վերաբերյալ: Այն հաճախ չափվում է օրական գրված ծածկագրի տողերի քանակով: Բայց ձեր աշխատանքը շատ ավելի օգտակար է, եթե ձերբազատվեք որոշակի թվով տողերից, քանի որ ավելի քիչ տեղ ունեք վրիպակների համար: Իսկ կոդից ազատվելու ամենադյուրին ճանապարհը առաջին քայլն է։ Հնարավոր է, որ ձեզ պարզապես պետք չեն բոլոր այն զանգերն ու սուլիչները, որոնք փորձում եք իրականացնել: Ծրագիրը պարզեցնելու և ժամանակ խնայելու ամենաարագ ճանապարհն այն է, որ չանել բաներ, որոնք չպետք է արվեն: Երկրորդ քայլն ունի երկրորդ ամենաբարձր ժամանակի ներուժը: Եթե դուք չափում եք արտադրողականությունը գրված տողերով, ապա մտածելը, թե ինչպես կատարել առաջադրանքը, ձեզ կստիպի պակաս արդյունավետ, քանի որ նույն խնդիրը կարող եք լուծել ավելի քիչ կոդով։ Ես ստույգ վիճակագրություն չեմ կարող տալ այստեղ, քանի որ ես ոչ մի կերպ չեմ կարող հաշվել այն տողերի քանակը, որոնք ես չեմ գրել, քանի որ ծախսել եմ ճշգրտման վրա, այսինքն ՝ առաջին և երկրորդ քայլերի վրա: Եվ մենք այստեղ նույնպես փորձարկում չենք կարող անել, քանի որ փորձի ժամանակ մենք իրավունք չունենք կատարել առաջին քայլը, խնդիրը նախապես որոշված է։
Հեշտ է անտեսել բազմաթիվ դժվարություններ ոչ պաշտոնական բնութագրերում: Ֆունկցիաների համար խիստ բնութագրեր գրելու մեջ դժվար բան չկա, ես դա չեմ քննարկի: Փոխարենը, մենք կխոսենք ստանդարտ վարքագծի համար ուժեղ բնութագրեր գրելու մասին: Կա մի թեորեմ, որն ասում է, որ վարքագծի ցանկացած հավաքածու կարելի է նկարագրել՝ օգտագործելով անվտանգության հատկությունը (անվտանգություն) և գոյատևման հատկությունները (կենդանություն). Անվտանգությունը նշանակում է, որ ոչ մի վատ բան չի լինի, ծրագիրը սխալ պատասխան չի տա։ Գոյատևումը նշանակում է, որ վաղ թե ուշ ինչ-որ լավ բան տեղի կունենա, այսինքն՝ ծրագիրը վաղ թե ուշ կտա ճիշտ պատասխանը: Որպես կանոն, անվտանգությունն ավելի կարևոր ցուցանիշ է, այստեղ ամենից հաճախ սխալներ են լինում։ Ուստի ժամանակ խնայելու համար չեմ խոսի գոյատևման մասին, թեև դա, իհարկե, նույնպես կարևոր է։
Մենք հասնում ենք անվտանգության՝ նախ նշելով հնարավոր սկզբնական վիճակների մի շարք: Եվ երկրորդ՝ հարաբերություններ յուրաքանչյուր պետության համար բոլոր հնարավոր հաջորդ պետությունների հետ։ Եկեք մեզ գիտնականների նման պահենք և մաթեմատիկորեն սահմանենք վիճակները։ Սկզբնական վիճակների բազմությունը նկարագրվում է բանաձևով, օրինակ, Էվկլիդեսյան ալգորիթմի դեպքում. (x = M) ∧ (y = N). Որոշակի արժեքների համար M и N կա միայն մեկ նախնական վիճակ. Հաջորդ վիճակի հետ կապը նկարագրվում է բանաձևով, որտեղ հաջորդ վիճակի փոփոխականները գրվում են պարզով, իսկ ընթացիկ վիճակի փոփոխականները՝ առանց պարզի։ Էվկլիդեսյան ալգորիթմի դեպքում գործ կունենանք երկու բանաձևերի անջատման հետ, որոնցից մեկում. x ամենամեծ արժեքն է, իսկ երկրորդում՝ y:
Առաջին դեպքում y-ի նոր արժեքը հավասար է y-ի նախորդ արժեքին, և մենք ստանում ենք x-ի նոր արժեքը՝ հանելով փոքր փոփոխականը մեծից։ Երկրորդ դեպքում մենք անում ենք հակառակը.
Վերադառնանք Էվկլիդեսյան ալգորիթմին։ Ենթադրենք նորից, որ M = 12, N = 18. Սա սահմանում է մեկ նախնական վիճակ, (x = 12) ∧ (y = 18). Այնուհետև մենք միացնում ենք այս արժեքները վերը նշված բանաձևի մեջ և ստանում.
Ահա միակ հնարավոր լուծումը. x' = 18 - 12 ∧ y' = 12, և մենք ստանում ենք վարքագիծը. [x = 12, y = 18]. Նույն կերպ մենք կարող ենք նկարագրել բոլոր վիճակները մեր վարքագծում. [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
Վերջին վիճակում [x = 6, y = 6] Արտահայտության երկու մասերն էլ կեղծ կլինեն, հետևաբար այն չունի հաջորդ վիճակ։ Այսպիսով, մենք ունենք երկրորդ քայլի ամբողջական ճշգրտում. ինչպես տեսնում ենք, սա բավականին սովորական մաթեմատիկա է, ինչպես ինժեներների և գիտնականների, և ոչ տարօրինակ, ինչպես համակարգչային գիտության մեջ:
Այս երկու բանաձևերը կարելի է միավորել ժամանակային տրամաբանության մեկ բանաձևի մեջ: Դա նրբագեղ է և հեշտ բացատրելի, բայց հիմա դրա համար ժամանակ չկա։ Ժամանակային տրամաբանությունը մեզ կարող է անհրաժեշտ լինել միայն աշխուժության հատկության համար, անվտանգության համար դա պետք չէ։ Ժամանակային տրամաբանությունը որպես այդպիսին չեմ սիրում, դա այնքան էլ սովորական մաթեմատիկա չէ, բայց աշխուժության դեպքում դա անհրաժեշտ չարիք է։
Էվկլիդեսյան ալգորիթմում յուրաքանչյուր արժեքի համար x и y կան եզակի արժեքներ x' и y', որոնք իսկական են դարձնում հարաբերությունը հաջորդ վիճակի հետ։ Այլ կերպ ասած, Էվկլիդեսյան ալգորիթմը դետերմինիստական է։ Ոչ դետերմինիստական ալգորիթմը մոդելավորելու համար ներկա վիճակը պետք է ունենա մի քանի հնարավոր ապագա վիճակներ, և unprimed փոփոխականի յուրաքանչյուր արժեք պետք է ունենա նախնական փոփոխականի մի քանի արժեքներ, որպեսզի հարաբերությունը հաջորդ վիճակի հետ լինի ճշմարիտ: Դա դժվար չէ անել, բայց ես հիմա օրինակներ չեմ բերի:
Աշխատանքային գործիք պատրաստելու համար անհրաժեշտ է ֆորմալ մաթեմատիկա։ Ինչպե՞ս ձևակերպել հստակեցումը: Դա անելու համար մեզ անհրաժեշտ կլինի պաշտոնական լեզու, օրինակ. . Էվկլիդեսյան ալգորիթմի ճշգրտումն այս լեզվով կունենա հետևյալ տեսքը.
Եռանկյունով հավասար նշանի նշանը նշանակում է, որ նշանի ձախ կողմում գտնվող արժեքը հավասար է նշանի աջ կողմում գտնվող արժեքին: Ըստ էության, հստակեցումը սահմանում է, մեր դեպքում երկու սահմանում: TLA+-ի հստակեցմանը պետք է ավելացնել հայտարարություններ և որոշ շարահյուսություն, ինչպես վերը նշված սլայդում: ASCII-ում այն կունենա հետևյալ տեսքը.
Ինչպես տեսնում եք, ոչ մի բարդ բան չկա: TLA+-ի ճշգրտումը կարող է ստուգվել, այսինքն՝ հնարավոր է շրջանցել բոլոր հնարավոր վարքագիծը փոքր մոդելում: Մեր դեպքում այս մոդելը կլինի որոշակի արժեքներ M и N. Սա շատ արդյունավետ և պարզ ստուգման մեթոդ է, որը լիովին ավտոմատ է: Բացի այդ, հնարավոր է գրել ճշմարտության պաշտոնական ապացույցներ և ստուգել դրանք մեխանիկորեն, բայց դա շատ ժամանակ է պահանջում, ուստի գրեթե ոչ ոք դա չի անում:
TLA+-ի հիմնական թերությունն այն է, որ այն մաթեմատիկա է, իսկ ծրագրավորողներն ու համակարգչային գիտնականները վախենում են մաթեմատիկայից։ Առաջին հայացքից սա կատակ է թվում, բայց, ցավոք, սա ասում եմ ամենայն լրջությամբ։ Իմ գործընկերներից մեկը պարզապես պատմում էր ինձ, թե ինչպես է փորձել բացատրել TLA+-ը մի քանի մշակողների: Հենց որ բանաձեւերը հայտնվեցին էկրանին, նրանց աչքերն անմիջապես ապակեպատվեցին։ Այսպիսով, եթե TLA+-ը սարսափելի է, կարող եք օգտագործել , մի տեսակ խաղալիք ծրագրավորման լեզու է։ PlusCal-ում արտահայտությունը կարող է լինել ցանկացած TLA+ արտահայտություն, այսինքն՝ հիմնականում ցանկացած մաթեմատիկական արտահայտություն: Բացի այդ, PlusCal-ն ունի շարահյուսություն ոչ դետերմինիստական ալգորիթմների համար: Քանի որ PlusCal-ը կարող է գրել ցանկացած TLA+ արտահայտություն, այն զգալիորեն ավելի արտահայտիչ է, քան ցանկացած իրական ծրագրավորման լեզու: Հաջորդը, PlusCal-ը կազմվում է հեշտ ընթեռնելի TLA+ հստակեցման մեջ: Սա, իհարկե, չի նշանակում, որ բարդ PlusCal սպեցիֆիկացումը TLA+-ում կվերածվի պարզի, պարզապես նրանց միջև համապատասխանությունն ակնհայտ է, լրացուցիչ բարդություն չի առաջանա: Վերջապես, այս ճշգրտումը կարող է ստուգվել TLA+ գործիքների միջոցով: Ընդհանուր առմամբ, PlusCal-ը կարող է օգնել հաղթահարել մաթեմատիկայի ֆոբիան, այն հեշտ է հասկանալ նույնիսկ ծրագրավորողների և համակարգչային գիտնականների համար: Անցյալում որոշ ժամանակ (մոտ 10 տարի) դրա վերաբերյալ ալգորիթմներ էի հրապարակել:
Միգուցե ինչ-որ մեկը առարկի, որ TLA+-ը և PlusCal-ը մաթեմատիկա են, և մաթեմատիկան աշխատում է միայն հորինված օրինակներով: Գործնականում ձեզ անհրաժեշտ է իրական լեզու՝ տեսակներով, ընթացակարգերով, օբյեկտներով և այլն: Սա սխալ է. Ահա թե ինչ է գրում Քրիս Նյուքոմբը, ով աշխատում էր Amazon-ում. «Մենք օգտագործել ենք TLA+-ը տասը խոշոր նախագծերում, և ամեն դեպքում դրա օգտագործումը զգալի փոփոխություն է թողել զարգացման վրա, քանի որ մենք կարողացանք վտանգավոր վրիպակներ որսալ նախքան դրանք արտադրվելը, և որովհետև դա մեզ տվեց պատկերացում և վստահություն, որն անհրաժեշտ էր ագրեսիվ լինելու համար: կատարողականի օպտիմալացում՝ առանց ծրագրի ճշմարտության վրա ազդելու». Հաճախ կարող եք լսել, որ ֆորմալ մեթոդների կիրառման ժամանակ մենք ստանում ենք անարդյունավետ ծածկագիր. գործնականում ամեն ինչ ճիշտ հակառակն է: Բացի այդ, կա ընկալում, որ ղեկավարները չեն կարող համոզվել ֆորմալ մեթոդների անհրաժեշտության մեջ, նույնիսկ եթե ծրագրավորողները համոզված են դրանց օգտակարության մեջ: Իսկ Նյուքոմբը գրում է. «Մենեջերներն այժմ ամեն կերպ փորձում են գրել տեխնիկական բնութագրերը TLA+-ում և հատուկ ժամանակ են հատկացնում դրա համար»:. Այսպիսով, երբ ղեկավարները տեսնում են, որ TLA+-ն աշխատում է, նրանք ընդունում են այն: Քրիս Նյուքոմբը սա գրել է մոտ վեց ամիս առաջ (2014թ. հոկտեմբեր), բայց հիմա, որքան գիտեմ, TLA+-ն օգտագործվում է 14 նախագծերում, ոչ թե 10-ում: Մեկ այլ օրինակ վերաբերում է XBox 360-ի նախագծմանը: Ստաժորը եկավ Չարլզ Թաքերի մոտ և գրել է հիշողության համակարգի հստակեցում: Այս բնութագրի շնորհիվ հայտնաբերվել է սխալ, որը հակառակ դեպքում չէր հայտնաբերվի և կհանգեցներ յուրաքանչյուր XBox 360-ի խափանման չորս ժամ օգտագործելուց հետո: IBM-ի ինժեներները հաստատել են, որ իրենց թեստերը չեն հայտնաբերի այս սխալը:
TLA+-ի մասին ավելին կարող եք կարդալ ինտերնետում, բայց հիմա եկեք խոսենք ոչ պաշտոնական բնութագրերի մասին: Մենք հազվադեպ ենք ստիպված լինում գրել ծրագրեր, որոնք հաշվարկում են նվազագույն ընդհանուր բաժանարարը և այլն: Շատ ավելի հաճախ մենք գրում ենք այնպիսի ծրագրեր, ինչպիսին է գեղեցիկ տպիչ գործիքը, որը ես գրել եմ TLA+-ի համար: Ամենապարզ մշակումից հետո TLA+ կոդը կունենա հետևյալ տեսքը.
Բայց վերը նշված օրինակում օգտագործողը, ամենայն հավանականությամբ, ցանկանում էր, որ կապի և հավասարության նշանները համապատասխանեցվեն: Այսպիսով, ճիշտ ձևաչափումը ավելի շատ նման կլինի հետևյալին.
Դիտարկենք ևս մեկ օրինակ.
Այստեղ, ընդհակառակը, սկզբնաղբյուրում հավասար նշանների, գումարման և բազմապատկման դասավորությունը պատահական էր, ուստի ամենապարզ մշակումը միանգամայն բավարար է։ Ընդհանրապես, ճիշտ ձևաչափման մաթեմատիկական ճշգրիտ սահմանում չկա, քանի որ «ճիշտ» այս դեպքում նշանակում է «այն ինչ ուզում է օգտագործողը», և դա հնարավոր չէ մաթեմատիկորեն որոշել:
Թվում է, թե եթե մենք չունենք ճշմարտության սահմանում, ապա հստակեցումն անօգուտ է։ Բայց դա ճիշտ չէ: Պարզապես այն պատճառով, որ մենք չգիտենք, թե ինչ պետք է անի ծրագիրը, չի նշանակում, որ մենք կարիք չունենք մտածելու, թե ինչպես պետք է այն աշխատի, ընդհակառակը, մենք պետք է ավելի շատ ջանք ծախսենք դրա վրա: Այստեղ հստակեցումը հատկապես կարևոր է: Անհնար է որոշել կառուցվածքային տպագրության օպտիմալ ծրագիրը, բայց դա չի նշանակում, որ մենք ընդհանրապես չպետք է դա ձեռնարկենք, իսկ կոդ գրելը որպես գիտակցության հոսք այդպես չէ։ Ես ավարտեցի վեց կանոնների հստակեցում գրել՝ սահմանումներով մեկնաբանությունների տեսքով Java ֆայլում: Ահա կանոններից մեկի օրինակ. a left-comment token is LeftComment aligned with its covering token. Այս կանոնը գրված է, ասենք, մաթեմատիկական անգլերենով. LeftComment aligned, left-comment и covering token - տերմիններ սահմանումներով: Մաթեմատիկոսներն այսպես են բնութագրում մաթեմատիկան՝ գրում են տերմինների սահմանումներ և դրանց հիման վրա ստեղծում կանոններ։ Այս ճշգրտման առավելությունն այն է, որ վեց կանոնները շատ ավելի հեշտ են հասկանալ և կարգաբերել, քան 850 տող կոդ: Պետք է ասեմ, որ այս կանոնները գրելը հեշտ չէր, բավական երկար ժամանակ պահանջվեց դրանք կարգաբերելու համար: Ես հատուկ այդ նպատակով գրեցի կոդ, որն ինձ ասում էր, թե որ կանոնն է օգտագործվում: Քանի որ ես փորձարկեցի այս վեց կանոնները մի քանի օրինակներով, ես ստիպված չէի վրիպազերծել 850 տող կոդ, և սխալները բավականին հեշտ էր գտնել: Java-ն դրա համար հիանալի գործիքներ ունի: Եթե ես հենց նոր գրեի կոդը, ինձանից շատ ավելի երկար կխներ, և ֆորմատավորումն ավելի անորակ կլիներ։
Ինչու՞ չի կարող օգտագործվել պաշտոնական հստակեցում: Մի կողմից, ճիշտ կատարումն այստեղ այնքան էլ կարևոր չէ։ Կառուցվածքային տպագրությունը, անշուշտ, ոմանց համար չի բավարարում, ուստի ես ստիպված չէի այն ճիշտ աշխատել բոլոր անսովոր իրավիճակներում: Առավել կարևոր է այն փաստը, որ ես չունեի համապատասխան գործիքներ։ TLA+ մոդելի ստուգիչն այստեղ անօգուտ է, ուստի ես ստիպված կլինեի օրինակները գրել ձեռքով:
Տվյալ ճշգրտումն ունի բոլոր բնութագրերի համար ընդհանուր հատկանիշներ: Դա ավելի բարձր մակարդակ է, քան կոդը: Այն կարող է իրականացվել ցանկացած լեզվով: Այն գրելու գործիքներ կամ մեթոդներ չկան: Ծրագրավորման ոչ մի դասընթաց չի օգնի ձեզ գրել այս առանձնահատկությունը: Եվ չկան գործիքներ, որոնք կարող են անհարկի դարձնել այս ճշգրտումը, եթե իհարկե դուք լեզու չեք գրում հատուկ TLA+-ում կառուցվածքային տպագրության ծրագրեր գրելու համար: Ի վերջո, այս հստակեցումը ոչինչ չի ասում այն մասին, թե կոնկրետ ինչպես ենք մենք գրելու կոդը, այն պարզապես նշում է, թե ինչ է անում կոդը: Մենք գրում ենք հստակեցում, որը կօգնի մեզ մտածել խնդրի շուրջ՝ նախքան կոդի մասին մտածելը:
Բայց այս հատկանիշն ունի նաև առանձնահատկություններ, որոնք այն տարբերում են այլ բնութագրերից: Այլ բնութագրերի 95%-ը շատ ավելի կարճ և պարզ է.
Ավելին, այս հստակեցումը կանոնների մի շարք է: Սա սովորաբար վատ ճշգրտման նշան է: Մի շարք կանոնների հետևանքները հասկանալը բավականին դժվար է, այդ իսկ պատճառով ես ստիպված էի շատ ժամանակ ծախսել դրանց վրիպազերծման համար: Այնուամենայնիվ, այս դեպքում ես չկարողացա ավելի լավ ճանապարհ գտնել:
Արժե մի քանի խոսք ասել անընդհատ աշխատող ծրագրերի մասին։ Սովորաբար նրանք աշխատում են զուգահեռաբար, ինչպիսիք են օպերացիոն համակարգերը կամ բաշխված համակարգերը: Շատ քչերը կարող են դրանք հասկանալ իրենց մտքում կամ թղթի վրա, իսկ ես նրանցից չեմ, թեև ժամանակին կարողացել եմ դա անել։ Հետևաբար, մեզ անհրաժեշտ են գործիքներ, որոնք կստուգեն մեր աշխատանքը, օրինակ՝ TLA+ կամ PlusCal:
Ինչու՞ պետք է հստակեցում գրեի, եթե արդեն գիտեի, թե ինչ պետք է անի կոդը: Իրականում ես միայն կարծում էի, որ դա գիտեմ: Ի հավելումն, հստակեցման առկայության դեպքում, օտարերկրացին այլևս կարիք չունի փնտրելու ծածկագիրը՝ հասկանալու համար, թե կոնկրետ ինչ է այն անում: Ես մի կանոն ունեմ՝ ընդհանուր կանոններ չպետք է լինեն։ Այս կանոնից, իհարկե, կա բացառություն, սա միակ ընդհանուր կանոնն է, որը ես հետևում եմ. այն հստակեցումը, թե ինչ է անում կոդը, պետք է մարդկանց ասի այն ամենը, ինչ նրանք պետք է իմանան այդ կոդը օգտագործելիս:
Այսպիսով, ի՞նչ կոնկրետ պետք է իմանան ծրագրավորողները մտածողության մասին: Սկզբից, նույնը, ինչ բոլորի համար. եթե չես գրում, ուրեմն քեզ միայն թվում է, թե մտածում ես։ Բացի այդ, դուք պետք է մտածեք նախքան կոդավորումը, ինչը նշանակում է, որ դուք պետք է գրեք նախքան կոդավորումը: Հստակեցումն այն է, ինչ մենք գրում ենք նախքան կոդավորումը սկսելը: Հստակեցում է անհրաժեշտ ցանկացած կոդի համար, որը կարող է օգտագործվել կամ փոփոխվել որևէ մեկի կողմից: Եվ այս «ինչ-որ մեկը» կարող է կոդի հեղինակը գրվելուց մեկ ամիս անց պարզվի։ Հստակեցում է անհրաժեշտ խոշոր ծրագրերի և համակարգերի, դասերի, մեթոդների և երբեմն նույնիսկ մեկ մեթոդի բարդ հատվածների համար: Կոնկրետ ի՞նչ պետք է գրել կոդի մասին։ Դուք պետք է նկարագրեք, թե ինչ է դա անում, այսինքն՝ մի բան, որը կարող է օգտակար լինել այս կոդը օգտագործող յուրաքանչյուրի համար: Երբեմն կարող է անհրաժեշտ լինել նաև նշել, թե կոնկրետ ինչպես է կոդը հասնում իր նպատակին: Եթե մենք անցել ենք այս մեթոդը ալգորիթմների դասընթացում, ապա այն անվանում ենք ալգորիթմ։ Եթե դա ավելի մասնագիտացված և նոր բան է, ապա մենք այն անվանում ենք բարձր մակարդակի դիզայն։ Այստեղ ֆորմալ տարբերություն չկա. երկուսն էլ ծրագրի վերացական մոդելներ են։
Ինչպե՞ս ճիշտ գրել կոդի հստակեցում: Հիմնական բանը. այն պետք է լինի մեկ մակարդակ բարձր, քան ինքնին կոդը: Այն պետք է նկարագրի վիճակներ և վարքագիծ: Այն պետք է լինի այնքան խիստ, որքան խնդիրը պահանջում է: Եթե դուք հստակեցում եք գրում, թե ինչպես իրականացնել առաջադրանքը, ապա այն կարող է գրվել կեղծ կոդով կամ օգտագործելով PlusCal: Դուք պետք է սովորեք գրել բնութագրեր՝ օգտագործելով պաշտոնական բնութագրերը: Սա ձեզ կտրամադրի անհրաժեշտ հմտություններ, որոնք կօգնեն նաև ոչ պաշտոնականներին: Ինչպե՞ս կարող եք սովորել գրել պաշտոնական բնութագրեր: Երբ մենք սովորեցինք ծրագրավորել, մենք գրում էինք ծրագրեր և ապա վրիպազերծում դրանք: Նույնը այստեղ. պետք է գրել հստակեցում, ստուգել այն մոդելի ստուգիչով և ուղղել սխալները: TLA+-ը չի կարող լավագույն լեզուն լինել պաշտոնական ճշգրտման համար, և մեկ այլ լեզու, հավանաբար, ավելի հարմար կլինի ձեր հատուկ կարիքների համար: TLA+-ի հիանալի բանն այն է, որ այն հիանալի աշխատանք է կատարում մաթեմատիկական մտածողության ուսուցման գործում:
Ինչպե՞ս կապել բնութագրերը և կոդը: Օգտագործելով մեկնաբանություններ, որոնք կապում են մաթեմատիկական հասկացությունները և դրանց իրականացումը: Եթե դուք աշխատում եք գրաֆիկների հետ, ապա ծրագրի մակարդակում դուք կունենաք հանգույցների զանգվածներ և հղումների զանգվածներ։ Այսպիսով, դուք պետք է գրեք, թե կոնկրետ ինչպես է գրաֆիկը իրականացվում այս ծրագրավորման կառույցների կողմից:
Հարկ է նշել, որ վերը նշվածներից ոչ մեկը չի վերաբերում բուն կոդ գրելու գործընթացին: Երբ դուք գրում եք կոդ, այսինքն կատարում եք երրորդ քայլը, դուք նույնպես պետք է մտածեք և մտածեք ծրագրի միջոցով: Եթե պարզվում է, որ ենթաառաջադրանքը բարդ է կամ ակնհայտ չէ, ապա դրա համար պետք է հստակեցում գրել: Բայց ես այստեղ չեմ խոսում հենց կոդի մասին: Դուք կարող եք օգտագործել ցանկացած ծրագրավորման լեզու, ցանկացած մեթոդաբանություն, խոսքը նրանց մասին չէ։ Բացի այդ, վերը նշվածներից ոչ մեկը չի վերացնում ձեր կոդը փորձարկելու և վրիպազերծելու անհրաժեշտությունը: Նույնիսկ եթե վերացական մոդելը գրված է ճիշտ, դրա իրականացման մեջ կարող են լինել սխալներ։
Տեխնիկական պայմանները գրելը լրացուցիչ քայլ է կոդավորման գործընթացում: Դրա շնորհիվ շատ սխալներ կարելի է հայտնաբերել ավելի քիչ ջանքերով. մենք դա գիտենք Amazon-ի ծրագրավորողների փորձից: Տեխնիկական պայմանների դեպքում ծրագրերի որակն ավելի բարձր է դառնում։ Ուրեմն ինչու՞ ենք մենք այդքան հաճախ գնում առանց նրանց: Որովհետև գրելը դժվար է: Բայց գրելը դժվար է, քանի որ դրա համար պետք է մտածել, և մտածելն էլ է դժվար։ Միշտ ավելի հեշտ է ձևացնել, որ մտածում ես: Այստեղ դուք կարող եք անալոգիա անել վազքի հետ՝ որքան քիչ եք վազում, այնքան դանդաղ եք վազում: Դուք պետք է մարզեք ձեր մկանները և գրեք: Դա պրակտիկա է պահանջում:
Հստակեցումը կարող է սխալ լինել: Հնարավոր է, որ ինչ-որ տեղ սխալվել եք, կամ պահանջները կարող են փոխվել, կամ բարելավման կարիք լինի: Ցանկացած կոդ, որն օգտագործում է որևէ մեկը, պետք է փոխվի, ուստի վաղ թե ուշ ճշգրտումն այլևս չի համապատասխանի ծրագրին: Իդեալում, այս դեպքում, դուք պետք է գրեք նոր ճշգրտում և ամբողջությամբ վերագրեք կոդը: Մենք շատ լավ գիտենք, որ ոչ ոք դա չի անում։ Գործնականում մենք կարկատում ենք կոդը և, հավանաբար, թարմացնում ենք ճշգրտումը: Եթե դա անպայման տեղի կունենա վաղ թե ուշ, ապա ինչու՞ ընդհանրապես գրել բնութագրեր: Նախ, այն անձի համար, ով կխմբագրի ձեր կոդը, ճշգրտման յուրաքանչյուր ավելորդ բառը կարժենա իր կշիռը ոսկով, և այս մարդը կարող է լինել դուք: Ես հաճախ ոտքով եմ անում ինքս ինձ, քանի որ իմ կոդը խմբագրելիս բավականաչափ կոնկրետ չեմ: Եվ ես ավելի շատ բնութագրեր եմ գրում, քան կոդ: Հետևաբար, երբ դուք խմբագրում եք կոդը, ճշգրտումը միշտ պետք է թարմացվի: Երկրորդ, յուրաքանչյուր խմբագրման դեպքում կոդը վատանում է, դժվարանում է կարդալն ու պահպանելը։ Սա էնտրոպիայի աճ է: Բայց եթե դուք չեք սկսում հստակեցումով, ապա ձեր գրած յուրաքանչյուր տող կլինի խմբագրում, և կոդը կլինի ծավալուն և դժվար կարդացվող սկզբից:
Ինչպես ասվեց , ոչ մի ճակատամարտ չի հաղթվել ըստ ծրագրի, և ոչ մի ճակատամարտ չի հաղթել առանց ծրագրի. Եվ նա ինչ-որ բան գիտեր մարտերի մասին: Կարծիք կա, որ բնութագրերը գրելը ժամանակի վատնում է։ Երբեմն դա ճիշտ է, և խնդիրն այնքան պարզ է, որ իմաստ չունի մտածել դրա մասին: Բայց դուք միշտ պետք է հիշեք, որ երբ ձեզ խորհուրդ են տալիս չգրել տեխնիկական բնութագրեր, դա նշանակում է, որ ձեզ խորհուրդ են տալիս չմտածել։ Եվ դուք պետք է ամեն անգամ մտածեք այս մասին: Առաջադրանքի շուրջ մտածելը չի երաշխավորում, որ սխալներ չեք գործի: Ինչպես գիտենք, ոչ ոք կախարդական փայտիկ չի հորինել, իսկ ծրագրավորումը բարդ խնդիր է։ Բայց եթե չմտածեք առաջադրանքի շուրջ, ապա երաշխավորված եք սխալներ թույլ տալու համար:
Դուք կարող եք ավելին կարդալ TLA+-ի և PlusCal-ի մասին հատուկ կայքում, կարող եք գնալ այնտեղ իմ գլխավոր էջից . Դա ինձ համար է, շնորհակալություն ուշադրության համար:
Հիշեք, որ սա թարգմանություն է։ Մեկնաբանություններ գրելիս հիշեք, որ հեղինակը չի կարդա դրանք։ Եթե իսկապես ցանկանում եք զրուցել հեղինակի հետ, նա կլինի Hydra 2019 կոնֆերանսին, որը կանցկացվի 11 թվականի հուլիսի 12-2019-ը Սանկտ Պետերբուրգում։ Տոմսերը կարելի է ձեռք բերել .
Source: www.habr.com