2.21 Mifumo ya aina na uchambuzi tuli

Muhtasari na msukumo

Kasoro nyingi hunaswa kuchelewa, wakati wa kuendesha, na jaribio au mtumiaji au tukio. Darasa zima lao halihitaji kufika huko kamwe. Mfumo wa aina na zana nzuri ya uchambuzi tuli wa programu husoma msimbo wako kabla haujaendeshwa na kuthibitisha kwamba makosa fulani hayawezi kutokea: mfuatano unaotumika mahali pa namba inayohitajika, null iliyofuatwa, kigeu kinachosomwa kabla ya kuandikwa, kesi iliyoachwa bila kushughulikiwa. Sura hii inahusu kusukuma usahihi kushoto, karibu zaidi na wakati unaoandika mstari, ambapo marekebisho yanagharimu sekunde badala ya ukurasa katika mapitio ya tukio.

Uchambuzi tuli ni mbinu yoyote inayochunguza chanzo au msimbo uliokusanywa bila kuutekeleza. Ukaguzi wa aina ndio umbo lililoenea zaidi, lakini familia hiyo pia inajumuisha linters (zana zinazoweka alama kwenye mifumo ya mtindo na usahihi), wachambuzi wa mtiririko wa data, na, mwisho kabisa, uthibitisho rasmi. Ahadi ya pamoja ni darasa la hakikisho unalolipata bure kwa kila ujenzi, milele, bila jaribio la kuandika na bila mpitiaji wa kukumbuka. Ahadi hiyo ndiyo sababu nidhamu hii inakaa kando ya viwango vya uandishi wa msimbo (sura ya 2.1), kanuni za usanifu wa programu (sura ya 2.2), na mkakati wa majaribio (sura ya 2.4): ni njia moja zaidi ya kiotomatiki ya kufanya msimbo mkubwa uwe salama kubadilisha.

Kwa timu kubwa, thamani hujumlika. Mamia ya wahandisi wanapogusa mfumo wa pamoja, saini ya aina ni mkataba ambao mkusanyaji huutekeleza kwa kila mmoja wao, na kikaguzi kwenye bomba ni mpitiaji asiyechoka na asiyependelea mtu. Katika mazingira ya mashirika makubwa hili hupunguza gharama ya utambulisho na uunganishaji, kwa sababu aina huandika nia na wachambuzi hunasa makosa ambayo wageni hufanya. Katika serikali na mifumo mingine yenye dau kubwa, ambapo jibu lisilo sahihi linaweza kumnyima mtu manufaa au kufichua data, hakikisho zinazokaguliwa na mashine ni ushahidi: zinaonyesha kwa mkaguzi kwamba kategoria nzima za kasoro haziwezekani kwa muundo, si kwamba hazijajaribiwa tu. Hili linaunganishwa moja kwa moja na ubora wa programu (sura ya 2.11) na usalama wa programu (sura ya 4.2).

Kanuni kuu

Sukuma usahihi kushoto: nasa kasoro wakati wa kuandika, si kwenye uzalishaji.
Pendelea hakikisho ambazo mashine inazikagua kuliko kanuni ambazo binadamu lazima wazikumbuke.
Weka nia ndani ya aina ili hali zisizo halali zisiweze kuwakilishwa kabisa.
Pokea aina hatua kwa hatua katika msimbo wa kidinamiki; huhitaji yote au hakuna.
Chukulia maonyo kama makosa, na uongeze kipimo cha msingi kwa kishindo ili kiboreshe tu.
Endesha wachambuzi walewale kwenye kihariri na kwenye bomba, kwa kanuni zilezile.
Simamia matokeo ya uongo chanya kwa ukandamizaji wenye nidhamu, wenye sababu, unaoweza kupitiwa.

Mapendekezo

Chagua uaji wa aina tuli au wa kidinamiki ukiwa na macho wazi

Katika lugha yenye aina tuli, aina hukaguliwa kabla programu haijaendeshwa; katika yenye aina za kidinamiki, hukaguliwa inapoendesha, kama kabisa. Hakuna iliyo sahihi kwa ulimwengu mzima, na uundaji wa uaminifu ni biashara ya hakikisho kwa unyumbufu. Aina tuli hukununulia mikataba iliyokaguliwa na mashine, urekebishaji wa muundo unaoweza kuuamini, na zana (ukamilishaji otomatiki, kubadilisha jina kwa usalama, kuruka hadi ufafanuzi) zinazojua vitu ni nini. Aina za kidinamiki hukununulia uundaji wa mifano ya haraka, msimbo mfupi, na taratibu chache zinazofaa hati na kazi ya uchunguzi. Kadiri mfumo ulivyo mkubwa, wa muda mrefu, na wenye dau kubwa, ndivyo upande tuli unavyolipa zaidi, kwa sababu gharama ya urekebishaji wa muundo wa msimbo mzima na gharama ya kosa la aina la wakati wa kuendesha zote hukua kwa ukubwa.

Kuwa sahihi kuhusu mhimili wa pili, tofauti: aina imara dhidi ya dhaifu. Lugha yenye aina imara hukataa kubadilisha kimyakimya aina zisizooana (kuongeza namba kwenye mfuatano huleta kosa); yenye dhaifu hubadilisha kimyakimya, ikizalisha mshangao kama "3" + 4 kutoa kitu ambacho hukukusudia. Unaweza kuwa na tuli na dhaifu, au kidinamiki na imara. Unapotathmini lugha, uliza maswali yote mawili tofauti, kwa sababu “imara” mara nyingi ndicho watu wanachotaka kweli wanaposema “yenye aina.”

Tegemea uchukuzi wa aina kuweka aina kuwa nafuu

