Iki artikel terjemahan . Nanging sadurunge iku ana introduksi singkat. Kepiye carane zombie dibentuk? Saben uwong wis nemokake dhewe ing kahanan sing pengin nggawa kanca utawa kolega nganti tingkat, nanging ora bisa. Menapa malih, "ora bisa ditindakake" ora akeh kanggo sampeyan, nanging kanggo dheweke: ing sisih siji ukuran ana gaji normal, tugas, lan liya-liyane, lan ing liyane iku perlu kanggo mikir. Mikir iku ora nyenengake lan nglarani. Dheweke cepet nyerah lan terus nulis kode tanpa nggunakake otak. Sampeyan ngerti carane akeh gaweyan kanggo ngatasi alangan saka helplessness sinau, lan sampeyan mung ora nindakake. Iki carane nir kawangun, kang koyone bisa kanggo nambani, nanging misale jek sing ora ana sing bakal nindakake iki.
Nalika aku weruh sing (ya, kanca sing padha saka buku teks) lan ora menehi laporan, nanging sesi pitakonan-jawaban, aku rada waspada. Yen ngono, Leslie minangka ilmuwan sing misuwur ing saindenging jagad, penulis karya seminal ing komputasi sing disebarake, lan sampeyan uga bisa ngerti dheweke kanthi huruf La ing LaTeX - "Lamport TeX". Faktor nguwatirake kapindho yaiku syarate: saben wong sing teka kudu (gratis gratis) ngrungokake sawetara laporan sadurunge, nggawe paling ora siji pitakonan babagan dheweke, lan banjur teka. Aku mutusake kanggo ndeleng apa sing disiarkan Lamport ing kana - lan apik banget! Iki persis sing, link-pil ajaib kanggo nambani zombie. Aku ngelingake sampeyan: teks kasebut bisa uga ngobong wong sing seneng metodologi super-lincah lan sing ora seneng nyoba apa sing ditulis.
Sawise habrokat, terjemahan seminar pancen diwiwiti. Seneng maca!
Apa wae tugas sing ditindakake, sampeyan kudu ngliwati telung langkah:
- mutusake apa tujuan sing pengin digayuh;
- mutusake carane sampeyan bakal entuk gol;
- tekan tujuan sampeyan.
Iki uga ditrapake kanggo pemrograman. Nalika kita nulis kode, kita kudu:
- mutusake apa sing kudu ditindakake program kasebut;
- nemtokake persis carane kudu nindakake tugas;
- nulis kode sing cocog.
Langkah pungkasan, mesthi, penting banget, nanging aku ora bakal ngomong babagan dina iki. Nanging, kita bakal ngrembug loro pisanan. Saben programmer nindakake sadurunge miwiti kerja. Sampeyan ora lungguh kanggo nulis kajaba sampeyan wis mutusake apa sing sampeyan tulis: browser utawa database. Gagasan tartamtu babagan tujuan kasebut kudu ana. Lan sampeyan mesthi mikir babagan apa sing bakal ditindakake program kasebut, lan aja nulis kanthi sembarangan kanthi pangarep-arep kode kasebut bakal dadi browser.
Kepiye carane pre-thiking kode iki kedadeyan? Carane akeh gaweyan kudu kita sijine menyang iki? Iku kabeh gumantung carane Komplek masalah kita mecahaken. Ayo dadi ngomong kita arep nulis sistem distribusi fault-tolerant. Ing kasus iki, kita kudu mikir kanthi teliti sadurunge lungguh kanggo kode. Apa yen kita mung kudu nambah variabel integer kanthi 1? Sepisanan, kabeh ing kene ora pati penting lan ora perlu dipikirake, nanging banjur kita ngelingi yen kebanjiran bisa kedadeyan. Mulane, sanajan kanggo mangerteni apa masalah iku prasaja utawa rumit, sampeyan kudu mikir dhisik.
Yen sampeyan mikir babagan solusi sing bisa ditindakake sadurunge masalah, sampeyan bisa ngindhari kesalahan. Nanging iki mbutuhake pikiran sampeyan dadi cetha. Kanggo entuk iki, sampeyan kudu nulis pikirane. Aku seneng karo kutipan Dick Guindon: "Nalika sampeyan nulis, alam nuduhake sampeyan carane ora mikir sampeyan." Yen sampeyan ora nulis, sampeyan mung mikir sampeyan mikir. Lan sampeyan kudu nulis pikirane ing wangun spesifikasi.
Spesifikasi nyedhiyakake akeh fungsi, utamane ing proyek gedhe. Nanging aku mung bakal ngomong babagan siji: dheweke mbantu kita mikir kanthi jelas. Mikir kanthi cetha iku penting banget lan cukup angel, mula kita butuh bantuan ing kene. Apa basa sing kudu kita tulis ing spesifikasi? Umumé, iki minangka pitakonan pisanan kanggo programer: basa apa sing bakal kita tulis? Ora ana jawaban sing bener: masalah sing kita rampungake macem-macem. Kanggo sawetara wong, TLA + minangka basa spesifikasi sing dikembangake. Kanggo wong liya, luwih trep nggunakake basa Cina. Iku kabeh gumantung ing kahanan.
Pitakonan sing luwih penting yaiku: kepiye carane bisa entuk pikiran sing luwih jelas? Wangsulan: Kita kudu mikir kaya ilmuwan. Iki minangka cara mikir sing wis makarya kanthi apik sajrone 500 taun kepungkur. Ing ilmu kita mbangun model matematika saka kasunyatan. Astronomi mbok menawa ilmu pisanan ing pangertèn ketat tembung. Ing model matématika sing digunakake ing astronomi, benda langit katon minangka titik kanthi massa, posisi lan momentum, sanajan nyatane obyek kasebut minangka obyek sing rumit banget kanthi gunung lan samudra, pasang surut lan mili. Model iki, kaya liyane, digawe kanggo ngatasi masalah tartamtu. Iku apik kanggo nemtokake ngendi kanggo ngarahake teleskop yen sampeyan pengin nemokake planet. Nanging yen sampeyan pengin prédhiksi cuaca ing planet iki, model iki ora bakal bisa.
Matematika ngidini kita nemtokake sifat model. Lan ilmu nuduhake kepiye sifat-sifat kasebut ana gandhengane karo kasunyatan. Ayo kita ngomong babagan ilmu komputer, ilmu komputer. Kasunyatan sing digunakake yaiku sistem komputasi saka macem-macem jinis: prosesor, konsol game, komputer sing mbukak program, lan liya-liyane. Aku bakal ngomong babagan nglakokake program ing komputer, nanging, umume, kabeh kesimpulan kasebut ditrapake kanggo sistem komputasi apa wae. Ing ilmu pengetahuan kita nggunakake macem-macem model: mesin Turing, sawetara acara sing diurutake, lan liya-liyane.
Apa program kasebut? Iki kode apa wae sing bisa dianggep dhewe. Ayo kita kudu nulis browser. Kita nindakake telung tugas: ngrancang presentation pangguna program, banjur nulis diagram tingkat dhuwur saka program, lan pungkasanipun nulis kode. Nalika kita nulis kode, kita ngerti yen kita kudu nulis formatter teks. Kene maneh kita kudu ngatasi telung masalah: nemtokake teks apa alat iki bakal bali; pilih algoritma kanggo format; nulis kode. Tugas iki nduweni subtugas dhewe: nglebokake tanda hubung menyang tembung kanthi bener. Kita uga ngrampungake subtugas iki kanthi telung langkah - kaya sing kita deleng, diulang ing pirang-pirang tingkat.
Ayo goleki kanthi luwih cetha ing langkah pisanan: masalah apa sing diatasi program. Kene kita paling kerep model program minangka fungsi sing njupuk sawetara input lan menehi sawetara output. Ing matématika, sawijining fungsi biasane diterangake minangka pasangan sing diurutake. Contone, fungsi kuadrat kanggo nomer alami diterangake minangka set {<0,0>, <1,1>, <2,4>, <3,9>, …}. Domain definisi fungsi kasebut yaiku himpunan unsur pisanan saben pasangan, yaiku, nomer alami. Kanggo nemtokake fungsi, kita kudu nemtokake domain lan rumus.
Nanging fungsi ing matématika ora padha karo fungsi ing basa program. Matematika luwih prasaja. Awit aku ora duwe wektu kanggo conto Komplek, ayo kang nimbang siji prasaja: fungsi ing C utawa cara statis ing Jawa sing ngasilake divisor umum paling gedhe saka rong wilangan bulat. Ing specification saka cara iki kita bakal nulis: ngetung GCD(M,N) kanggo argumentasi M и Nngendi GCD(M,N) - fungsi sing domain minangka sakumpulan pasangan integer, lan nilai bali minangka integer paling gedhe sing dibagi karo M и N. Kepiye kasunyatan dibandhingake karo model iki? Model kasebut beroperasi kanthi integer, lan ing C utawa Jawa kita duwe 32-bit int. Model iki ngidini kita mutusake manawa algoritma kasebut bener GCD, nanging ora bakal nyegah kasalahan overflow. Iki bakal mbutuhake model sing luwih rumit, sing ora ana wektu.
Ayo dadi pirembagan bab watesan saka fungsi minangka model. Sawetara program (kayata sistem operasi) ora mung ngasilake nilai tartamtu kanggo argumen tartamtu; bisa mlaku terus. Kajaba iku, fungsi minangka model kurang cocog kanggo langkah kapindho: ngrancang carane ngatasi masalah kasebut. Quicksort lan gelembung ngetung fungsi sing padha, nanging padha algoritma temen beda. Mula, kanggo njlèntrèhaké cara kanggo nggayuh tujuan program, aku nggunakake model liya, ayo diarani model prilaku standar. Program kasebut diwakili minangka sakumpulan kabeh prilaku sing bener, sing saben-saben, minangka urutan negara, lan negara minangka penugasan nilai kanggo variabel.
Ayo ndeleng apa langkah kapindho kanggo algoritma Euclidean bakal katon. Kita kudu ngitung GCD(M, N). We initialize M carane xlan N carane y, banjur bola-bali nyuda variabel sing luwih cilik saka variabel sing luwih gedhe nganti padha. Contone, yen M = 12lan N = 18, kita bisa njlèntrèhaké prilaku ing ngisor iki:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
Lan yen M = 0 и N = 0? Zero bisa dibagi dening kabeh nomer, supaya ora ana pembagi paling gedhe ing kasus iki. Ing kahanan iki, kita kudu bali menyang langkah pisanan lan takon: apa kita pancene kudu ngetung GCD kanggo nomer non-positif? Yen iki ora perlu, sampeyan mung kudu ngganti spesifikasi.
Digression cendhak babagan produktivitas ana ing kene. Asring diukur ing jumlah baris kode sing ditulis saben dina. Nanging pakaryan sampeyan luwih migunani yen sampeyan nyingkirake sawetara garis, amarga sampeyan duwe ruangan kurang kanggo kewan omo. Lan cara paling gampang kanggo nyisihake kode yaiku ing langkah pisanan. Sampeyan bisa uga ora mbutuhake kabeh lonceng lan peluit sing sampeyan coba lakoni. Cara paling cepet kanggo nyederhanakake program lan ngirit wektu yaiku ora nindakake perkara sing ora kudu ditindakake. Langkah kapindho duweni potensi irit wektu paling dhuwur kaloro. Yen sampeyan ngukur produktivitas saka segi garis sing ditulis, banjur mikir babagan carane ngrampungake tugas bakal nggawe sampeyan kurang produktif, amarga sampeyan bisa ngatasi masalah sing padha karo kode kurang. Aku ora bisa menehi statistik pas kene, amarga aku ora duwe cara kanggo ngetung nomer baris sing aku ora nulis amarga wektu aku ngginakaken ing specification, sing, ing langkah pisanan lan kaloro. Lan kita uga ora bisa nindakake eksperimen ing kene, amarga ing eksperimen kita ora duwe hak kanggo ngrampungake langkah pisanan, tugas kasebut ditemtokake luwih dhisik.
Iku gampang kanggo klalen akeh kangelan ing specifications informal. Ora ana sing angel nulis spesifikasi sing ketat kanggo fungsi; Aku ora bakal ngrembug babagan iki. Nanging, kita bakal ngomong babagan nulis spesifikasi sing kuat kanggo prilaku standar. Ana téoréma sing nyatakake yen sembarang set prilaku bisa diterangake nggunakake properti keamanan (slametan) lan sifat kelangsungan urip (urip). Safety tegese ora ana sing ala, program kasebut ora bakal menehi jawaban sing salah. Survivability tegese cepet utawa mengko soko apik bakal kelakon, yaiku program cepet utawa mengko bakal menehi jawaban sing bener. Minangka aturan, keamanan minangka indikator sing luwih penting; kesalahan paling asring kedadeyan ing kene. Mulane, kanggo ngirit wektu, aku ora bakal ngomong babagan kelangsungan hidup, sanajan, mesthine, uga penting.
Kita entuk safety kanthi nemtokake sakumpulan kahanan awal sing bisa ditindakake. Lan kapindho, hubungan karo kabeh negara sabanjure bisa kanggo saben negara. Ayo dadi kaya ilmuwan lan nemtokake negara kanthi matematis. Sakumpulan negara wiwitan diterangake kanthi rumus, contone, ing kasus algoritma Euclidean: (x = M) ∧ (y = N). Kanggo nilai tartamtu M и N mung ana siji negara wiwitan. Hubungan karo negara sabanjure diterangake kanthi rumus ing ngendi variabel negara sabanjure ditulis kanthi prima, lan variabel negara saiki ditulis tanpa prima. Ing kasus algoritma Euclidean, kita bakal ngatasi disjunction saka rong rumus, ing salah sijine x minangka nilai paling gedhe, lan ing nomer loro - y:
Ing kasus sing sepisanan, nilai anyar y padha karo nilai y sadurunge, lan entuk nilai anyar x kanthi nyuda variabel sing luwih cilik saka sing luwih gedhe. Ing kasus kapindho, kita nindakake sebaliknya.
Ayo bali menyang algoritma Euclidean. Upamane maneh M = 12, N = 18. Iki nemtokake negara wiwitan siji, (x = 12) ∧ (y = 18). Banjur kita pasang nilai kasebut menyang rumus ing ndhuwur lan entuk:
Mangkene siji-sijine solusi sing bisa ditindakake: x' = 18 - 12 ∧ y' = 12, lan kita entuk prilaku: [x = 12, y = 18]. Kanthi cara sing padha, kita bisa nggambarake kabeh negara ing prilaku kita: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
Ing negara pungkasan [x = 6, y = 6] loro bagéan saka expression bakal palsu, mulane iku ora duwe negara sabanjuré. Dadi, kita duwe spesifikasi lengkap langkah kapindho - kaya sing kita deleng, iki matématika sing cukup biasa, kaya para insinyur lan ilmuwan, lan ora aneh, kaya ing ilmu komputer.
Rumus loro iki bisa digabung dadi siji rumus logika temporal. Iku elegan lan gampang kanggo nerangake, nanging saiki ora ana wektu. Kita bisa uga butuh logika temporal mung kanggo properti liveliness; kanggo keamanan ora dibutuhake. Aku ora kaya logika temporal, iku ora cukup matematika biasa, nanging ing cilik saka liveliness iku ala perlu.
Ing algoritma Euclidean kanggo saben nilai x и y ana nilai unik x' и y', sing nggawe hubungan karo negara sabanjure bener. Ing tembung liyane, algoritma Euclidean iku deterministik. Kanggo model algoritma nondeterministik, negara saiki kudu sawetara kemungkinan negara mangsa, lan saben nilai saka variabel unprimed kudu duwe sawetara nilai saka variabel primed supaya hubungan kanggo negara sabanjuré bener. Iki ora angel ditindakake, nanging aku ora bakal menehi conto saiki.
Kanggo nggawe alat kerja, sampeyan butuh matematika formal. Kepiye carane nggawe spesifikasi resmi? Kanggo nindakake iki, kita butuh basa resmi, contone. . Spesifikasi algoritma Euclidean ing basa iki bakal katon kaya iki:
Simbol tandha padha karo segi telu tegese nilai ing sisih kiwa tandha ditemtokake padha karo nilai ing sisih tengen tandha. Intine, spesifikasi minangka definisi, ing kasus kita rong definisi. Kanggo spesifikasi ing TLA + sampeyan kudu nambah deklarasi lan sawetara sintaks, kaya ing slide ing ndhuwur. Ing ASCII bakal katon kaya iki:
Nalika sampeyan bisa ndeleng, ora ana sing rumit. Spesifikasi ing TLA + bisa diverifikasi, yaiku, bisa ngliwati kabeh prilaku sing bisa ditindakake ing model cilik. Ing kasus kita, model iki bakal dadi nilai tartamtu M и N. Iki minangka cara verifikasi sing efektif lan gampang banget kanthi otomatis. Kajaba iku, iku bisa kanggo nulis bukti resmi saka bebener lan mriksa wong mechanically, nanging iki njupuk akèh wektu, supaya meh ora ana sing nindakake iki.
Kerugian utama TLA + yaiku matematika, lan programer lan ilmuwan komputer wedi karo matematika. Sepisanan iki muni kaya guyon, nanging, sayangé, aku ngomong iki ing kabeh serius. Sawijining kanca kerjaku mung ngandhani kepiye carane dheweke nyoba nerangake TLA + menyang sawetara pangembang. Sanalika formula katon ing layar, mripate langsung dadi kaca. Dadi yen TLA + medeni, sampeyan bisa nggunakake , yaiku sejenis basa pemrograman dolanan. Ekspresi ing PlusCal bisa dadi ekspresi TLA +, yaiku ekspresi matematika. Kajaba iku, PlusCal duwe sintaks kanggo algoritma non-deterministik. Amarga PlusCal bisa nulis ekspresi TLA +, luwih ekspresif tinimbang basa pemrograman sing nyata. Sabanjure, PlusCal dikompilasi dadi spesifikasi TLA+ sing gampang diwaca. Iki ora ateges, mesthi, spesifikasi PlusCal sing kompleks bakal dadi prasaja ing TLA + - mung yen korespondensi ing antarane dheweke jelas, ora ana kerumitan tambahan sing bakal katon. Pungkasan, spesifikasi iki bisa diverifikasi nggunakake alat TLA +. Umumé, PlusCal bisa mbantu ngatasi fobia matématika; gampang dimangertèni malah kanggo programer lan ilmuwan komputer. Aku nerbitake algoritma kanggo sawetara wektu (udakara 10 taun) kepungkur.
Mbok menawa ana sing bakal mbantah manawa TLA + lan PlusCal minangka matematika, lan matématika mung bisa digunakake kanthi conto sing digawe. Ing laku, sampeyan butuh basa nyata kanthi jinis, prosedur, obyek, lan liya-liyane. Iki salah. Mangkene Chris Newcomb, sing kerja ing Amazon, nulis: "Kita wis nggunakake TLA + ing sepuluh proyek gedhe, lan ing saben kasus panggunaane nggawe bedane sing signifikan kanggo pangembangan amarga kita bisa nyekel kewan omo sing mbebayani sadurunge produksi, lan amarga menehi wawasan lan kapercayan sing dibutuhake kanggo nggawe agresif. optimasi kinerja tanpa mengaruhi bebener program". Sampeyan bisa kerep krungu yen nggunakake cara formal kita njaluk kode ora efisien - ing laku, kabeh iku persis ngelawan. Kajaba iku, ana persepsi yen manajer ora bisa yakin yen perlu kanggo metode formal, sanajan programer yakin babagan kegunaane. Lan Newcomb nyerat: "Manager saiki meksa nindakake kabeh cara kanggo nulis spesifikasi ing TLA +, lan khusus nyedhiyakake wektu kanggo iki". Dadi, nalika manajer ndeleng manawa TLA + bisa digunakake, dheweke bakal nampa. Chris Newcomb nulis iki kira-kira nem sasi kepungkur (Oktober 2014), nanging saiki, aku ngerti, TLA + digunakake ing 14 proyek, ora 10. Conto liyane ana hubungane karo desain XBox 360. Intern teka Charles Thacker lan wrote specifications kanggo sistem memori. Thanks kanggo spesifikasi iki, bug ditemokake sing ora bisa dideteksi lan bakal nyebabake saben XBox 360 nabrak sawise patang jam digunakake. Insinyur saka IBM ngonfirmasi manawa tes kasebut ora bakal ndeteksi bug iki.
Sampeyan bisa maca liyane babagan TLA + ing Internet, nanging saiki ayo ngomong babagan spesifikasi informal. Kita arang kudu nulis program sing ngitung pembagi paling umum lan liya-liyane. Luwih kerep kita nulis program kaya alat printer cantik sing daktulis kanggo TLA +. Sawise pangolahan sing paling gampang, kode TLA + bakal katon kaya iki:
Nanging ing conto ing ndhuwur, pangguna paling kamungkinan pengin konjungsi lan pratandha witjaksono didadekake siji. Dadi format sing bener bakal katon kaya iki:
Coba conto liyane:
Ing kene, ing nalisir, Alignment saka pratandha witjaksono, tambahan lan multiplikasi ing sumber wis acak, supaya Processing paling prasaja cukup cukup. Umumé, ora ana definisi matematika sing tepat babagan format sing bener, amarga "bener" ing kasus iki tegese "apa sing dikarepake pangguna," lan iki ora bisa ditemtokake kanthi matematis.
Kayane yen kita ora duwe definisi bebener, mula spesifikasi kasebut ora ana gunane. Nanging kuwi ora bener. Mung amarga kita ora ngerti apa sing kudu ditindakake dening program, ora ateges kita ora perlu mikir babagan cara kerjane - sebaliknya, kita kudu ngupayakake luwih akeh. Spesifikasi utamane penting ing kene. Ora mungkin kanggo nemtokake program optimal kanggo printing terstruktur, nanging iki ora ateges kita ora kudu nindakake kabeh, lan nulis kode minangka aliran kesadaran ora kaya ngono. Aku rampung nulis specification saka enem aturan karo definisi ing wangun komentar ing file Jawa. Ing ngisor iki conto salah sawijining aturan: a left-comment token is LeftComment aligned with its covering token. Aturan iki ditulis ing, ayo ngomong, matematika Inggris: LeftComment aligned, left-comment и covering token - istilah karo definisi. Iki carane matématikawan njlèntrèhaké matématika: padha nulis definisi istilah lan, adhedhasar iku, nggawe aturan. Keuntungan saka spesifikasi iki yaiku enem aturan luwih gampang dingerteni lan debug tinimbang 850 baris kode. Aku kudu ujar manawa nulis aturan kasebut ora gampang; butuh wektu akeh kanggo debug. Aku nulis kode khusus kanggo maksud iki sing ngandhani aturan sing digunakake. Amarga aku dites enem aturan iki karo sawetara conto, Aku ora kudu debug 850 baris kode, lan kewan omo cukup gampang kanggo nggoleki. Jawa duwe alat sing apik kanggo iki. Yen aku mung nulis kode kasebut, mesthine bakal saya suwe saya suwe lan format kasebut bakal kurang kualitas.
Napa spesifikasi formal ora bisa digunakake? Ing tangan siji, eksekusi sing bener ora penting banget ing kene. Cetakan sing wis kabentuk mesthi ora kepenak kanggo sawetara, mula aku ora kudu nindakake kanthi bener ing kabeh kahanan sing ora biasa. Sing luwih penting yaiku aku ora duwe alat sing cukup. Pemeriksa model TLA + ora ana gunane ing kene, mula aku kudu nulis conto kanthi tangan.
Spesifikasi sing diwenehake nduweni fitur sing umum kanggo kabeh spesifikasi. Tingkat sing luwih dhuwur tinimbang kode. Bisa dileksanakake ing basa apa wae. Ora ana piranti utawa cara kanggo nulis. Ora ana kursus pemrograman sing bakal mbantu sampeyan nulis spesifikasi iki. Lan ora ana alat sing bisa nggawe spesifikasi iki ora perlu, kajaba manawa sampeyan nulis basa khusus kanggo nulis program cetakan terstruktur ing TLA +. Akhire, specification iki ora ngomong apa-apa bab carane persis kita bakal nulis kode, iku mung negara apa kode. Kita nulis spesifikasi kanggo mbantu kita mikir babagan masalah kasebut sadurunge miwiti mikir babagan kode kasebut.
Nanging spesifikasi iki uga nduweni fitur sing mbedakake karo spesifikasi liyane. 95% spesifikasi liyane luwih cendhek lan luwih prasaja:
Kajaba iku, spesifikasi iki minangka set aturan. Iki biasane minangka tandha spesifikasi sing ora apik. Ngerteni konsekwensi saka seperangkat aturan cukup angel, mula aku kudu nglampahi akeh wektu kanggo debugging. Nanging, ing kasus iki aku ora bisa nemokake cara sing luwih apik.
Sampeyan kudu ngomong sawetara tembung babagan program sing terus-terusan. Biasane padha operate ing podo karo, kayata sistem operasi utawa sistem mbagekke. Mung sawetara wong sing bisa ngerti ing pikirane utawa ing kertas, lan aku ora kalebu, sanajan aku biyen bisa nindakake. Mulane, kita butuh alat sing bakal mriksa karya kita - contone, TLA + utawa PlusCal.
Napa aku kudu nulis spesifikasi yen aku wis ngerti apa sing kudu ditindakake kode kasebut? Nyatane, aku mung mikir aku ngerti. Kajaba iku, kanthi spesifikasi sing ana, wong njaba ora perlu maneh ndeleng kode kasebut kanggo ngerti apa sing ditindakake. Aku duwe aturan: ora ana aturan umum. Ana pangecualian kanggo aturan iki mesthi, iki mung aturan umum aku tindakake: specification saka apa kode ngirim wong kabeh padha kudu ngerti nalika nggunakake kode sing.
Dadi, apa sing kudu dingerteni para programer babagan mikir? Kanggo miwiti, padha karo saben wong: yen sampeyan ora nulis, sampeyan mung mikir. Uga, sampeyan kudu mikir sadurunge kode, sing tegese sampeyan kudu nulis sadurunge kode. Spesifikasi yaiku apa sing kita tulis sadurunge miwiti coding. Spesifikasi dibutuhake kanggo kode apa wae sing bisa digunakake utawa diganti dening sapa wae. Lan "wong" iki bisa uga dadi penulis kode sasi sawise ditulis. A specification dibutuhake kanggo program gedhe lan sistem, kanggo kelas, kanggo cara, lan kadhangkala malah kanggo bagean Komplek saka cara siji. Apa persis sampeyan kudu nulis babagan kode kasebut? Sampeyan kudu njlèntrèhaké apa sing ditindakake, yaiku, sing bisa migunani kanggo sapa wae sing nggunakake kode iki. Kadhangkala uga perlu kanggo nemtokake persis carane kode bisa nggayuh tujuane. Yen kita ngliwati metode iki ing kursus algoritma, banjur diarani algoritma. Yen ana sing luwih khusus lan anyar, mula diarani desain tingkat dhuwur. Ora ana prabédan resmi ing kene: loro-lorone minangka model abstrak saka program kasebut.
Kepiye carane sampeyan kudu nulis spesifikasi kode? Wangsulan: Bab ingkang utama: iku kudu siji tingkat luwih dhuwur tinimbang kode dhewe. Iku kudu njlèntrèhaké negara lan prilaku. Sampeyan kudu ketat kaya tugas sing dibutuhake. Yen sampeyan nulis spesifikasi babagan cara ngleksanakake tugas, mula bisa ditulis nganggo pseudocode utawa nggunakake PlusCal. Sampeyan kudu sinau nulis spesifikasi nggunakake spesifikasi formal. Iki bakal menehi katrampilan sing dibutuhake sing uga bakal mbantu karo sing ora resmi. Kepiye carane sampeyan bisa sinau nulis spesifikasi resmi? Nalika kita sinau kanggo program, kita wrote program lan banjur debugged mau. Bab sing padha ing kene: sampeyan kudu nulis spesifikasi, mriksa karo model checker, lan ndandani kesalahane. TLA+ bisa uga dudu basa sing paling apik kanggo spesifikasi resmi, lan basa liya bakal luwih cocog kanggo kabutuhan khusus sampeyan. Sing paling apik babagan TLA + yaiku nindakake tugas sing apik kanggo ngajar pamikiran matematika.
Kepiye cara ngubungake spesifikasi lan kode? Nggunakake komentar sing nyambungake konsep matematika lan implementasine. Yen sampeyan nggarap grafik, banjur ing tingkat program sampeyan bakal duwe susunan node lan array pranala. Dadi, sampeyan kudu nulis kepiye carane grafik ditindakake dening struktur pemrograman kasebut.
Perlu dicathet yen ora ana sing kasebut ing ndhuwur sing ditrapake kanggo proses nulis kode dhewe. Nalika sampeyan nulis kode, yaiku, nindakake langkah katelu, sampeyan uga kudu mikir lan mikir liwat program kasebut. Yen subtugas dadi rumit utawa ora jelas, sampeyan kudu nulis spesifikasi kasebut. Nanging aku ora ngomong babagan kode dhewe ing kene. Sampeyan bisa nggunakake basa pamrograman apa wae, metodologi apa wae, iki dudu babagan. Uga, ora ana ing ndhuwur sing ngilangi kabutuhan kanggo nyoba lan debug kode sampeyan. Sanajan model abstrak ditulis kanthi bener, bisa uga ana kewan omo ing implementasine.
Spesifikasi nulis minangka langkah tambahan ing proses coding. Thanks kanggo iku, akeh kesalahan bisa kejiret karo kurang gaweyan - kita ngerti iki saka pengalaman programer saka Amazon. Kanthi spesifikasi, kualitas program dadi luwih dhuwur. Dadi, kenapa kita asring lunga tanpa dheweke? Amarga nulis iku angel. Nanging nulis iku angel, amarga iki sampeyan kudu mikir, lan mikir uga angel. Iku tansah luwih gampang kanggo ndalang sampeyan mikir. Analogi bisa digambar ing kene kanthi mlaku - luwih sithik sampeyan mlayu, luwih alon sampeyan mlayu. Sampeyan kudu nglatih otot lan latihan nulis. Butuh latihan.
Spesifikasi bisa uga salah. Sampeyan bisa uga wis nggawe kesalahan nang endi wae, utawa syarat bisa diganti, utawa perbaikan bisa uga kudu ditindakake. Kode apa wae sing digunakake sapa wae kudu diganti, supaya cepet utawa mengko spesifikasi kasebut ora cocog karo program kasebut. Saenipun, ing kasus iki, sampeyan kudu nulis specification anyar lan rampung nulis ulang kode. Kita ngerti banget yen ora ana sing nindakake iki. Ing laku, kita patch kode lan mbok menawa nganyari specification. Yen iki bound kanggo kelakon cepet utawa mengko, banjur apa nulis specifications ing kabeh? Kaping pisanan, kanggo wong sing bakal nyunting kode sampeyan, saben tembung tambahan ing spesifikasi bakal entuk bobote emas, lan wong iki bisa uga sampeyan. Aku kerep nyepak dhewe amarga ora cukup spesifik nalika nyunting kode. Lan aku nulis luwih specifications saka kode. Mulane, nalika sampeyan ngowahi kode, spesifikasi kudu tansah dianyari. Kapindho, saben suntingan kode dadi luwih elek, dadi luwih angel diwaca lan dijaga. Iki minangka paningkatan entropi. Nanging yen sampeyan ora miwiti karo specification, banjur saben baris sampeyan nulis bakal suntingan, lan kode bakal gedhe banget lan hard kanggo maca saka wiwitan.
Minangka ngandika , ora ana perang sing menang miturut rencana, lan ora ana perang sing menang tanpa rencana. Lan dheweke ngerti babagan perang. Ana panemu manawa nulis spesifikasi minangka mbuwang wektu. Kadhangkala iki bener, lan tugas kasebut gampang banget, mula ora ana gunane kanggo mikir. Nanging sampeyan kudu tansah elinga yen sampeyan menehi saran ora kanggo nulis specifications, iku ateges sing ora kanggo mikir. Lan sampeyan kudu mikir babagan iki saben wektu. Mikir liwat tugas ora njamin sampeyan ora bakal nggawe kesalahan. Kaya sing kita ngerteni, ora ana sing nemokke tongkat sihir, lan program minangka tugas sing angel. Nanging yen sampeyan ora mikir babagan tugas kasebut, sampeyan mesthi bakal nggawe kesalahan.
Sampeyan bisa maca liyane babagan TLA + lan PlusCal ing situs web khusus, sampeyan bisa pindhah menyang kaca ngarep . Mekaten kagem kula, matur nuwun kawigatosanipun.
Elinga yen iki terjemahan. Nalika sampeyan nulis komentar, elinga yen penulis ora bakal maca. Yen sampeyan pengin ngobrol karo penulis, dheweke bakal ana ing konferensi Hydra 2019, sing bakal dianakake tanggal 11-12 Juli 2019 ing St. Tiket bisa dituku .
Source: www.habr.com