Ushbu maqola tarjimadir . Ammo uning oldida bir oz tanishish. Zombi qanday hosil bo'ladi? Har bir inson do'st yoki hamkasbini o'z darajasiga ko'tarmoqchi bo'lgan vaziyatga tushib qoldi, ammo bu ishlamayapti. Va siz bilan emas, balki u bilan "ishlamaydi": o'lchovning bir tomonida oddiy ish haqi, vazifalar va boshqalar, ikkinchisida esa o'ylash kerak. Fikrlash yoqimsiz va og'riqli. U tezda taslim bo'ladi va miyasini umuman yoqmasdan kod yozishni davom ettiradi. O'rganilgan nochorlik to'sig'ini yengib o'tish uchun qancha kuch sarflanishini tasavvur qilasiz va buni qilmaysiz. Zombilar shunday shakllanadi, ularni davolash mumkin, ammo hech kim buni qilmaydi.
Men buni ko'rganimda (ha, darslikdagi o'sha o'rtoq) va ma'ruza qilmaydi, lekin savol-javob sessiyasi, men biroz ehtiyotkor edim. Har holda, Lesli dunyoga mashhur olim, taqsimlangan hisoblash bo'yicha fundamental asarlar muallifi va siz uni LaTeX - "Lamport TeX" so'zidagi La harflari orqali ham bilishingiz mumkin. Ikkinchi tashvishli omil - uning talabi: kelgan har bir kishi (mutlaqo bepul) uning bir nechta hisobotlarini oldindan tinglashi, kamida bitta savol bilan chiqishi va shundan keyingina kelishi kerak. Men u erda Lamport nima eshittirishini ko'rishga qaror qildim - va bu ajoyib! Aynan o'sha narsa, zombilarni davolash uchun sehrli havola. Men sizni ogohlantiraman: matndan o'ta moslashuvchan metodologiyani sevuvchilar va yozilgan narsalarni sinab ko'rishni yoqtirmaydiganlar sezilarli darajada yonib ketishi mumkin.
Habrokatdan so'ng, aslida, seminarning tarjimasi boshlanadi. O'qishdan zavqlaning!
Qaysi vazifani bajarishingizdan qat'i nazar, siz doimo uchta bosqichdan o'tishingiz kerak:
- qanday maqsadga erishmoqchi ekanligingizni hal qiling;
- maqsadingizga qanday erishishingizni hal qiling;
- maqsadingizga keling.
Bu dasturlash uchun ham amal qiladi. Kodni yozishda biz quyidagilarni bajarishimiz kerak:
- dastur nima qilishi kerakligini hal qilish;
- o'z vazifasini qanday bajarishi kerakligini aniqlash;
- tegishli kodni yozing.
Oxirgi qadam, albatta, juda muhim, lekin bugun men bu haqda gapirmayman. Buning o'rniga biz birinchi ikkitasini muhokama qilamiz. Har bir dasturchi ularni ishga kirishishdan oldin bajaradi. Brauzer yoki ma'lumotlar bazasini yozishni hal qilmaguningizcha, yozish uchun o'tirmaysiz. Maqsad haqida ma'lum bir fikr mavjud bo'lishi kerak. Va siz aniq dastur nima qilishi haqida o'ylaysiz va kod qandaydir tarzda brauzerga aylanadi degan umidda yozmang.
Ushbu kodni oldindan o'ylash qanday sodir bo'ladi? Bunga qancha kuch sarflashimiz kerak? Bularning barchasi biz hal qilayotgan muammoning qanchalik murakkabligiga bog'liq. Aytaylik, biz nosozliklarga chidamli taqsimlangan tizimni yozmoqchimiz. Bunday holda, kodlash uchun o'tirishdan oldin hamma narsani yaxshilab o'ylab ko'rishimiz kerak. Agar butun o'zgaruvchini 1 ga oshirishimiz kerak bo'lsa-chi? Bir qarashda, bu erda hamma narsa ahamiyatsiz va hech qanday o'ylash kerak emas, lekin keyin biz toshib ketishi mumkinligini eslaymiz. Shuning uchun, muammo oddiy yoki murakkab ekanligini tushunish uchun ham, avvalo, o'ylab ko'rishingiz kerak.
Muammoning mumkin bo'lgan echimlari haqida oldindan o'ylab ko'rsangiz, xatolardan qochishingiz mumkin. Ammo bu sizning fikringiz aniq bo'lishini talab qiladi. Bunga erishish uchun siz o'z fikrlaringizni yozishingiz kerak. Menga Dik Gindonning iqtiboslari juda yoqadi: "Yozganingizda, tabiat sizning fikringiz qanchalik beparvo ekanligini ko'rsatadi." Agar siz yozmasangiz, faqat o'ylayotganingizni o'ylaysiz. Va o'z fikrlaringizni spetsifikatsiyalar shaklida yozishingiz kerak.
Texnik xususiyatlar, ayniqsa, yirik loyihalarda ko'p funktsiyalarni bajaradi. Ammo men ulardan faqat bittasi haqida gapiraman: ular bizga aniq fikrlashga yordam beradi. Aniq fikrlash juda muhim va juda qiyin, shuning uchun bu erda bizga har qanday yordam kerak. Texnik tavsiflarni qaysi tilda yozishimiz kerak? Umuman olganda, bu dasturchilar uchun har doim birinchi savol: biz qaysi tilda yozamiz. Bunga bitta to'g'ri javob yo'q: biz hal qilayotgan muammolar juda xilma-xildir. Ba'zilar uchun TLA+ men ishlab chiqqan spetsifikatsiya tilidir. Boshqalar uchun xitoy tilidan foydalanish qulayroq. Hamma narsa vaziyatga bog'liq.
Yana bir muhim savol: aniq fikrlashga qanday erishish mumkin? Javob: Biz olimlar kabi fikr yuritishimiz kerak. Bu so'nggi 500 yil ichida o'zini isbotlagan fikrlash usuli. Fanda biz haqiqatning matematik modellarini quramiz. Astronomiya, ehtimol, so'zning qat'iy ma'nosida birinchi fan edi. Astronomiyada qo'llaniladigan matematik modelda osmon jismlari massasi, pozitsiyasi va impulslari bo'lgan nuqtalar sifatida namoyon bo'ladi, lekin aslida ular tog'lar va okeanlar, suv toshqini va suv toshqini bilan juda murakkab ob'ektlardir. Ushbu model, har qanday boshqa kabi, muayyan muammolarni hal qilish uchun yaratilgan. Agar sayyorani topish kerak bo'lsa, teleskopni qaerga yo'naltirish kerakligini aniqlash uchun juda yaxshi. Ammo bu sayyoradagi ob-havoni bashorat qilishni istasangiz, bu model ishlamaydi.
Matematika bizga modelning xususiyatlarini aniqlash imkonini beradi. Va fan bu xususiyatlarning haqiqatga qanday aloqasi borligini ko'rsatadi. Keling, fanimiz, informatika haqida gapiraylik. Biz ishlayotgan haqiqat har xil turdagi hisoblash tizimlari: protsessorlar, o'yin konsollari, kompyuterlar, dasturlarni bajaruvchi va boshqalar. Men kompyuterda dasturni ishga tushirish haqida gapiraman, lekin umuman olganda, bu barcha xulosalar har qanday hisoblash tizimiga tegishli. Bizning fanimizda biz juda ko'p turli xil modellardan foydalanamiz: Tyuring mashinasi, qisman tartiblangan voqealar to'plami va boshqalar.
Dastur nima? Bu mustaqil ravishda ko'rib chiqilishi mumkin bo'lgan har qanday kod. Aytaylik, biz brauzer yozishimiz kerak. Biz uchta vazifani bajaramiz: foydalanuvchining dastur ko'rinishini loyihalashtiramiz, keyin dasturning yuqori darajali diagrammasini yozamiz va nihoyat kodni yozamiz. Kodni yozish jarayonida biz matn formatlagichini yozishimiz kerakligini tushunamiz. Bu erda yana uchta muammoni hal qilishimiz kerak: bu vosita qaysi matnni qaytarishini aniqlang; formatlash algoritmini tanlash; kod yozish. Bu topshiriqning o'ziga xos kichik vazifasi bor: so'zlarga defisni to'g'ri qo'ying. Shuningdek, biz ushbu kichik vazifani uch bosqichda hal qilamiz - ko'rib turganingizdek, ular ko'p darajalarda takrorlanadi.
Keling, birinchi qadamni batafsil ko'rib chiqaylik: dastur qanday muammoni hal qiladi. Bu erda biz ko'pincha dasturni ma'lum bir kirishni qabul qiladigan va ba'zi natijalarni chiqaradigan funksiya sifatida modellashtiramiz. Matematikada funktsiya odatda juftlarning tartiblangan to'plami sifatida tavsiflanadi. Masalan, natural sonlar uchun kvadratlash funksiyasi {<0,0>, <1,1>, <2,4>, <3,9>, …} toʻplami sifatida tavsiflanadi. Bunday funktsiyaning sohasi har bir juftlikning birinchi elementlari, ya'ni natural sonlar to'plamidir. Funksiyani aniqlash uchun uning qamrovi va formulasini belgilashimiz kerak.
Lekin matematikadagi funksiyalar dasturlash tillaridagi funksiyalar bilan bir xil emas. Matematika ancha oson. Murakkab misollar uchun vaqtim yo'qligi sababli, keling, oddiy birini ko'rib chiqaylik: C tilidagi funksiya yoki Java-da ikkita butun sonning eng katta umumiy bo'luvchisini qaytaruvchi statik usul. Ushbu usulning spetsifikatsiyasida biz yozamiz: hisoblaydi GCD(M,N) argumentlar uchun M и Nqayerda GCD(M,N) - sohasi butun sonlar juftligi to‘plami bo‘lgan funksiya, qaytariladigan qiymati esa unga bo‘linadigan eng katta butun sondir. M и N. Ushbu model haqiqatga qanday aloqasi bor? Model butun sonlarda ishlaydi, C yoki Java-da bizda 32-bit mavjud int. Ushbu model bizga algoritm to'g'ri yoki yo'qligini aniqlash imkonini beradi GCD, lekin u ortiqcha xatolarni oldini olmaydi. Bu murakkabroq modelni talab qiladi, buning uchun vaqt yo'q.
Keling, model sifatida funktsiyaning cheklovlari haqida gapiraylik. Ba'zi dasturlar (masalan, operatsion tizimlar) faqat ma'lum argumentlar uchun ma'lum qiymatni qaytarmaydi, ular uzluksiz ishlashi mumkin. Bundan tashqari, model sifatida funksiya ikkinchi bosqichga yaxshi mos kelmaydi: muammoni qanday hal qilishni rejalashtirish. Tez tartiblash va pufakchali tartiblash bir xil funktsiyani hisoblaydi, ammo ular butunlay boshqacha algoritmlardir. Shuning uchun, dastur maqsadiga qanday erishilganligini tasvirlash uchun men boshqa modeldan foydalanaman, uni standart xatti-harakatlar modeli deb ataymiz. Undagi dastur barcha ruxsat etilgan xatti-harakatlar to'plami sifatida ifodalanadi, ularning har biri o'z navbatida holatlar ketma-ketligidir va holat o'zgaruvchilarga qiymatlarni belgilashdir.
Keling, Evklid algoritmining ikkinchi bosqichi qanday bo'lishini ko'rib chiqaylik. Biz hisoblashimiz kerak GCD(M, N). Biz ishga tushiramiz M qanday xva N qanday y, keyin bu o'zgaruvchilarning kichikini kattasidan teng bo'lguncha qayta-qayta ayiring. Masalan, agar M = 12va N = 18, biz quyidagi xatti-harakatni tasvirlashimiz mumkin:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
Agar M = 0 и N = 0? Nol barcha raqamlarga bo'linadi, shuning uchun bu holatda eng katta bo'luvchi yo'q. Bunday vaziyatda biz birinchi bosqichga qaytib, so'rashimiz kerak: biz haqiqatan ham ijobiy bo'lmagan raqamlar uchun GCDni hisoblashimiz kerakmi? Agar bu kerak bo'lmasa, unda siz faqat spetsifikatsiyani o'zgartirishingiz kerak.
Bu erda biz unumdorlik haqida kichik bir fikr yuritishimiz kerak. Ko'pincha kuniga yozilgan kod satrlari soni bilan o'lchanadi. Ammo ma'lum bir qator qatorlardan xalos bo'lsangiz, sizning ishingiz ancha foydali bo'ladi, chunki sizda xatolar uchun kamroq joy bor. Va koddan xalos bo'lishning eng oson yo'li birinchi bosqichda. Siz amalga oshirmoqchi bo'lgan barcha qo'ng'iroqlar va hushtaklarga muhtoj emasligingiz mutlaqo mumkin. Dasturni soddalashtirish va vaqtni tejashning eng tezkor usuli bu qilinmasligi kerak bo'lgan ishlarni qilmaslikdir. Ikkinchi bosqich - bu vaqtni tejashning ikkinchi potentsiali. Agar siz hosildorlikni yozilgan satrlar bo'yicha o'lchasangiz, vazifani qanday bajarish haqida o'ylash sizni qiladi unumdorligi past, chunki siz kamroq kod bilan bir xil muammoni hal qilishingiz mumkin. Men bu erda aniq statistik ma'lumotlarni keltira olmayman, chunki men spetsifikatsiyaga, ya'ni birinchi va ikkinchi bosqichlarga vaqt sarflaganim sababli yozmagan qatorlar sonini sanashning imkoni yo'q. Va tajribani bu erda ham o'rnatish mumkin emas, chunki tajribada biz birinchi bosqichni bajarish huquqiga ega emasmiz, vazifa oldindan belgilanadi.
Norasmiy spetsifikatsiyalarda ko'plab qiyinchiliklarni e'tiborsiz qoldirish oson. Funktsiyalar uchun qat'iy xususiyatlarni yozishda qiyin narsa yo'q, men buni muhokama qilmayman. Buning o'rniga biz standart xatti-harakatlar uchun kuchli spetsifikatsiyalarni yozish haqida gaplashamiz. Har qanday xatti-harakatlar to'plamini xavfsizlik xususiyatidan foydalanib tasvirlash mumkinligini aytadigan teorema mavjud (xavfsizlik) va omon qolish xususiyatlari (tiriklik). Xavfsizlik degani, hech qanday yomon narsa bo'lmaydi, dastur noto'g'ri javob bermaydi. Omon qolish, ertami-kechmi yaxshi narsa sodir bo'lishini anglatadi, ya'ni dastur ertami-kechmi to'g'ri javob beradi. Qoida tariqasida, xavfsizlik muhimroq ko'rsatkichdir, xatolar ko'pincha bu erda sodir bo'ladi. Shuning uchun, vaqtni tejash uchun men omon qolish haqida gapirmayman, garchi bu, albatta, muhim.
Biz birinchi navbatda mumkin bo'lgan dastlabki holatlar to'plamini belgilash orqali xavfsizlikka erishamiz. Ikkinchidan, har bir davlat uchun barcha mumkin bo'lgan keyingi davlatlar bilan munosabatlar. Keling, olimlar kabi harakat qilaylik va holatlarni matematik tarzda aniqlaylik. Boshlang'ich holatlar to'plami formula bilan tavsiflanadi, masalan, Evklid algoritmi misolida: (x = M) ∧ (y = N). Muayyan qiymatlar uchun M и N faqat bitta boshlang'ich holat mavjud. Keyingi holat bilan bog'liqlik formula bilan tavsiflanadi, unda keyingi holatning o'zgaruvchilari tub bilan, joriy holatning o'zgaruvchilari esa tubsiz yoziladi. Evklid algoritmida biz ikkita formulani ajratish bilan shug'ullanamiz, ulardan birida. x eng katta qiymat, ikkinchisida esa - y:
Birinchi holda, y ning yangi qiymati y ning oldingi qiymatiga teng bo'ladi va biz kattaroq o'zgaruvchidan kichikroq o'zgaruvchini ayirish orqali x ning yangi qiymatini olamiz. Ikkinchi holda, biz buning aksini qilamiz.
Keling, Evklid algoritmiga qaytaylik. Yana shuni taxmin qilaylik M = 12, N = 18. Bu yagona boshlang'ich holatni belgilaydi, (x = 12) ∧ (y = 18). Keyin biz ushbu qiymatlarni yuqoridagi formulaga kiritamiz va quyidagilarni olamiz:
Mana yagona mumkin bo'lgan yechim: x' = 18 - 12 ∧ y' = 12va biz xatti-harakatni olamiz: [x = 12, y = 18]. Xuddi shunday, biz xatti-harakatlarimizdagi barcha holatlarni tasvirlashimiz mumkin: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
Oxirgi holatda [x = 6, y = 6] ifodaning ikkala qismi ham yolg'on bo'ladi, shuning uchun uning keyingi holati yo'q. Shunday qilib, bizda ikkinchi bosqichning to'liq tavsifi bor - ko'rib turganingizdek, bu muhandislar va olimlardagi kabi oddiy matematika va informatika kabi g'alati emas.
Bu ikki formulani vaqtinchalik mantiqning bitta formulasiga birlashtirish mumkin. U nafis va tushuntirish oson, lekin hozir unga vaqt yo'q. Vaqtinchalik mantiq bizga faqat tiriklik xususiyati uchun kerak bo'lishi mumkin, bu xavfsizlik uchun kerak emas. Menga vaqtinchalik mantiq yoqmaydi, bu oddiy matematika emas, lekin jonlilik uchun bu zaruriy yovuzlikdir.
Evklid algoritmida har bir qiymat uchun x и y noyob qadriyatlarga ega x' и y', bu keyingi holat bilan munosabatni to'g'ri qiladi. Boshqacha qilib aytganda, Evklid algoritmi deterministikdir. Deterministik bo'lmagan algoritmni modellashtirish uchun joriy holat bir nechta mumkin bo'lgan kelajakdagi holatlarga ega bo'lishi kerak va har bir astarlanmagan o'zgaruvchining qiymati keyingi holatga bo'lgan munosabat to'g'ri bo'lishi uchun bir nechta boshlang'ich o'zgaruvchi qiymatlariga ega bo'lishi kerak. Buni qilish oson, lekin men hozir misollar keltirmayman.
Ishchi vositani yaratish uchun sizga rasmiy matematika kerak. Spetsifikatsiyani qanday rasmiylashtirish kerak? Buning uchun bizga rasmiy til kerak, masalan, . Evklid algoritmining spetsifikatsiyasi ushbu tilda quyidagicha ko'rinadi:
Uchburchak bilan tenglik belgisi belgisi belgining chap tomonidagi qiymat belgining o'ng tomonidagi qiymatga teng ekanligi aniqlanganligini anglatadi. Aslida, spetsifikatsiya ta'rif, bizning holatlarimizda ikkita ta'rif. TLA+ dagi spetsifikatsiyaga yuqoridagi slaydda bo'lgani kabi deklaratsiyalar va ba'zi sintaksislarni qo'shishingiz kerak. ASCII da u quyidagicha ko'rinadi:
Ko'rib turganingizdek, hech qanday murakkab narsa yo'q. TLA+ uchun spetsifikatsiya sinovdan o'tkazilishi mumkin, ya'ni kichik modeldagi barcha mumkin bo'lgan xatti-harakatlarni chetlab o'tish mumkin. Bizning holatda, bu model ma'lum qiymatlar bo'ladi M и N. Bu butunlay avtomatik bo'lgan juda samarali va oddiy tekshirish usuli. Rasmiy haqiqat dalillarini yozish va ularni mexanik tekshirish ham mumkin, lekin bu juda ko'p vaqtni oladi, shuning uchun deyarli hech kim buni qilmaydi.
TLA+ ning asosiy kamchiligi shundaki, u matematika bo‘lib, dasturchilar va kompyuter olimlari matematikadan qo‘rqishadi. Bir qarashda bu hazilga o'xshaydi, lekin, afsuski, men buni jiddiylik bilan aytaman. Mening hamkasbim menga TLA+ ni bir nechta ishlab chiquvchilarga qanday tushuntirishga harakat qilganini aytib berdi. Formulalar ekranda paydo bo'lishi bilanoq, ular darhol shishasimon ko'zlarga aylandi. Shunday qilib, agar TLA + sizni qo'rqitsa, foydalanishingiz mumkin , bu o'yinchoq dasturlash tilining bir turi. PlusCal-dagi ifoda har qanday TLA+ ifodasi, ya'ni umuman olganda har qanday matematik ifoda bo'lishi mumkin. Bundan tashqari, PlusCal deterministik bo'lmagan algoritmlar uchun sintaksisga ega. PlusCal har qanday TLA+ ifodasini yozishi mumkinligi sababli, PlusCal har qanday haqiqiy dasturlash tiliga qaraganda ancha ifodali. Keyinchalik, PlusCal oson o'qiladigan TLA+ spetsifikatsiyasiga kompilyatsiya qilinadi. Bu, albatta, murakkab PlusCal spetsifikatsiyasi TLA+ da oddiyga aylanadi degani emas - shunchaki ular orasidagi yozishmalar aniq, qo'shimcha murakkablik bo'lmaydi. Nihoyat, bu spetsifikatsiyani TLA+ vositalari bilan tekshirish mumkin. Umuman olganda, PlusCal matematik fobiyani engishga yordam beradi va hatto dasturchilar va kompyuter olimlari uchun ham tushunarli. Ilgari men bir muncha vaqt (taxminan 10 yil) algoritmlarni nashr qildim.
Ehtimol, kimdir TLA + va PlusCal matematika ekanligiga e'tiroz bildirishi mumkin va matematika faqat ixtiro qilingan misollarda ishlaydi. Amalda sizga turlar, protseduralar, ob'ektlar va boshqalar bilan haqiqiy til kerak. Bu unday emas. Amazonda ishlagan Kris Nyukomb shunday yozadi: “Biz TLA+ dan o‘nta yirik loyihada foydalandik va har bir holatda undan foydalanish rivojlanishga sezilarli o‘zgarishlar kiritdi, chunki biz ishlab chiqarishga kirishishdan oldin xavfli xatolarni aniqlay oldik va bu bizga zarur bo‘lgan tushuncha va ishonchni berdi. dasturning haqiqatiga ta'sir qilmasdan agressiv ishlash optimallashtirishlarini amalga oshiring". Rasmiy usullardan foydalanganda biz samarasiz kodni olishimizni tez-tez eshitishingiz mumkin - amalda hamma narsa aksincha. Bundan tashqari, dasturchilar ularning foydaliligiga ishonch hosil qilgan taqdirda ham, menejerlarni rasmiy usullarning zarurligiga ishontira olmaydi, degan fikr mavjud. Va Nyukomb yozadi: "Menejerlar endi TLA + uchun spetsifikatsiyalarni yozishga va buning uchun vaqt ajratishga qattiq intilmoqda". Shunday qilib, menejerlar TLA+ ishlayotganini ko'rganlarida, ular buni mamnuniyat bilan qabul qilishadi. Kris Nyukomb buni taxminan olti oy oldin (2014 yil oktabr) yozgan edi, lekin hozir, men bilishimcha, TLA+ 14 ta emas, 10 ta loyihada qoʻllaniladi. Yana bir misol XBox 360 dizayni bilan bogʻliq. Stajyor Charlz Tekerga keldi va xotira tizimi uchun spetsifikatsiyani yozdi. Ushbu spetsifikatsiya tufayli, aks holda e'tiborga olinmaydigan xatolik aniqlandi va shu sababli har bir XBox 360 to'rt soatlik foydalanishdan keyin ishdan chiqadi. IBM muhandislari o'zlarining sinovlarida bu xato topilmasligini tasdiqladilar.
TLA+ haqida ko'proq Internetda o'qishingiz mumkin, ammo endi norasmiy xususiyatlar haqida gapiraylik. Biz kamdan-kam hollarda eng kichik umumiy bo'luvchi va shunga o'xshashlarni hisoblaydigan dasturlarni yozishimiz kerak. Biz TLA+ uchun yozgan chiroyli printer vositasi kabi dasturlarni tez-tez yozamiz. Eng oddiy ishlov berishdan so'ng, TLA + kodi quyidagicha ko'rinadi:
Ammo yuqoridagi misolda foydalanuvchi, ehtimol, birikma va teng belgilarning mos kelishini xohlaydi. Shunday qilib, to'g'ri formatlash quyidagicha ko'rinadi:
Keling, yana bir misolni ko'rib chiqaylik:
Bu erda, aksincha, manbadagi tenglik, qo'shish va ko'paytirish belgilarining tekislanishi tasodifiy edi, shuning uchun eng oddiy ishlov berish juda etarli. Umuman olganda, to'g'ri formatlashning aniq matematik ta'rifi yo'q, chunki bu holda "to'g'ri" "foydalanuvchi nimani xohlaydi" degan ma'noni anglatadi va buni matematik tarzda aniqlab bo'lmaydi.
Agar bizda haqiqat ta'rifi bo'lmasa, spetsifikatsiya befoyda bo'lib tuyuladi. Ammo bu unday emas. Dastur nima qilishi kerakligini bilmasligimiz uning qanday ishlashi haqida o'ylashning hojati yo'qligini anglatmaydi - aksincha, biz unga ko'proq kuch sarflashimiz kerak. Bu erda spetsifikatsiya ayniqsa muhimdir. Strukturaviy bosib chiqarish uchun optimal dasturni aniqlash mumkin emas, lekin bu biz uni umuman qabul qilmasligimiz kerak degani emas va kodni ong oqimi sifatida yozish yaxshi narsa emas. Oxir-oqibat, men ta'riflar bilan oltita qoidalarning spetsifikatsiyasini yozdim sharhlar shaklida java faylida. Mana qoidalardan biriga misol: a left-comment token is LeftComment aligned with its covering token. Bu qoida, aytaylik, matematik ingliz tilida yozilgan: LeftComment aligned, left-comment и covering token - ta'riflar bilan atamalar. Matematiklar matematikani shunday ta'riflaydilar: atamalarning ta'riflarini va ularga asoslanib, qoidalarni yozadilar. Bunday spetsifikatsiyaning afzalligi shundaki, oltita qoidani tushunish va disk raskadrovka qilish 850 satr kodga qaraganda ancha oson. Aytishim kerakki, ushbu qoidalarni yozish oson emas edi, ularni tuzatish uchun juda ko'p vaqt kerak bo'ldi. Ayniqsa, bu maqsadda men qaysi qoida ishlatilganligi haqida xabar beradigan kod yozdim. Men ushbu oltita qoidani bir nechta misollarda sinab ko'rganim sababli, 850 qator kodni disk raskadrovka qilishim shart emas edi va xatolarni topish juda oson bo'ldi. Java-da buning uchun ajoyib vositalar mavjud. Agar kodni hozirgina yozgan bo'lsam, bu menga ko'proq vaqt talab qilgan bo'lardi va formatlash sifatsizroq bo'lar edi.
Nima uchun rasmiy spetsifikatsiyani ishlatib bo'lmadi? Bir tomondan, bu erda to'g'ri ijro etish juda muhim emas. Strukturaviy bosma nashrlar hech kimga yoqmaydi, shuning uchun men uni barcha g'alati vaziyatlarda to'g'ri ishlashiga majbur qilishim shart emas edi. Bundan ham muhimi, menda tegishli vositalar yo'q edi. TLA+ model tekshiruvi bu erda foydasiz, shuning uchun misollarni qo'lda yozishim kerak edi.
Yuqoridagi spetsifikatsiya barcha spetsifikatsiyalar uchun umumiy xususiyatlarga ega. Bu koddan yuqori daraja. U har qanday tilda amalga oshirilishi mumkin. Uni yozish uchun hech qanday vositalar yoki usullar foydasiz. Hech bir dasturlash kursi bu spetsifikatsiyani yozishingizga yordam bermaydi. Va bu spetsifikatsiyani keraksiz qiladigan vositalar yo'q, agar siz TLA+ da tuzilgan bosma dasturlarni yozish uchun maxsus til yozmasangiz. Nihoyat, ushbu spetsifikatsiya kodni qanday yozishimiz haqida hech narsa aytmaydi, faqat ushbu kod nima qilishini bildiradi. Kod haqida o'ylashni boshlashdan oldin muammoni o'ylab ko'rishga yordam beradigan spetsifikatsiyani yozamiz.
Lekin bu spetsifikatsiyani boshqa spetsifikatsiyalardan ajratib turadigan xususiyatlari ham bor. Boshqa xususiyatlarning 95% sezilarli darajada qisqaroq va sodda:
Bundan tashqari, ushbu spetsifikatsiya qoidalar to'plamidir. Qoida tariqasida, bu sifatsiz spetsifikatsiyaning belgisidir. Bir qator qoidalarning oqibatlarini tushunish juda qiyin, shuning uchun men ularni tuzatish uchun ko'p vaqt sarflashim kerak edi. Biroq, bu holatda, men yaxshiroq yo'l topa olmadim.
Uzluksiz ishlaydigan dasturlar haqida bir necha so'z aytishga arziydi. Qoida tariqasida, ular parallel ravishda ishlaydi, masalan, operatsion tizimlar yoki taqsimlangan tizimlar. Juda kam odam ularni aqlan yoki qog'ozda tushuna oladi va men ulardan biri emasman, garchi men bir paytlar buni uddalay olganman. Shuning uchun bizga ishimizni tekshiradigan vositalar kerak - masalan, TLA + yoki PlusCal.
Agar kod aniq nima qilish kerakligini bilsam, nima uchun spetsifikatsiyani yozish kerak edi? Aslida, men buni bilaman deb o'yladim. Bundan tashqari, spetsifikatsiyaga ega bo'lgan holda, begona odam nima qilayotganini tushunish uchun endi kodga kirishi shart emas. Menda bir qoida bor: umumiy qoidalar bo'lmasligi kerak. Bu qoidadan istisno bor, albatta, bu men amal qiladigan yagona umumiy qoida: kod nima qilishining spetsifikatsiyasi odamlarga koddan foydalanishda bilishi kerak bo'lgan hamma narsani aytib berishi kerak.
Xo'sh, dasturchilar fikrlash haqida aniq nimani bilishlari kerak? Yangi boshlanuvchilar uchun, boshqalar kabi: agar siz yozmasangiz, unda siz faqat o'ylayotgandek tuyuladi. Bundan tashqari, kodlashdan oldin o'ylab ko'rishingiz kerak, ya'ni kodlashdan oldin yozishingiz kerak. Spetsifikatsiya - kodlashni boshlashdan oldin biz yozgan narsamiz. Har kim tomonidan ishlatilishi yoki o'zgartirilishi mumkin bo'lgan har qanday kod uchun spetsifikatsiya kerak. Va bu "kimdir" kod yozilganidan bir oy o'tgach, uning muallifi bo'lishi mumkin. Spetsifikatsiya katta dasturlar va tizimlar, sinflar, usullar va ba'zan bitta usulning murakkab bo'limlari uchun kerak bo'ladi. Kod haqida aniq nima yozilishi kerak? Siz u nima qilishini tasvirlab berishingiz kerak, ya'ni ushbu koddan foydalanadigan har qanday odamga nima foydali bo'lishi mumkin. Ba'zan kod o'z maqsadiga qanday erishishini ko'rsatish kerak bo'lishi mumkin. Agar biz algoritmlar jarayonida ushbu usuldan o'tgan bo'lsak, uni algoritm deb ataymiz. Agar u o'ziga xos va yangi narsa bo'lsa, biz uni yuqori darajadagi dizayn deb ataymiz. Bu erda hech qanday rasmiy farq yo'q: ikkalasi ham dasturning mavhum modelidir.
Kod spetsifikatsiyasini qanday yozish kerak? Asosiysi: u kodning o'zidan bir daraja yuqori bo'lishi kerak. U holatlar va xatti-harakatlarni tasvirlashi kerak. Vazifa talab qiladigan darajada qat'iy bo'lishi kerak. Agar siz vazifani qanday amalga oshirish kerakligi haqida spetsifikatsiya yozayotgan bo'lsangiz, uni psevdokodda yoki PlusCal bilan yozishingiz mumkin. Rasmiy spetsifikatsiyalar bo'yicha spetsifikatsiyalarni qanday yozishni o'rganishingiz kerak. Bu sizga norasmiy ko'nikmalar bilan ham yordam beradigan kerakli ko'nikmalarni beradi. Rasmiy spetsifikatsiyalarni yozishni qanday o'rganasiz? Dasturlashni o'rganganimizda, biz dasturlar yozdik va keyin ularni tuzatdik. Bu erda ham xuddi shunday: spetsifikatsiyani yozing, uni model tekshiruvi bilan tekshiring va xatolarni tuzating. TLA+ rasmiy spetsifikatsiya uchun eng yaxshi til bo'lmasligi mumkin va boshqa til sizning maxsus ehtiyojlaringiz uchun yaxshiroq bo'lishi mumkin. TLA+ ning afzalligi shundaki, u matematik fikrlashni juda yaxshi o‘rgatadi.
Spetsifikatsiya va kodni qanday bog'lash mumkin? Matematik tushunchalarni va ularni amalga oshirishni bog'laydigan sharhlar yordamida. Agar siz grafikalar bilan ishlasangiz, dastur darajasida sizda tugunlar massivlari va havolalar massivlari bo'ladi. Shuning uchun, ushbu dasturlash tuzilmalari tomonidan grafik qanday amalga oshirilayotganini aniq yozishingiz kerak.
Shuni ta'kidlash kerakki, yuqoridagilarning hech biri kod yozishning haqiqiy jarayoniga taalluqli emas. Kodni yozganingizda, ya'ni uchinchi bosqichni bajarasiz, siz ham dastur orqali o'ylashingiz va o'ylashingiz kerak. Agar pastki vazifa murakkab yoki noaniq bo'lib chiqsa, siz unga spetsifikatsiya yozishingiz kerak. Lekin men bu erda kodning o'zi haqida gapirmayapman. Siz har qanday dasturlash tilidan, har qanday metodologiyadan foydalanishingiz mumkin, bu ular haqida emas. Bundan tashqari, yuqoridagilarning hech biri kodni sinash va disk raskadrovka qilish zaruratini bartaraf etmaydi. Mavhum model to'g'ri yozilgan bo'lsa ham, uni amalga oshirishda xatolar bo'lishi mumkin.
Xususiyatlarni yozish kodlash jarayonida qo'shimcha qadamdir. Buning yordamida ko'p xatolarni kamroq harakat bilan ushlash mumkin - biz buni Amazon dasturchilari tajribasidan bilamiz. Spetsifikatsiyalar bilan dasturlarning sifati yuqori bo'ladi. Xo'sh, nega biz ularsiz tez-tez yuramiz? Chunki yozish qiyin. Yozish esa qiyin, chunki buning uchun siz o'ylashingiz kerak va fikrlash ham qiyin. O'z fikringni ko'rsatish har doim osonroq. Bu erda siz yugurish bilan o'xshashlikni chizishingiz mumkin - qancha kam yugursangiz, shunchalik sekin yugurasiz. Mushaklaringizni mashq qilishingiz va yozishni mashq qilishingiz kerak. Amaliyot kerak.
Spetsifikatsiya noto'g'ri bo'lishi mumkin. Siz biror joyda xatoga yo'l qo'ygan bo'lishingiz mumkin yoki talablar o'zgargan bo'lishi mumkin yoki yaxshilash kerak bo'lishi mumkin. Har kim ishlatadigan har qanday kodni o'zgartirish kerak, shuning uchun ertami-kechmi spetsifikatsiya dasturga mos kelmaydi. Ideal holda, bu holda siz yangi spetsifikatsiyani yozishingiz va kodni to'liq qayta yozishingiz kerak. Biz buni hech kim qilmasligini juda yaxshi bilamiz. Amalda biz kodni tuzatamiz va ehtimol spetsifikatsiyani yangilaymiz. Agar bu ertami-kechmi sodir bo'ladigan bo'lsa, unda nima uchun umuman texnik xususiyatlarni yozish kerak? Birinchidan, kodingizni tahrir qiladigan odam uchun spetsifikatsiyadagi har bir qo'shimcha so'z oltin bilan baholanadi va bu odam siz ham bo'lishi mumkin. Kodimni tahrir qilayotganda ko'pincha spetsifikatsiyani olmaganim uchun o'zimni haqorat qilaman. Va men koddan ko'ra ko'proq xususiyatlarni yozaman. Shuning uchun, kodni tahrir qilganingizda, spetsifikatsiya har doim yangilanishi kerak. Ikkinchidan, har bir tahrir bilan kod yomonlashadi, uni o'qish va saqlash tobora qiyinlashadi. Bu entropiyaning oshishi. Lekin agar siz spetsifikatsiya bilan boshlamasangiz, unda siz yozgan har bir satr tahrir bo'ladi va kodni boshidanoq o'qish qiyin va qiyin bo'ladi.
Aytgancha , hech bir jangda reja bo‘yicha g‘alaba qozonilmagan, hech bir jangda rejasiz g‘alaba qozonilmagan. U janglar haqida bir-ikki narsani bilardi. Xususiyatlarni yozish vaqtni behuda sarflash degan fikr bor. Ba'zan bu to'g'ri va vazifa shunchalik soddaki, bu haqda o'ylash uchun hech narsa yo'q. Ammo shuni yodda tutish kerakki, sizga texnik shartlarni yozmaslik aytilganda, o'ylamaslik kerak. Va har safar bu haqda o'ylashingiz kerak. Vazifani o'ylab ko'rish xato qilmasligingizga kafolat bermaydi. Ma'lumki, sehrli tayoqchani hech kim ixtiro qilmagan va dasturlash juda qiyin ish. Ammo muammoni o'ylab ko'rmasangiz, xato qilishingiz kafolatlanadi.
TLA + va PlusCal haqida ko'proq ma'lumotni maxsus veb-saytda o'qishingiz mumkin, u erga mening bosh sahifamdan o'tishingiz mumkin . Hammasi men uchun, e'tiboringiz uchun rahmat.
Iltimos, bu tarjima ekanligini unutmang. Izohlarni yozayotganda, muallif ularni o'qimasligini unutmang. Agar siz haqiqatan ham muallif bilan suhbatlashmoqchi bo'lsangiz, u holda u 2019 yil 11-12 iyul kunlari Sankt-Peterburgda bo'lib o'tadigan Hydra 2019 konferentsiyasida bo'ladi. Chiptalarni sotib olish mumkin .
Manba: www.habr.com