Artikel ini adalah terjemahan . Tapi sebelum dia sedikit perkenalan. Bagaimana zombie terbentuk? Setiap orang mengalami situasi di mana mereka ingin menarik teman atau kolega ke level mereka, tetapi itu tidak berhasil. Dan bukan dengan Anda seperti dengan dia yang "tidak berhasil": di satu sisi skala adalah gaji normal, tugas, dan seterusnya, dan di sisi lain, kebutuhan untuk berpikir. Berpikir itu tidak menyenangkan dan menyakitkan. Dia cepat menyerah dan terus menulis kode tanpa memutar otaknya sama sekali. Anda membayangkan berapa banyak upaya yang diperlukan untuk mengatasi penghalang ketidakberdayaan yang dipelajari, dan Anda tidak melakukannya. Beginilah cara zombie terbentuk, yang sepertinya bisa disembuhkan, tapi sepertinya tidak ada yang mau melakukannya.
Ketika saya melihat itu (ya, kawan yang sama dari buku teks) dan tidak membuat laporan, melainkan sesi tanya jawab, saya sedikit was-was. Untuk berjaga-jaga, Leslie adalah seorang ilmuwan terkenal di dunia, penulis karya mendasar dalam komputasi terdistribusi, dan Anda juga dapat mengenalnya dengan huruf La dalam kata LaTeX - "Lamport TeX". Faktor mengkhawatirkan kedua adalah persyaratannya: setiap orang yang datang harus (benar-benar gratis) mendengarkan beberapa laporannya terlebih dahulu, mengajukan setidaknya satu pertanyaan tentangnya, dan baru kemudian datang. Saya memutuskan untuk melihat apa yang disiarkan Lamport di sana - dan itu bagus! Persis seperti itu, pil penghubung ajaib untuk menyembuhkan zombie. Saya peringatkan Anda: dari teks, pecinta metodologi yang sangat fleksibel dan mereka yang tidak suka menguji apa yang tertulis bisa sangat lelah.
Usai habrokat, sebenarnya penerjemahan seminar dimulai. Selamat membaca!
Apa pun tugas yang Anda lakukan, Anda harus selalu melalui tiga langkah:
- putuskan tujuan apa yang ingin Anda capai;
- putuskan bagaimana Anda akan mencapai tujuan Anda;
- datang ke tujuan Anda.
Ini juga berlaku untuk pemrograman. Saat kita menulis kode, kita perlu:
- memutuskan apa yang harus dilakukan program;
- menentukan bagaimana ia harus melakukan tugasnya;
- menulis kode yang sesuai.
Langkah terakhir tentu saja sangat penting, tetapi saya tidak akan membicarakannya hari ini. Sebagai gantinya, kita akan membahas dua yang pertama. Setiap programmer melakukannya sebelum mulai bekerja. Anda tidak duduk untuk menulis kecuali Anda telah memutuskan apakah Anda sedang menulis browser atau database. Gagasan tertentu tentang tujuan harus ada. Dan Anda pasti memikirkan apa sebenarnya yang akan dilakukan program tersebut, dan jangan menulis entah bagaimana dengan harapan bahwa kode tersebut akan berubah menjadi browser.
Bagaimana tepatnya kode pra-pemikiran ini terjadi? Berapa banyak upaya yang harus kita lakukan untuk ini? Itu semua tergantung pada seberapa kompleks masalah yang kita selesaikan. Misalkan kita ingin menulis sistem terdistribusi yang toleran terhadap kesalahan. Dalam hal ini, kita harus memikirkan semuanya dengan hati-hati sebelum kita mulai membuat kode. Bagaimana jika kita hanya perlu menambah variabel integer sebesar 1? Sekilas, semuanya sepele di sini, dan tidak perlu dipikirkan, tetapi kemudian kita ingat bahwa luapan bisa terjadi. Oleh karena itu, bahkan untuk memahami apakah suatu masalah itu sederhana atau rumit, Anda harus berpikir terlebih dahulu.
Jika Anda memikirkan kemungkinan solusi untuk masalah tersebut sebelumnya, Anda dapat menghindari kesalahan. Tetapi ini membutuhkan pemikiran Anda yang jernih. Untuk mencapai ini, Anda perlu menuliskan pemikiran Anda. Saya sangat menyukai kutipan Dick Guindon: "Saat Anda menulis, alam menunjukkan betapa cerobohnya pemikiran Anda." Jika Anda tidak menulis, Anda hanya berpikir bahwa Anda sedang berpikir. Dan Anda perlu menuliskan pemikiran Anda dalam bentuk spesifikasi.
Spesifikasi melakukan banyak fungsi, terutama dalam proyek besar. Tetapi saya hanya akan berbicara tentang salah satunya: mereka membantu kita berpikir jernih. Berpikir jernih itu sangat penting dan cukup sulit, jadi disini kami butuh bantuan. Dalam bahasa apa kita harus menulis spesifikasi? Secara umum, ini selalu menjadi pertanyaan pertama bagi programmer: bahasa apa yang akan kita tulis. Tidak ada jawaban yang benar untuk itu: masalah yang kami pecahkan terlalu beragam. Untuk beberapa orang, TLA+ adalah bahasa spesifikasi yang saya kembangkan. Bagi yang lain, lebih nyaman menggunakan bahasa Mandarin. Semuanya tergantung pada situasinya.
Yang lebih penting adalah pertanyaan lain: bagaimana mencapai pemikiran yang lebih jernih? Jawaban: Kita harus berpikir seperti ilmuwan. Ini adalah cara berpikir yang telah terbukti selama 500 tahun terakhir. Dalam sains, kami membangun model matematis dari realitas. Astronomi mungkin adalah sains pertama dalam arti sebenarnya. Dalam model matematika yang digunakan dalam astronomi, benda langit muncul sebagai titik dengan massa, posisi, dan momentum, meskipun pada kenyataannya mereka adalah objek yang sangat kompleks dengan gunung dan lautan, pasang surut. Model ini, seperti model lainnya, diciptakan untuk memecahkan masalah tertentu. Ini bagus untuk menentukan ke mana mengarahkan teleskop jika Anda perlu menemukan planet. Namun jika Anda ingin memprediksi cuaca di planet ini, model ini tidak akan berfungsi.
Matematika memungkinkan kita untuk menentukan sifat-sifat model. Dan sains menunjukkan bagaimana sifat-sifat ini berhubungan dengan kenyataan. Mari kita bicara tentang sains kita, ilmu komputer. Realitas tempat kami bekerja adalah sistem komputasi dari berbagai jenis: prosesor, konsol game, komputer, program pelaksana, dan sebagainya. Saya akan berbicara tentang menjalankan program di komputer, tetapi pada umumnya, semua kesimpulan ini berlaku untuk sistem komputasi apa pun. Dalam sains kami, kami menggunakan banyak model berbeda: mesin Turing, rangkaian acara yang dipesan sebagian, dan banyak lainnya.
Apa itu program? Ini adalah kode apa pun yang dapat dipertimbangkan secara mandiri. Misalkan kita perlu menulis browser. Kami melakukan tiga tugas: kami merancang tampilan program oleh pengguna, kemudian kami menulis diagram tingkat tinggi dari program tersebut, dan terakhir kami menulis kodenya. Saat kami menulis kode, kami menyadari bahwa kami perlu menulis pemformat teks. Di sini sekali lagi kita perlu menyelesaikan tiga masalah: tentukan teks apa yang akan dikembalikan alat ini; pilih algoritme untuk pemformatan; menulis kode. Tugas ini memiliki subtugasnya sendiri: menyisipkan tanda hubung dengan benar ke dalam kata-kata. Kami juga menyelesaikan subtugas ini dalam tiga langkah - seperti yang Anda lihat, subtugas ini diulangi di banyak tingkatan.
Mari pertimbangkan lebih detail langkah pertama: masalah apa yang dipecahkan oleh program. Di sini, kita paling sering memodelkan sebuah program sebagai fungsi yang mengambil beberapa input dan menghasilkan beberapa output. Dalam matematika, suatu fungsi biasanya digambarkan sebagai himpunan pasangan terurut. Misalnya, fungsi kuadrat untuk bilangan asli dideskripsikan sebagai himpunan {<0,0>, <1,1>, <2,4>, <3,9>, β¦}. Domain dari fungsi tersebut adalah himpunan elemen pertama dari setiap pasangan, yaitu bilangan asli. Untuk mendefinisikan suatu fungsi, kita perlu menentukan ruang lingkup dan rumusnya.
Namun fungsi dalam matematika tidak sama dengan fungsi dalam bahasa pemrograman. Matematika jauh lebih mudah. Karena saya tidak punya waktu untuk contoh yang rumit, mari pertimbangkan yang sederhana: fungsi di C atau metode statis di Java yang mengembalikan pembagi persekutuan terbesar dari dua bilangan bulat. Dalam spesifikasi metode ini, kami akan menulis: menghitung GCD(M,N) untuk argumen M ΠΈ NDimana GCD(M,N) - fungsi yang domainnya adalah himpunan pasangan bilangan bulat, dan nilai kembaliannya adalah bilangan bulat terbesar yang habis dibagi M ΠΈ N. Bagaimana model ini berhubungan dengan kenyataan? Model beroperasi pada bilangan bulat, sedangkan di C atau Java kami memiliki 32-bit int. Model ini memungkinkan kita untuk memutuskan apakah algoritmanya benar GCD, tetapi itu tidak akan mencegah kesalahan luapan. Ini akan membutuhkan model yang lebih kompleks, yang tidak ada waktu.
Mari kita bicara tentang batasan fungsi sebagai model. Beberapa program (seperti sistem operasi) tidak hanya mengembalikan nilai tertentu untuk argumen tertentu, tetapi juga dapat berjalan terus menerus. Selain itu, fungsi sebagai model tidak cocok untuk langkah kedua: merencanakan cara menyelesaikan masalah. Pengurutan cepat dan pengurutan gelembung menghitung fungsi yang sama, tetapi keduanya merupakan algoritme yang sama sekali berbeda. Oleh karena itu, untuk menggambarkan bagaimana tujuan program tercapai, saya menggunakan model yang berbeda, sebut saja model perilaku standar. Program di dalamnya direpresentasikan sebagai sekumpulan dari semua perilaku yang diizinkan, yang masing-masing, pada gilirannya, adalah urutan status, dan status adalah penetapan nilai ke variabel.
Mari kita lihat seperti apa langkah kedua untuk algoritme Euclid. Kita perlu menghitung GCD(M, N). Kami menginisialisasi M sebagai xDan N sebagai y, lalu berulang kali kurangi variabel yang lebih kecil dari yang lebih besar hingga sama. Misalnya, jika M = 12Dan N = 18, kita dapat menggambarkan perilaku berikut:
[x = 12, y = 18] β [x = 12, y = 6] β [x = 6, y = 6]
Dan jika M = 0 ΠΈ N = 0? Nol habis dibagi semua angka, jadi tidak ada pembagi terbesar dalam kasus ini. Dalam situasi ini, kita perlu kembali ke langkah pertama dan bertanya: apakah kita benar-benar perlu menghitung GCD untuk bilangan non-positif? Jika ini tidak diperlukan, maka Anda hanya perlu mengubah spesifikasinya.
Di sini kita harus membuat penyimpangan kecil tentang produktivitas. Ini sering diukur dalam jumlah baris kode yang ditulis per hari. Tetapi pekerjaan Anda jauh lebih berguna jika Anda menghilangkan sejumlah baris, karena Anda memiliki lebih sedikit ruang untuk bug. Dan cara termudah untuk menghilangkan kode tersebut adalah pada langkah pertama. Sangat mungkin bahwa Anda tidak membutuhkan semua lonceng dan peluit yang Anda coba terapkan. Cara tercepat untuk menyederhanakan program dan menghemat waktu adalah dengan tidak melakukan hal-hal yang seharusnya tidak dilakukan. Langkah kedua adalah potensi penghematan waktu kedua yang paling banyak. Jika Anda mengukur produktivitas dalam bentuk garis tertulis, maka memikirkan tentang bagaimana menyelesaikan suatu tugas akan membuat Anda kurang produktif, karena Anda dapat memecahkan masalah yang sama dengan lebih sedikit kode. Saya tidak dapat memberikan statistik yang tepat di sini, karena saya tidak dapat menghitung jumlah baris yang tidak saya tulis karena saya menghabiskan waktu untuk spesifikasi, yaitu pada langkah pertama dan kedua. Dan eksperimen juga tidak bisa diatur disini, karena dalam eksperimen kita tidak berhak menyelesaikan langkah pertama, tugas sudah ditentukan sebelumnya.
Sangat mudah untuk mengabaikan banyak kesulitan dalam spesifikasi informal. Tidak ada yang sulit dalam menulis spesifikasi fungsi yang ketat, saya tidak akan membahas ini. Sebagai gantinya, kita akan berbicara tentang menulis spesifikasi yang kuat untuk perilaku standar. Ada teorema yang mengatakan bahwa setiap rangkaian perilaku dapat dideskripsikan menggunakan properti keamanan (keamanan) dan sifat bertahan hidup (kehidupan). Keamanan berarti tidak ada hal buruk yang akan terjadi, program tidak akan memberikan jawaban yang salah. Bertahan berarti cepat atau lambat sesuatu yang baik akan terjadi, yaitu program akan memberikan jawaban yang benar cepat atau lambat. Biasanya, keamanan adalah indikator yang lebih penting, kesalahan paling sering terjadi di sini. Oleh karena itu, untuk menghemat waktu, saya tidak akan berbicara tentang kemampuan bertahan hidup, meskipun tentu saja ini juga penting.
Kami mencapai keamanan dengan meresepkan, pertama, set keadaan awal yang mungkin. Dan kedua, hubungan dengan semua kemungkinan keadaan berikutnya untuk setiap keadaan. Mari bertindak seperti ilmuwan dan mendefinisikan keadaan secara matematis. Himpunan keadaan awal dijelaskan oleh rumus, misalnya, dalam kasus algoritme Euclid: (x = M) β§ (y = N). Untuk nilai-nilai tertentu M ΠΈ N hanya ada satu keadaan awal. Hubungan dengan keadaan berikutnya dijelaskan dengan rumus di mana variabel keadaan berikutnya ditulis dengan bilangan prima, dan variabel keadaan saat ini ditulis tanpa bilangan prima. Dalam kasus algoritme Euclid, kita akan membahas disjungsi dua rumus, yang salah satunya x adalah nilai terbesar, dan yang kedua - y:
Dalam kasus pertama, nilai baru y sama dengan nilai y sebelumnya, dan kita mendapatkan nilai baru x dengan mengurangkan variabel yang lebih kecil dari variabel yang lebih besar. Dalam kasus kedua, kami melakukan yang sebaliknya.
Mari kembali ke algoritme Euclid. Mari kita asumsikan lagi itu M = 12, N = 18. Ini mendefinisikan satu keadaan awal, (x = 12) β§ (y = 18). Kami kemudian memasukkan nilai-nilai itu ke dalam rumus di atas dan mendapatkan:
Inilah satu-satunya solusi yang mungkin: x' = 18 - 12 β§ y' = 12dan kami mendapatkan perilaku: [x = 12, y = 18]. Demikian pula, kita dapat menggambarkan semua keadaan dalam perilaku kita: [x = 12, y = 18] β [x = 12, y = 6] β [x = 6, y = 6].
Dalam keadaan terakhir [x = 6, y = 6] kedua bagian ekspresi akan salah, sehingga tidak memiliki status berikutnya. Jadi, kami memiliki spesifikasi lengkap untuk langkah kedua - seperti yang Anda lihat, ini adalah matematika yang cukup biasa, seperti pada insinyur dan ilmuwan, dan tidak aneh, seperti pada ilmu komputer.
Kedua rumus ini dapat digabungkan menjadi satu rumus logika temporal. Dia anggun dan mudah dijelaskan, tetapi tidak ada waktu untuknya sekarang. Kita mungkin membutuhkan logika temporal hanya untuk properti keaktifan, tidak diperlukan untuk keamanan. Saya tidak suka logika temporal seperti itu, ini bukan matematika biasa, tetapi dalam kasus keaktifan itu adalah kejahatan yang perlu.
Dalam algoritme Euclid, untuk setiap nilai x ΠΈ y memiliki nilai unik x' ΠΈ y', yang membuat hubungan dengan keadaan berikutnya menjadi benar. Dengan kata lain, algoritma Euclid bersifat deterministik. Untuk memodelkan algoritma non-deterministik, keadaan saat ini perlu memiliki beberapa kemungkinan keadaan di masa depan, dan bahwa setiap nilai variabel yang tidak diprioritaskan memiliki beberapa nilai variabel yang diprioritaskan sedemikian rupa sehingga hubungan ke keadaan berikutnya benar. Ini mudah dilakukan, tetapi saya tidak akan memberikan contoh sekarang.
Untuk membuat alat kerja, Anda membutuhkan matematika formal. Bagaimana membuat spesifikasi formal? Untuk melakukan ini, kita memerlukan bahasa formal, misalnya, . Spesifikasi algoritme Euclid akan terlihat seperti ini dalam bahasa berikut:
Simbol tanda sama dengan dengan segitiga berarti bahwa nilai di sebelah kiri tanda didefinisikan sama dengan nilai di sebelah kanan tanda. Intinya, spesifikasi adalah definisi, dalam kasus kami ada dua definisi. Untuk spesifikasi di TLA+, Anda perlu menambahkan deklarasi dan beberapa sintaks, seperti pada slide di atas. Di ASCII akan terlihat seperti ini:
Seperti yang Anda lihat, tidak ada yang rumit. Spesifikasi untuk TLA+ dapat diuji, misalnya melewati semua kemungkinan perilaku dalam model kecil. Dalam kasus kami, model ini akan menjadi nilai tertentu M ΠΈ N. Ini adalah metode verifikasi yang sangat efisien dan sederhana yang sepenuhnya otomatis. Dimungkinkan juga untuk menulis bukti kebenaran formal dan memeriksanya secara mekanis, tetapi ini membutuhkan banyak waktu, jadi hampir tidak ada yang melakukannya.
Kelemahan utama TLA+ adalah matematika, dan pemrogram serta ilmuwan komputer takut dengan matematika. Sekilas, ini terdengar seperti lelucon, tapi, sayangnya, saya bersungguh-sungguh. Rekan saya baru saja memberi tahu saya bagaimana dia mencoba menjelaskan TLA + ke beberapa pengembang. Begitu formula muncul di layar, mereka langsung menjadi mata berkaca-kaca. Jadi jika TLA+ membuat Anda takut, Anda dapat menggunakannya , itu semacam bahasa pemrograman mainan. Ekspresi dalam PlusCal dapat berupa ekspresi TLA+ apa pun, yaitu, pada umumnya, ekspresi matematis apa pun. Selain itu, PlusCal memiliki sintaks untuk algoritme non-deterministik. Karena PlusCal dapat menulis ekspresi TLA+ apa pun, PlusCal jauh lebih ekspresif daripada bahasa pemrograman yang sebenarnya. Selanjutnya, PlusCal dikompilasi menjadi spesifikasi TLA+ yang mudah dibaca. Ini tidak berarti, tentu saja, bahwa spesifikasi PlusCal yang kompleks akan berubah menjadi yang sederhana di TLA + - hanya korespondensi di antara keduanya sudah jelas, tidak akan ada kerumitan tambahan. Terakhir, spesifikasi ini dapat diverifikasi oleh alat TLA+. Secara keseluruhan, PlusCal dapat membantu mengatasi fobia matematika dan mudah dipahami bahkan untuk pemrogram dan ilmuwan komputer. Di masa lalu, saya menerbitkan algoritme untuk beberapa waktu (sekitar 10 tahun).
Mungkin seseorang akan keberatan bahwa TLA + dan PlusCal adalah matematika, dan matematika hanya bekerja pada contoh yang ditemukan. Dalam praktiknya, Anda memerlukan bahasa nyata dengan tipe, prosedur, objek, dan sebagainya. Ini salah. Inilah yang ditulis Chris Newcomb, yang bekerja di Amazon: βKami telah menggunakan TLA+ pada sepuluh proyek besar, dan dalam setiap kasus, penggunaannya telah membuat perbedaan yang signifikan pada pengembangan karena kami dapat menemukan bug berbahaya sebelum mencapai produksi, dan karena ini memberi kami wawasan dan keyakinan yang kami butuhkan untuk melakukan pengoptimalan kinerja yang agresif tanpa memengaruhi kebenaran program". Anda sering mendengar bahwa saat menggunakan metode formal, kami mendapatkan kode yang tidak efisien - dalam praktiknya, semuanya justru sebaliknya. Selain itu, ada pendapat bahwa manajer tidak dapat diyakinkan tentang perlunya metode formal, meskipun pemrogram yakin akan kegunaannya. Dan Newcomb menulis: βManajer sekarang berusaha keras untuk menulis spesifikasi untuk TLA +, dan secara khusus mengalokasikan waktu untuk iniβ. Jadi ketika manajer melihat bahwa TLA+ berfungsi, mereka dengan senang hati menerimanya. Chris Newcomb menulis ini sekitar enam bulan lalu (Oktober 2014), tapi sekarang, setahu saya, TLA+ digunakan di 14 proyek, bukan 10. Contoh lain ada di desain XBox 360. Seorang magang mendatangi Charles Thacker dan menulis spesifikasi untuk sistem memori. Berkat spesifikasi ini, ditemukan bug yang tidak diketahui, dan karenanya setiap XBox 360 akan mogok setelah empat jam penggunaan. Insinyur IBM mengonfirmasi bahwa pengujian mereka tidak akan menemukan bug ini.
Anda dapat membaca lebih lanjut tentang TLA + di Internet, tetapi sekarang mari kita bicara tentang spesifikasi informal. Kita jarang harus menulis program yang menghitung pembagi persekutuan terkecil dan sejenisnya. Lebih sering kita menulis program seperti alat printer cantik yang saya buat untuk TLA+. Setelah pemrosesan paling sederhana, kode TLA + akan terlihat seperti ini:
Namun dalam contoh di atas, pengguna kemungkinan besar menginginkan tanda sambung dan tanda sama dengan disejajarkan. Jadi pemformatan yang benar akan terlihat seperti ini:
Pertimbangkan contoh lain:
Di sini, sebaliknya, penyelarasan tanda sama dengan, penjumlahan, dan perkalian dalam sumber dilakukan secara acak, jadi pemrosesan yang paling sederhana sudah cukup. Secara umum, tidak ada definisi matematis yang pasti tentang pemformatan yang benar, karena "benar" dalam hal ini berarti "apa yang diinginkan pengguna", dan ini tidak dapat ditentukan secara matematis.
Nampaknya jika kita tidak memiliki definisi kebenaran, maka spesifikasi tersebut tidak ada gunanya. Tapi ternyata tidak. Hanya karena kita tidak tahu apa yang seharusnya dilakukan oleh suatu program, bukan berarti kita tidak perlu memikirkan cara kerjanyaβsebaliknya, kita harus berusaha lebih keras lagi. Spesifikasi sangat penting di sini. Tidak mungkin untuk menentukan program optimal untuk pencetakan terstruktur, tetapi ini tidak berarti bahwa kita tidak boleh mengambilnya sama sekali, dan menulis kode sebagai aliran kesadaran bukanlah hal yang baik. Pada akhirnya, saya menulis spesifikasi enam aturan dengan definisi dalam bentuk komentar dalam file java. Berikut adalah contoh salah satu aturannya: a left-comment token is LeftComment aligned with its covering token. Aturan ini ditulis dalam, katakanlah, bahasa Inggris matematis: LeftComment aligned, left-comment ΠΈ covering token - istilah dengan definisi. Beginilah cara ahli matematika mendeskripsikan matematika: mereka menulis definisi istilah dan, berdasarkan definisi tersebut, aturan. Keuntungan dari spesifikasi seperti itu adalah bahwa enam aturan jauh lebih mudah dipahami dan di-debug daripada 850 baris kode. Saya harus mengatakan bahwa menulis aturan ini tidak mudah, butuh banyak waktu untuk men-debugnya. Khusus untuk tujuan ini, saya menulis kode yang melaporkan aturan mana yang digunakan. Berkat fakta bahwa saya menguji keenam aturan ini pada beberapa contoh, saya tidak perlu men-debug 850 baris kode, dan bug ternyata cukup mudah ditemukan. Java memiliki alat yang hebat untuk ini. Jika saya baru saja menulis kodenya, itu akan memakan waktu lebih lama, dan pemformatannya akan menjadi kualitas yang lebih buruk.
Mengapa spesifikasi formal tidak dapat digunakan? Di satu sisi, eksekusi yang benar tidak terlalu penting di sini. Cetakan struktural pasti tidak menyenangkan siapa pun, jadi saya tidak harus membuatnya berfungsi dengan benar dalam semua situasi yang aneh. Yang lebih penting adalah kenyataan bahwa saya tidak memiliki alat yang memadai. Pemeriksa model TLA+ tidak berguna di sini, jadi saya harus menulis contoh secara manual.
Spesifikasi di atas memiliki fitur yang sama untuk semua spesifikasi. Ini level yang lebih tinggi dari kode. Itu dapat diimplementasikan dalam bahasa apa pun. Alat atau metode apa pun tidak berguna untuk menulisnya. Tidak ada kursus pemrograman yang akan membantu Anda menulis spesifikasi ini. Dan tidak ada alat yang dapat membuat spesifikasi ini tidak diperlukan, kecuali, tentu saja, Anda sedang menulis bahasa khusus untuk menulis program cetak terstruktur di TLA+. Terakhir, spesifikasi ini tidak mengatakan apa-apa tentang bagaimana tepatnya kita akan menulis kode, ini hanya menyatakan apa yang dilakukan kode ini. Kami menulis spesifikasi untuk membantu kami memikirkan masalahnya sebelum kami mulai memikirkan kodenya.
Namun spesifikasi ini juga memiliki fitur yang membedakannya dengan spesifikasi lainnya. 95% spesifikasi lainnya jauh lebih pendek dan sederhana:
Selanjutnya, spesifikasi ini adalah seperangkat aturan. Sebagai aturan, ini adalah tanda spesifikasi yang buruk. Cukup sulit untuk memahami konsekuensi dari seperangkat aturan, itulah sebabnya saya harus menghabiskan banyak waktu untuk men-debugnya. Namun, dalam hal ini, saya tidak dapat menemukan cara yang lebih baik.
Perlu dikatakan beberapa patah kata tentang program yang berjalan terus menerus. Sebagai aturan, mereka bekerja secara paralel, misalnya, sistem operasi atau sistem terdistribusi. Sangat sedikit orang yang dapat memahaminya secara mental atau di atas kertas, dan saya bukan salah satu dari mereka, walaupun saya pernah bisa melakukannya. Oleh karena itu, kami membutuhkan alat yang akan memeriksa pekerjaan kami - misalnya, TLA + atau PlusCal.
Mengapa perlu menulis spesifikasi jika saya sudah tahu persis apa yang harus dilakukan kode? Bahkan, saya hanya berpikir saya tahu itu. Selain itu, dengan spesifikasinya, orang luar tidak perlu lagi masuk ke dalam kode untuk memahami apa sebenarnya yang dia lakukan. Saya punya aturan: tidak boleh ada aturan umum. Ada pengecualian untuk aturan ini, tentu saja, itu satu-satunya aturan umum yang saya ikuti: spesifikasi dari apa yang dilakukan kode harus memberi tahu orang semua yang perlu mereka ketahui saat menggunakan kode.
Jadi, apa sebenarnya yang perlu diketahui pemrogram tentang berpikir? Sebagai permulaan, sama seperti orang lain: jika Anda tidak menulis, maka Anda hanya berpikir bahwa Anda sedang berpikir. Selain itu, Anda harus berpikir sebelum membuat kode, yang berarti Anda harus menulis sebelum membuat kode. Spesifikasi adalah apa yang kita tulis sebelum kita mulai coding. Spesifikasi diperlukan untuk setiap kode yang dapat digunakan atau dimodifikasi oleh siapa saja. Dan "seseorang" ini mungkin adalah pembuat kode itu sendiri sebulan setelah kode itu ditulis. Spesifikasi diperlukan untuk program dan sistem besar, untuk kelas, untuk metode, dan terkadang bahkan untuk bagian kompleks dari satu metode. Apa sebenarnya yang harus ditulis tentang kode tersebut? Anda perlu menjelaskan apa fungsinya, yaitu apa yang berguna bagi siapa pun yang menggunakan kode ini. Terkadang juga perlu untuk menentukan bagaimana kode mencapai tujuannya. Jika kami menggunakan metode ini selama algoritme, maka kami menyebutnya algoritme. Jika itu sesuatu yang lebih istimewa dan baru, maka kami menyebutnya desain tingkat tinggi. Tidak ada perbedaan formal di sini: keduanya merupakan model abstrak dari suatu program.
Bagaimana tepatnya Anda harus menulis spesifikasi kode? Hal utama: itu harus satu tingkat lebih tinggi dari kode itu sendiri. Itu harus menggambarkan keadaan dan perilaku. Itu harus seketat tugas yang dibutuhkan. Jika Anda menulis spesifikasi tentang bagaimana suatu tugas akan diimplementasikan, Anda dapat menuliskannya dalam kodesemu atau dengan PlusCal. Anda perlu mempelajari cara menulis spesifikasi pada spesifikasi formal. Ini akan memberi Anda keterampilan yang diperlukan yang akan membantu Anda dengan yang informal juga. Bagaimana Anda belajar menulis spesifikasi formal? Ketika kami belajar memprogram, kami menulis program dan kemudian men-debugnya. Di sini sama saja: tulis spek, periksa dengan pemeriksa model, dan perbaiki bug. TLA+ mungkin bukan bahasa terbaik untuk spesifikasi formal, dan bahasa lain mungkin lebih baik untuk kebutuhan khusus Anda. Keuntungan dari TLA+ adalah mengajarkan pemikiran matematis dengan sangat baik.
Bagaimana cara menautkan spesifikasi dan kode? Dengan bantuan komentar yang menghubungkan konsep matematika dan penerapannya. Jika Anda bekerja dengan grafik, maka pada tingkat program Anda akan memiliki susunan node dan susunan tautan. Oleh karena itu, Anda perlu menulis dengan tepat bagaimana grafik diimplementasikan oleh struktur pemrograman ini.
Perlu dicatat bahwa tidak satu pun di atas berlaku untuk proses penulisan kode yang sebenarnya. Saat Anda menulis kode, yaitu, Anda melakukan langkah ketiga, Anda juga perlu memikirkan dan memikirkan programnya. Jika subtugas ternyata rumit atau tidak jelas, Anda perlu menulis spesifikasinya. Tapi saya tidak berbicara tentang kode itu sendiri di sini. Anda dapat menggunakan bahasa pemrograman apa pun, metodologi apa pun, ini bukan tentang mereka. Selain itu, tidak satu pun di atas menghilangkan kebutuhan untuk menguji dan men-debug kode. Bahkan jika model abstrak ditulis dengan benar, mungkin ada bug dalam penerapannya.
Menulis spesifikasi adalah langkah tambahan dalam proses pengkodean. Berkat itu, banyak kesalahan dapat ditangkap dengan sedikit usaha - kami mengetahui hal ini dari pengalaman programmer dari Amazon. Dengan spesifikasi, kualitas program menjadi lebih tinggi. Jadi, mengapa kita begitu sering pergi tanpa mereka? Karena menulis itu sulit. Dan menulis itu sulit, karena untuk ini Anda perlu berpikir, dan berpikir juga sulit. Itu selalu lebih mudah untuk berpura-pura apa yang Anda pikirkan. Di sini Anda dapat menggambar analogi dengan berlari - semakin sedikit Anda berlari, semakin lambat Anda berlari. Anda perlu melatih otot dan berlatih menulis. Butuh latihan.
Spesifikasi mungkin salah. Anda mungkin telah membuat kesalahan di suatu tempat, atau persyaratan mungkin telah berubah, atau perbaikan mungkin perlu dilakukan. Kode apa pun yang digunakan siapa pun harus diubah, jadi cepat atau lambat spesifikasinya tidak lagi sesuai dengan program. Idealnya, dalam hal ini, Anda perlu menulis spesifikasi baru dan menulis ulang kode sepenuhnya. Kami tahu betul bahwa tidak ada yang melakukan itu. Dalam praktiknya, kami menambal kode dan mungkin memperbarui spesifikasinya. Jika ini pasti akan terjadi cepat atau lambat, lalu mengapa menulis spesifikasi? Pertama, untuk orang yang akan mengedit kode Anda, setiap kata tambahan dalam spesifikasi akan bernilai emas, dan orang ini mungkin Anda sendiri. Saya sering mencaci diri sendiri karena tidak mendapatkan spesifikasi yang cukup saat mengedit kode. Dan saya menulis lebih banyak spesifikasi daripada kode. Oleh karena itu, saat Anda mengedit kode, spesifikasi selalu perlu diperbarui. Kedua, dengan setiap revisi, kode menjadi lebih buruk, menjadi semakin sulit untuk dibaca dan dipelihara. Ini adalah peningkatan entropi. Tetapi jika Anda tidak memulai dengan spek, maka setiap baris yang Anda tulis akan menjadi editan, dan kode akan berat dan sulit dibaca sejak awal.
Seperti Yang Dikatakan , tidak ada pertempuran yang dimenangkan dengan rencana, dan tidak ada pertempuran yang dimenangkan tanpa rencana. Dan dia tahu satu atau dua hal tentang pertempuran. Ada pendapat bahwa menulis spesifikasi hanya membuang-buang waktu. Terkadang ini benar, dan tugasnya sangat sederhana sehingga tidak ada yang perlu dipikirkan. Tapi Anda harus selalu ingat bahwa ketika Anda disuruh untuk tidak menulis spesifikasi, Anda disuruh untuk tidak berpikir. Dan Anda harus memikirkannya setiap saat. Memikirkan tugas tidak menjamin bahwa Anda tidak akan membuat kesalahan. Seperti yang kita ketahui, tidak ada yang menemukan tongkat ajaib, dan pemrograman adalah tugas yang sulit. Tetapi jika Anda tidak memikirkan masalahnya, Anda dijamin akan melakukan kesalahan.
Anda dapat membaca lebih lanjut tentang TLA + dan PlusCal di situs web khusus, Anda dapat membukanya dari beranda saya . Sekian dari saya, terima kasih atas perhatiannya.
Harap dicatat bahwa ini adalah terjemahan. Saat Anda menulis komentar, ingatlah bahwa penulis tidak akan membacanya. Jika memang ingin ngobrol dengan penulis, maka dia akan hadir di konferensi Hydra 2019 yang akan diadakan pada 11-12 Juli 2019 di St. Tiket dapat dibeli .
Sumber: www.habr.com