Pingamizi la kawaida kwa aina tuli ni kelele ya kuandika aina kwenye kila mstari. Uchukuzi wa aina huondoa sehemu kubwa ya gharama hiyo: mkusanyaji hudhania aina kutoka muktadha, kwa hiyo unaandika aina kwenye mipaka (saini za kazi, violesura vya umma) na kuacha ndani ichukuliwe. Lugha za kisasa hudhania kwa ukali, zikikupa usalama wa ukaguzi tuli na sehemu kubwa ya ufupi wa msimbo wa kidinamiki. Pokea kanuni ya nyumba inayoandika aina kwenye sehemu ambazo msomaji anazitegemea kama mkataba, kazi zinazosafirishwa nje na aina za umma, na kuacha vigeu vya ndani vidhaniwe. Hii huweka saini za uaminifu na zinazojieleza huku ikiokoa ndani kutokana na msongamano, na inarejea kwenye malengo ya usomekaji ya sura ya 2.1.

Fanya hali zisizo halali zisiwezekane kuwakilishwa

Wazo lenye nguvu zaidi katika usanifu wa aina wa kiutendaji ni kuumba aina zako ili hali isiyo sahihi isiweze kuandikwa. Agizo likiwa ama “rasimu” bila malipo au “limewekwa” na malipo, usiliumbe kama muundo mmoja wenye nyanja zinazoweza kuwa null ambapo rasimu inaweza kubeba malipo kwa bahati mbaya na agizo lililowekwa likabeba hakuna. Liumbe kama aina ya jumla (pia huitwa muungano wenye lebo, muungano unaobagua, au tofauti): thamani ambayo ni hasa moja ya seti ya maumbo yaliyowekwa, kila moja likibeba data yake. Sasa mchanganyiko usio halali haupo, na msimbo unaoshughulikia thamani lazima uzingatie kila kesi au mkusanyaji analalamika. Hii hugeuza “haipaswi kutokea kamwe” ya wakati wa kuendesha kuwa “haiwezi kutokea” ya wakati wa kukusanya, ambayo ndiyo hoja nzima.

Silika ileile huendesha zana kadhaa za kila siku. Tumia aina iliyoorodheshwa badala ya mfuatano wa kichawi kwa seti thabiti ya hali. Funga thamani iliyothibitishwa katika aina tofauti (EmailAddress badala ya mfuatano mtupu) ili “ingizo lisilothibitishwa” na “barua pepe iliyothibitishwa” ziwe aina tofauti ambazo mkusanyaji huzitenganisha. Hii ni usemi wa mfumo wa aina wa nidhamu ya uthibitisho wa mpaka kutoka ushughulikiaji wa makosa (sura ya 2.20): thibitisha mara moja kwenye ukingo, geuza kuwa aina inayoweka hakikisho, na uache msimbo wa ndani uiamini.

Chukulia uwezekano wa null na jenerikis kwa uzito

Kiashiria cha null, ambacho mvumbuzi wake aliita “kosa lake la dola bilioni,” ndiyo njia ya kawaida zaidi ambayo mfumo wa aina tuli ulikuwa ukisema uongo: thamani iliyoandikwa kama mfuatano inaweza kuwa null kwa siri, na ulijua kwa kuanguka. Mifumo ya kisasa ya aina hurekebisha hili kwa kufanya uwezekano wa null kuwa wazi. Thamani ni ama String ambayo si null kamwe au aina ya Option/Maybe/inayoweza null unayopaswa kuifungua kabla ya matumizi, na mkusanyaji anakulazimisha kushughulikia kesi tupu. Ikiwa lugha yako inatoa aina zisizo null au aina ya hiari, zitumie kila mahali na uchukulie aina mtupu inayoweza null kama harufu. Hii huondoa jenasi nzima ya ajali za uzalishaji.

Jenerikis, pia huitwa upolimofia wa kigezo, hukuruhusu kuandika msimbo unaofanya kazi juu ya aina nyingi bila kuacha usalama wa aina: List<T> ni orodha ya aina mahususi T, inayokaguliwa wakati wa kukusanya, badala ya orodha ya vitu visivyo na aina unavyovigeuza na kuombea. Fikia jenerikis kujenga vyombo, kazi, na dhana zinazoweza kutumika tena zinazobaki na aina imara. Uoanishaji wa aina za jumla, aina zisizo null, na jenerikis ndio unaoruhusu mfumo wa kisasa wa aina kueleza kanuni halisi za kikoa badala ya kuweka lebo kwa vitu vya kawaida tu.

Pokea aina hatua kwa hatua katika msimbo wa kidinamiki uliopo

Huhitaji kuandika upya msimbo wa kidinamiki ili kupata faida za uandishi wa aina. Uandishi wa aina wa hatua kwa hatua huruhusu msimbo wenye aina na usio na aina kuishi pamoja, ili uongeze aina kwa kuongezeka pale zinapolipa zaidi. Mifumo mingi ya ikolojia sasa inaunga mkono hili moja kwa moja: vidokezo vya aina katika Python vinavyokaguliwa na kikaguzi tofauti, seti kuu yenye aina inayokusanywa kuwa lugha ya kidinamiki, au maelezo ya aina yaliyowekwa juu ya wakati wa kuendesha uliopo. Anza kwenye mipaka na moduli muhimu zaidi (msimbo wa fedha, msimbo wa usalama, kielelezo cha data), washa kikaguzi katika hali ya ruhusa, na kaza kwa muda. Ongeza kanuni kwamba msimbo mpya lazima uwe na aina hata msimbo wa zamani ukiendelea kufikia. Ndani ya robo chache msimbo mkubwa usio na aina unaweza kufikia hatua ambapo mabadiliko mengi yanakaguliwa aina, na sehemu zinazojalisha zaidi zimefunikwa kwanza.

