Artikel ini adalah terjemahan . Tetapi sebelum dia pengenalan sedikit. Bagaimanakah zombi terbentuk? Semua orang mengalami situasi di mana mereka ingin menarik rakan atau rakan sekerja ke tahap mereka, tetapi ia tidak berjaya. Dan ia tidak begitu banyak dengan anda seperti dengan dia bahawa "ia tidak berjaya": pada satu sisi skala adalah gaji biasa, tugas, dan sebagainya, dan di sisi lain, keperluan untuk berfikir. Berfikir tidak menyenangkan dan menyakitkan. Dia cepat berputus asa dan terus menulis kod tanpa menghidupkan otaknya langsung. Anda bayangkan betapa banyak usaha yang diperlukan untuk mengatasi halangan ketidakberdayaan yang dipelajari, dan anda tidak melakukannya. Ini adalah bagaimana zombi terbentuk, yang, nampaknya, boleh disembuhkan, tetapi nampaknya tiada siapa yang akan melakukannya.
Apabila saya melihat itu (ya, rakan yang sama dari buku teks) dan tidak membuat laporan, tetapi sesi soal jawab, saya agak berhati-hati. Sekiranya berlaku, Leslie ialah seorang saintis yang terkenal di dunia, pengarang karya asas dalam pengkomputeran teragih, dan anda juga boleh mengenalinya dengan huruf La dalam perkataan LaTeX - "Lamport TeX". Faktor membimbangkan kedua ialah keperluannya: setiap orang yang datang mesti (benar-benar percuma) mendengar beberapa laporannya terlebih dahulu, mengemukakan sekurang-kurangnya satu soalan mengenainya, dan kemudian datang. Saya memutuskan untuk melihat apa yang disiarkan oleh Lamport di sana - dan ia hebat! Ia betul-betul perkara itu, pil pautan ajaib untuk menyembuhkan zombi. Saya memberi amaran kepada anda: dari teks, pencinta metodologi super-fleksibel dan mereka yang tidak suka menguji apa yang ditulis boleh terbakar.
Selepas habrokat, sebenarnya terjemahan seminar pun bermula. Selamat membaca!
Apa sahaja tugas yang anda pikul, anda sentiasa perlu melalui tiga langkah:
- tentukan matlamat yang ingin anda capai;
- tentukan bagaimana anda akan mencapai matlamat anda;
- datang ke matlamat anda.
Ini juga terpakai kepada pengaturcaraan. Apabila kita menulis kod, kita perlu:
- memutuskan apa yang perlu dilakukan oleh program;
- menentukan bagaimana ia harus melaksanakan tugasnya;
- tulis kod yang sepadan.
Langkah terakhir, sudah tentu, sangat penting, tetapi saya tidak akan bercakap mengenainya hari ini. Sebaliknya, kita akan membincangkan dua yang pertama. Setiap pengaturcara melaksanakannya sebelum mula bekerja. Anda tidak perlu duduk untuk menulis melainkan anda telah memutuskan sama ada anda menulis pelayar atau pangkalan data. Idea tertentu tentang matlamat mesti ada. Dan anda pasti memikirkan apa sebenarnya program itu akan lakukan, dan jangan menulis entah bagaimana dengan harapan bahawa kod itu entah bagaimana akan berubah menjadi penyemak imbas.
Bagaimanakah sebenarnya pra-pemikiran kod ini berlaku? Berapa banyak usaha yang perlu kita lakukan untuk ini? Semuanya bergantung pada betapa kompleksnya masalah yang kita selesaikan. Katakan kita ingin menulis sistem teragih bertolak ansur kesalahan. Dalam kes ini, kita harus memikirkan perkara dengan teliti sebelum kita duduk untuk membuat kod. Bagaimana jika kita hanya perlu menambah pembolehubah integer sebanyak 1? Pada pandangan pertama, segala-galanya adalah remeh di sini, dan tiada pemikiran diperlukan, tetapi kemudian kita ingat bahawa limpahan boleh berlaku. Oleh itu, walaupun untuk memahami sama ada masalah itu mudah atau kompleks, anda perlu berfikir terlebih dahulu.
Jika anda memikirkan penyelesaian yang mungkin untuk masalah itu terlebih dahulu, anda boleh mengelakkan kesilapan. Tetapi ini memerlukan pemikiran anda jelas. Untuk mencapai matlamat ini, anda perlu menulis pemikiran anda. Saya sangat suka petikan Dick Guindon: "Apabila anda menulis, alam semula jadi menunjukkan kepada anda betapa cerobohnya pemikiran anda." Jika anda tidak menulis, anda hanya berfikir bahawa anda sedang berfikir. Dan anda perlu menulis pemikiran anda dalam bentuk spesifikasi.
Spesifikasi melaksanakan banyak fungsi, terutamanya dalam projek besar. Tetapi saya hanya akan bercakap tentang salah satu daripada mereka: mereka membantu kita berfikir dengan jelas. Berfikir dengan jelas adalah sangat penting dan agak sukar, jadi di sini kami memerlukan sebarang bantuan. Dalam bahasa apa kita harus menulis spesifikasi? Secara umum, ini sentiasa menjadi soalan pertama untuk pengaturcara: bahasa apa yang akan kami tulis. Tidak ada jawapan yang betul untuknya: masalah yang kami selesaikan terlalu pelbagai. Bagi sesetengah orang, TLA+ ialah bahasa spesifikasi yang saya bangunkan. Bagi yang lain, lebih senang menggunakan bahasa Cina. Semuanya bergantung kepada keadaan.
Lebih penting ialah satu lagi soalan: bagaimana untuk mencapai pemikiran yang lebih jelas? Jawapan: Kita mesti berfikir seperti saintis. Ini adalah cara berfikir yang telah membuktikan dirinya sejak 500 tahun yang lalu. Dalam sains, kita membina model matematik realiti. Astronomi mungkin merupakan sains pertama dalam erti kata yang ketat. Dalam model matematik yang digunakan dalam astronomi, jasad angkasa muncul sebagai titik dengan jisim, kedudukan dan momentum, walaupun pada hakikatnya ia adalah objek yang sangat kompleks dengan gunung dan lautan, pasang surut dan pasang surut. Model ini, seperti yang lain, dicipta untuk menyelesaikan masalah tertentu. Ia bagus untuk menentukan ke mana hendak menghalakan teleskop jika anda perlu mencari planet. Tetapi jika anda ingin meramalkan cuaca di planet ini, model ini tidak akan berfungsi.
Matematik membolehkan kita menentukan sifat-sifat model. Dan sains menunjukkan bagaimana sifat-sifat ini berkaitan dengan realiti. Mari kita bercakap tentang sains kita, sains komputer. Realiti yang kami gunakan ialah sistem pengkomputeran pelbagai jenis: pemproses, konsol permainan, komputer, pelaksanaan program dan sebagainya. Saya akan bercakap tentang menjalankan program pada komputer, tetapi pada umumnya, semua kesimpulan ini digunakan untuk mana-mana sistem pengkomputeran. Dalam sains kami, kami menggunakan banyak model yang berbeza: mesin Turing, set acara yang dipesan separa dan banyak lagi.
Apakah program? Ini adalah sebarang kod yang boleh dipertimbangkan secara bebas. Katakan kita perlu menulis pelayar. Kami melaksanakan tiga tugas: kami mereka bentuk pandangan pengguna program, kemudian kami menulis rajah peringkat tinggi program, dan akhirnya kami menulis kod. Semasa kami menulis kod, kami menyedari bahawa kami perlu menulis pemformat teks. Di sini kita sekali lagi perlu menyelesaikan tiga masalah: tentukan teks apa yang akan dikembalikan oleh alat ini; pilih algoritma untuk pemformatan; tulis kod. Tugasan ini mempunyai subtugasnya sendiri: masukkan sempang ke dalam perkataan dengan betul. Kami juga menyelesaikan subtugas ini dalam tiga langkah - seperti yang anda lihat, ia diulang pada banyak peringkat.
Mari kita pertimbangkan dengan lebih terperinci langkah pertama: masalah apa yang diselesaikan oleh program. Di sini, kami paling kerap memodelkan program sebagai fungsi yang mengambil beberapa input dan menghasilkan beberapa output. Dalam matematik, fungsi biasanya digambarkan sebagai set pasangan tersusun. Sebagai contoh, fungsi kuasa dua untuk nombor asli diterangkan sebagai set {<0,0>, <1,1>, <2,4>, <3,9>, β¦}. Domain bagi fungsi sedemikian ialah set elemen pertama setiap pasangan, iaitu nombor asli. Untuk menentukan fungsi, kita perlu menentukan skop dan formulanya.
Tetapi fungsi dalam matematik tidak sama dengan fungsi dalam bahasa pengaturcaraan. Matematik lebih mudah. Oleh kerana saya tidak mempunyai masa untuk contoh yang rumit, mari kita pertimbangkan yang mudah: fungsi dalam C atau kaedah statik di Jawa yang mengembalikan pembahagi sepunya terbesar bagi dua integer. Dalam spesifikasi kaedah ini, kami akan menulis: mengira GCD(M,N) untuk hujah M ΠΈ NJika GCD(M,N) - fungsi yang domainnya ialah set pasangan integer, dan nilai pulangan ialah integer terbesar yang boleh dibahagikan dengan M ΠΈ N. Bagaimanakah model ini berkaitan dengan realiti? Model ini beroperasi pada integer, manakala dalam C atau Java kita mempunyai 32-bit int. Model ini membolehkan kita memutuskan sama ada algoritma itu betul GCD, tetapi ia tidak akan menghalang ralat limpahan. Ini memerlukan model yang lebih kompleks, yang tidak mempunyai masa.
Mari kita bincangkan tentang batasan fungsi sebagai model. Sesetengah program (seperti sistem pengendalian) tidak hanya mengembalikan nilai tertentu untuk argumen tertentu, ia boleh dijalankan secara berterusan. Selain itu, fungsi sebagai model tidak sesuai untuk langkah kedua: merancang cara menyelesaikan masalah. Isih cepat dan isih gelembung mengira fungsi yang sama, tetapi ia adalah algoritma yang berbeza sama sekali. Oleh itu, untuk menerangkan bagaimana matlamat program itu dicapai, saya menggunakan model yang berbeza, mari kita panggil model tingkah laku standard. Program di dalamnya diwakili sebagai satu set semua tingkah laku yang dibenarkan, setiap satunya, pada gilirannya, adalah urutan keadaan, dan keadaan adalah penetapan nilai kepada pembolehubah.
Mari lihat bagaimana rupa langkah kedua untuk algoritma Euclid. Kita perlu mengira GCD(M, N). Kami mulakan M sebagai xDan N sebagai y, kemudian tolak berulang kali pembolehubah yang lebih kecil ini daripada yang lebih besar sehingga sama. Contohnya, jika M = 12Dan N = 18, kita boleh menerangkan tingkah laku berikut:
[x = 12, y = 18] β [x = 12, y = 6] β [x = 6, y = 6]
Dan jika M = 0 ΠΈ N = 0? Sifar boleh dibahagikan dengan semua nombor, jadi tiada pembahagi terbesar dalam kes ini. Dalam keadaan ini, kita perlu kembali ke langkah pertama dan bertanya: adakah kita benar-benar perlu mengira GCD untuk nombor bukan positif? Jika ini tidak perlu, maka anda hanya perlu menukar spesifikasi.
Di sini kita harus membuat penyimpangan kecil tentang produktiviti. Ia selalunya diukur dalam bilangan baris kod yang ditulis setiap hari. Tetapi kerja anda adalah lebih berguna jika anda menyingkirkan sebilangan baris, kerana anda mempunyai lebih sedikit ruang untuk pepijat. Dan cara paling mudah untuk menyingkirkan kod adalah pada langkah pertama. Kemungkinan besar anda tidak memerlukan semua loceng dan wisel yang anda cuba laksanakan. Cara terpantas untuk memudahkan program dan menjimatkan masa adalah dengan tidak melakukan perkara yang tidak sepatutnya dilakukan. Langkah kedua ialah potensi kedua paling menjimatkan masa. Jika anda mengukur produktiviti dari segi garis yang ditulis, maka memikirkan cara untuk menyelesaikan tugas akan membuat anda kurang produktif, kerana anda boleh menyelesaikan masalah yang sama dengan kurang kod. Saya tidak dapat memberikan statistik yang tepat di sini, kerana saya tidak mempunyai cara untuk mengira bilangan baris yang saya tidak tulis kerana fakta bahawa saya menghabiskan masa pada spesifikasi, iaitu, pada langkah pertama dan kedua. Dan percubaan tidak boleh disediakan di sini sama ada, kerana dalam percubaan kami tidak mempunyai hak untuk menyelesaikan langkah pertama, tugas itu telah ditetapkan.
Sangat mudah untuk mengabaikan banyak kesukaran dalam spesifikasi tidak formal. Tidak ada yang sukar dalam menulis spesifikasi yang ketat untuk fungsi, saya tidak akan membincangkan perkara ini. Sebaliknya, kita akan bercakap tentang menulis spesifikasi yang kukuh untuk tingkah laku standard. Terdapat teorem yang mengatakan bahawa sebarang set tingkah laku boleh diterangkan menggunakan sifat keselamatan (keselamatan) dan sifat kebolehmandirian (kehidupan). Keselamatan bermakna tiada perkara buruk akan berlaku, program tidak akan memberikan jawapan yang salah. Kebolehtahanan bermakna lambat laun sesuatu yang baik akan berlaku, iaitu program akan memberikan jawapan yang betul lambat laun. Sebagai peraturan, keselamatan adalah penunjuk yang lebih penting, ralat paling kerap berlaku di sini. Oleh itu, untuk menjimatkan masa, saya tidak akan bercakap tentang kemandirian, walaupun ia, tentu saja, juga penting.
Kami mencapai keselamatan dengan menetapkan, pertama, set keadaan awal yang mungkin. Dan kedua, hubungan dengan semua kemungkinan negeri seterusnya untuk setiap negeri. Mari kita bertindak seperti saintis dan mentakrifkan keadaan secara matematik. Set keadaan awal diterangkan oleh formula, sebagai contoh, dalam kes algoritma Euclid: (x = M) β§ (y = N). Untuk nilai tertentu M ΠΈ N hanya terdapat satu keadaan awal. Hubungan dengan keadaan seterusnya diterangkan dengan formula di mana pembolehubah keadaan seterusnya ditulis dengan perdana, dan pembolehubah keadaan semasa ditulis tanpa perdana. Dalam kes algoritma Euclid, kita akan berurusan dengan pemisahan dua formula, dalam satu daripadanya x adalah nilai terbesar, dan dalam kedua - y:
Dalam kes pertama, nilai baru y adalah sama dengan nilai sebelumnya y, dan kita mendapat nilai baru x dengan menolak pembolehubah yang lebih kecil daripada yang lebih besar. Dalam kes kedua, kita melakukan sebaliknya.
Mari kita kembali kepada algoritma Euclid. Mari kita andaikan sekali lagi M = 12, N = 18. Ini mentakrifkan satu keadaan awal, (x = 12) β§ (y = 18). Kami kemudian masukkan nilai tersebut ke dalam formula di atas dan dapatkan:
Inilah satu-satunya penyelesaian yang mungkin: x' = 18 - 12 β§ y' = 12dan kami mendapat tingkah laku: [x = 12, y = 18]. Begitu juga, kita boleh menerangkan semua keadaan dalam tingkah laku kita: [x = 12, y = 18] β [x = 12, y = 6] β [x = 6, y = 6].
Dalam keadaan terakhir [x = 6, y = 6] kedua-dua bahagian ungkapan akan palsu, jadi ia tidak mempunyai keadaan seterusnya. Jadi, kami mempunyai spesifikasi lengkap langkah kedua - seperti yang anda lihat, ini adalah matematik yang agak biasa, seperti dalam jurutera dan saintis, dan tidak pelik, seperti dalam sains komputer.
Kedua-dua formula ini boleh digabungkan menjadi satu formula logik temporal. Dia elegan dan mudah untuk dijelaskan, tetapi tidak ada masa untuknya sekarang. Kita mungkin memerlukan logik temporal hanya untuk harta keceriaan, ia tidak diperlukan untuk keselamatan. Saya tidak suka logik temporal seperti itu, ia bukan matematik biasa, tetapi dalam kes kemeriahan ia adalah kejahatan yang perlu.
Dalam algoritma Euclid, untuk setiap nilai x ΠΈ y mempunyai nilai yang unik x' ΠΈ y', yang menjadikan hubungan dengan keadaan seterusnya benar. Dengan kata lain, algoritma Euclid adalah deterministik. Untuk memodelkan algoritma bukan deterministik, keadaan semasa perlu mempunyai berbilang keadaan masa hadapan yang mungkin, dan setiap nilai pembolehubah tidak prima mempunyai berbilang nilai pembolehubah prima supaya perkaitan dengan keadaan seterusnya adalah benar. Ini mudah dilakukan, tetapi saya tidak akan memberikan contoh sekarang.
Untuk membuat alat kerja, anda memerlukan matematik formal. Bagaimana untuk membuat spesifikasi formal? Untuk melakukan ini, kita memerlukan bahasa formal, contohnya, . Spesifikasi algoritma Euclid akan kelihatan seperti ini dalam bahasa ini:
Simbol tanda sama dengan segitiga bermakna nilai di sebelah kiri tanda ditakrifkan sama dengan nilai di sebelah kanan tanda. Pada dasarnya, spesifikasi adalah definisi, dalam kes kami dua definisi. Untuk spesifikasi dalam TLA+, anda perlu menambah pengisytiharan dan beberapa sintaks, seperti dalam slaid di atas. Dalam ASCII ia akan kelihatan seperti ini:
Seperti yang anda lihat, tiada yang rumit. Spesifikasi untuk TLA+ boleh diuji, iaitu memintas semua tingkah laku yang mungkin dalam model kecil. Dalam kes kami, model ini akan menjadi nilai tertentu M ΠΈ N. Ini adalah kaedah pengesahan yang sangat cekap dan mudah yang sepenuhnya automatik. Anda juga boleh menulis bukti kebenaran rasmi dan menyemaknya secara mekanikal, tetapi ini memerlukan banyak masa, jadi hampir tiada siapa yang melakukan ini.
Kelemahan utama TLA+ ialah ia adalah matematik, dan pengaturcara dan saintis komputer takut dengan matematik. Pada pandangan pertama, ini terdengar seperti jenaka, tetapi, malangnya, saya maksudkannya dengan serius. Rakan sekerja saya hanya memberitahu saya cara dia cuba menerangkan TLA+ kepada beberapa pembangun. Sebaik sahaja formula itu muncul di skrin, mereka serta-merta menjadi mata berkaca. Jadi jika TLA+ menakutkan anda, anda boleh gunakan , ia adalah sejenis bahasa pengaturcaraan mainan. Ungkapan dalam PlusCal boleh menjadi sebarang ungkapan TLA+, iaitu, secara umumnya, sebarang ungkapan matematik. Selain itu, PlusCal mempunyai sintaks untuk algoritma bukan deterministik. Kerana PlusCal boleh menulis sebarang ungkapan TLA+, PlusCal jauh lebih ekspresif daripada mana-mana bahasa pengaturcaraan sebenar. Seterusnya, PlusCal disusun menjadi spesifikasi TLA+ yang mudah dibaca. Ini tidak bermakna, sudah tentu, spesifikasi PlusCal yang kompleks akan berubah menjadi yang mudah pada TLA + - hanya surat-menyurat di antara mereka yang jelas, tidak akan ada kerumitan tambahan. Akhir sekali, spesifikasi ini boleh disahkan oleh alat TLA+. Secara keseluruhan, PlusCal boleh membantu mengatasi fobia matematik dan mudah difahami walaupun untuk pengaturcara dan saintis komputer. Pada masa lalu, saya menerbitkan algoritma padanya untuk beberapa waktu (kira-kira 10 tahun).
Mungkin seseorang akan membantah bahawa TLA + dan PlusCal adalah matematik, dan matematik hanya berfungsi pada contoh yang dicipta. Dalam amalan, anda memerlukan bahasa sebenar dengan jenis, prosedur, objek, dan sebagainya. Ini adalah salah. Inilah yang ditulis oleh Chris Newcomb, yang bekerja di Amazon: βKami telah menggunakan TLA+ pada sepuluh projek utama, dan dalam setiap kes ia telah membuat perbezaan yang ketara kepada pembangunan kerana kami dapat menangkap pepijat berbahaya sebelum kami mencapai pengeluaran, dan kerana ia memberi kami wawasan dan keyakinan yang kami perlukan untuk membuat prestasi agresif pengoptimuman tanpa menjejaskan kebenaran program". Anda sering mendengar bahawa apabila menggunakan kaedah formal, kami mendapat kod yang tidak cekap - dalam amalan, semuanya betul-betul bertentangan. Di samping itu, terdapat pendapat bahawa pengurus tidak dapat diyakinkan tentang keperluan untuk kaedah formal, walaupun pengaturcara yakin akan kegunaannya. Dan Newcomb menulis: "Pengurus kini berusaha keras untuk menulis spesifikasi untuk TLA +, dan secara khusus memperuntukkan masa untuk ini". Oleh itu, apabila pengurus melihat bahawa TLA+ berfungsi, mereka dengan senang hati menerimanya. Chris Newcomb menulis ini kira-kira enam bulan yang lalu (Oktober 2014), tetapi kini, sejauh yang saya tahu, TLA+ digunakan dalam 14 projek, bukan 10. Contoh lain berkaitan dengan reka bentuk XBox 360. Seorang pelatih datang ke Charles Thacker dan menulis spesifikasi untuk sistem ingatan. Terima kasih kepada spesifikasi ini, pepijat ditemui yang sebaliknya tidak akan disedari, dan kerana itu setiap XBox 360 akan ranap selepas empat jam digunakan. Jurutera IBM mengesahkan bahawa ujian mereka tidak akan menemui pepijat ini.
Anda boleh membaca lebih lanjut mengenai TLA + di Internet, tetapi sekarang mari kita bercakap tentang spesifikasi tidak formal. Kami jarang perlu menulis program yang mengira pembahagi paling tidak biasa dan seumpamanya. Lebih kerap kita menulis program seperti alat pencetak cantik yang saya tulis untuk TLA+. Selepas pemprosesan yang paling mudah, kod TLA + akan kelihatan seperti ini:
Tetapi dalam contoh di atas, pengguna berkemungkinan besar mahu kata hubung dan tanda sama diselaraskan. Jadi pemformatan yang betul akan kelihatan lebih seperti ini:
Mari kita pertimbangkan contoh lain:
Di sini, sebaliknya, penjajaran tanda sama, penambahan, dan pendaraban dalam sumber adalah rawak, jadi pemprosesan paling mudah sudah cukup. Secara umum, tiada definisi matematik yang tepat bagi pemformatan yang betul, kerana "betul" dalam kes ini bermaksud "apa yang pengguna mahu", dan ini tidak boleh ditentukan secara matematik.
Nampaknya jika kita tidak mempunyai definisi kebenaran, maka spesifikasi itu tidak berguna. Tetapi tidak. Hanya kerana kita tidak tahu apa yang sepatutnya dilakukan oleh sesuatu program tidak bermakna kita tidak perlu memikirkan cara ia berfungsiβsebaliknya, kita perlu berusaha lebih keras ke dalamnya. Spesifikasi amat penting di sini. Adalah mustahil untuk menentukan program optimum untuk percetakan berstruktur, tetapi ini tidak bermakna kita tidak boleh mengambilnya sama sekali, dan menulis kod sebagai aliran kesedaran bukanlah perkara yang baik. Pada akhirnya, saya menulis spesifikasi enam peraturan dengan definisi dalam bentuk komen dalam fail java. Berikut adalah contoh salah satu peraturan: a left-comment token is LeftComment aligned with its covering token. Peraturan ini ditulis dalam, bolehkah kita katakan, bahasa Inggeris matematik: LeftComment aligned, left-comment ΠΈ covering token - istilah dengan definisi. Beginilah cara ahli matematik menerangkan matematik: mereka menulis definisi istilah dan, berdasarkannya, peraturan. Faedah spesifikasi sedemikian ialah enam peraturan lebih mudah difahami dan nyahpepijat daripada 850 baris kod. Saya mesti mengatakan bahawa menulis peraturan ini tidak mudah, ia mengambil masa yang agak lama untuk menyahpepijatnya. Terutama untuk tujuan ini, saya menulis kod yang melaporkan peraturan yang digunakan. Terima kasih kepada fakta bahawa saya telah menguji enam peraturan ini pada beberapa contoh, saya tidak perlu menyahpepijat 850 baris kod, dan pepijat ternyata agak mudah dicari. Java mempunyai alat yang hebat untuk ini. Jika saya baru sahaja menulis kod itu, saya akan mengambil masa yang lebih lama, dan pemformatan akan menjadi lebih berkualiti.
Mengapakah spesifikasi formal tidak boleh digunakan? Di satu pihak, pelaksanaan yang betul tidak terlalu penting di sini. Cetakan struktur pasti tidak menggembirakan sesiapa pun, jadi saya tidak perlu membuatnya berfungsi dengan betul dalam semua situasi ganjil. Lebih penting lagi ialah hakikat bahawa saya tidak mempunyai alat yang mencukupi. Pemeriksa model TLA+ tidak berguna di sini, jadi saya perlu menulis contoh secara manual.
Spesifikasi di atas mempunyai ciri yang sama dengan semua spesifikasi. Ia adalah tahap yang lebih tinggi daripada kod. Ia boleh dilaksanakan dalam mana-mana bahasa. Sebarang alat atau kaedah tidak berguna untuk menulisnya. Tiada kursus pengaturcaraan akan membantu anda menulis spesifikasi ini. Dan tiada alat yang boleh menjadikan spesifikasi ini tidak diperlukan, melainkan, sudah tentu, anda menulis bahasa khusus untuk menulis program cetakan berstruktur dalam TLA+. Akhir sekali, spesifikasi ini tidak menyatakan apa-apa tentang bagaimana tepatnya kita akan menulis kod, ia hanya menyatakan apa yang dilakukan oleh kod ini. Kami menulis spesifikasi untuk membantu kami memikirkan masalah sebelum kami mula memikirkan kod tersebut.
Tetapi spesifikasi ini juga mempunyai ciri-ciri yang membezakannya daripada spesifikasi lain. 95% daripada spesifikasi lain adalah jauh lebih pendek dan lebih ringkas:
Selanjutnya, spesifikasi ini adalah satu set peraturan. Sebagai peraturan, ini adalah tanda spesifikasi yang lemah. Memahami akibat set peraturan agak sukar, itulah sebabnya saya terpaksa menghabiskan banyak masa menyahpepijat peraturan itu. Walau bagaimanapun, dalam kes ini, saya tidak dapat mencari jalan yang lebih baik.
Ia bernilai mengatakan beberapa perkataan tentang program yang berjalan secara berterusan. Sebagai peraturan, mereka berfungsi secara selari, sebagai contoh, sistem pengendalian atau sistem teragih. Sangat sedikit orang yang boleh memahami mereka secara mental atau di atas kertas, dan saya bukan salah seorang daripada mereka, walaupun saya pernah dapat melakukannya. Oleh itu, kami memerlukan alat yang akan menyemak kerja kami - contohnya, TLA + atau PlusCal.
Mengapa perlu menulis spesifikasi jika saya sudah tahu apa sebenarnya yang perlu dilakukan oleh kod itu? Sebenarnya, saya hanya fikir saya tahu. Di samping itu, dengan spesifikasi, orang luar tidak lagi perlu masuk ke dalam kod untuk memahami apa sebenarnya yang dia lakukan. Saya mempunyai peraturan: tidak sepatutnya ada peraturan am. Terdapat pengecualian kepada peraturan ini, sudah tentu, ia adalah satu-satunya peraturan umum yang saya ikuti: spesifikasi perkara yang dilakukan oleh kod harus memberitahu orang semua yang mereka perlu tahu apabila menggunakan kod tersebut.
Jadi apa sebenarnya yang perlu diketahui oleh pengaturcara tentang pemikiran? Sebagai permulaan, sama seperti orang lain: jika anda tidak menulis, maka nampaknya anda hanya berfikir. Selain itu, anda perlu berfikir sebelum anda membuat kod, yang bermaksud anda perlu menulis sebelum anda membuat kod. Spesifikasi adalah apa yang kita tulis sebelum kita mula mengekod. Spesifikasi diperlukan untuk sebarang kod yang boleh digunakan atau diubah suai oleh sesiapa sahaja. Dan "seseorang" ini mungkin pengarang kod itu sendiri sebulan selepas ia ditulis. Spesifikasi diperlukan untuk program dan sistem yang besar, untuk kelas, untuk kaedah, dan kadang-kadang juga untuk bahagian kompleks bagi satu kaedah. Apa sebenarnya yang perlu ditulis tentang kod itu? Anda perlu menerangkan apa yang ia lakukan, iaitu, apa yang boleh berguna kepada mana-mana orang yang menggunakan kod ini. Kadangkala ia juga mungkin perlu untuk menentukan cara kod mencapai tujuannya. Jika kita melalui kaedah ini dalam perjalanan algoritma, maka kita memanggilnya algoritma. Jika ia sesuatu yang lebih istimewa dan baharu, maka kami memanggilnya reka bentuk peringkat tinggi. Tiada perbezaan formal di sini: kedua-duanya adalah model abstrak program.
Bagaimana sebenarnya anda harus menulis spesifikasi kod? Perkara utama: ia sepatutnya satu tahap lebih tinggi daripada kod itu sendiri. Ia harus menggambarkan keadaan dan tingkah laku. Ia harus seketat yang diperlukan oleh tugas. Jika anda menulis spesifikasi untuk cara sesuatu tugasan dilaksanakan, anda boleh menulisnya dalam pseudokod atau dengan PlusCal. Anda perlu belajar cara menulis spesifikasi pada spesifikasi formal. Ini akan memberi anda kemahiran yang diperlukan yang akan membantu anda dengan yang tidak formal juga. Bagaimanakah anda belajar menulis spesifikasi formal? Apabila kami belajar memprogram, kami menulis program dan kemudian menyahpenyahnya. Perkara yang sama di sini: tulis spesifikasi, semak dengan penyemak model dan betulkan pepijat. TLA+ mungkin bukan bahasa terbaik untuk spesifikasi formal dan bahasa lain mungkin lebih baik untuk keperluan khusus anda. Kelebihan TLA+ ialah ia mengajar pemikiran matematik dengan baik.
Bagaimana untuk memautkan spesifikasi dan kod? Dengan bantuan ulasan yang menghubungkan konsep matematik dan pelaksanaannya. Jika anda bekerja dengan graf, maka pada peringkat program anda akan mempunyai tatasusunan nod dan tatasusunan pautan. Oleh itu, anda perlu menulis dengan tepat bagaimana graf dilaksanakan oleh struktur pengaturcaraan ini.
Perlu diingatkan bahawa tiada satu pun perkara di atas terpakai untuk proses sebenar menulis kod. Apabila anda menulis kod, iaitu, anda melakukan langkah ketiga, anda juga perlu berfikir dan berfikir melalui program ini. Jika subtugasan ternyata rumit atau tidak jelas, anda perlu menulis spesifikasi untuknya. Tetapi saya tidak bercakap tentang kod itu sendiri di sini. Anda boleh menggunakan mana-mana bahasa pengaturcaraan, apa-apa metodologi, ia bukan tentang mereka. Selain itu, tiada satu pun di atas menghapuskan keperluan untuk menguji dan menyahpepijat kod. Walaupun model abstrak ditulis dengan betul, mungkin terdapat pepijat dalam pelaksanaannya.
Spesifikasi penulisan adalah langkah tambahan dalam proses pengekodan. Terima kasih kepadanya, banyak ralat boleh ditangkap dengan sedikit usaha - kami tahu ini daripada pengalaman pengaturcara dari Amazon. Dengan spesifikasi, kualiti program menjadi lebih tinggi. Jadi mengapa, kemudian, kita sering pergi tanpa mereka? Kerana menulis itu susah. Dan menulis adalah sukar, kerana untuk ini anda perlu berfikir, dan berfikir juga sukar. Ia sentiasa lebih mudah untuk berpura-pura apa yang anda fikirkan. Di sini anda boleh melukis analogi dengan berlari - semakin kurang anda berlari, semakin perlahan anda berlari. Anda perlu melatih otot anda dan berlatih menulis. Perlu latihan.
Spesifikasi mungkin tidak betul. Anda mungkin telah membuat kesilapan di suatu tempat, atau keperluan mungkin telah berubah, atau penambahbaikan mungkin perlu dibuat. Mana-mana kod yang digunakan oleh sesiapa sahaja perlu ditukar, jadi lambat laun spesifikasi tidak akan sepadan dengan program itu lagi. Sebaik-baiknya, dalam kes ini, anda perlu menulis spesifikasi baharu dan menulis semula kod sepenuhnya. Kami sangat tahu bahawa tiada siapa yang berbuat demikian. Dalam amalan, kami menampal kod dan mungkin mengemas kini spesifikasi. Jika ini pasti berlaku lambat laun, maka mengapa menulis spesifikasi sama sekali? Pertama, bagi orang yang akan mengedit kod anda, setiap perkataan tambahan dalam spesifikasi akan bernilai emas, dan orang ini mungkin anda sendiri. Saya sering memarahi diri saya sendiri kerana tidak mendapat spesifikasi yang mencukupi semasa saya mengedit kod saya. Dan saya menulis lebih banyak spesifikasi daripada kod. Oleh itu, apabila anda mengedit kod, spesifikasi sentiasa perlu dikemas kini. Kedua, dengan setiap semakan, kod menjadi lebih teruk, ia menjadi semakin sukar untuk dibaca dan diselenggara. Ini adalah peningkatan dalam entropi. Tetapi jika anda tidak bermula dengan spesifikasi, maka setiap baris yang anda tulis akan menjadi suntingan, dan kod itu akan menjadi sukar dan sukar dibaca dari awal.
Seperti yang dikatakan , tiada pertempuran yang dimenangi dengan rancangan, dan tiada pertempuran yang dimenangi tanpa rancangan. Dan dia tahu satu atau dua perkara tentang pertempuran. Terdapat pendapat bahawa spesifikasi penulisan adalah membuang masa. Kadang-kadang ini benar, dan tugasnya sangat mudah sehingga tiada apa-apa untuk difikirkan. Tetapi anda harus sentiasa ingat bahawa apabila anda diberitahu untuk tidak menulis spesifikasi, anda diberitahu untuk tidak berfikir. Dan anda harus memikirkannya setiap masa. Memikirkan tugas itu tidak menjamin bahawa anda tidak akan melakukan kesilapan. Seperti yang kita tahu, tiada siapa yang mencipta tongkat ajaib, dan pengaturcaraan adalah tugas yang sukar. Tetapi jika anda tidak memikirkan masalah itu, anda dijamin akan melakukan kesilapan.
Anda boleh membaca lebih lanjut mengenai TLA + dan PlusCal di tapak web khas, anda boleh pergi ke sana dari halaman utama saya . Itu sahaja untuk saya, terima kasih atas perhatian anda.
Sila ambil perhatian bahawa ini adalah terjemahan. Apabila anda menulis komen, ingat bahawa penulis tidak akan membacanya. Jika anda benar-benar ingin berbual dengan penulis, maka dia akan berada di persidangan Hydra 2019, yang akan diadakan pada 11-12 Julai 2019 di St. Tiket boleh dibeli .
Sumber: www.habr.com