Бұл аударма мақаласы . Бірақ оның алдында қысқаша кіріспе бар. Зомбилер қалай пайда болады? Әр адам досын немесе әріптесін өз деңгейіне жеткізгісі келетін жағдайға тап болды, бірақ бұл нәтиже бермейді. Оның үстіне, сіз үшін емес, ол үшін «жұмыс істемейді»: таразының бір жағында қалыпты жалақы, міндеттер және т.б. бар, ал екінші жағында ойлау қажеттілігі бар. Ойлау жағымсыз және азапты. Ол тез бас тартады және миын мүлдем пайдаланбай код жазуды жалғастырады. Сіз үйренген дәрменсіздік кедергісін жеңу үшін қанша күш жұмсау керектігін түсінесіз, бірақ сіз мұны істемейсіз. Міне, зомбилер осылай қалыптасады, оларды емдеуге болатын сияқты, бірақ мұны ешкім жасамайтын сияқты.
Мен мұны көргенде (иә, оқулықтардағы сол дос) және баяндама емес, сұрақ-жауап түрінде өтіп жатыр, мен сәл сақ болдым. Қалай болғанда да, Лесли - әлемге әйгілі ғалым, бөлінген есептеулер бойынша маңызды жұмыстардың авторы және сіз оны LaTeX - «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, бірақ ол толып кету қателеріне жол бермейді. Бұл күрделірек модельді қажет етеді, оған уақыт жоқ.
Модель ретінде функцияның шектеулері туралы сөйлесейік. Кейбір бағдарламалар (мысалы, операциялық жүйелер) белгілі бір аргументтер үшін белгілі бір мәнді қайтармайды, олар үздіксіз жұмыс істей алады. Сонымен қатар, модель ретінде функция екінші қадамға нашар сәйкес келеді: мәселені шешу жолын жоспарлау. Жылдам сұрыптау және көпіршікті сұрыптау бірдей функцияны есептейді, бірақ олар мүлдем басқа алгоритмдер. Сондықтан бағдарламаның мақсатына жету жолын сипаттау үшін мен басқа модельді қолданамын, оны стандартты мінез-құлық моделі деп атаймыз. Бағдарлама онда барлық жарамды мінез-құлықтардың жиынтығы ретінде ұсынылған, олардың әрқайсысы өз кезегінде күйлер тізбегі, ал күй айнымалыларға мәндерді тағайындау болып табылады.
Евклид алгоритмінің екінші қадамы қандай болатынын көрейік. Біз есептеуіміз керек 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:
Бірінші жағдайда у-ның жаңа мәні у-ның алдыңғы мәніне тең және үлкенінен кіші айнымалыны алып тастау арқылы х-тің жаңа мәнін аламыз. Екінші жағдайда біз керісінше жасаймыз.
Евклид алгоритміне оралайық. Тағы да солай делік 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', бұл келесі күймен қатынасты ақиқат етеді. Басқаша айтқанда, Евклид алгоритмі детерминирленген. Детерминирленбеген алгоритмді модельдеу үшін ағымдағы күйде бірнеше ықтимал болашақ күйлер болуы керек, ал бастапқы күйге келтірілмеген айнымалының әрбір мәнінде келесі күйге қатынас ақиқат болатындай бастапқы айнымалының бірнеше мәндері болуы керек. Мұны істеу қиын емес, бірақ мен қазір мысалдар келтірмеймін.
Жұмыс құралын жасау үшін сізге ресми математика қажет. Техникалық сипаттаманы қалай ресми түрде жасауға болады? Мұны істеу үшін бізге ресми тіл қажет, мысалы. . Бұл тілдегі Евклид алгоритмінің спецификациясы келесідей болады:
Үшбұрышты теңдік белгісінің таңбасы таңбаның сол жағындағы мән белгінің оң жағындағы мәнге тең болатынын білдіреді. Негізінде спецификация - бұл анықтама, біздің жағдайда екі анықтама. 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 туралы қосымша ақпаратты арнайы веб-сайттан оқи аласыз, ол жерге менің басты бетімнен кіре аласыз . Мұның бәрі мен үшін, назарларыңызға рахмет.
Бұл аударма екенін есте сақтаңыз. Пікір жазғанда автор оларды оқымайтынын есте сақтаңыз. Егер сіз шынымен автормен сөйлескіңіз келсе, ол 2019 жылдың 11-12 шілдесінде Санкт-Петербургте өтетін Hydra 2019 конференциясында болады. Билеттерді сатып алуға болады .
Ақпарат көзі: www.habr.com