Artikel ieu mangrupa tarjamahan . Tapi saméméh nya bubuka saeutik. Kumaha zombies kabentuk? Sarerea ngagaduhan kana kaayaan dimana maranéhna rék narik babaturan atawa batur sapagawean nepi ka tingkat maranéhna, tapi teu hasil. Tur éta teu jadi loba sareng anjeun sakumaha kalayan anjeunna yén "teu dianggo kaluar": dina hiji sisi skala mangrupa gaji normal, tugas, jeung saterusna, sarta di sisi séjén, kudu mikir. Pikiran teu pikaresepeun sareng nyeri. Anjeunna gancang nyerah sarta terus nulis kode tanpa ngahurungkeun otak na pisan. Anjeun ngabayangkeun sabaraha usaha nu diperlukeun pikeun nungkulan halangan tina helplessness diajar, sarta anjeun ngan teu ngalakukeun eta. Ieu kumaha zombies kabentuk, nu, sigana, bisa diubaran, tapi sigana teu saurang ogé bakal ngalakukeun eta.
Nalika kuring ningali éta (enya, sarua sobat ti buku ajar) sarta teu nyieun laporan, tapi sesi tanya jawab, Kuring éta saeutik waspada. Bisi wae, Leslie mangrupakeun élmuwan kawentar dunya, panulis karya fundamental dina komputasi disebarkeun, sarta anjeun ogé tiasa kenal anjeunna ku hurup La dina kecap LaTeX - "Lamport TeX". Faktor pikahariwangeun kadua nyaéta saratna: saha waé anu datang kedah (leres-leres gratis) ngadangukeun sababaraha laporan sateuacanna, naroskeun sahenteuna hiji patarosan ngeunaan aranjeunna, teras sumping. Kuring mutuskeun ningali naon anu disiarkeun ku Lamport di dinya - sareng éta saé! Éta persis éta, tautan-pil sihir pikeun ngubaran zombie. Kuring ngingetkeun anjeun: tina téks, pencinta metodologi super-fléksibel sareng jalma-jalma anu henteu resep nguji naon anu ditulis tiasa diduruk.
Sanggeus habrokat, nyatana tarjamahan seminar dimimitian. Senang maca!
Naon waé tugas anu anjeun lakukeun, anjeun kedah ngaliwat tilu léngkah:
- mutuskeun naon tujuan anjeun hoyong ngahontal;
- mutuskeun kumaha anjeun bakal ngahontal tujuan anjeun;
- datang ka tujuan anjeun.
Ieu ogé lumaku pikeun programming. Nalika urang nyerat kode, urang kedah:
- mutuskeun naon program kudu ngalakukeun;
- nangtukeun kumaha kudu ngalakukeun tugas na;
- nulis kode nu cocog.
Léngkah terakhir, tangtosna, penting pisan, tapi kuring moal nyarioskeun ayeuna. Gantina, urang bakal ngabahas dua kahiji. Unggal programer ngalakukeun aranjeunna sateuacan ngamimitian damel. Anjeun moal calik pikeun nyerat kecuali anjeun parantos mutuskeun naha anjeun nyerat browser atanapi pangkalan data. Hiji gagasan tangtu tujuan kudu hadir. Sareng anjeun pasti mikirkeun naon anu bakal dilakukeun ku program éta, sareng henteu nyerat kumaha waé kalayan harepan kodeu kumaha waé bakal janten panyungsi.
Kumaha kahayang kode ieu pre-pamikiran lumangsung? Sabaraha usaha urang kedah nempatkeun kana ieu? Eta sadayana gumantung kana kumaha kompléks masalah urang ngarengsekeun. Anggap urang rék nulis sistem distribusi toleran-lepat. Dina hal ieu, urang kedah mikirkeun hal-hal sacara saksama sateuacan urang calik kana kode. Kumaha lamun urang ngan perlu increment variabel integer ku 1? Dina glance kahiji, sagalana geus trivial dieu, sarta euweuh pamikiran diperlukeun, tapi lajeng urang inget yen hiji mudal bisa lumangsung. Ku alatan éta, sanajan dina urutan ngartos naha hiji masalah basajan atawa kompléks, Anjeun mimitina kudu mikir.
Upami anjeun mikirkeun solusi anu mungkin pikeun masalah sateuacanna, anjeun tiasa nyingkahan kasalahan. Tapi ieu merlukeun pamikiran anjeun jelas. Pikeun ngahontal ieu, anjeun kedah nyerat pikiran anjeun. Abdi resep pisan kana kutipan Dick Guindon: "Nalika anjeun nyerat, alam nunjukkeun anjeun kumaha jalanna pamikiran anjeun." Upami anjeun henteu nyerat, anjeun ngan ukur mikir yén anjeun mikir. Sareng anjeun kedah nyerat pikiran anjeun dina bentuk spésifikasi.
Spésifikasi ngalakukeun seueur fungsi, khususna dina proyék ageung. Tapi kuring ngan ukur bakal ngobrol ngeunaan salah sahijina: aranjeunna ngabantosan urang mikir sacara jelas. Pikiran anu jelas penting pisan sareng sesah, janten di dieu urang peryogi bantosan. Dina basa naon urang kedah nyerat spésifikasi? Sacara umum, ieu mangrupikeun patarosan anu munggaran pikeun programer: basa naon anu bakal urang tulis. Henteu aya jawaban anu leres pikeun éta: masalah anu urang rengsekeun rupa-rupa teuing. Kanggo sababaraha, TLA + mangrupikeun basa spésifikasi anu kuring dikembangkeun. Pikeun batur, éta leuwih merenah ngagunakeun Cina. Sagalana gumantung kana kaayaan.
Anu langkung penting nyaéta patarosan anu sanés: kumaha carana ngahontal pamikiran anu langkung jelas? Jawaban: Urang kedah mikir sapertos ilmuwan. Ieu mangrupikeun cara mikir anu parantos ngabuktikeun dirina salami 500 taun ka pengker. Dina sains, urang ngawangun model matematik realitas. Astronomi éta sugan elmu munggaran dina rasa ketat kecap. Dina modél matematika anu digunakeun dina astronomi, benda langit némbongan salaku titik kalayan massa, posisi sareng moméntum, sanaos kanyataanana éta objék anu kompleks pisan sareng gunung sareng sagara, pasang sareng pasang. Modél ieu, kawas sagala séjén, dijieun pikeun ngajawab masalah tangtu. Éta hadé pikeun nangtukeun dimana nunjuk teleskop upami anjeun kedah mendakan planét. Tapi upami anjeun hoyong ngaramalkeun cuaca di planét ieu, modél ieu moal jalan.
Matematika ngamungkinkeun urang pikeun nangtukeun sipat model. Sareng élmu nunjukkeun kumaha sipat ieu pakait sareng kanyataan. Hayu urang ngobrol ngeunaan elmu urang, elmu komputer. Realitas anu kami damel nyaéta sistem komputasi tina rupa-rupa: prosesor, konsol kaulinan, komputer, program palaksanaan, sareng sajabana. Kuring bakal ngobrol ngeunaan ngajalankeun program dina komputer, tapi sacara umum, sakabéh conclusions ieu dilarapkeun ka sagala sistem komputasi. Dina élmu urang, urang ngagunakeun loba model béda: mesin Turing, sawaréh maréntahkeun susunan acara, sarta loba batur.
Naon program? Ieu mangrupikeun kode anu tiasa dianggap mandiri. Anggap urang kedah nyerat browser. Kami ngalaksanakeun tilu pancén: urang ngarancang pandangan pangguna ngeunaan program, teras nyerat diagram tingkat luhur program, sareng tungtungna nyerat kodeu. Nalika urang nyerat kodeu, urang sadar yén urang kedah nyerat formatter téks. Di dieu urang deui kudu ngajawab tilu masalah: nangtukeun naon téks alat ieu bakal balik; pilih algoritma pikeun pormat; nulis kode. Tugas ieu gaduh subtugas sorangan: leres nyelapkeun tanda hubung kana kecap. Kami ogé ngabéréskeun subtugas ieu dina tilu léngkah - sakumaha anu anjeun tingali, aranjeunna diulang dina sababaraha tingkatan.
Hayu urang nganggap di leuwih jéntré lengkah kahiji: naon masalah program solves. Di dieu, urang paling sering model program salaku fungsi nu nyokot sababaraha input sarta ngahasilkeun sababaraha kaluaran. Dina matematika, hiji fungsi biasana digambarkeun salaku susunan susunan pasangan. Contona, fungsi kuadrat pikeun wilangan alam digambarkeun salaku set {<0,0>, <1,1>, <2,4>, <3,9>, …}. Domain tina fungsi ieu mangrupikeun set unsur-unsur mimiti unggal pasangan, nyaéta, wilangan alami. Pikeun nangtukeun hiji fungsi, urang kudu nangtukeun wengkuan jeung rumus na.
Tapi fungsi dina matematika henteu sarua jeung fungsi dina basa program. Matematika langkung gampang. Kusabab kuring teu boga waktu pikeun conto kompléks, hayu urang nganggap hiji basajan: fungsi dina C atawa métode statik di Java nu mulih divisor umum greatest dua integer. Dina spésifikasi metoda ieu, urang bakal nulis: ngitung GCD(M,N) pikeun argumen M и Ndimana GCD(M,N) - fungsi anu domainna mangrupa susunan pasangan integer, sarta nilai balikna mangrupa integer pangbadagna anu bisa dibagi ku M и N. Kumaha model ieu pakait sareng kanyataan? Modelna beroperasi dina integer, sedengkeun dina C atanapi Java urang gaduh 32-bit int. Modél ieu ngamungkinkeun urang pikeun mutuskeun naha algoritma éta leres GCD, tapi moal nyegah kasalahan overflow. Ieu ngabutuhkeun modél anu langkung kompleks, anu henteu aya waktos.
Hayu urang ngobrol ngeunaan watesan fungsi salaku modél. Sababaraha program (sapertos sistem operasi) henteu ngan ukur ngabalikeun nilai anu tangtu pikeun argumen anu tangtu, aranjeunna tiasa jalan terus. Salaku tambahan, fungsi salaku modél henteu cocog pikeun léngkah kadua: ngarencanakeun kumaha ngabéréskeun masalah. Diurutkeun gancang sareng gelembung diurutkeun ngitung fungsi anu sami, tapi aranjeunna algoritma anu béda-béda. Ku alatan éta, pikeun ngajelaskeun kumaha tujuan program kahontal, kuring ngagunakeun modél béda, hayu urang sebut wae model behavioral standar. Program di jerona digambarkeun salaku set sadaya paripolah anu diidinan, masing-masing, kahareupna mangrupikeun sekuen nagara, sareng nagara mangrupikeun tugas nilai kana variabel.
Hayu urang tingali kumaha léngkah kadua pikeun algoritma Euclid. Urang kudu ngitung GCD(M, N). Urang initialize M kumaha xjeung N kumaha y, teras sababaraha kali ngirangan variabel anu langkung alit tina variabel anu langkung ageung dugi ka sami. Contona, upami M = 12jeung N = 18, urang tiasa ngajelaskeun paripolah ieu:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
Sareng upami M = 0 и N = 0? Nol bisa dibagi ku sakabéh angka, jadi euweuh divisor greatest dina hal ieu. Dina kaayaan ieu, urang kedah uih deui ka lengkah munggaran sareng naroskeun: naha urang leres-leres kedah ngitung GCD pikeun nomer non-positip? Upami ieu henteu diperyogikeun, maka anjeun ngan ukur kedah ngarobih spésifikasi.
Di dieu urang kedah ngadamel digression leutik ngeunaan produktivitas. Hal ieu mindeng diukur dina jumlah baris kode ditulis per poé. Tapi karya anjeun leuwih mangpaat lamun anjeun meunang leupas tina sababaraha garis, sabab anjeun boga kamar kirang pikeun bug. Sareng cara panggampangna pikeun ngaleungitkeun kode nyaéta dina léngkah munggaran. Éta mungkin pisan yén anjeun henteu peryogi sadayana lonceng sareng bisik anu anjeun badé laksanakeun. Cara panggancangna pikeun nyederhanakeun program sareng ngahémat waktos nyaéta henteu ngalakukeun hal-hal anu henteu kedah dilakukeun. Léngkah kadua nyaéta poténsi anu paling hemat waktos kadua. Upami anjeun ngukur produktivitas tina segi garis anu ditulis, teras mikirkeun kumaha ngalaksanakeun tugas bakal ngajantenkeun anjeun kurang produktif, sabab bisa ngajawab masalah anu sarua kalawan kode kirang. Abdi teu tiasa masihan statistik pasti di dieu, sabab kuring teu boga jalan ka cacah jumlah garis nu kuring teu nulis alatan kanyataan yén kuring spent waktos on spésifikasi, nyaeta, dina hambalan kahiji jeung kadua. Sareng percobaan henteu tiasa disetél di dieu ogé, sabab dina ékspérimén urang henteu ngagaduhan hak pikeun ngarengsekeun léngkah anu munggaran, tugasna parantos ditangtukeun.
Gampang mopohokeun seueur kasusah dina spésifikasi informal. Aya nanaon hésé dina nulis spésifikasi ketat pikeun fungsi, Kuring moal ngabahas ieu. Gantina, urang bakal ngobrol ngeunaan nulis spésifikasi kuat pikeun paripolah standar. Aya téoréma nu nyebutkeun yén sagala susunan paripolah bisa digambarkeun ngagunakeun sipat kaamanan (kaamanan) jeung sipat survivability (kahirupan). Kaamanan hartosna teu aya anu goréng, program moal masihan jawaban anu salah. Survivability hartina sooner atanapi engké hal alus bakal kajadian, nyaéta program bakal masihan jawaban nu bener sooner atanapi engké. Sakumaha aturan, kaamanan mangrupikeun indikator anu langkung penting, kasalahan anu paling sering lumangsung di dieu. Ku alatan éta, pikeun ngahemat waktos, abdi moal ngobrol ngeunaan survivability, sanajan éta, tangtosna, ogé penting.
Urang ngahontal kaamanan ku resep, kahiji, susunan mungkin kaayaan awal. Sareng kadua, hubungan sareng sadaya kaayaan salajengna anu mungkin pikeun unggal nagara. Hayu urang meta salaku élmuwan jeung nangtukeun kaayaan matematis. Susunan kaayaan awal digambarkeun ku rumus, contona, dina kasus algoritma Euclid: (x = M) ∧ (y = N). Pikeun nilai tangtu M и N ngan aya hiji kaayaan awal. Hubungan jeung kaayaan hareup digambarkeun ku rumus nu variabel kaayaan hareup ditulis kalawan prima, sarta variabel kaayaan ayeuna ditulis tanpa prima a. Dina kasus algoritma Euclid, urang bakal nungkulan disjunction dua rumus, dina salah sahiji nu. x nyaeta nilai pangbadagna, sarta dina kadua - y:
Dina kasus kahiji, nilai anyar y sarua jeung nilai saméméhna y, sarta kami meunang nilai anyar x ku subtracting variabel leutik ti nu leuwih gede. Dina kasus kadua, urang ngalakukeun sabalikna.
Hayu urang balik ka algoritma Euclid urang. Hayu urang nganggap deui éta M = 12, N = 18. Ieu nangtukeun kaayaan awal tunggal, (x = 12) ∧ (y = 18). Urang teras pasang nilai-nilai éta kana rumus di luhur sareng kéngingkeun:
Ieu hiji-hijina solusi anu mungkin: x' = 18 - 12 ∧ y' = 12sarta kami meunang kabiasaan: [x = 12, y = 18]. Nya kitu, urang tiasa ngajelaskeun sagala kaayaan dina kabiasaan urang: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
Dina kaayaan panungtungan [x = 6, y = 6] duanana bagian ekspresi bakal palsu, jadi teu boga kaayaan salajengna. Ku kituna, urang boga spésifikasi lengkep lengkah kadua - sakumaha anjeun tiasa ningali, ieu téh matematik rada biasa, kawas dina insinyur sarta élmuwan, sarta teu aneh, kawas dina elmu komputer.
Dua rumus ieu bisa digabungkeun jadi hiji rumus logika temporal. Anjeunna elegan sareng gampang dijelaskeun, tapi ayeuna teu aya waktos pikeun anjeunna. Urang bisa butuh logika temporal ukur keur harta liveliness, teu diperlukeun pikeun kaamanan. Abdi henteu resep logika temporal sapertos kitu, éta sanés matematika anu biasa, tapi dina hal liveliness mangrupikeun jahat anu diperyogikeun.
Dina algoritma Euclid, pikeun tiap nilai x и y boga nilai unik x' и y', anu ngajantenkeun hubungan sareng kaayaan salajengna leres. Dina basa sejen, algoritma Euclid nyaéta deterministik. Pikeun model algoritma non-deterministik, kaayaan ayeuna kudu boga sababaraha mungkin kaayaan hareup, sarta yén unggal nilai variabel unprimed boga sababaraha nilai variabel primed sahingga hubungan jeung kaayaan salajengna bener. Ieu gampang dilakukeun, tapi kuring moal masihan conto ayeuna.
Pikeun nyieun alat anu tiasa dianggo, anjeun peryogi matematika formal. Kumaha carana sangkan spésifikasi formal? Pikeun ngalakukeun ieu, urang peryogi basa formal, contona, . Spésifikasi algoritma Euclid bakal siga kieu dina basa ieu:
Simbol tanda sarua jeung segitiga hartina nilai di kénca tanda diartikeun sarua jeung nilai katuhu tanda. Intina, spésifikasi mangrupikeun definisi, dina hal urang dua definisi. Pikeun spésifikasi dina TLA +, anjeun kedah nambihan deklarasi sareng sababaraha sintaksis, sapertos dina slide di luhur. Dina ASCII bakal katingali sapertos kieu:
Sakumaha anjeun tiasa tingali, euweuh pajeulit. Spésifikasi pikeun TLA + tiasa diuji, nyaéta ngaliwat sadaya paripolah anu mungkin dina modél leutik. Dina hal urang, model ieu bakal nilai tangtu M и N. Ieu mangrupikeun metode verifikasi anu efisien sareng saderhana anu lengkep otomatis. Ieu oge mungkin keur nulis proofs bebeneran formal jeung pariksa aranjeunna mechanically, tapi ieu butuh loba waktu, jadi ampir teu saurang ogé ngalakukeun ieu.
Karugian utama TLA + nyaéta yén éta matematika, sareng programer sareng élmuwan komputer sieun matématika. Dina glance kahiji, ieu disada kawas lulucon, tapi, hanjakalna, maksudna dina sagala seriousness. Babaturan kuring ngan ukur nyarioskeun kumaha anjeunna nyobian ngajelaskeun TLA + ka sababaraha pamekar. Pas rumus muncul dina layar, aranjeunna langsung janten panon kaca. Janten upami TLA + nyingsieunan anjeun, anjeun tiasa nganggo , éta jenis basa programming kaulinan. Ekspresi dina PlusCal tiasa janten ekspresi TLA + naon waé, nyaéta, sacara umum, éksprési matematik naon waé. Salaku tambahan, PlusCal gaduh sintaksis pikeun algoritma non-deterministik. Kusabab PlusCal tiasa nyerat ekspresi TLA + naon waé, PlusCal langkung ekspresif tibatan basa pamrograman anu nyata. Salajengna, PlusCal disusun kana spésifikasi TLA+ anu gampang dibaca. Ieu henteu hartosna, tangtosna, spésifikasi PlusCal kompléks bakal janten basajan dina TLA + - ngan korespondensi antara aranjeunna atra, moal aya pajeulitna tambahan. Tungtungna, spésifikasi ieu tiasa diverifikasi ku alat TLA +. Sadayana, PlusCal tiasa ngabantosan ngatasi phobia matematika sareng gampang kahartos bahkan pikeun programer sareng élmuwan komputer. Baheula, kuring nyebarkeun algoritma pikeun sababaraha waktos (sakitar 10 taun).
Panginten aya anu bakal ngabantah yén TLA + sareng PlusCal mangrupikeun matematika, sareng matématika ngan ukur dianggo dina conto anu diciptakeun. Dina prakna, anjeun peryogi basa anu nyata sareng jinis, prosedur, objék, sareng sajabana. Ieu salah. Ieu naon Chris Newcomb, anu damel di Amazon, nyerat: "Kami parantos nganggo TLA + dina sapuluh proyék utama, sareng dina unggal kasus, ngagunakeun éta parantos ngajantenkeun bédana anu signifikan pikeun pangwangunan sabab kami tiasa nangkep bug anu bahaya sateuacan urang pencét produksi, sareng kusabab éta masihan kami wawasan sareng kapercayaan anu kami peryogikeun. ngadamel optimasi kinerja agrésif tanpa mangaruhan kabeneran program". Anjeun mindeng bisa ngadéngé yén nalika ngagunakeun métode formal, urang meunang kode episien - dina prakna, sagalana persis sabalikna. Sajaba ti éta, aya hiji pamadegan yén manajer teu bisa yakin kana kabutuhan métode formal, sanajan programer anu yakin kana usefulness maranéhanana. Sareng Newcomb nyerat: "Manajer ayeuna ngadorong keras nyerat spésifikasi pikeun TLA +, sareng sacara khusus nyayogikeun waktos pikeun ieu". Janten nalika manajer ningali yén TLA + berpungsi, aranjeunna resep nampi éta. Chris Newcomb nyerat ieu sakitar genep bulan kapengker (Oktober 2014), tapi ayeuna, sajauh anu kuring terang, TLA + dianggo dina 14 proyék, sanés 10. Conto sanésna aya hubunganana sareng desain XBox 360. Hiji intern sumping ka Charles Thacker sareng wrote spésifikasi pikeun sistem memori. Hatur nuhun kana spésifikasi ieu, bug anu kapanggih anu disebutkeun bakal balik unnoticed, sarta alatan nu unggal XBox 360 bakal ngadat sanggeus opat jam pamakéan. Insinyur IBM negeskeun yén tésna moal mendakan bug ieu.
Anjeun tiasa maca langkung seueur ngeunaan TLA + dina Internét, tapi ayeuna hayu urang ngobrol ngeunaan spésifikasi informal. Urang jarang kudu nulis program nu ngitung divisor pangsaeutikna umum jeung kawas. Langkung sering urang nyerat program sapertos alat panyitak anu saé anu kuring nyerat pikeun TLA +. Saatos ngolah pangbasajanna, kode TLA + bakal siga kieu:
Tapi dina conto di luhur, pamaké paling dipikaresep hayang konjungsi jeung tanda sarua bisa Blok. Janten pormat anu leres bakal katingali sapertos kieu:
Hayu urang mikirkeun conto sejen:
Di dieu, sabalikna, alignment tina sarua, tambahan, sarta multiplication tanda dina sumber éta acak, jadi processing pangbasajanna cukup. Sacara umum, teu aya harti matematik pasti ngeunaan pormat bener, sabab "bener" dina hal ieu hartina "naon pamaké hayang", sarta ieu teu bisa matematis ditangtukeun.
Éta sigana upami urang henteu gaduh definisi bebeneran, maka spésifikasina henteu aya gunana. Tapi henteu. Ngan kusabab urang henteu terang naon anu kedah dilakukeun ku program sanés hartosna urang henteu kedah mikirkeun kumaha jalanna-sabalikna, urang kedah langkung seueur usaha. spésifikasi hususna penting di dieu. Teu mungkin pikeun nangtukeun program optimal pikeun percetakan terstruktur, tapi ieu lain hartosna yén urang teu kedah nyandak eta, sarta nulis kode salaku aliran eling - teu hiji hal anu alus. Tungtungna, kuring nulis spésifikasi genep aturan jeung definisi dina wangun koméntar dina file java. Ieu conto salah sahiji aturan: a left-comment token is LeftComment aligned with its covering token. Aturan ieu ditulis dina, bakal urang sebutkeun, matematika Inggris: LeftComment aligned, left-comment и covering token - istilah jeung definisi. Ieu kumaha ahli matematika ngajelaskeun matematika: aranjeunna nyerat definisi istilah sareng, dumasar kana éta, aturan. Kauntungan tina spésifikasi sapertos kitu nyaéta genep aturan langkung gampang kahartos sareng debug tibatan 850 garis kode. Kuring kudu nyebutkeun yén nulis aturan ieu teu gampang, éta nyandak rada loba waktu pikeun debug aranjeunna. Utamana pikeun tujuan ieu, kuring nyerat kode anu ngalaporkeun aturan mana anu dianggo. Hatur nuhun kana kanyataan yén kuring diuji genep aturan ieu dina sababaraha conto, kuring teu kudu debug 850 garis kode, jeung bug tétéla cukup gampang pikeun manggihan. Java gaduh alat anu saé pikeun ieu. Upami kuring nembé nyerat kodeu, éta bakal nyandak kuring langkung lami, sareng pormatna bakal langkung saé.
Naha spésifikasi formal henteu tiasa dianggo? Di hiji sisi, palaksanaan anu leres henteu penting teuing di dieu. Cetakan struktural pasti moal nyenangkeun saha waé, janten kuring henteu kedah ngajantenkeun éta leres dina sadaya kaayaan anu ganjil. Anu langkung penting nyaéta kanyataan yén kuring henteu gaduh alat anu cekap. Pamariksaan modél TLA + henteu aya gunana di dieu, janten kuring kedah nyerat conto sacara manual.
Spésifikasi di luhur ngagaduhan fitur umum pikeun sadaya spésifikasi. Éta tingkat luhur batan kode. Éta tiasa dilaksanakeun dina basa naon waé. Alat atanapi metode naon waé henteu aya gunana pikeun nyeratna. Henteu aya kursus program anu bakal ngabantosan anjeun nyerat spésifikasi ieu. Sareng teu aya alat anu tiasa ngajantenkeun spésifikasi ieu henteu diperyogikeun, kecuali, tangtosna, anjeun nyerat basa khusus pikeun nyerat program citak terstruktur dina TLA +. Tungtungna, spésifikasi ieu teu ngomong nanaon ngeunaan persis kumaha urang bakal nulis kode, eta ngan nyebutkeun naon kode ieu teu. Urang nulis spésifikasi pikeun mantuan urang mikir ngaliwatan masalah saméméh urang mimitian mikir ngeunaan kode.
Tapi spésifikasi ieu ogé gaduh fitur anu ngabédakeun tina spésifikasi anu sanés. 95% tina spésifikasi séjén nyata pondok tur basajan:
Salajengna, spésifikasi ieu mangrupikeun sakumpulan aturan. Sakumaha aturan, ieu mangrupikeun tanda spésifikasi anu goréng. Ngartos konsékuansi tina sakumpulan aturan anu rada hese, naha kuring kedah nyéépkeun waktos pikeun debugging aranjeunna. Nanging, dina hal ieu, kuring henteu mendakan jalan anu langkung saé.
Eta sia nyebutkeun sababaraha kecap ngeunaan program anu ngajalankeun terus. Sakumaha aturan, aranjeunna tiasa dianggo paralel, contona, sistem operasi atanapi sistem anu disebarkeun. Saeutik pisan jalma anu tiasa ngartos aranjeunna sacara mental atanapi dina kertas, sareng kuring sanés salah sahijina, sanaos kuring sakali tiasa ngalakukeunana. Ku alatan éta, urang peryogi alat anu bakal pariksa karya urang - contona, TLA + atanapi PlusCal.
Naha éta perlu nulis spésifikasi lamun kuring geus terang naon kahayang kode kedah ngalakukeun? Kanyataanna, kuring ngan panginten kuring terang éta. Salaku tambahan, kalayan spésifikasi, urang luar henteu kedah deui asup kana kode pikeun ngartos naon anu anjeunna laksanakeun. Kuring boga aturan: teu kudu aya aturan umum. Aya pengecualian kana aturan ieu, tangtosna, éta hiji-hijina aturan umum anu kuring nuturkeun: spésifikasi naon kodeu kedah nyarioskeun ka jalma sadayana anu peryogi terang nalika nganggo kodeu.
Jadi naon kahayang programer peryogi kauninga ngeunaan pamikiran? Pikeun ngamimitian, sami sareng anu sanés: upami anjeun henteu nyerat, maka sigana anjeun ngan ukur mikir. Ogé, anjeun kedah mikir sateuacan anjeun kode, anu hartosna anjeun kedah nyerat sateuacan anjeun kode. Spésifikasi nyaéta naon anu urang tulis sateuacan urang ngamimitian coding. A spésifikasi diperlukeun pikeun sagala kode nu bisa dipaké atawa dirobah ku saha. Sareng ieu "batur" tiasa janten panulis kode nyalira sabulan saatos ditulis. A spésifikasi diperlukeun pikeun program badag sarta sistem, pikeun kelas, pikeun métode, sarta sakapeung malah pikeun bagian kompléks metoda tunggal. Naon kahayang kudu ditulis ngeunaan kode? Anjeun kedah ngajelaskeun naon anu dilakukeun, nyaéta, naon anu tiasa mangpaat pikeun jalma anu nganggo kode ieu. Kadang-kadang ogé perlu pikeun nangtukeun kumaha kode nu accomplishes tujuanana. Upami urang ngalangkungan metode ieu dina kursus algoritma, maka urang nyauran éta algoritma. Upami éta hal anu langkung khusus sareng énggal, maka kami nyebat éta desain tingkat luhur. Henteu aya bédana formal di dieu: duanana mangrupikeun modél abstrak tina program.
Kumaha kahayang anjeun kedah nyerat spésifikasi kode? Hal utama: kudu hiji tingkat leuwih luhur ti kode sorangan. Éta kedah ngajelaskeun kaayaan sareng paripolah. Kudu jadi ketat sakumaha tugas merlukeun. Upami anjeun nyerat spésifikasi pikeun kumaha ngalaksanakeun tugas, anjeun tiasa nyerat dina pseudocode atanapi nganggo PlusCal. Anjeun kedah diajar kumaha nyerat spésifikasi dina spésifikasi formal. Ieu bakal masihan anjeun katerampilan anu dipikabutuh anu bakal ngabantosan anjeun sareng anu henteu resmi ogé. Kumaha anjeun diajar nulis spésifikasi formal? Nalika urang diajar program, urang nulis program lajeng debugged aranjeunna. Éta sami di dieu: tuliskeun spésifikasina, parios sareng pamariksa modél, sareng ngalereskeun bug. TLA + tiasa janten basa anu pangsaéna pikeun spésifikasi formal, sareng basa sanés sigana langkung saé pikeun kabutuhan khusus anjeun. Kauntungannana TLA + nyaéta ngajarkeun pamikiran matematik anu saé pisan.
Kumaha ngaitkeun spésifikasi sareng kode? Kalayan bantosan koméntar anu ngaitkeun konsép matematika sareng palaksanaanna. Upami anjeun damel sareng grafik, maka dina tingkat program anjeun bakal ngagaduhan susunan titik sareng susunan tautan. Ku alatan éta, anjeun kedah nyerat persis kumaha grafik dilaksanakeun ku struktur pamrograman ieu.
Ieu kudu dicatet yén euweuh di luhur manglaku ka prosés sabenerna nulis kode. Nalika anjeun nyerat kodeu, nyaéta, anjeun ngalaksanakeun léngkah katilu, anjeun ogé kedah mikir sareng mikirkeun program. Upami subtugas tétéla rumit atanapi henteu écés, anjeun kedah nyerat spésifikasi pikeun éta. Tapi kuring henteu ngawangkong ngeunaan kodeu sorangan di dieu. Anjeun tiasa nganggo basa pamrograman naon waé, metodologi naon waé, sanés ngeunaan éta. Ogé, teu aya anu di luhur ngaleungitkeun kabutuhan pikeun nguji sareng debug kode. Malah lamun model abstrak ditulis leres, meureun aya bug dina palaksanaan na.
Nulis spésifikasi mangrupa léngkah tambahan dina prosés coding. Hatur nuhun kana éta, seueur kasalahan tiasa ditangkep ku usaha anu kirang - urang terang ieu tina pangalaman programer ti Amazon. Kalayan spésifikasi, kualitas program janten langkung luhur. Ku kituna naha, teras, urang jadi mindeng balik tanpa aranjeunna? Sabab nulis téh hésé. Jeung nulis téh hésé, sabab pikeun ieu anjeun kudu mikir, jeung mikir oge hésé. Éta salawasna gampang pura-pura naon anu anjeun pikirkeun. Di dieu anjeun tiasa ngagambar analogi sareng lumpat - langkung saeutik anjeun ngajalankeun, langkung laun anjeun ngajalankeun. Anjeun kedah ngalatih otot sareng latihan nyerat. Peryogi latihan.
spésifikasi bisa jadi salah. Anjeun tiasa ngalakukeun kasalahan dimana waé, atanapi syaratna parantos robih, atanapi perbaikan panginten kedah dilakukeun. Sakur kode anu dianggo ku saha waé kedah dirobih, janten engké atanapi engké spésifikasina moal cocog deui sareng program éta. Ideally, dina hal ieu, anjeun kudu nulis spésifikasi anyar jeung lengkep nulis balik kode. Urang terang pisan yén teu aya anu ngalakukeun éta. Dina prakték, urang patch kode jeung kamungkinan ngamutahirkeun spésifikasi. Upami ieu pasti kajantenan engké atanapi engké, naha nyerat spésifikasi pisan? Anu mimiti, pikeun jalma anu bakal ngédit kode anjeun, unggal kecap tambahan dina spésifikasina bakal beuratna emas, sareng jalma ieu tiasa janten anjeun nyalira. Kuring mindeng berate sorangan keur teu meunang spésifikasi cukup lamun Kuring ngédit kode abdi. Na kuring nulis leuwih spésifikasi ti kode. Ku alatan éta, nalika anjeun ngédit kode, spésifikasi salawasna perlu diropéa. Bréh, kalayan unggal révisi, kode janten parah, janten langkung sesah maca sareng ngajaga. Ieu paningkatan éntropi. Tapi upami anjeun henteu ngamimitian ku spésifikasi, maka unggal baris anu anjeun tulis bakal janten éditan, sareng kodeu bakal teu kuat sareng sesah dibaca ti mimiti.
Sakumaha ceuk , moal aya perang anu dimeunangkeun ku rencana, sareng moal aya perang anu dimeunangkeun tanpa rencana. Sarta anjeunna terang hiji atawa dua hal ngeunaan battles. Aya pamadegan yén spésifikasi nulis téh runtah waktu. Kadang-kadang ieu leres, sareng tugasna saderhana pisan yén teu aya anu dipikiran. Tapi anjeun kedah salawasna émut yén nalika anjeun nyarios henteu nyerat spésifikasi, anjeun nyarios henteu mikir. Jeung anjeun kudu mikir ngeunaan eta unggal waktu. Pamikiran ngaliwatan tugas teu ngajamin yén anjeun moal nyieun kasalahan. Sakumaha urang terang, teu aya anu nimukeun tongkat sihir, sareng program mangrupikeun tugas anu sesah. Tapi lamun anjeun teu mikir ngaliwatan masalah, anjeun dijamin nyieun kasalahan.
Anjeun tiasa maca langkung seueur ngeunaan TLA + sareng PlusCal dina halaman wéb khusus, anjeun tiasa angkat ka dinya ti halaman bumi kuring . Sakitu wae kanggo simkuring, hatur nuhun kana perhatosanana.
Punten dicatet yén ieu tarjamahan. Nalika anjeun nyerat koméntar, émut yén pangarang moal maca éta. Upami anjeun leres-leres hoyong ngobrol sareng panulis, maka anjeunna bakal aya dina konferensi Hydra 2019, anu bakal dilaksanakeun 11-12 Juli 2019 di St. Tiket bisa dibeuli .
sumber: www.habr.com