Endesha linters, vikaguzi vya aina, na wachambuzi wa kina pamoja

Ukaguzi wa aina ni safu moja; ongeza zingine. Zana ya lint hunasa mifumo ya kutia shaka ambayo kikaguzi cha aina hukipuuza: mgawo ambao daima ni kweli, kigeu kisichotumika, kuanguka katika switch, rasilimali isiyofungwa kamwe. Wachambuzi wa kina hufikiri kuhusu tabia ya programu. Uchambuzi wa mtiririko wa data hufuatilia thamani zinavyosogea kupitia msimbo kujibu maswali kama “je, kigeu hiki kinatumika kabla ya kupewa thamani” au “je, kishikio hiki cha faili kinaweza kuvuja kwenye njia ya kosa.” Zana nyingi kati ya hizi zimejengwa juu ya ufasiri wa kiabstrakti, mbinu inayoendesha programu kwa dhahania juu ya seti za thamani zinazowezekana (kwa mfano “chanya,” “sifuri,” au “hasi” badala ya namba halisi) kuthibitisha sifa juu ya utekelezaji wote kwa wakati mmoja, bila kuendesha hata mmoja.

Baadhi ya wachambuzi hukaa kando ya zana za usalama. Upimaji tuli wa usalama wa programu (SAST) huchanganua chanzo kwa mifumo ya udhaifu kama uingizaji, upotoshaji usio salama, au data iliyochafuliwa inayofika kwenye shimo hatari, na hushiriki mashine ya mtiririko wa data iliyoelezwa hapa; ichukulie kama sehemu ya familia hii na uiratibu na usalama wa programu (sura ya 4.2). Pendekezo la kiutendaji ni seti ya tabaka: linter ya haraka kwa mtindo na hitilafu dhahiri, kikaguzi cha aina kwa mikataba, na mchambuzi mmoja au zaidi wa kina kwa sifa zinazojalisha kwa kikoa chako. Zisanidi kutoka faili zilizo kwenye udhibiti wa matoleo ili kanuni ziwe zilezile kwa kila mtu.

Chukulia maonyo kama makosa na uongeze kipimo cha msingi kwa kishindo

Onyo lisilofeli ujenzi ni onyo litakalopuuzwa. Kumbukumbu inapojaa mamia ya maonyo yanayovumiliwa, hakuna anayeisoma, na lile linalojalisha hujificha kwenye kelele. Pokea sera ya kuchukulia maonyo kama makosa ili onyo jipya livunje ujenzi na lirekebishwe wakati ni nafuu zaidi. Katika msimbo wa urithi wenye maelfu ya maonyo yaliyopo, huwezi kugeuza swichi hiyo kwa usiku mmoja, kwa hiyo tumia kishindo: rekodi hesabu ya sasa kama kipimo cha msingi, zuia badiliko lolote linaloiongeza, na ishushe kwa muda. Kipimo cha msingi kinaweza kushuka tu. Hii inakuruhusu kuwasha kanuni kali leo bila usafishaji mkubwa wa awali, huku ikihakikisha hali haizidi kuwa mbaya na inaendelea kuwa bora.

Unganisha uchambuzi kwenye vihariri na CI, kwa maoni ya haraka

Uchambuzi tuli hulipa zaidi maoni yanapokuwa ya papo hapo. Endesha ukaguzi uleule kwenye kihariri, kupitia Language Server Protocol au sawa nayo, ili msanidi aone kosa anapoandika, kabla hata hajahifadhi. Kisha endesha seti ileile ya kanuni kwenye ujumuishaji endelevu (CI) ili kisiunganishwe chochote bila kupita, ukifunga hili na bomba la sura ya 8.1. Hizi mbili lazima zikubaliane: kihariri kikiwa legevu na CI ikiwa kali, au kinyume chake, watu hupoteza imani kwa vyote viwili. Weka uchambuzi wa haraka wa kutosha kuendeshwa kwa kila badiliko, hifadhi matokeo kwenye kache, na uchambue tu kilichobadilika pale unapoweza, ili kikaguzi kiwe msaada badala ya kodi. Kihariri na bomba vinapotekeleza kanuni zilezile kwa njia ileile, kiwango huacha kuwa waraka ambao watu wanausahau na kuwa sifa ya mazingira.

Hifadhi uthibitisho rasmi kwa msimbo unaostahili

Mwisho wa wigo kuna uthibitisho rasmi: kuthibitisha kihisabati kwamba programu inatimiza ubainishaji sahihi, si kwamba inapita majaribio tu. Mbinu huanzia ukaguzi wa kielelezo (kuchunguza hali zote za mfumo kikamilifu) hadi uthibitishaji wa nadharia na aina tegemezi (aina zenye uwezo wa kutosha kuweka ubainishaji kamili). Hiki ndicho hakikisho la kina zaidi linalopatikana na la gharama kubwa zaidi kuzalisha, kwa hiyo hupata nafasi yake tu pale kasoro ni ya maafa au uthibitisho unapodai: maktaba za kriptografia, msimbo wa udhibiti wa ndege, hypervisor, itifaki muhimu. Kwa programu nyingi uwekezaji sahihi ni aina imara pamoja na wachambuzi wazuri, vinavyonasa faida nyingi kwa sehemu ndogo ya gharama. Jua kwamba mbinu rasmi (zilizoletwa katika sura ya 2.12) zipo na mstari uko wapi, ili uzifikie kwa makusudi kwa kijenzi nadra kinachohitaji.

Weka ukandamizaji wa uaminifu

