Bu məqalə tərcümədir . Ancaq ondan əvvəl kiçik bir giriş. Zombilər necə yaranır? Hər kəs bir dostunu və ya həmkarını öz səviyyəsinə qaldırmaq istədikləri bir vəziyyətə düşdü, amma alınmadı. Və sizinlə çox deyil, onunla birlikdə "bu, alınmır": tərəzinin bir tərəfində normal maaş, vəzifələr və s., digər tərəfdən isə düşünmək ehtiyacı var. Düşünmək xoşagəlməz və ağrılıdır. Tez təslim olur və beynini heç işə salmadan kod yazmağa davam edir. Öyrənilmiş çarəsizliyin baryerini aşmaq üçün nə qədər zəhmət tələb olunduğunu təsəvvür edirsiniz və sadəcə bunu etmirsiniz. Zombilər belə yaranır, görünür, onları müalicə etmək olar, amma görünür, bunu heç kim etməyəcək.
Mən bunu görəndə (bəli, dərsliklərdən eyni yoldaş) və hesabat deyil, sual-cavab şəklində bir az ehtiyatlı davrandım. Hər halda, Lesli dünya şöhrətli alimdir, paylanmış hesablamalarda fundamental əsərlərin müəllifidir və siz onu LaTeX - “Lamport TeX” sözündəki La hərfləri ilə də tanıya bilərsiniz. İkinci həyəcanverici amil onun tələbidir: gələn hər kəs (tamamilə pulsuz) onun bir-iki hesabatını əvvəlcədən dinləməli, onlara ən azı bir sual verməli və yalnız bundan sonra gəlməlidir. Mən Lamportun orada nə yayımladığını görmək qərarına gəldim - və bu, əladır! Məhz bu şey, zombiləri müalicə etmək üçün sehrli həbdir. Sizi xəbərdar edirəm: mətndən super çevik metodologiyaları sevənlər və yazılanları sınamağı sevməyənlər nəzərəçarpacaq dərəcədə tükənə bilər.
Habrokatdan sonra əslində seminarın tərcüməsi başlayır. Oxumaqdan həzz alın!
Nə tapşırırsınızsa, onda siz həmişə üç addımdan keçməlisiniz:
- hansı məqsədə çatmaq istədiyinizə qərar verin;
- məqsədinizə necə çatacağınıza qərar verin;
- məqsədinə çat.
Bu proqramlaşdırmaya da aiddir. Kod yazarkən bizə lazımdır:
- proqramın nə etməli olduğuna qərar vermək;
- vəzifəsini necə yerinə yetirməli olduğunu müəyyən etmək;
- müvafiq kodu yazın.
Son addım, əlbəttə ki, çox vacibdir, amma bu gün bu barədə danışmayacağam. Bunun əvəzinə ilk ikisini müzakirə edəcəyik. Hər bir proqramçı işə başlamazdan əvvəl onları yerinə yetirir. Brauzer və ya verilənlər bazası yazmağınıza qərar vermədiyiniz halda yazmaq üçün oturmursunuz. Məqsəd haqqında müəyyən bir fikir mövcud olmalıdır. Və siz mütləq proqramın tam olaraq nə edəcəyini düşünürsünüz və kodun bir növ brauzerə çevriləcəyi ümidi ilə yazmayın.
Bu kod əvvəlcədən düşünmə necə baş verir? Bunun üçün nə qədər səy göstərməliyik? Hər şey həll etdiyimiz problemin nə qədər mürəkkəb olmasından asılıdır. Tutaq ki, xətaya dözümlü paylanmış sistem yazmaq istəyirik. Bu halda, kod yazmağa başlamazdan əvvəl hər şeyi diqqətlə düşünməliyik. Əgər tam dəyişəni 1-ə qədər artırmaq lazımdırsa? İlk baxışdan burada hər şey mənasızdır və heç bir fikrə ehtiyac yoxdur, amma sonra daşqın baş verə biləcəyini xatırlayırıq. Buna görə də, problemin sadə və ya mürəkkəb olduğunu başa düşmək üçün əvvəlcə düşünmək lazımdır.
Problemin mümkün həll yollarını əvvəlcədən düşünsəniz, səhvlərdən qaça bilərsiniz. Ancaq bu, fikrinizin aydın olmasını tələb edir. Buna nail olmaq üçün fikirlərinizi yazmalısınız. Dik Guindon sitatını çox bəyənirəm: "Yazdığınız zaman təbiət sizə düşüncənizin nə qədər səliqəsiz olduğunu göstərir." Yazmırsansa, yalnız düşündüyünü düşünürsən. Və fikirlərinizi spesifikasiya şəklində yazmalısınız.
Xüsusiyyətlər, xüsusən də böyük layihələrdə bir çox funksiyaları yerinə yetirir. Ancaq mən onlardan yalnız biri haqqında danışacağam: aydın düşünməyimizə kömək edirlər. Aydın düşünmək çox vacib və olduqca çətindir, ona görə də burada hər hansı bir köməyə ehtiyacımız var. Spesifikasiyaları hansı dildə yazmalıyıq? Ümumiyyətlə, proqramçılar üçün həmişə ilk sual budur: hansı dildə yazacağıq. Buna bir düzgün cavab yoxdur: həll etdiyimiz problemlər çox müxtəlifdir. Bəziləri üçün TLA+ mənim hazırladığım spesifikasiya dilidir. Digərləri üçün Çin dilini istifadə etmək daha rahatdır. Hər şey vəziyyətdən asılıdır.
Daha vacib olan başqa bir sual: daha aydın düşüncəyə necə nail olmaq olar? Cavab: Biz alimlər kimi düşünməliyik. Bu, son 500 ildə özünü doğrultmuş düşüncə tərzidir. Elmdə biz reallığın riyazi modellərini qururuq. Astronomiya bəlkə də sözün tam mənasında ilk elm idi. Astronomiyada istifadə olunan riyazi modeldə səma cisimləri kütləsi, mövqeyi və impulsu olan nöqtələr kimi görünür, baxmayaraq ki, əslində onlar dağlar və okeanlar, gelgit və gelgitlərlə son dərəcə mürəkkəb obyektlərdir. Bu model, hər hansı digər kimi, müəyyən problemləri həll etmək üçün yaradılmışdır. Bir planet tapmaq lazımdırsa, teleskopu hara yönəltəcəyini müəyyən etmək üçün əladır. Ancaq bu planetdəki havanı proqnozlaşdırmaq istəyirsinizsə, bu model işləməyəcək.
Riyaziyyat bizə modelin xassələrini təyin etməyə imkan verir. Elm isə bu xüsusiyyətlərin reallıqla necə əlaqəli olduğunu göstərir. Gəlin öz elmimizdən, informatikadan danışaq. Bizim işlədiyimiz reallıq müxtəlif növ hesablama sistemləridir: prosessorlar, oyun konsolları, kompüterlər, icraçı proqramlar və s. Mən bir proqramın kompüterdə işləməsi haqqında danışacağam, lakin ümumilikdə bütün bu nəticələr istənilən hesablama sisteminə aiddir. Elmimizdə biz bir çox müxtəlif modellərdən istifadə edirik: Turinq maşını, qismən sifariş edilmiş hadisələr dəstləri və bir çox başqaları.
Proqram nədir? Bu, müstəqil hesab edilə bilən hər hansı bir koddur. Tutaq ki, brauzer yazmalıyıq. Biz üç tapşırığı yerinə yetiririk: istifadəçinin proqrama baxışını tərtib edirik, sonra proqramın yüksək səviyyəli diaqramını yazırıq və nəhayət kodu yazırıq. Kodu yazarkən anlayırıq ki, mətn formatlayıcısı yazmalıyıq. Burada yenə üç problemi həll etməliyik: bu alətin hansı mətni qaytaracağını müəyyənləşdirin; formatlaşdırma üçün alqoritm seçin; kodu yazın. Bu tapşırığın öz alt tapşırığı var: sözlərə düzgün defis qoyun. Bu alt tapşırığı da üç addımda həll edirik - gördüyünüz kimi, onlar bir çox səviyyələrdə təkrarlanır.
İlk addımı daha ətraflı nəzərdən keçirək: proqram hansı problemi həll edir. Burada biz tez-tez proqramı bəzi giriş qəbul edən və müəyyən bir nəticə çıxaran funksiya kimi modelləşdiririk. Riyaziyyatda funksiya adətən sifarişli cütlər dəsti kimi təsvir edilir. Məsələn, natural ədədlər üçün kvadratlaşdırma funksiyası {<0,0>, <1,1>, <2,4>, <3,9>, …} çoxluğu kimi təsvir olunur. Belə funksiyanın oblastı hər bir cütün ilk elementlərinin, yəni natural ədədlərin çoxluğudur. Funksiyanı təyin etmək üçün onun əhatə dairəsini və düsturunu təyin etməliyik.
Lakin riyaziyyatdakı funksiyalar proqramlaşdırma dillərindəki funksiyalarla eyni deyil. Riyaziyyat çox asandır. Mürəkkəb misallar üçün vaxtım olmadığı üçün sadə birini nəzərdən keçirək: C-də funksiya və ya Java-da iki tam ədədin ən böyük ortaq bölənini qaytaran statik metod. Bu metodun spesifikasiyasında yazacağıq: hesablayır GCD(M,N) arqumentlər üçün M и NHara GCD(M,N) - domeni tam ədəd cütləri dəsti olan və qaytarılan dəyəri bölünə bilən ən böyük tam ədəd olan funksiya M и N. Bu modelin reallıqla necə əlaqəsi var? Model tam ədədlərlə işləyir, C və ya Java-da isə bizdə 32 bit var int. Bu model alqoritmin düzgün olub-olmadığına qərar verməyə imkan verir GCD, lakin daşqın xətalarının qarşısını almayacaq. Bunun üçün daha mürəkkəb bir model tələb olunur, bunun üçün vaxt yoxdur.
Model olaraq funksiyanın məhdudiyyətlərindən danışaq. Bəzi proqramlar (məsələn, əməliyyat sistemləri) yalnız müəyyən arqumentlər üçün müəyyən bir dəyər qaytarmır, onlar davamlı olaraq işləyə bilərlər. Bundan əlavə, bir model kimi funksiya ikinci addım üçün uyğun deyil: problemin necə həll olunacağını planlaşdırmaq. Tez çeşidləmə və qabarcıq çeşidləmə eyni funksiyanı hesablayır, lakin onlar tamamilə fərqli alqoritmlərdir. Buna görə də, proqramın məqsədinə necə nail olunduğunu təsvir etmək üçün fərqli bir modeldən istifadə edirəm, buna standart davranış modeli deyək. İçindəki proqram, hər biri öz növbəsində vəziyyətlərin ardıcıllığı olan bütün icazə verilən davranışların məcmusu kimi təmsil olunur və vəziyyət dəyişənlərə dəyərlərin təyin edilməsidir.
Evklid alqoritmi üçün ikinci addımın necə görünəcəyini görək. Biz hesablamalıyıq GCD(M, N). Biz işə salırıq M kimi xVə N kimi y, sonra bərabər olana qədər bu dəyişənlərin kiçikini böyükdən təkrar-təkrar çıxarın. Məsələn, əgər M = 12Və N = 18, biz aşağıdakı davranışı təsvir edə bilərik:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
Və əgər M = 0 и N = 0? Sıfır bütün ədədlərə bölünür, ona görə də bu halda ən böyük bölən yoxdur. Bu vəziyyətdə, ilk addıma qayıtmaq və soruşmaq lazımdır: həqiqətən müsbət olmayan nömrələr üçün GCD hesablamaq lazımdırmı? Bu lazım deyilsə, onda sadəcə spesifikasiyanı dəyişdirməlisiniz.
Burada məhsuldarlıqla bağlı kiçik bir kənara çıxmalıyıq. Çox vaxt gündə yazılan kod sətirlərinin sayı ilə ölçülür. Ancaq müəyyən sayda sətirdən xilas olsanız, işiniz daha faydalıdır, çünki səhvlər üçün daha az yer var. Və koddan qurtulmağın ən asan yolu ilk addımdır. Tamamilə mümkündür ki, həyata keçirməyə çalışdığınız bütün zənglərə və fitlərə ehtiyacınız yoxdur. Proqramı sadələşdirməyin və vaxta qənaət etməyin ən sürətli yolu edilməməsi lazım olan işləri etməməkdir. İkinci addım ikinci ən çox vaxta qənaət edən potensialdır. Əgər siz məhsuldarlığı yazılan sətirlərlə ölçsəniz, o zaman bir tapşırığı necə yerinə yetirəcəyinizi düşünmək sizi vadar edər daha az məhsuldar, çünki eyni problemi daha az kodla həll edə bilərsiniz. Burada dəqiq statistika verə bilmərəm, çünki spesifikasiyaya, yəni birinci və ikinci addımlara vaxt sərf etdiyim üçün yazmadığım sətirlərin sayını hesablamaq imkanım yoxdur. Təcrübəni də burada qurmaq olmaz, çünki eksperimentdə birinci addımı tamamlamaq hüququmuz yoxdur, vəzifə əvvəlcədən müəyyən edilib.
Qeyri-rəsmi spesifikasiyalarda bir çox çətinlikləri nəzərdən qaçırmaq asandır. Funksiyalar üçün ciddi spesifikasiyalar yazmaqda çətin bir şey yoxdur, mən bunu müzakirə etməyəcəyəm. Bunun əvəzinə standart davranışlar üçün güclü spesifikasiyaların yazılması haqqında danışacağıq. Təhlükəsizlik xassəsindən istifadə edərək hər hansı bir davranış dəstinin təsvir oluna biləcəyini söyləyən bir teorem var (təhlükəsizlik) və sağ qalma xüsusiyyətləri (canlılıq). Təhlükəsizlik o deməkdir ki, pis bir şey olmayacaq, proqram səhv cavab verməyəcək. Sağ qalma o deməkdir ki, gec-tez yaxşı bir şey olacaq, yəni proqram gec-tez düzgün cavab verəcəkdir. Bir qayda olaraq, təhlükəsizlik daha vacib bir göstəricidir, səhvlər ən çox burada baş verir. Buna görə də, vaxta qənaət etmək üçün, əlbəttə ki, vacib olsa da, sağ qalma haqqında danışmayacağam.
Biz ilk növbədə mümkün ilkin vəziyyətlər toplusunu təyin etməklə təhlükəsizliyə nail oluruq. İkincisi, hər bir dövlət üçün mümkün olan bütün sonrakı dövlətlərlə əlaqələr. Gəlin alim kimi davranaq və dövlətləri riyazi olaraq təyin edək. İlkin vəziyyətlər dəsti, məsələn, Evklid alqoritmi vəziyyətində bir düsturla təsvir edilir: (x = M) ∧ (y = N). Müəyyən dəyərlər üçün M и N yalnız bir başlanğıc vəziyyəti var. Növbəti vəziyyətlə əlaqə, növbəti vəziyyətin dəyişənlərinin sadə, cari vəziyyətin dəyişənlərinin isə əsas olmadan yazıldığı düsturla təsvir edilir. Evklid alqoritmi vəziyyətində biz iki düsturun diszyunkasiyası ilə məşğul olacağıq, onlardan birində x ən böyük dəyərdir, ikincidə isə - y:
Birinci halda y-nin yeni qiyməti y-nin əvvəlki qiymətinə bərabərdir və kiçik dəyişəni böyük dəyişəndən çıxarmaqla x-in yeni qiymətini alırıq. İkinci halda, biz bunun əksini edirik.
Yevklidin alqoritminə qayıdaq. Bir daha güman edək ki M = 12, N = 18. Bu, vahid ilkin vəziyyəti müəyyən edir, (x = 12) ∧ (y = 18). Sonra həmin dəyərləri yuxarıdakı düstura daxil edirik və əldə edirik:
Budur yeganə mümkün həll: x' = 18 - 12 ∧ y' = 12və davranışı əldə edirik: [x = 12, y = 18]. Eynilə, davranışımızdakı bütün vəziyyətləri təsvir edə bilərik: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
Son vəziyyətdə [x = 6, y = 6] ifadənin hər iki hissəsi yalan olacaq, ona görə də onun növbəti vəziyyəti yoxdur. Beləliklə, biz ikinci addımın tam spesifikasiyasına sahibik - gördüyünüz kimi, bu, mühəndislər və alimlərdəki kimi olduqca adi riyaziyyatdır və kompüter elmindəki kimi qəribə deyil.
Bu iki formul müvəqqəti məntiqin bir formulunda birləşdirilə bilər. O, zərif və izah etmək asandır, lakin indi onun üçün vaxt yoxdur. Bizə müvəqqəti məntiq yalnız canlılıq xüsusiyyəti üçün lazım ola bilər, təhlükəsizlik üçün lazım deyil. Mən müvəqqəti məntiqi belə sevmirəm, bu, adi riyaziyyat deyil, amma canlılıq baxımından bu, zəruri bir pislikdir.
Evklid alqoritmində hər bir dəyər üçün x и y unikal dəyərlərə malikdir x' и y', növbəti vəziyyətlə əlaqəni doğru edən. Başqa sözlə, Evklidin alqoritmi deterministikdir. Qeyri-deterministik alqoritmi modelləşdirmək üçün cari vəziyyətin çoxlu mümkün gələcək vəziyyətləri olmalıdır və hər bir təyin olunmamış dəyişən dəyərinin növbəti vəziyyətlə əlaqəsi doğru olduğu üçün çoxlu əsaslı dəyişən qiymətləri olmalıdır. Bunu etmək asandır, amma indi nümunələr verməyəcəyəm.
İş aləti hazırlamaq üçün sizə rəsmi riyaziyyat lazımdır. Spesifikasiyanı necə rəsmiləşdirmək olar? Bunun üçün bizə rəsmi dil lazımdır, məsələn, . Evklid alqoritminin spesifikasiyası bu dildə belə görünür:
Üçbucaqlı bərabər işarə simvolu o deməkdir ki, işarənin solunda olan qiymət işarənin sağındakı qiymətə bərabərdir. Əslində, spesifikasiya bir tərifdir, bizim vəziyyətimizdə iki tərifdir. TLA+-da spesifikasiyaya yuxarıdakı slaydda olduğu kimi bəyannamələr və bəzi sintaksis əlavə etməlisiniz. ASCII-də bu belə görünür:
Gördüyünüz kimi, mürəkkəb bir şey yoxdur. TLA+ üçün spesifikasiya sınaqdan keçirilə bilər, yəni kiçik bir modeldə bütün mümkün davranışlardan yan keçə bilər. Bizim vəziyyətimizdə bu model müəyyən dəyərlər olacaq M и N. Bu, tamamilə avtomatik olan çox səmərəli və sadə yoxlama üsuludur. Formal həqiqət sübutlarını yazmaq və onları mexaniki şəkildə yoxlamaq da mümkündür, lakin bu çox vaxt aparır, ona görə də demək olar ki, heç kim bunu etmir.
TLA+-nın əsas çatışmazlığı onun riyaziyyat olmasıdır və proqramçılar və kompüter alimləri riyaziyyatdan qorxurlar. İlk baxışdan bu zarafat kimi səslənir, amma təəssüf ki, bütün ciddiliyimlə bunu nəzərdə tuturam. Həmkarım sadəcə mənə TLA+-nı bir neçə tərtibatçıya necə izah etməyə çalışdığını danışırdı. Formullar ekranda görünən kimi dərhal şüşə kimi gözlərə çevrildi. Beləliklə, TLA+ sizi qorxudursa, istifadə edə bilərsiniz , bir növ oyuncaq proqramlaşdırma dilidir. PlusCal-dakı ifadə istənilən TLA+ ifadəsi ola bilər, yəni hər hansı riyazi ifadə ola bilər. Bundan əlavə, PlusCal qeyri-deterministik alqoritmlər üçün sintaksisə malikdir. PlusCal istənilən TLA+ ifadəsini yaza bildiyi üçün PlusCal istənilən real proqramlaşdırma dilindən daha ifadəlidir. Bundan sonra PlusCal asanlıqla oxuna bilən TLA+ spesifikasiyasına tərtib edilir. Bu, əlbəttə ki, mürəkkəb PlusCal spesifikasiyasının TLA+-da sadə birinə çevriləcəyi demək deyil - sadəcə aralarındakı yazışmalar göz qabağındadır, əlavə mürəkkəblik olmayacaq. Nəhayət, bu spesifikasiya TLA+ alətləri ilə yoxlanıla bilər. Bütövlükdə, PlusCal riyaziyyat fobiyasını aradan qaldırmağa kömək edə bilər və hətta proqramçılar və kompüter alimləri üçün də başa düşülməsi asandır. Keçmişdə bir müddət (təxminən 10 il) onun üzərində alqoritmlər dərc etmişdim.
Bəlkə kimsə etiraz edəcək ki, TLA+ və PlusCal riyaziyyatdır və riyaziyyat yalnız icad edilmiş nümunələr üzərində işləyir. Praktikada növləri, prosedurları, obyektləri və s. olan real dil lazımdır. Bu səhvdir. Amazonda işləyən Chris Newcomb yazır: “Biz TLA+-dan on böyük layihədə istifadə etdik və hər bir halda ondan istifadə inkişafda əhəmiyyətli fərq yaratdı, çünki istehsala başlamazdan əvvəl təhlükəli səhvləri tuta bildik və bu, bizə lazım olan fikir və əminliyi verdi. proqramın həqiqətinə təsir etmədən aqressiv performans optimallaşdırmaları edin". Tez-tez eşitmək olar ki, formal metodlardan istifadə edərkən biz səmərəsiz kod alırıq - praktikada hər şey tam əksinədir. Bundan əlavə, belə bir fikir var ki, proqramçılar onların faydalılığına əmin olsalar belə, menecerləri formal metodların zəruriliyinə inandırmaq olmaz. Və Newcomb yazır: "Menecerlər indi TLA + üçün spesifikasiyaları yazmağa və xüsusi olaraq bunun üçün vaxt ayırmağa çalışırlar". Beləliklə, menecerlər TLA+ işlədiyini görəndə bunu məmnuniyyətlə qəbul edirlər. Chris Newcomb bunu təxminən altı ay əvvəl (oktyabr 2014) yazmışdı, amma indi bildiyimə görə, TLA+ 14 deyil, 10 layihədə istifadə olunur. Başqa bir misal XBox 360 dizaynındadır. Təcrübəçi Çarlz Tekerə gəldi və yaddaş sistemi üçün spesifikasiya yazdı. Bu spesifikasiya sayəsində, əks halda diqqətdən kənarda qalacaq bir səhv tapıldı və buna görə də hər XBox 360 dörd saat istifadədən sonra qəzaya uğrayacaq. IBM mühəndisləri testlərinin bu səhvi tapmayacağını təsdiqləyiblər.
İnternetdə TLA+ haqqında daha çox oxuya bilərsiniz, lakin indi qeyri-rəsmi spesifikasiyalar haqqında danışaq. Biz nadir hallarda ən kiçik ümumi bölücünü hesablayan proqramlar yazmalıyıq. Çox vaxt biz TLA+ üçün yazdığım gözəl printer aləti kimi proqramlar yazırıq. Ən sadə emaldan sonra TLA + kodu belə görünəcək:
Lakin yuxarıdakı misalda istifadəçi çox güman ki, birləşmə və bərabər işarələrin uyğunlaşdırılmasını istəyir. Beləliklə, düzgün formatlaşdırma daha çox belə görünür:
Başqa bir nümunəni nəzərdən keçirək:
Burada isə əksinə, mənbədə bərabərlik, toplama və vurma işarələrinin düzülüşü təsadüfi olduğundan, ən sadə emal kifayət qədər kifayətdir. Ümumiyyətlə, düzgün formatlaşdırmanın dəqiq riyazi tərifi yoxdur, çünki "düzgün" bu halda "istifadəçinin istədiyi" deməkdir və bunu riyazi olaraq təyin etmək mümkün deyil.
Belə görünür ki, əgər bizdə həqiqətin tərifi yoxdursa, spesifikasiya faydasızdır. Amma elə deyil. Proqramın nə etməli olduğunu bilməməyimiz o demək deyil ki, onun necə işlədiyi barədə düşünməyə ehtiyac yoxdur, əksinə, biz ona daha çox səy göstərməliyik. Burada spesifikasiya xüsusilə vacibdir. Strukturlaşdırılmış çap üçün optimal proqramı müəyyən etmək mümkün deyil, lakin bu o demək deyil ki, biz onu ümumiyyətlə qəbul etməməliyik və şüur axını kimi kodu yazmaq yaxşı hal deyil. Sonda təriflərlə altı qaydadan ibarət spesifikasiya yazdım şərhlər şəklində java faylında. Qaydalardan birinin nümunəsi: a left-comment token is LeftComment aligned with its covering token. Bu qayda riyazi ingilis dilində, deyək ki, yazılıb: LeftComment aligned, left-comment и covering token - tərifləri olan terminlər. Riyaziyyatçılar riyaziyyatı belə təsvir edirlər: terminlərin təriflərini və onlara əsaslanaraq qaydaları yazırlar. Belə bir spesifikasiyanın üstünlüyü ondan ibarətdir ki, altı qayda 850 sətir koddan daha asan başa düşülür və sazlanır. Deməliyəm ki, bu qaydaları yazmaq asan deyildi, onları aradan qaldırmaq üçün kifayət qədər vaxt lazım idi. Xüsusilə bu məqsədlə hansı qaydadan istifadə edildiyini bildirən bir kod yazdım. Bu altı qaydanı bir neçə misalda sınaqdan keçirdiyim üçün 850 sətir kodu ayırmaq məcburiyyətində qalmadım və səhvləri tapmaq olduqca asan oldu. Java-nın bunun üçün əla alətləri var. Əgər kodu təzəcə yazsaydım, bu, mənim üçün çox vaxt aparardı və formatlaşdırma daha keyfiyyətsiz olardı.
Niyə rəsmi spesifikasiyadan istifadə oluna bilmədi? Bir tərəfdən burada düzgün icra çox da vacib deyil. Struktur çaplar heç kimə xoş gəlmir, ona görə də bütün qeyri-adi vəziyyətlərdə düzgün işləmək məcburiyyətində deyildim. Daha da vacibi odur ki, mənim adekvat alətlərim yox idi. TLA+ model yoxlayıcısı burada yararsızdır, ona görə də nümunələri əl ilə yazmalıyam.
Yuxarıdakı spesifikasiya bütün spesifikasiyalar üçün ümumi xüsusiyyətlərə malikdir. Bu koddan daha yüksək səviyyədədir. İstənilən dildə həyata keçirilə bilər. Onu yazmaq üçün heç bir vasitə və ya üsul faydasızdır. Heç bir proqramlaşdırma kursu bu spesifikasiyanı yazmağınıza kömək etməyəcək. Əlbəttə ki, siz TLA+-da strukturlaşdırılmış çap proqramlarının yazılması üçün xüsusi dil yazmırsınızsa, bu spesifikasiyanı lazımsız hala gətirə biləcək heç bir alət yoxdur. Nəhayət, bu spesifikasiya kodu tam olaraq necə yazacağımız haqqında heç nə demir, yalnız bu kodun nə etdiyini bildirir. Kod haqqında düşünməyə başlamazdan əvvəl problem üzərində düşünməyə kömək etmək üçün spesifikasiyanı yazırıq.
Lakin bu spesifikasiyanın digər spesifikasiyalardan fərqləndirən xüsusiyyətləri də var. Digər spesifikasiyaların 95%-i əhəmiyyətli dərəcədə daha qısa və sadədir:
Bundan əlavə, bu spesifikasiya qaydalar toplusudur. Bir qayda olaraq, bu zəif spesifikasiyanın əlamətidir. Qaydalar toplusunun nəticələrini başa düşmək olduqca çətindir, buna görə də onları aradan qaldırmaq üçün çox vaxt sərf etməli oldum. Ancaq bu vəziyyətdə daha yaxşı bir yol tapa bilmədim.
Davamlı işləyən proqramlar haqqında bir neçə söz söyləməyə dəyər. Bir qayda olaraq, onlar paralel işləyirlər, məsələn, əməliyyat sistemləri və ya paylanmış sistemlər. Çox az adam onları əqli və ya kağız üzərində başa düşə bilər və mən onlardan deyiləm, baxmayaraq ki, bir vaxtlar bunu bacarmışam. Buna görə də, işimizi yoxlayacaq vasitələrə ehtiyacımız var - məsələn, TLA + və ya PlusCal.
Əgər kodun dəqiq nə etməli olduğunu bilirdimsə, niyə spesifikasiya yazmaq lazım idi? Əslində, mən sadəcə bildiyimi düşündüm. Bundan əlavə, bir spesifikasiya ilə, kənar adamın tam olaraq nə etdiyini başa düşmək üçün artıq koda daxil olmağa ehtiyac yoxdur. Mənim bir qaydam var: ümumi qaydalar olmamalıdır. Bu qaydanın bir istisnası var, əlbəttə ki, bu, mənim əməl etdiyim yeganə ümumi qaydadır: kodun nə etdiyinin spesifikasiyası insanlara koddan istifadə edərkən bilməli olduqları hər şeyi söyləməlidir.
Beləliklə, proqramçılar düşüncə haqqında tam olaraq nəyi bilməlidirlər? Başlayanlar üçün, hamı kimi: yazmırsınızsa, o zaman sizə yalnız düşündüyünüz görünür. Həmçinin, kodlaşdırmadan əvvəl düşünmək lazımdır, yəni kodlaşdırmadan əvvəl yazmaq lazımdır. Spesifikasiya kodlaşdırmaya başlamazdan əvvəl yazdığımız şeydir. Hər kəs tərəfindən istifadə edilə və ya dəyişdirilə bilən hər hansı kod üçün spesifikasiya tələb olunur. Və bu “kimsə” kod yazıldıqdan bir ay sonra onun müəllifi ola bilər. Böyük proqramlar və sistemlər, siniflər, metodlar və bəzən hətta bir metodun mürəkkəb bölmələri üçün spesifikasiya tələb olunur. Kod haqqında dəqiq nə yazılmalıdır? Bunun nə etdiyini, yəni bu kodu istifadə edən hər hansı bir şəxs üçün nəyin faydalı ola biləcəyini təsvir etməlisiniz. Bəzən kodun məqsədini necə yerinə yetirdiyini müəyyən etmək lazım ola bilər. Əgər biz alqoritmlərin gedişində bu üsuldan keçmişiksə, ona alqoritm deyirik. Əgər daha xüsusi və yeni bir şeydirsə, biz bunu yüksək səviyyəli dizayn adlandırırıq. Burada heç bir formal fərq yoxdur: hər ikisi proqramın mücərrəd modelidir.
Kod spesifikasiyasını tam olaraq necə yazmalısınız? Əsas odur ki, kodun özündən bir səviyyə yüksək olmalıdır. O, vəziyyətləri və davranışları təsvir etməlidir. Tapşırıq tələb etdiyi qədər ciddi olmalıdır. Əgər tapşırığın necə yerinə yetiriləcəyi ilə bağlı spesifikasiya yazırsanız, onu psevdokodda və ya PlusCal ilə yaza bilərsiniz. Siz formal spesifikasiyalara spesifikasiyaları yazmağı öyrənməlisiniz. Bu, sizə qeyri-rəsmi bacarıqlarla da kömək edəcək lazımi bacarıqları verəcəkdir. Rəsmi spesifikasiyaları yazmağı necə öyrənirsiniz? Biz proqramlaşdırmağı öyrənəndə proqramlar yazdıq və sonra onları sazladıq. Burada da eynidir: spesifikasiyanı yazın, model yoxlayıcı ilə yoxlayın və səhvləri düzəldin. TLA+ formal spesifikasiya üçün ən yaxşı dil olmaya bilər və başqa dil sizin xüsusi ehtiyaclarınız üçün daha yaxşı ola bilər. TLA+-ın üstünlüyü ondan ibarətdir ki, o, riyazi düşüncəni çox yaxşı öyrədir.
Spesifikasiya və kodu necə əlaqələndirmək olar? Riyazi anlayışları və onların həyata keçirilməsini əlaqələndirən şərhlərin köməyi ilə. Əgər siz qrafiklərlə işləyirsinizsə, onda proqram səviyyəsində qovşaq massivləri və bağlantı massivləri olacaq. Buna görə də qrafikin bu proqramlaşdırma strukturları tərəfindən necə həyata keçirildiyini dəqiq yazmalısınız.
Qeyd etmək lazımdır ki, yuxarıda göstərilənlərin heç biri kodun yazılmasının faktiki prosesinə aid deyil. Kodu yazanda, yəni üçüncü addımı yerinə yetirirsən, həm də proqram vasitəsilə düşünüb düşünmək lazımdır. Əgər alt tapşırığın mürəkkəb və ya qeyri-aşkar olduğu ortaya çıxarsa, onun üçün spesifikasiya yazmalısınız. Amma mən burada kodun özündən danışmıram. İstənilən proqramlaşdırma dilindən, istənilən metodologiyadan istifadə edə bilərsiniz, söhbət onlara aid deyil. Həmçinin, yuxarıda göstərilənlərin heç biri kodu sınamaq və sazlamaq ehtiyacını aradan qaldırmır. Abstrakt model düzgün yazılsa belə, onun həyata keçirilməsində səhvlər ola bilər.
Spesifikasiyaların yazılması kodlaşdırma prosesində əlavə bir addımdır. Bunun sayəsində bir çox səhvlər daha az səylə tutula bilər - biz bunu Amazon proqramçılarının təcrübəsindən bilirik. Spesifikasiyalarla proqramların keyfiyyəti daha yüksək olur. Bəs niyə biz tez-tez onlarsız gedirik? Çünki yazmaq çətindir. Yazmaq isə çətindir, çünki bunun üçün düşünmək lazımdır, düşünmək də çətindir. Düşündüyünüzü iddia etmək həmişə daha asandır. Burada qaçışla bir bənzətmə çəkə bilərsiniz - nə qədər az qaçsanız, bir o qədər yavaş qaçırsınız. Əzələlərinizi məşq etməli və yazı yazmağa məşq etməlisiniz. Təcrübə lazımdır.
Spesifikasiya səhv ola bilər. Siz haradasa səhv etmiş ola bilərsiniz və ya tələblər dəyişmiş ola bilər və ya təkmilləşdirmə tələb oluna bilər. Hər kəsin istifadə etdiyi hər hansı kod dəyişdirilməlidir, ona görə də gec-tez spesifikasiya artıq proqrama uyğun gəlməyəcək. İdeal olaraq, bu halda, yeni bir spesifikasiya yazmaq və kodu tamamilə yenidən yazmaq lazımdır. Biz yaxşı bilirik ki, bunu heç kim etmir. Təcrübədə biz kodu düzəldirik və ola bilsin spesifikasiyanı yeniləyirik. Əgər bu, gec-tez baş verəcəksə, onda niyə ümumiyyətlə spesifikasiyaları yazmaq lazımdır? Birincisi, kodunuzu redaktə edəcək şəxs üçün spesifikasiyadakı hər bir əlavə söz qızıl kimi dəyərli olacaq və bu şəxs siz özünüz ola bilərsiniz. Kodumu redaktə edərkən kifayət qədər spesifikasiya əldə etmədiyim üçün tez-tez özümü qınayıram. Mən koddan daha çox spesifikasiya yazıram. Buna görə də, kodu redaktə edərkən, spesifikasiya həmişə yenilənməlidir. İkincisi, hər düzəlişlə kod daha da pisləşir, oxumaq və saxlamaq getdikcə çətinləşir. Bu entropiyanın artmasıdır. Ancaq bir spesifikasiya ilə başlamasanız, onda yazdığınız hər sətir redaktə olacaq və kodu başdan oxumaq çətin və çətin olacaq.
Dedi , heç bir döyüş planla qalib gəlmədi və heç bir döyüş plansız qalib gəlmədi. Və döyüşlər haqqında bir-iki şey bilirdi. Spesifikasiyaların yazılması vaxt itkisi olduğuna dair bir fikir var. Bəzən bu doğrudur və tapşırıq o qədər sadədir ki, onun üzərində düşünmək üçün heç bir şey yoxdur. Ancaq həmişə yadda saxlamalısınız ki, sizə spesifikasiyaları yazmamağınız deyildikdə, düşünməməyiniz deyilir. Və hər dəfə bu barədə düşünməlisən. Tapşırığın üzərində düşünmək səhv etməyəcəyinizə zəmanət vermir. Bildiyimiz kimi, sehrli çubuğu heç kim icad etməyib və proqramlaşdırma çətin bir işdir. Ancaq problemi düşünməsəniz, səhvlərə yol verəcəyinizə zəmanət verilir.
TLA+ və PlusCal haqqında daha ətraflı xüsusi vebsaytda oxuya bilərsiniz, mənim ana səhifəmdən ora daxil ola bilərsiniz . Hamısı mənim üçündür, diqqətinizə görə təşəkkür edirəm.
Nəzərə alın ki, bu tərcümədir. Şərh yazarkən unutmayın ki, müəllif onları oxumayacaq. Əgər həqiqətən müəlliflə söhbət etmək istəyirsinizsə, o zaman o, 2019-11 iyul 12-cu il tarixlərində Sankt-Peterburqda keçiriləcək Hydra 2019 konfransında olacaq. Biletləri əldə etmək olar .
Mənbə: www.habr.com