Atik sa a se yon tradiksyon . Men, anvan li yon ti entwodiksyon. Ki jan zonbi yo fòme? Tout moun te antre nan yon sitiyasyon kote yo vle rale yon zanmi oswa yon kòlèg jiska nivo yo, men li pa travay deyò. Epi li pa tèlman avèk ou menm jan avè l 'ke "li pa travay deyò": sou yon bò nan echèl la se yon salè nòmal, travay, ak sou sa, ak sou lòt la, bezwen an panse. Panse se dezagreyab ak douloure. Li byen vit abandone epi li kontinye ekri kòd san li pa vire sou sèvo li ditou. Ou imajine konbyen efò li pran pou simonte baryè enpuisans aprann, epi ou jis pa fè li. Sa a se ki jan zonbi yo fòme, ki, sanble, ka geri, men li sanble ke pèsonn pa pral fè li.
Lè mwen te wè sa (wi, menm kamarad ki soti nan liv yo) epi li pa fè yon rapò, men yon sesyon kesyon ak repons, mwen te yon ti kras mefyan. Jis nan ka, Leslie se yon syantis ki pi popilè nan lemonnantye, otè a nan travay fondamantal nan distribye informatique, epi ou ka konnen l 'yo ak lèt La nan mo LaTeX - "Lamport TeX". Dezyèm faktè alarmant la se egzijans li: tout moun ki vini yo dwe (absoliman gratis) koute yon koup nan rapò li yo davans, vini ak omwen yon kesyon sou yo, epi sèlman Lè sa a, vini. Mwen deside wè sa Lamport t ap difize la - e li bon! Se egzakteman bagay sa a, majik lyen-grenn pou geri zonbi. Mwen avèti ou: soti nan tèks la, rayisab metodoloji super-fleksib ak moun ki pa renmen teste sa ki ekri yo ka miyò boule.
Apre habrokat, an reyalite, tradiksyon seminè a kòmanse. Jwi lekti!
Kèlkeswa travay ou pran, ou toujou bezwen ale nan twa etap:
- deside ki objektif ou vle reyalize;
- deside ki jan ou pral reyalize objektif ou;
- vini nan objektif ou.
Sa a aplike tou pou pwogramasyon. Lè nou ekri kòd, nou bezwen:
- deside kisa pwogram nan ta dwe fè;
- detèmine kijan li ta dwe fè travay li;
- ekri kòd ki koresponn lan.
Dènye etap la, nan kou, trè enpòtan, men mwen pa pral pale sou li jodi a. Olye de sa, nou pral diskite sou de premye yo. Chak pwogramè fè yo anvan yo kòmanse travay. Ou pa chita pou w ekri sof si w ap deside si w ap ekri yon navigatè oswa yon baz done. Yon sèten lide sou objektif la dwe prezan. Epi ou definitivman panse sou ki sa egzakteman pwogram nan pral fè, epi yo pa ekri yon jan kanmenm nan espwa ke kòd la pral yon jan kanmenm vire nan yon navigatè.
Ki jan egzakteman kòd sa a pre-panse rive? Konbyen efò nou ta dwe mete nan sa a? Li tout depann sou ki jan konplèks pwoblèm nan nou ap rezoud. Sipoze nou vle ekri yon sistèm distribiye ki toleran fay. Nan ka sa a, nou ta dwe reflechi ak anpil atansyon anvan nou chita nan kòd. E si nou jis bezwen ogmante yon varyab nonb antye relatif pa 1? Nan premye gade, tout bagay se trivial isit la, epi pa gen okenn panse ki nesesè, men Lè sa a, nou sonje ke yon debòde ka rive. Se poutèt sa, menm yo nan lòd yo konprann si yon pwoblèm se senp oswa konplèks, ou bezwen premye reflechi.
Si ou panse sou solisyon posib pou pwoblèm nan davans, ou ka evite erè. Men, sa mande pou panse ou klè. Pou reyalize sa, ou bezwen ekri panse ou. Mwen vrèman renmen sitasyon Dick Guindon an: "Lè w ekri, lanati montre w jan panse w pa bon." Si ou pa ekri, ou sèlman panse ke ou ap panse. Epi ou bezwen ekri panse ou sou fòm espesifikasyon yo.
Espesifikasyon fè anpil fonksyon, espesyalman nan gwo pwojè. Men, mwen pral sèlman pale sou youn nan yo: yo ede nou panse aklè. Panse byen klè trè enpòtan ak byen difisil, kidonk isit la nou bezwen nenpòt èd. Nan ki lang nou ta dwe ekri spesifikasyon? An jeneral, sa a se toujou premye kesyon pou pwogramè yo: nan ki lang nou pral ekri. Pa gen yon repons ki kòrèk pou li: pwoblèm nou ap rezoud yo twò divès. Pou kèk moun, TLA+ se yon lang spesifikasyon ke mwen devlope. Pou lòt moun, li pi bon pou itilize Chinwa. Tout depann sou sitiyasyon an.
Pi enpòtan se yon lòt kesyon: ki jan yo reyalize panse pi klè? Repons: Nou dwe panse tankou syantifik. Sa a se yon fason pou panse ki te pwouve tèt li sou 500 ane ki sot pase yo. Nan syans, nou bati modèl matematik reyalite. Astwonomi te petèt premye syans nan sans strik mo a. Nan modèl matematik yo itilize nan astwonomi, kò selès yo parèt kòm pwen ki gen mas, pozisyon ak momantòm, byenke an reyalite yo se objè trè konplèks ak mòn ak oseyan, mare ak mare. Modèl sa a, tankou nenpòt lòt, te kreye pou rezoud pwoblèm sèten. Li bon pou detèmine kote yo montre teleskòp la si ou bezwen jwenn yon planèt. Men, si ou vle predi move tan an sou planèt sa a, modèl sa a pa pral travay.
Matematik pèmèt nou detèmine pwopriyete modèl la. Ak syans montre kouman pwopriyete sa yo gen rapò ak reyalite. Ann pale de syans nou an, enfòmatik. Reyalite nou travay ak sistèm enfòmatik divès kalite: processeur, konsole jwèt, òdinatè, pwogram egzekite, elatriye. Mwen pral pale sou kouri yon pwogram sou yon òdinatè, men an jeneral, tout konklizyon sa yo aplike nan nenpòt sistèm informatique. Nan syans nou an, nou itilize anpil modèl diferan: machin Turing, seri evènman ki pasyèlman òdone, ak anpil lòt.
Ki sa ki se yon pwogram? Sa a se nenpòt kòd ki ka konsidere poukont li. Sipoze nou bezwen ekri yon navigatè. Nou fè twa travay: nou konsepsyon opinyon itilizatè a nan pwogram nan, Lè sa a, nou ekri dyagram nan wo nivo nan pwogram nan, epi finalman nou ekri kòd la. Pandan n ap ekri kòd la, nou reyalize ke nou bezwen ekri yon fòmatè tèks. Isit la nou ankò bezwen rezoud twa pwoblèm: detèmine ki tèks zouti sa a pral retounen; chwazi yon algorithm pou fòma; ekri kòd. Travay sa a gen pwòp travay li: kòrèkteman mete yon tire nan mo yo. Nou menm tou nou rezoud travay sa a nan twa etap - jan ou ka wè, yo repete nan plizyè nivo.
Ann konsidere an plis detay premye etap la: ki pwoblèm pwogram nan rezoud. Isit la, nou pi souvan modèl yon pwogram kòm yon fonksyon ki pran kèk opinyon ak pwodui kèk pwodiksyon. Nan matematik, yon fonksyon anjeneral dekri kòm yon seri òdone pè. Pa egzanp, fonksyon kare pou nonm natirèl yo dekri kòm seri {<0,0>, <1,1>, <2,4>, <3,9>, …}. Domèn yon fonksyon konsa se ansanm premye eleman chak pè, sa vle di nimewo natirèl yo. Pou defini yon fonksyon, nou bezwen presize dimansyon li ak fòmil.
Men, fonksyon nan matematik yo pa menm jan ak fonksyon nan langaj pwogramasyon. Matematik la pi fasil. Depi mwen pa gen tan pou egzanp konplèks, ann konsidere yon senp: yon fonksyon nan C oswa yon metòd estatik nan Java ki retounen pi gwo divizè komen nan de nonm antye. Nan spesifikasyon metòd sa a, nou pral ekri: kalkile GCD(M,N) pou diskisyon M и Nkote GCD(M,N) - yon fonksyon ki gen domèn se seri pè nonm antye, ak valè retounen se pi gwo nonb antye ki divizib pa M и N. Ki jan modèl sa a gen rapò ak reyalite? Modèl la opere sou nonm antye, pandan y ap nan C oswa Java nou gen yon 32-bit int. Modèl sa a pèmèt nou deside si algorithm la kòrèk GCD, men li pa pral anpeche erè debòde. Sa a ta mande pou yon modèl pi konplèks, pou ki pa gen tan.
Ann pale sou limit yo nan yon fonksyon kòm yon modèl. Gen kèk pwogram (tankou sistèm opere) pa jis retounen yon sèten valè pou sèten agiman, yo ka kouri kontinyèlman. Anplis de sa, fonksyon an kòm yon modèl pa byen adapte pou dezyèm etap la: planifye ki jan yo rezoud pwoblèm nan. Triye rapid ak sòt jarèt kalkile menm fonksyon an, men yo se algoritm konplètman diferan. Se poutèt sa, pou dekri kijan objektif pwogram nan reyalize, mwen sèvi ak yon modèl diferan, ann rele li modèl konpòtman estanda. Pwogram nan li reprezante kòm yon seri tout konpòtman akseptab, chak nan yo ki, nan vire, se yon sekans nan eta, ak eta a se plasman nan valè nan varyab.
Ann wè ki jan dezyèm etap la pou algorithm Euclid la ta sanble. Nou bezwen kalkile GCD(M, N). Nou inisyalize M kòm xAk N kòm y, Lè sa a, repete soustraksyon ki pi piti a nan varyab sa yo soti nan pi gwo a jiskaske yo egal. Pou egzanp, si M = 12Ak N = 18, nou ka dekri konpòtman sa a:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
Men, si M = 0 и N = 0? Zewo divizib pa tout nimewo, kidonk pa gen pi gwo divizè nan ka sa a. Nan sitiyasyon sa a, nou bezwen tounen nan premye etap la epi mande: èske nou reyèlman bezwen kalkile GCD pou nimewo ki pa pozitif? Si sa a pa nesesè, Lè sa a, ou jis bezwen chanje spesifikasyon la.
Isit la nou ta dwe fè yon ti digression sou pwodiktivite. Li souvan mezire nan kantite liy kòd ekri chak jou. Men, travay ou a pi itil si ou debarase m de yon sèten kantite liy, paske ou gen mwens plas pou pinèz. Ak fason ki pi fasil yo debarase m de kòd la se nan premye etap la. Li posib ke ou jis pa bezwen tout klòch ak sifle w ap eseye aplike. Fason ki pi rapid pou senplifye yon pwogram epi ekonomize tan se pa fè bagay ki pa ta dwe fèt. Dezyèm etap la se dezyèm potansyèl ki pi ekonomize tan. Si ou mezire pwodiktivite an tèm de liy ekri, Lè sa a, panse sou fason pou akonpli yon travay ap fè ou mwens pwodiktif, paske ou ka rezoud pwoblèm nan menm ak mwens kòd. Mwen pa ka bay estatistik egzak isit la, paske mwen pa gen okenn fason yo konte kantite liy ke mwen pa t 'ekri akòz lefèt ke mwen te pase tan sou spesifikasyon la, se sa ki nan premye ak dezyèm etap yo. Ak eksperyans la pa ka mete kanpe isit la tou, paske nan eksperyans la nou pa gen dwa ranpli premye etap la, travay la se Predetermined.
Li fasil pou neglije anpil difikilte nan espesifikasyon enfòmèl. Pa gen anyen difisil nan ekri espesifikasyon strik pou fonksyon, mwen pa pral diskite sou sa a. Olye de sa, nou pral pale sou ekri espesifikasyon fò pou konpòtman estanda. Gen yon teyorèm ki di ke nenpòt seri konpòtman ka dekri lè l sèvi avèk pwopriyete sekirite a (sekirite) ak pwopriyete sivivabilite (vivans). Sekirite vle di ke pa gen anyen move ki pral rive, pwogram nan pa pral bay yon repons kòrèk. Sivivabilite vle di ke pi bonè oswa pita yon bagay bon pral rive, sa vle di pwogram nan pral bay repons ki kòrèk la pi bonè oswa pita. Kòm yon règ, sekirite se yon endikatè ki pi enpòtan, erè pi souvan rive isit la. Se poutèt sa, pou konsève pou tan, mwen pa pral pale sou sivivabilite, byenke li se, nan kou, tou enpòtan.
Nou reyalize sekirite lè nou preskri, premye, seri inisyal eta posib yo. Epi dezyèmman, relasyon ak tout pwochen eta posib pou chak eta. Ann aji tankou syantis epi defini eta matematikman. Se yon fòmil ki dekri seri eta inisyal la, pou egzanp, nan ka algorithm Euclid la: (x = M) ∧ (y = N). Pou sèten valè M и N gen yon sèl eta inisyal. Relasyon ak pwochen eta a dekri pa yon fòmil kote varyab eta pwochen yo ekri ak yon prim, epi varyab eta aktyèl la ekri san premye. Nan ka algorithm Euclid la, nou pral fè fas ak disjonksyon de fòmil, nan youn nan yo. x se pi gwo valè a, ak nan dezyèm lan - y:
Nan premye ka a, nouvo valè y egal a valè y anvan an, epi nou jwenn nouvo valè x lè w retire pi piti varyab la nan pi gwo a. Nan dezyèm ka a, nou fè opoze a.
Ann tounen nan algorithm Euclid la. Ann sipoze ankò sa M = 12, N = 18. Sa a defini yon sèl eta inisyal, (x = 12) ∧ (y = 18). Lè sa a, nou ploge valè sa yo nan fòmil ki anwo a epi jwenn:
Men sèl solisyon posib: x' = 18 - 12 ∧ y' = 12epi nou jwenn konpòtman an: [x = 12, y = 18]. Menm jan an tou, nou ka dekri tout eta yo nan konpòtman nou an: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
Nan dènye eta [x = 6, y = 6] tou de pati nan ekspresyon an pral fo, kidonk li pa gen okenn eta pwochen. Se konsa, nou gen yon spesifikasyon konplè sou dezyèm etap la - jan ou ka wè, sa a se byen òdinè matematik, tankou nan enjenyè ak syantis, epi yo pa etranj, tankou nan syans òdinatè.
De fòmil sa yo ka konbine nan yon fòmil lojik tanporèl. Li se elegant ak fasil yo eksplike, men pa gen tan pou li kounye a. Nou ka bezwen lojik tanporèl sèlman pou pwopriyete vivan, pou sekirite li pa nesesè. Mwen pa renmen lojik tanporèl kòm sa, se pa matematik byen òdinè, men nan ka vivan li se yon mal nesesè.
Nan algorithm Euclid a, pou chak valè x и y gen valè inik x' и y', ki fè relasyon ak pwochen eta a vre. Nan lòt mo, algorithm Euclid a se detèminist. Pou modèl yon algorithm ki pa detèminist, eta aktyèl la bezwen gen plizyè eta posib nan lavni, e ke chak valè varyab san premye gen plizyè valè varyab primè konsa ke relasyon an ak pwochen eta a se vre. Sa a se fasil fè, men mwen pa pral bay egzanp kounye a.
Pou fè yon zouti k ap travay, ou bezwen matematik fòmèl. Ki jan yo fè spesifikasyon an fòmèl? Pou fè sa, nou bezwen yon langaj fòmèl, pa egzanp, . Spesifikasyon algorithm Euclid la ta sanble sa a nan lang sa a:
Yon senbòl siy egal ak yon triyang vle di ke valè ki sou bò gòch siy la defini pou egal a valè ki sou bò dwat siy la. Nan sans, spesifikasyon la se yon definisyon, nan ka nou an de definisyon. Nan spesifikasyon nan TLA +, ou bezwen ajoute deklarasyon ak kèk sentaks, tankou nan glise ki anwo a. Nan ASCII li ta sanble sa a:
Kòm ou ka wè, pa gen anyen konplike. Espesifikasyon pou TLA + ka teste, sa vle di kontoune tout konpòtman posib nan yon ti modèl. Nan ka nou an, modèl sa a pral sèten valè M и N. Sa a se yon metòd verifikasyon trè efikas ak senp ki konplètman otomatik. Li posib tou pou ekri prèv laverite fòmèl epi tcheke yo mekanikman, men sa pran anpil tan, kidonk prèske pa gen moun ki fè sa.
Dezavantaj prensipal la nan TLA + se ke li se matematik, ak pwogramasyon ak syantis òdinatè yo pè nan matematik. Nan premye gade, sa a son tankou yon blag, men, malerezman, mwen vle di li nan tout gravite. Kolèg mwen an te jis di m 'ki jan li te eseye eksplike TLA+ bay plizyè devlopè. Le pli vit ke fòmil yo parèt sou ekran an, yo imedyatman te vin je vit. Se konsa, si TLA+ fè ou pè, ou ka itilize , se yon kalite langaj pwogramasyon jwèt. Yon ekspresyon nan PlusCal kapab nenpòt ekspresyon TLA+, sa vle di, an jeneral, nenpòt ekspresyon matematik. Anplis de sa, PlusCal gen yon sentaks pou algoritm ki pa detèminist. Paske PlusCal ka ekri nenpòt ekspresyon TLA+, PlusCal pi ekspresif pase nenpòt langaj pwogramasyon reyèl. Apre sa, PlusCal konpile nan yon spesifikasyon TLA + fasil lizib. Sa a pa vle di, nan kou, spesifikasyon konplèks PlusCal la pral tounen yon senp sou TLA + - jis korespondans ki genyen ant yo se evidan, pa pral gen okenn konpleksite adisyonèl. Finalman, spesifikasyon sa a ka verifye pa zouti TLA +. An jeneral, PlusCal ka ede simonte fobi matematik epi li fasil pou konprann menm pou pwogramasyon ak syantis enfòmatik yo. Nan tan lontan, mwen pibliye algoritm sou li pou kèk tan (apeprè 10 ane).
Petèt yon moun pral objeksyon ke TLA + ak PlusCal se matematik, e matematik sèlman travay sou egzanp envante. Nan pratik, ou bezwen yon lang reyèl ak kalite, pwosedi, objè, ak sou sa. Sa a se mal. Men sa Chris Newcomb, ki te travay nan Amazon, ekri: “Nou te itilize TLA+ nan dis gwo pwojè, epi nan chak ka, lè l sèvi avèk li te fè yon diferans enpòtan nan devlopman paske nou te kapab trape pinèz danjere anvan nou frape pwodiksyon, epi paske li te ban nou insight ak konfyans nou te bezwen pou fè optimize pèfòmans agresif san yo pa afekte verite pwogram nan". Ou ka tande souvan ke lè w ap itilize metòd fòmèl, nou jwenn ensifizan kòd - nan pratik, tout bagay se egzakteman opoze a. Anplis de sa, gen yon opinyon ke manadjè yo pa ka konvenki nan bezwen an pou metòd fòmèl, menm si pwogramasyon yo konvenki nan itilite yo. Epi Newcomb ekri: "Manadjè yo kounye a ap pouse di yo ekri espesifikasyon pou TLA +, epi espesyalman asiyen tan pou sa a". Se konsa, lè manadjè yo wè ke TLA+ ap travay, yo kontan aksepte li. Chris Newcomb te ekri sa a sou sis mwa de sa (Oktòb 2014), men kounye a, jan mwen konnen, TLA + yo itilize nan 14 pwojè, pa 10. Yon lòt egzanp se nan konsepsyon XBox 360 la. Yon estajyè te vin jwenn Charles Thacker ak te ekri spesifikasyon pou sistèm memwa a. Mèsi a spesifikasyon sa a, yo te jwenn yon ensèk ki ta ka pase inapèsi, e poutèt sa chak XBox 360 ta aksidan apre kat èdtan nan itilize. Enjenyè IBM konfime ke tès yo pa ta jwenn ensèk sa a.
Ou ka li plis sou TLA + sou entènèt la, men kounye a ann pale sou espesifikasyon enfòmèl. Nou raman oblije ekri pwogram ki kalkile pi piti divizè komen ak tankou. Anpil pi souvan nou ekri pwogram tankou zouti bèl-enprimant mwen te ekri pou TLA+. Apre pwosesis ki pi senp la, kòd TLA + ta sanble sa a:
Men, nan egzanp ki anwo a, itilizatè a gen plis chans te vle konjonksyon an ak siy egal yo dwe aliyen. Se konsa, fòma kòrèk la ta sanble plis tankou sa a:
Konsidere yon lòt egzanp:
Isit la, okontrè, aliyman egal, adisyon, ak siy miltiplikasyon nan sous la te o aza, kidonk pwosesis ki pi senp la ase. An jeneral, pa gen okenn definisyon matematik egzak nan fòma kòrèk, paske "kòrèk" nan ka sa a vle di "sa itilizatè a vle", epi sa a pa ka detèmine matematikman.
Li ta sanble ke si nou pa gen yon definisyon nan verite, Lè sa a, spesifikasyon la se initil. Men, se pa sa. Jis paske nou pa konnen ki sa yon pwogram sipoze fè pa vle di nou pa bezwen reflechi sou ki jan li fonksyone - okontrè, nou dwe mete plis efò toujou nan li. Spesifikasyon la espesyalman enpòtan isit la. Li enposib detèmine pwogram nan pi bon pou enprime estriktire, men sa pa vle di ke nou pa ta dwe pran li nan tout, ak ekri kòd kòm yon kouran konsyans se pa yon bon bagay. Nan fen a, mwen te ekri yon spesifikasyon nan sis règ ak definisyon nan fòm kòmantè nan yon fichye java. Men yon egzanp sou youn nan règ yo: a left-comment token is LeftComment aligned with its covering token. Règ sa a ekri nan lang angle matematik, pou nou di: LeftComment aligned, left-comment и covering token - tèm ak definisyon. Men ki jan matematisyen yo dekri matematik: yo ekri definisyon tèm epi, ki baze sou yo, règ. Benefis yon spesifikasyon konsa se ke sis règ yo pi fasil pou konprann ak debogaj pase 850 liy kòd. Mwen dwe di ke ekri règ sa yo pa t fasil, li te pran anpil tan pou debogaj yo. Espesyalman pou objektif sa a, mwen te ekri yon kòd ki te rapòte ki règ yo te itilize. Mèsi a lefèt ke mwen teste sis règ sa yo sou plizyè egzanp, mwen pa t 'gen debogaj liy 850 nan kòd, ak pinèz yo te tounen byen fasil jwenn. Java gen gwo zouti pou sa. Si mwen te jis ekri kòd la, li ta pran m 'pi lontan ankò, epi fòma a ta gen pi bon kalite.
Poukisa pa t 'kapab yon spesifikasyon fòmèl dwe itilize? Sou yon bò, ekzekisyon kòrèk la pa twò enpòtan isit la. Enpresyon estriktirèl yo oblije pa fè pèsonn plezi, kidonk mwen pa t 'gen jwenn li nan travay dwat nan tout sitiyasyon yo enpè. Menm pi enpòtan se lefèt ke mwen pa t 'gen zouti adekwa. TLA + modèl chèk la pa itil isit la, kidonk mwen ta oblije ekri egzanp yo manyèlman.
Spesifikasyon ki anwo a gen karakteristik komen nan tout espesifikasyon. Li se pi wo nivo pase kòd la. Li kapab aplike nan nenpòt lang. Nenpòt zouti oswa metòd pa itil pou ekri li. Pa gen kou pwogramasyon ki pral ede w ekri spesifikasyon sa a. Epi pa gen okenn zouti ki ka fè spesifikasyon sa a pa nesesè, sof si, nan kou, w ap ekri yon lang espesyalman pou ekri pwogram enprime estriktire nan TLA+. Finalman, spesifikasyon sa a pa di anyen sou egzakteman ki jan nou pral ekri kòd la, li sèlman deklare ki sa kòd sa a fè. Nou ekri spesifikasyon an pou ede nou reflechi sou pwoblèm nan anvan nou kòmanse reflechi sou kòd la.
Men, spesifikasyon sa a tou gen karakteristik ki fè distenksyon ant li ak lòt espesifikasyon. 95% nan lòt karakteristik yo siyifikativman pi kout ak pi senp:
Anplis de sa, spesifikasyon sa a se yon seri règ. Kòm yon règ, sa a se yon siy spesifikasyon pòv. Konprann konsekans yon seri règ se byen difisil, se poutèt sa mwen te oblije pase anpil tan debogaj yo. Sepandan, nan ka sa a, mwen pa t 'kapab jwenn yon pi bon fason.
Li vo di kèk mo sou pwogram ki kouri kontinyèlman. Kòm yon règ, yo travay nan paralèl, pou egzanp, sistèm opere oswa sistèm distribiye. Trè kèk moun ka konprann yo mantalman oswa sou papye, epi mwen pa youn nan yo, byenke yon fwa mwen te kapab fè li. Se poutèt sa, nou bezwen zouti ki pral tcheke travay nou an - pou egzanp, TLA + oswa PlusCal.
Poukisa li te nesesè yo ekri yon spesifikasyon si mwen te deja konnen ki sa egzakteman kòd la ta dwe fè? An reyalite, mwen jis te panse mwen te konnen li. Anplis de sa, ak yon spesifikasyon, yon etranje pa bezwen antre nan kòd la pou konprann ki sa egzakteman li fè. Mwen gen yon règ: pa ta dwe gen okenn règ jeneral. Gen yon eksepsyon nan règ sa a, nan kou, se sèl règ jeneral mwen swiv: spesifikasyon nan sa ki kòd la fè ta dwe di moun tout sa yo bezwen konnen lè w ap itilize kòd la.
Se konsa, ki sa egzakteman pwogramasyon yo bezwen konnen sou panse? Pou kòmanse, menm jan ak tout lòt moun: si ou pa ekri, Lè sa a, li sèlman sanble ou ke ou ap panse. Epitou, ou bezwen panse anvan ou kòd, ki vle di ou bezwen ekri anvan ou kòd. Spesifikasyon an se sa nou ekri anvan nou kòmanse kodaj. Yon spesifikasyon nesesè pou nenpòt kòd ki ka itilize oswa modifye pa nenpòt moun. Ak "yon moun" sa a ka otè a nan kòd la tèt li yon mwa apre li te ekri. Yon spesifikasyon nesesè pou gwo pwogram ak sistèm, pou klas, pou metòd, epi pafwa menm pou seksyon konplèks nan yon sèl metòd. Ki sa egzakteman yo ta dwe ekri sou kòd la? Ou bezwen dekri kisa li fè, se sa ki ka itil nenpòt moun ki sèvi ak kòd sa a. Pafwa li ka nesesè tou pou presize kijan kòd la akonpli objektif li. Si nou te ale nan metòd sa a nan kou a nan algoritm, Lè sa a, nou rele li yon algorithm. Si li se yon bagay ki pi espesyal ak nouvo, Lè sa a, nou rele li konsepsyon wo nivo. Pa gen okenn diferans fòmèl isit la: tou de se yon modèl abstrè nan yon pwogram.
Ki jan egzakteman ou ta dwe ekri yon spesifikasyon kòd? Bagay pwensipal lan: li ta dwe yon nivo pi wo pase kòd la tèt li. Li ta dwe dekri eta ak konpòtman. Li ta dwe osi strik ke travay la mande. Si w ap ekri yon spesifikasyon pou kijan yon travay dwe aplike, ou ka ekri li nan pseudocode oswa ak PlusCal. Ou bezwen aprann kijan pou ekri spécifications sou spécifications fòmèl. Sa a pral ba ou ladrès ki nesesè yo ki pral ede w ak enfòmèl yo tou. Ki jan ou aprann ekri spesifikasyon fòmèl? Lè nou te aprann pwograme, nou te ekri pwogram epi debogaj yo. Se menm bagay la tou isit la: ekri spesifikasyon an, tcheke li ak chèk modèl la, epi ranje pinèz yo. TLA+ ka pa pi bon lang pou yon spesifikasyon fòmèl, epi gen yon lòt lang ki pi bon pou bezwen espesifik ou yo. Avantaj TLA+ se ke li anseye panse matematik trè byen.
Ki jan yo konekte spesifikasyon ak kòd? Avèk èd nan kòmantè ki konekte konsèp matematik ak aplikasyon yo. Si w ap travay ak graf, Lè sa a, nan nivo pwogram nan w ap gen etalaj de nœuds ak etalaj de lyen. Se poutèt sa, ou bezwen ekri egzakteman ki jan graf la aplike pa estrikti pwogram sa yo.
Li ta dwe remake ke okenn nan pi wo a pa aplike nan pwosesis aktyèl la nan ekri kòd. Lè ou ekri kòd la, se sa ki, ou fè twazyèm etap la, ou bezwen tou panse ak panse nan pwogram nan. Si yon sous-tâche vin konplèks oswa ki pa evidan, ou bezwen ekri yon spesifikasyon pou li. Men, mwen pa pale sou kòd nan tèt li isit la. Ou ka sèvi ak nenpòt langaj pwogramasyon, nenpòt metodoloji, li pa sou yo. Epitou, pa youn nan pi wo a elimine nesesite pou teste ak debug kòd. Menm si modèl abstrè a ekri kòrèkteman, ka gen pinèz nan aplikasyon li.
Ekri espesifikasyon se yon etap adisyonèl nan pwosesis kodaj la. Mèsi a li, anpil erè ka kenbe ak mwens efò - nou konnen sa a nan eksperyans nan pwogramasyon ki soti nan Amazon. Avèk espesifikasyon, bon jan kalite a nan pwogram yo vin pi wo. Kidonk, poukisa nou souvan ale san yo? Paske ekri se difisil. Ak ekri se difisil, paske pou sa a ou bezwen panse, ak panse tou se difisil. Li toujou pi fasil pou w pretann sa w panse. Isit la ou ka trase yon analoji ak kouri - mwens ou kouri, pi dousman ou kouri. Ou bezwen antrene misk ou ak pratike ekri. Bezwen pratik.
Spesifikasyon an ka pa kòrèk. Ou ta ka fè yon erè yon kote, oswa kondisyon yo ta ka chanje, oswa yon amelyorasyon ta ka bezwen fè. Nenpòt kòd ke nenpòt moun itilize dwe chanje, kidonk pi bonè oswa pita spesifikasyon an pa pral matche ak pwogram nan. Idealman, nan ka sa a, ou bezwen ekri yon nouvo spesifikasyon ak konplètman reekri kòd la. Nou konnen byen ke pèsonn pa fè sa. Nan pratik, nou patch kòd la epi pètèt mete ajou spesifikasyon la. Si sa a oblije rive pi bonè oswa pita, Lè sa a, poukisa ekri espesifikasyon nan tout? Premyèman, pou moun ki pral modifye kòd ou a, chak mo siplemantè nan spesifikasyon la pral vo pwa li an lò, epi moun sa a ka byen ou menm. Mwen souvan reprimande tèt mwen paske mwen pa jwenn ase spesifikasyon lè m ap modifye kòd mwen an. Apre sa, mwen ekri plis espesifikasyon pase kòd. Se poutèt sa, lè ou modifye kòd la, spesifikasyon la toujou bezwen mete ajou. Dezyèmman, ak chak revizyon, kòd la vin pi mal, li vin pi plis ak pi difisil pou li epi kenbe. Sa a se yon ogmantasyon nan entropi. Men, si ou pa kòmanse ak yon espèk, Lè sa a, chak liy ou ekri yo pral yon modifye, epi kòd la pral difisil ak difisil pou li depi nan kòmansman an.
Kòm te di , pa gen okenn batay te genyen pa plan, e pa gen okenn batay te genyen san yon plan. Epi li te konnen yon bagay oswa de sou batay. Gen yon opinyon ke ekri spesifikasyon se yon fatra nan tan. Pafwa sa a se vre, ak travay la se tèlman senp ke pa gen anyen yo panse nan li. Men, ou ta dwe toujou sonje ke lè yo di ou pa ekri espesifikasyon, yo di ou pa panse. Epi ou ta dwe reflechi sou li chak fwa. Panse nan travay la pa garanti ke ou pa pral fè erè. Kòm nou konnen, pèsonn pa envante ralonj majik la, ak pwogramasyon se yon travay difisil. Men, si ou pa panse nan pwoblèm nan, ou gen garanti ou fè erè.
Ou ka li plis enfòmasyon sou TLA + ak PlusCal sou yon sit entènèt espesyal, ou ka ale la nan paj lakay mwen . Se tout pou mwen, mèsi pou atansyon ou.
Tanpri sonje ke sa a se yon tradiksyon. Lè ou ekri kòmantè, sonje ke otè a pa pral li yo. Si ou reyèlman vle chat ak otè a, Lè sa a, li pral nan Hydra 2019 konferans lan, ki pral fèt Jiyè 11-12, 2019 nan Saint Petersburg. Tikè yo ka achte .
Sous: www.habr.com