Hakuna mchambuzi aliyekamilika, na nidhamu inayotenganisha zana inayoaminika na inayopuuzwa ni jinsi unavyoshughulikia makosa yake. Kila zana makini hukuruhusu kukandamiza matokeo. Hitaji kila ukandamizaji uwe mwembamba (mstari mmoja au matokeo moja, kamwe faili nzima au kanuni nzima), ubebe sababu kwenye maoni, na uonekane kwenye mapitio kama msimbo mwingine wowote. Kuzima kwa jumla juu ya faili ndivyo ufikiaji unavyooza kimyakimya. Kagua ukandamizaji mara kwa mara na uchukulie rundo linalokua la ukandamizaji kama ishara kwamba kanuni imewekwa vibaya au kwamba msimbo una tatizo halisi ambalo mtu analificha. Ukandamizaji wa uaminifu huweka zana ikiaminika; ukandamizaji wa kimya, wa jumla huigeuza kuwa maigizo.

Mabadilishano: faida na hasara

Mbinu	Faida	Hasara
Aina tuli	Mikataba iliyokaguliwa na mashine; urekebishaji salama wa muundo; zana tajiri	Taratibu zaidi mapema; uundaji wa mifano wa mapema ni polepole
Aina za kidinamiki	Haraka kuandika; zinanyumbulika; taratibu chache	Makosa ya aina hujitokeza wakati wa kuendesha; urekebishaji wa muundo ni hatari
Uchukuzi wa aina	Usalama na ufupi; kelele ndogo ya maelezo	Aina zinazodhaniwa zinaweza kuficha nia zikitumiwa kupita kiasi
Uandishi wa aina wa hatua kwa hatua	Upokeaji wa kuongezeka; funika msimbo muhimu kwanza	Kingo zisizo na aina bado huvuja; hakikisho za sehemu
Linters na uchambuzi wa mtiririko wa data	Hunasa hitilafu ambazo aina hazizioni; nafuu kuendesha	Uongo chanya; kelele zisiposanidiwa
Maonyo-kama-makosa na kishindo	Masuala mapya yanazuiwa; kipimo cha msingi kinaboreka tu	Inaweza kuhisi kizuizi; inahitaji sera ya ukandamizaji
Uthibitisho rasmi	Hakikisho kali zaidi; huthibitisha sifa kwa ingizo zote	Ghali, ya kitaalamu; mara chache inahalalishwa

Mvutano unaojirudia ni hakikisho dhidi ya msuguano. Kila hatua kuelekea aina kali zaidi na uchambuzi wa kina hukununulia darasa la hitilafu linalokuwa lisilowezekana, na kila hatua inaongeza taratibu, muda wa kuendesha zana, na uongo chanya wa mara kwa mara unaomgharimu msanidi dakika. Utatue kwa dau na kwa maisha. Hati ya mara moja au spike inataka mwisho mwepesi, wa haraka, wa kidinamiki. Leja ya malipo, ukaguzi wa ruhusa, au mfumo ambao serikali itauendesha kwa miaka kumi na mitano unataka aina imara, wachambuzi wa tabaka, maonyo-kama-makosa, na, kwa kiini chake hatari zaidi, labda uthibitisho rasmi. Linganisha ukali na gharama ya kukosea, na uache uchukuzi na upokeaji wa hatua kwa hatua kuweka msuguano ukiwa wa kumudu.

Maswali ya kujadili na timu yako

Wapi katika msimbo wetu mfumo wa aina ungezuia matukio yetu kadhaa ya mwisho ya uzalishaji, na je, tunajua? Timu nyingi hubishana kuhusu uandishi wa aina kwa dhahania wakati ushahidi umekaa kwenye historia yao ya matukio. Vuta kasoro kumi au ishirini za mwisho za uzalishaji na uzipange: ngapi zilikuwa null mahali thamani ilitarajiwa, umbo lisilo sahihi lililopitishwa kuvuka mpaka, kesi isiyoshughulikiwa, thamani ya mfuatano iliyoteleza? Hizo ndizo hasa kasoro ambazo kikaguzi cha aina na linter hunasa bure. Sehemu kubwa ya matukio yenu ikiwa kwenye kapu hilo, una hoja madhubuti, yenye dola ya aina imara zaidi katika moduli ambamo yalitokea. Karibu hakuna yakiwa humo, hitilafu zenu zinaishi kwingine (mantiki, ulinganifu, mahitaji) na aina nzito zaidi huenda si hatua yenu yenye thamani ya juu zaidi. Vyovyote, unabadilisha maoni na data.
Tungepokea uandishi wa aina wa hatua kwa hatua, tungeanzia wapi, na “imetosha” ingemaanisha nini? Kuwasha kikaguzi kuvuka msimbo mkubwa wa kidinamiki ni programu, si kugeuza swichi, na mpangilio huamua kama inafanikiwa au inakwama. Jadilini moduli zipi zinabeba hatari kubwa zaidi (fedha, uthibitishaji, kielelezo cha msingi cha data) na kwa hiyo zinastahili aina kwanza, dhidi ya zipi ni thabiti na za dau la chini vya kutosha kuachwa bila aina kwa sasa. Kubaliana kanuni kwa msimbo mpya (wenye aina tangu siku ya kwanza) ili uso usio na aina uache kukua huku mnapunguza rundo. Fafanua lengo: labda kila saini ya kazi ya umma iwe na aina, kila mpaka uthibitishwe kuwa aina, kikaguzi kiendeshe katika hali kali kwenye vifurushi muhimu. Bila mstari wa kumaliza uliofafanuliwa, uandishi wa aina wa hatua kwa hatua huwa wa milele na nusu-umefunikwa, ambayo ni mbaya zaidi ya yote mawili.
Sera yetu ni ipi mchambuzi tuli anapokosea, na je, inaweka zana ikiaminika? Kila mchambuzi huzalisha uongo chanya, na jinsi unavyoshughulikia huamua kama zana inabaki yenye manufaa au inazimwa kwa kuchoka. Pitieni kesi madhubuti: matokeo yanapokuwa uongo chanya wa kweli, je, ukandamizaji ni mwembamba, una maoni yenye sababu, na unaonekana kwenye mapitio, au mtu anazima kanuni nzima kwa hazina nzima? Tazama ukandamizaji wenu wa sasa: ni mingapi, je, inabeba sababu, na lini mara ya mwisho yeyote aliikagua? Rundo la ukandamizaji mpana usioelezwa linamaanisha ufikiaji wenu ni tupu kimyakimya. Lengo ni nidhamu ya pamoja, inayotekelezwa inayoweka mchambuzi akiaminika, ili matokeo yake yaaminike na kutendewa kazi badala ya kunyamazishwa kwa silika.
Tunasawazisha lugha na wachambuzi gani, na tunaweka vipi seti moja ya kanuni mfumo wetu unapogawanyika kuvuka timu? Mamia ya wahandisi wanapofanya kazi kwa lugha kadhaa, kila timu ikielekea kwenye kikaguzi chake, kanuni zake za lint, na mpangilio wake wa ukali huharibu hakikisho kimyakimya, kwa sababu mkataba unaotekelezwa kwenye hazina moja ni pendekezo tu kwenye inayofuata. Mvuto unaoshindana ni halisi: usawazishaji wa kati unakupa wahandisi wanaohamishika na ushahidi sare wa ukaguzi, hata hivyo seti ya kanuni iliyowekwa kutoka katikati inaweza kupingana na misemo ya lugha au kupunguza kasi ya timu iliyokuwa na sababu nzuri za usanidi wake. Leta orodha ya lugha zilizo kwenye uzalishaji, wachambuzi na matoleo ambayo kila timu inaendesha, na tofauti ya seti zao za kanuni ili kuteleza kuonekane badala ya kudhaniwa. Katika mazingira ya mashirika makubwa au serikali, funga jibu na ununuzi na ukaguzi: usanidi mmoja ulio kwenye udhibiti wa matoleo ambao kila hazina inaurithi ndio unaomruhusu mkaguzi kuthibitisha ukaguzi uleule uliendeshwa kila mahali, na ndio unaomzuia muuzaji kusafirisha msimbo chini ya kanuni dhaifu kuliko wafanyakazi wako wanazotakiwa kutimiza.
Uchambuzi wetu ni wa haraka kiasi gani, na lini watu wanaanza kuuzunguka? Kikaguzi ni hakikisho tu ikiwa kinaendeshwa kwa kila badiliko, na wakati kinapofanya mzunguko wa kuhariri-kujenga kuwa na maumivu, wahandisi hujifunza kukiruka, kukizima kwa ndani, au kuunganisha kikiwa nyekundu na kuahidi kukirekebisha baadaye. Mvutano ni kina dhidi ya kasi: mtiririko wa data wa kina au pasi ya usalama hupata hitilafu ambazo linter ya haraka inazikosa, lakini ikiwa seti kamili inachukua dakika ishirini watu huacha kuisubiri, na ukaguzi ambao hakuna anayeusubiri hauhifadhi chochote. Leta namba halisi kwenye mjadala: ucheleweshaji wa maoni ya kihariri, muda wa saa ya ukuta wa CI kwa hatua ya uchambuzi, viwango vya mafanikio ya kache, mara ngapi ujenzi unaunganishwa huku ukaguzi umerukwa au kubatilishwa, na kiasi gani cha uendeshaji ni cha kuongezeka dhidi ya kamili. Kwa shirika kubwa au la umma, ongeza bili ya kokotoo na gharama ya uwezo wa kupitisha, kwa sababu kwa ukubwa wa meli hatua ya uchambuzi ya lazima ya polepole ni mstari wa bajeti na foleni inayochelewesha kila toleo, na suluhisho la uaminifu kwa kawaida ni uchambuzi wa kuongezeka na kache badala ya kulegeza kanuni kimyakimya.
Ni ushahidi gani unaokaguliwa na mashine tunaoweza kuzalisha kwa mkaguzi, na ni vigeu gani visivyobadilika muhimu vyetu vinavyofunika? Katika mifumo inayodhibitiwa na yenye dau kubwa, hoja ya aina na uchambuzi tuli ni uthibitisho unaoonekana kwamba kategoria nzima za kasoro haziwezekani kwa muundo, zaidi ya hitilafu za kila siku unazozuia, na dai hilo halina thamani usipoweza kuonyesha vigeu visivyobadilika vipi vinatekelezwa na wapi. Mabadilishano ni wigo dhidi ya gharama: kuthibitisha zaidi (kutokuwa null kila mahali, aina za jumla kwa kila hali halali, uthibitisho rasmi wa hesabu ya msingi) hununua ushahidi imara zaidi, hata hivyo kila hatua juu katika ukali hugharimu juhudi ya maelezo, muda wa mtaalamu, na ugumu wa ujenzi ambao huenda huuhitaji kwa msimbo wa dau la chini. Leta ramani ya moduli zenu muhimu kwa usalama kwa hakikisho ambazo kila moja inabeba sasa, orodha ya ukandamizaji wazi na sababu zake, na mapengo yoyote ambapo kanuni muhimu inatekelezwa na desturi badala ya mkusanyaji. Kwa serikali au shirika kubwa linalodhibitiwa, liweke hili kama ushahidi wa uthibitisho: mkaguzi anapaswa kuweza kufuatilia sifa inayohitajika hadi aina au uthibitisho unaokaguliwa na mashine na kuona kumbukumbu ya ukandamizaji inayoandika kila kighairi, ili uzingatiaji usimame juu ya vitu ambavyo mnyororo wa zana unazalisha badala ya mapitio ya mkono baada ya tukio.

Mtazamo wa sekta

Kampuni changa. Kasi inashinda, kwa hiyo fikia usalama wa bei nafuu zaidi usiokupunguza kasi: lugha yenye aina imara au kikaguzi cha aina katika hali ya ruhusa, pamoja na linter ya haraka kwenye kihariri, na uandike aina za msimbo wako wa fedha na uthibitishaji kwanza. Ruka uthibitisho rasmi na seti za mtiririko wa data wa kina kabisa; zinagharimu muda ambao huna. Malipo unayoyataka mapema ni urekebishaji wa muundo unaoweza kuuamini kwa mistari elfu kumi, kwa hiyo washa kikaguzi kabla msimbo haujawa mkubwa mno kuudhibiti.

Biashara ndogo. Bila mtaalamu wa uchambuzi tuli kwenye wafanyakazi, pendelea lugha na mnyororo wa zana ambapo chaguo-msingi nzuri huja zimejengwa ndani badala ya seti unayopaswa kurekebisha na kuangalia. Nunua uchambuzi uliojengwa ndani ya IDE yako na CI inayohifadhiwa badala ya kuanzisha jukwaa lako, na uweke seti ya kanuni karibu na kiwango cha jamii ili mkandarasi au mwajiriwa mpya aitambue. Chukulia maonyo-kama-makosa na kiini kidogo chenye aina kama hatua zenye kiegemeo cha juu zaidi ambazo bajeti yako ndogo inaweza kuchukua.

Biashara kubwa. Kazi ni utawala kuvuka timu nyingi: usanidi mmoja ulio kwenye udhibiti wa matoleo ambao kila hazina inaurithi, kanuni zilezile kwenye kihariri na bomba, na kipimo cha msingi cha kishindo ili ufikiaji wa timu yoyote usishuke kimyakimya. Sawazisha wachambuzi, fuatilia ufikiaji wa aina na hesabu za ukandamizaji kama vipimo vya jalada, na ukague ukandamizaji kwa ratiba thabiti ili hakikisho zinazokaguliwa na mashine zibaki sare vya kutosha mkaguzi aziamini. Weka bajeti ya timu ya jukwaa inayomiliki usanidi wa pamoja, kwa sababu uthabiti kuvuka maelfu ya wahandisi haujidumishi wenyewe.

Serikali. Ununuzi, uwazi, na maisha marefu hutawala. Hitaji kwenye mikataba kwamba wagavi watimize kanuni zilezile za uchambuzi ambazo wafanyakazi wako wanatimiza na wakabidhi usanidi na kumbukumbu za ukandamizaji kama vitu vya kutoa, ili hakikisho linusurike mabadiliko ya muuzaji. Pendelea ushahidi unaokaguliwa na mashine kuliko uhakikisho wa mkono kwa mantiki ya kustahiki na malipo, hifadhi uthibitisho rasmi kwa hesabu ambazo kushindwa kwake kungenyima manufaa kinyume cha sheria, na uandike kila ukandamizaji kwa ukaguzi kwa muongo au zaidi ambao mfumo utaendesha.

Mifano

Kampuni changa. Kampuni changa ya watu sita inajenga bidhaa yake kwa lugha ya kidinamiki kwa kasi, ambayo inawatumikia vizuri hadi urekebishaji wa muundo kwa mistari elfu kumi unaanza kusababisha makosa ya aina ya wakati wa kuendesha wanayogundua tu kwenye uzalishaji. Wanapokea uandishi wa aina wa hatua kwa hatua: wanawasha kikaguzi cha aina katika hali ya ruhusa, wanaongeza vidokezo vya aina kwenye kielelezo chao cha msingi cha kikoa na msimbo wa malipo kwanza, na kuweka kanuni kwamba moduli zote mpya ziwe na aina kikamilifu. Wanaunganisha kikaguzi na linter kwenye kihariri chao na CI kwa usanidi uleule, na kuchukulia maonyo mapya kama makosa huku wakishusha yaliyopo kwa kishindo. Ndani ya robo mbili ajali kutokana na maumbo yasiyolingana zinatoweka, urekebishaji wa muundo unaacha kutisha, na ukamilishaji otomatiki wa mwajiriwa mpya unajua kweli kila kazi inarudisha nini. Uwekezaji uligharimu wiki chache za mhandisi na uliondoa chanzo kinachojirudia cha hitilafu zinazowakabili wateja.

Biashara kubwa. Benki ya kimataifa inasawazisha uchambuzi tuli kuvuka maelfu ya wahandisi. Kila hazina inarithi usanidi wa pamoja: kikaguzi cha aina katika hali kali, linter, mchambuzi wa mtiririko wa data, na kichanganuzi cha SAST kwa mifumo ya usalama, vyote vikiendesha kwenye kihariri na kutekelezwa kwenye bomba ili kisiunganishwe chochote bila kupita. Aina za kikoa hufanya hali zisizo halali zisiwezekane kuwakilishwa katika msimbo unaohamisha fedha: muamala uliowekwa na unaosubiri ni aina tofauti, sarafu zimeandikwa kwa aina ili usiweze kuongeza dola kwa euro, na ingizo zilizothibitishwa ni aina tofauti na ghafi. Maonyo ni makosa, na kipimo cha msingi cha kila timu kinaweza kushuka tu. Ukandamizaji unahitaji sababu na hukaguliwa kila robo mwaka. Kwa sababu hakikisho zinakaguliwa na mashine na ni sare, wakaguzi wanaweza kuona kwamba kategoria nzima za kasoro haziwezekani kwa muundo, na wahandisi wanahama kwa kujiamini kuvuka huduma zisizojulikana.

Serikali. Mamlaka ya kitaifa ya kodi inaboresha mfumo wa hesabu ya manufaa unaopaswa kuwa sahihi na unaoweza kuelezwa kwa miaka. Mantiki ya msingi ya kustahiki imeandikwa kwa lugha yenye aina imara ambapo kielelezo cha kikoa kinaweka kanuni: hali ya mwombaji ni aina ya jumla inayofunika kila kesi halali, kiasi cha fedha ni aina maalumu isiyoweza kuchanganywa na hesabu, na hakuna thamani inayoweza kukosekana inayoachwa kama aina mtupu inayoweza null. Uchambuzi tuli unaendeshwa kwenye CI kama lango, na moduli ya hesabu muhimu zaidi kwa usalama inakaguliwa zaidi kwa mbinu rasmi kuthibitisha vigeu visivyobadilika muhimu vinashikilia kwa ingizo zote, ikitimiza mahitaji ya uthibitisho. Kila ukandamizaji umeandikwa kwa ukaguzi. Waandishi wa asili wanapohama, warithi wao wanarithi msimbo ambao mikataba yake mkusanyaji anaitekeleza, kwa hiyo wanaweza kuubadilisha kwa usalama muongo mmoja baadaye.

Kesi ya biashara: sababu, ROI, na TCO

Mapato ya aina na uchambuzi tuli ni mabadiliko ya mahali unapolipia kasoro. Kasoro iliyonaswa na kikaguzi cha aina kwenye kihariri inagharimu sekunde; kasoro ileile iliyonaswa kwenye uzalishaji inagharimu tukio, uchunguzi, pengine madhara kwa wateja na matokeo ya udhibiti. Tafiti za uchumi wa kasoro mara kwa mara zinaonyesha gharama ikipanda kwa kipimo cha ukubwa katika kila hatua kasoro inayonusurika, kutoka kuandika hadi mapitio hadi jaribio hadi uzalishaji. Uchambuzi tuli huhamisha kategoria nzima ya kasoro hadi hatua ya bei nafuu zaidi, kwa kila ujenzi, bila kazi kwa kila kasoro. Hiyo ni gharama ya usanidi iliyowekwa, hasa ya mara moja, inayonunua mkondo usio na kikomo wa kasoro zilizozuiwa, ambao ni karibu kiegemeo bora kabisa katika uhandisi.

Gharama ni halisi lakini za wastani na za mapema. Unachagua na kusanidi zana, unalipa taratibu fulani kwenye maelezo (zinazopunguzwa na uchukuzi), unatumia muda wa mhandisi kupokea uandishi wa aina wa hatua kwa hatua katika msimbo wa urithi, na unakubali uongo chanya wa mara kwa mara. Dhidi ya hayo, pima jumla ya gharama ya umiliki ya mbadala: kila hitilafu yenye umbo la aina inayofika uzalishaji, kila urekebishaji hatari wa muundo ulioepukwa kwa sababu hakuna kinachohakikisha usahihi, kila utambulisho wa polepole kwa sababu msimbo hauandiki mikataba yake, na katika mazingira yanayodhibitiwa kila ukaguzi unaopaswa kutimizwa kwa mapitio ya mkono badala ya ushahidi unaokaguliwa na mashine. Kujenga hoja kwa uongozi, ifunge na vipimo wanavyofuatilia tayari: kiwango cha kushindwa kwa mabadiliko, kiwango cha kasoro zinazotoroka, muda wa wastani wa kurejesha, na sehemu ya matukio yanayoweza kuhusishwa na makosa ya aina na null yanayozuilika. Grafu inayoshawishi watu ni historia yenu ya matukio iliyopangwa kwa kama kikaguzi kingeyanasa.

Mifumo mibaya na mitego

Njia ya kutoroka kama tabia: kubadilisha kuwa any, dynamic, au sawa na isiyo na aina ili kunyamazisha kikaguzi, jambo linalofuta hakikisho hasa mahali ulipoihitaji zaidi.
Kila kitu kama mfuatano: kupitisha mfuatano mtupu na ramani zisizo na aina kuvuka mipaka badala ya kuunda hali kama aina halisi, kwa hiyo mkusanyaji hawezi kusaidia.
Inayoweza null kwa chaguo-msingi: kuacha thamani zinaweza kuwa null lugha inapotoa aina zisizo null na za hiari, kuhifadhi kosa la dola bilioni.
Maonyo ambayo hayashindi kamwe: maelfu ya maonyo yanayovumiliwa ambamo lile linalojalisha halionekani, kwa sababu hakuna kinachovunja ujenzi kamwe.
Kihariri na CI havikubaliani: legevu kwa ndani na kali kwenye bomba, au kinyume, kwa hiyo wasanidi hawaamini vyote viwili na uunganishaji unawashangaza watu.
Ukandamizaji wa jumla: kuzima kanuni nzima au faili badala ya matokeo moja yenye sababu, kuzamisha ufikiaji kimyakimya.
Maigizo ya uchambuzi: kuendesha zana ambazo matokeo yake hakuna anayeyasoma au kuyatendea kazi, kwa hiyo ripoti hurundikana na thamani ni sifuri.
Aina za yote-au-hakuna: kukataa kuanza kwa sababu huwezi kuweka aina kwa kila kitu kwa mara moja, ukipoteza faida kubwa za kuweka aina kwenye msimbo muhimu kwanza.
Uthibitisho kila mahali: kufikia mbinu rasmi kwa msimbo wa kawaida, kutumia juhudi adimu ya mtaalamu mahali aina imara zingetosha.

Kielelezo cha ukomavu

Ngazi ya 1, Kuanzisha: Uandishi wa aina na uchambuzi ni wa papo hapo na wa kila msanidi. Msimbo wa kidinamiki hauna kikaguzi, au lugha tuli inaendesha na maonyo yamepuuzwa. Hitilafu zenye umbo la aina (null, maumbo yasiyo sahihi, kesi zisizoshughulikiwa) hufika uzalishaji mara kwa mara, na urekebishaji wa muundo unaogopwa kwa sababu hakuna kinachothibitisha usahihi.
Ngazi ya 2, Kuendeleza: Linter na, inapohusika, kikaguzi cha aina huendesha kwenye baadhi ya miradi, lakini kanuni hutofautiana kati ya timu, maonyo hayashindi ujenzi, na njia za kutoroka na ukandamizaji mpana ni wa kawaida. Faida fulani inapatikana, lakini ufikiaji hauna uthabiti na imani kwa zana ni ya mtawanyiko.
Ngazi ya 3, Kusawazisha: Usanidi wa pamoja, ulio kwenye udhibiti wa matoleo unatekeleza ukaguzi wa aina na linting kwenye kihariri na CI kwa kanuni zilezile shirika zima. Maonyo ni makosa yenye kipimo cha msingi cha kishindo, uwezekano wa null na aina za jumla hutumika kufanya hali zisizo halali zisiwezekane kuwakilishwa kwenye mipaka, na kila ukandamizaji unahitaji sababu iliyoandikwa, inayoweza kupitiwa.
Ngazi ya 4, Kusimamia: Uchambuzi unapimwa na kudhibitiwa dhidi ya vipimo vya msingi. Ufikiaji wa aina kwenye moduli muhimu, hesabu za maonyo, viwango vya uongo chanya, hesabu za ukandamizaji, na sehemu ya matukio ya uzalishaji ambayo kikaguzi kingenasa yote yanafuatiliwa dhidi ya malengo wazi. Vipimo vinadhibiti mabadiliko: ufikiaji kwenye msimbo wa fedha na uthibitishaji hauwezi kushuka, kiwango cha uongo chanya kinachopanda huchochea kupanga upya kanuni, na dashibodi zinaonyesha kama hakikisho zinashikilia kweli badala ya kusanidiwa tu.
Ngazi ya 5, Kuratibu: Uchambuzi unaboreshwa kila wakati na kuunganishwa kuvuka shirika. Uandishi wa aina wa hatua kwa hatua umefika moduli muhimu, wachambuzi wa mtiririko wa data na usalama huendesha kwa kawaida, kanuni hubadilika lugha na vitisho vinapoendelea, na uthibitisho rasmi unatumika kwa makusudi kwa vijenzi vichache ambavyo kushindwa kwake kungekuwa maafa. Zana, vipimo, na seti ya kanuni hurudi kwenye usanifu, kuajiri, na ununuzi, kwa hiyo shirika zima linazidi kuwa salama kubadilisha.

Mawazo ya kujadili

Ni hitilafu zipi za hivi karibuni za uzalishaji ambazo kikaguzi cha aina au linter kingenasa, na zinawakilisha sehemu gani ya jumla?
Wapi katika kielelezo chenu cha kikoa aina ya jumla au aina ya kufunga iliyothibitishwa inaweza kugeuza “haipaswi kutokea kamwe” ya wakati wa kuendesha kuwa “haiwezi kutokea” ya wakati wa kukusanya?
Mkigeuza maonyo kuwa makosa kesho, mangapi yangevunja ujenzi, na kipimo gani cha msingi na kishindo kingewaruhusu kupokea sera bila vita vya kusafisha?
Je, kihariri chenu na bomba vinaendesha kanuni zilezile kabisa, na msanidi angejuaje kama zimetengana?
Ukandamizaji mwingi kiasi gani unaishi kwenye msimbo wenu sasa hivi, mingapi inabeba sababu, na lini ilikaguliwa mara ya mwisho?
Je, kuna kijenzi chochote katika mfumo wenu ambacho kushindwa kwake ni maafa ya kutosha kuhalalisha uthibitisho rasmi, na mngejuaje?

Mambo muhimu ya kukumbuka

Uandishi wa aina tuli na uchambuzi husukuma darasa zima la kasoro hadi wakati wa bei nafuu zaidi kuzirekebisha: unapoandika msimbo, kwa kila ujenzi, bila kazi kwa kila kasoro.
Pendelea hakikisho ambazo mashine inazikagua kuliko kanuni ambazo binadamu lazima wazikumbuke, na uweke nia ndani ya aina ili hali zisizo halali zisiweze kuwakilishwa kabisa.
Huhitaji yote au hakuna: uandishi wa aina wa hatua kwa hatua hukuruhusu kufunika msimbo muhimu (fedha, uthibitishaji, kielelezo cha data) kwanza huku mengine yakifikia.
Chukulia maonyo kama makosa yenye kipimo cha msingi cha kishindo, endesha kanuni zilezile kwenye kihariri na CI, na uweke ukandamizaji mwembamba, wenye sababu, na unaokaguliwa.
Linganisha ukali na dau: aina imara pamoja na wachambuzi wa tabaka kwa mifumo mingi, na uthibitisho rasmi uliohifadhiwa kwa kijenzi nadra ambacho kushindwa kwake ni maafa.

Marejeo na usomaji zaidi

Benjamin C. Pierce, Types and Programming Languages
Simon Peyton Jones (ed.), The Implementation of Functional Programming Languages
Flemming Nielson, Hanne Riis Nielson, and Chris Hankin, Principles of Program Analysis
Patrick Cousot and Radhia Cousot, “Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints”
Scott Wlaschin, Domain Modeling Made Functional
Steve McConnell, Code Complete: A Practical Handbook of Software Construction
Michael Barr and the MISRA Consortium, MISRA C: Guidelines for the Use of the C Language in Critical Systems
Al Bessey et al., “A Few Billion Lines of Code Later: Using Static Analysis to Find Bugs in the Real World,” Communications of the ACM