2.21 Systemau mathau a dadansoddiad statig

Trosolwg a chymhelliant

Delir y rhan fwyaf o ddiffygion yn hwyr, adeg rhedeg, gan brawf neu ddefnyddiwr neu ddigwyddiad. Nid oes angen i ddosbarth cyfan ohonynt gyrraedd mor bell â hynny o gwbl. Mae system fathau a theclyn dadansoddi rhaglenni statig da yn darllen eich cod cyn iddo redeg ac yn profi na all rhai camgymeriadau ddigwydd: llinyn a ddefnyddir lle mae angen rhif, dadgyfeirnod null, newidyn a ddarllenir cyn iddo gael ei ysgrifennu, achos a adewir heb ei drin. Mae’r bennod hon yn ymwneud â gwthio cywirdeb i’r chwith, yn nes at yr union eiliad y byddwch yn ysgrifennu’r llinell, lle mae trwsiad yn costio eiliadau yn hytrach na thudalen mewn adolygiad digwyddiad.

Mae dadansoddiad statig yn unrhyw dechneg sy’n archwilio cod ffynhonnell neu god wedi’i grynhoi heb ei redeg. Gwirio mathau yw’r ffurf fwyaf cyffredin, ond mae’r teulu hefyd yn cynnwys leinwyr (offer sy’n fflagio patrymau arddull a chywirdeb), dadansoddwyr llif data, ac, ar y pen pellaf, wiriad ffurfiol. Yr addewid cyffredin yw dosbarth o warantau a gewch am ddim ar bob adeiladwaith, am byth, heb brawf i’w ysgrifennu a heb adolygydd i’w gofio. Dyna pam mae’r ddisgyblaeth hon yn eistedd ochr yn ochr â safonau codio (pennod 2.1), egwyddorion dylunio meddalwedd (pennod 2.2), a strategaeth profi (pennod 2.4): mae’n ffordd awtomataidd arall o wneud cronfa god fawr yn ddiogel i’w newid.

I dimau mawr, mae’r gwerth yn cyfansymio. Pan fydd cannoedd o beirianwyr yn cyffwrdd â system a rennir, mae llofnod math yn gontract y mae crynhoydd yn ei orfodi ar bob un ohonynt, ac mae gwiriwr yn y biblinell yn adolygydd nad yw byth yn blino nac yn ffafrio neb. Mewn lleoliadau menter, mae hyn yn torri cost sefydlu ac integreiddio, oherwydd bod y mathau’n dogfennu bwriad a’r dadansoddwyr yn dal camgymeriadau’r newydd-ddyfodiaid. Mewn llywodraeth a systemau risg-uchel eraill, lle gall ateb anghywir wadu budd-dal neu ddatgelu data, mae gwarantau a wirir gan beiriant yn dystiolaeth: maent yn dangos i archwiliwr fod dosbarthiadau cyfan o ddiffyg yn amhosibl trwy adeiladwaith, nid yn ddim ond heb eu profi. Mae hyn yn cysylltu’n uniongyrchol ag ansawdd meddalwedd (pennod 2.11) a diogelwch cymwysiadau (pennod 4.2).

Egwyddorion allweddol

Gwthio cywirdeb i’r chwith: dal diffyg adeg awduro, nid mewn cynhyrchiad.
Ffafrio gwarantau y mae’r peiriant yn eu gwirio dros gonfensiynau y mae’n rhaid i bobl eu cofio.
Amgodio bwriad mewn mathau fel na ellir cynrychioli cyflyrau anghyfreithlon o gwbl.
Mabwysiadu mathau’n raddol mewn cod dynamig; nid oes angen popeth neu ddim byd.
Trin rhybuddion fel gwallau, a ratsio’r llinell sylfaen fel na all ond gwella.
Rhedeg yr un dadansoddwyr yn y golygydd ac yn y biblinell, gyda rheolau union yr un fath.
Rheoli canlyniadau positif ffug gyda diffygiad disgybledig, cyfiawnedig, y gellir ei adolygu.

Argymhellion

Dewis teipio statig neu ddynamig gyda llygaid agored

Mewn iaith wedi’i theipio’n statig, gwirir mathau cyn i’r rhaglen redeg; mewn un wedi’i theipio’n ddynamig, fe’u gwirir wrth iddi redeg, os o gwbl. Nid yw’r naill na’r llall yn gywir yn gyffredinol, a’r fframio gonest yw cyfnewid gwarantau am hyblygrwydd. Mae teipio statig yn prynu contractau a wirir gan beiriant, ailffactora y gallwch ymddiried ynddo, ac offer (awtogwblhau, ailenwi diogel, neidio-i-ddiffiniad) sy’n gwybod beth yw pethau. Mae teipio dynamig yn prynu prototeipio cyflym, cod cryno, a seremoni isel sy’n gweddu i sgriptiau a gwaith archwiliadol. Po fwyaf, hiraf ei oes, a risg-uwch yw’r system, mwyaf y mae’r ochr statig yn talu ar ei ganfed, oherwydd bod cost ailffactora cronfa god gyfan a chost gwall math adeg rhedeg ill dau’n tyfu gyda graddfa.

Byddwch yn fanwl gywir am ail echel, unionsyth: teipio cryf yn erbyn teipio gwan. Mae iaith wedi’i theipio’n gryf yn gwrthod trosi mathau anghydnaws yn dawel (mae adio rhif at linyn yn codi gwall); mae un wedi’i theipio’n wan yn trosi’n dawel, gan gynhyrchu synnau fel "3" + 4 yn rhoi rhywbeth na fwriadwyd gennych. Gallwch gael statig a gwan, neu ddynamig a chryf. Pan fyddwch yn gwerthuso iaith, gofynnwch y ddau gwestiwn ar wahân, oherwydd yn aml “cryf” yw’r hyn y mae pobl mewn gwirionedd eisiau pan ddywedant “wedi’i deipio.”

Pwyso ar gasgliad mathau i gadw mathau’n rhad

Gwrthwynebiad cyffredin i deipio statig yw sŵn ysgrifennu math ar bob llinell. Mae casgliad mathau yn dileu’r rhan fwyaf o’r gost honno: mae’r crynhoydd yn didynnu mathau o’r cyd-destun, felly byddwch yn nodi’r ffiniau (llofnodion swyddogaethau, rhyngwynebau cyhoeddus) ac yn gadael i’r tu mewn gael ei gasglu. Mae ieithoedd modern yn casglu’n ymosodol, gan roi i chi ddiogelwch gwirio statig gyda llawer o gryno-deb cod dynamig. Mabwysiadwch reol tŷ sy’n nodi’r rhannau y mae darllenydd yn dibynnu arnynt fel contract, y swyddogaethau a allforir a’r mathau cyhoeddus, ac sy’n gadael newidynnau lleol i gasgliad. Mae hyn yn cadw llofnodion yn onest ac yn hunan-ddogfennol tra’n arbed y tu mewn rhag annibendod, ac mae’n cysylltu’n ôl ag amcanion darllenadwyedd pennod 2.1.

Gwneud cyflyrau anghyfreithlon yn amhosibl eu cynrychioli

Y syniad mwyaf pwerus mewn dylunio mathau ymarferol yw llunio’ch mathau fel na ellir ysgrifennu cyflwr anghywir i lawr. Os yw archeb naill ai’n “ddrafft” heb daliad neu’n “wedi’i osod” gyda thaliad, peidiwch â’i fodelu fel un struct gyda meysydd y gellir eu gadael yn null lle gallai drafft gario taliad yn ddamweiniol a gallai archeb wedi’i gosod gario dim. Modelwch ef fel math swm (a elwir hefyd yn undeb wedi’i dagio, undeb gwahaniaethol, neu amrywiolyn): gwerth sy’n union un o set benodol o siapiau, pob un yn cario ei ddata ei hun. Nawr nid yw’r cyfuniadau annilys yn bodoli, a rhaid i’r cod sy’n trin y gwerth roi cyfrif am bob achos neu bydd y crynhoydd yn cwyno. Mae hyn yn troi “ni ddylai hyn ddigwydd byth” adeg rhedeg yn “ni all hyn ddigwydd” adeg crynhoi, sef holl bwynt yr ymarfer.

Yr un greddf sy’n gyrru sawl teclyn bob dydd. Defnyddiwch fath rhifedig yn lle llinyn hud ar gyfer set sefydlog o gyflyrau. Lapiwch werth dilysedig mewn math gwahanol (EmailAddress yn hytrach na llinyn moel) fel bod “mewnbwn heb ei ddilysu” a “e-bost dilysedig” yn fathau gwahanol y mae’r crynhoydd yn eu cadw ar wahân. Dyma fynegiant system-fathau o ddisgyblaeth dilysu ffiniau trin gwallau (pennod 2.20): dilyswch unwaith wrth yr ymyl, trosi i fath sy’n amgodio’r warant, a gadael i’r tu mewn ymddiried ynddo.

Cymryd null-adwyedd a generigau o ddifrif

Mae’r pwyntydd null, a alwodd ei ddyfeisiwr yn “gamgymeriad biliwn doler,” yn ffordd fwyaf cyffredin un y byddai system fathau statig arferol yn arfer dweud celwydd: gallai gwerth wedi’i deipio fel llinyn fod yn null yn gyfrinachol, a byddech yn darganfod hynny drwy chwalu. Mae systemau mathau modern yn trwsio hyn drwy wneud null-adwyedd yn benodol. Mae gwerth naill ai’n String na fydd byth yn null neu’n fath Option/Maybe/y gellir ei wneud yn null y mae’n rhaid i chi ei ddadlapio cyn ei ddefnyddio, a’r crynhoydd yn eich gorfodi i drin yr achos gwag. Os yw’ch iaith yn cynnig mathau na ellir eu gwneud yn null neu fath dewisol, defnyddiwch nhw ym mhobman a thriniwch null moel fel arogl drwg. Mae hyn yn dileu genws cyfan o chwalfa cynhyrchiad.

Mae generigau, a elwir hefyd yn amldduedd paramedrig, yn eich galluogi i ysgrifennu cod sy’n gweithio dros lawer o fathau heb ildio diogelwch mathau: mae List<T> yn rhestr o fath penodol T, wedi’i wirio adeg crynhoi, yn hytrach na rhestr o bethau heb eu teipio y byddwch yn eu bwrw ac yn gweddïo drostynt. Estynnwch am generigau i adeiladu cynwysyddion, swyddogaethau, a haniaethau y gellir eu hailddefnyddio sy’n aros wedi’u teipio’n gryf. Y paru rhwng mathau swm, mathau na ellir eu gwneud yn null, a generigau yw’r hyn sy’n galluogi system fathau fodern i fynegi rheolau parth go iawn yn hytrach na dim ond tagio cyntefigion.

Mabwysiadu mathau’n raddol mewn cod dynamig sy’n bodoli eisoes

Nid oes rhaid i chi ailysgrifennu cronfa god ddynamig i gael manteision teipio. Mae teipio graddol yn caniatáu i god wedi’i deipio a chod heb ei deipio gydfodoli, felly byddwch yn ychwanegu mathau’n gynyddrannol lle maent yn talu fwyaf. Mae llawer o ecosystemau bellach yn cefnogi hyn yn uniongyrchol: awgrymiadau math mewn Python a wirir gan wiriwr math ar wahân, uwchset wedi’i deipio sy’n crynhoi i iaith ddynamig, neu anodiadau math wedi’u haenu ar amser rhedeg sy’n bodoli eisoes. Dechreuwch wrth y ffiniau a’r modiwlau pwysicaf (y cod arian, y cod diogelwch, y model data), trowch y gwiriwr ymlaen mewn modd caniataol, a’i dynhau dros amser. Ychwanegwch reol bod yn rhaid i god newydd fod wedi’i deipio hyd yn oed wrth i’r hen god ddal i fyny. O fewn ychydig chwarteri gall cronfa god fawr heb ei theipio gyrraedd y pwynt lle mae’r rhan fwyaf o newidiadau wedi’u gwirio o ran math, a’r rhannau sydd bwysicaf yn cael eu gorchuddio gyntaf.

Rhedeg leinwyr, gwirwyr mathau, a dadansoddwyr dyfnach gyda’i gilydd

Un haen yw gwirio mathau; ychwanegwch y lleill. Mae teclyn leinio yn dal patrymau amheus y mae gwiriwr mathau’n eu hanwybyddu: aseiniad sydd bob amser yn wir, newidyn na ddefnyddir, cwymp-drwodd mewn switsh, adnodd na chaiff ei gau byth. Mae dadansoddwyr dyfnach yn rhesymu am ymddygiad y rhaglen. Mae dadansoddiad llif data yn olrhain sut mae gwerthoedd yn symud drwy’r cod i ateb cwestiynau fel “a yw’r newidyn hwn byth yn cael ei ddefnyddio cyn iddo gael ei aseinio” neu “a all y ffeil hon ollwng handlen ar lwybr gwall.” Mae llawer o’r offer hyn wedi’u hadeiladu ar ddehongli haniaethol, techneg sy’n rhedeg y rhaglen yn haniaethol dros setiau o werthoedd posibl (er enghraifft, “positif,” “sero,” neu “negatif” yn lle rhifau union) i brofi priodweddau dros bob gweithrediad ar unwaith, heb redeg yr un ohonynt.

Mae rhai dadansoddwyr yn eistedd wrth ochr offer diogelwch. Mae profi diogelwch cymwysiadau statig (SAST) yn sganio ffynhonnell am batrymau gwendid megis chwistrelliad, dadgyfresoli anniogel, neu ddata heintiedig yn cyrraedd sinc peryglus, ac mae’n rhannu’r peirianwaith llif data a ddisgrifiwyd yma; triniwch ef fel rhan o’r teulu hwn a’i gydgysylltu â diogelwch cymwysiadau (pennod 4.2). Yr argymhelliad ymarferol yw set haenog: leiniwr cyflym ar gyfer arddull a gwallau amlwg, gwiriwr mathau ar gyfer contractau, ac un neu ragor o ddadansoddwyr dyfnach ar gyfer y priodweddau sy’n bwysig i’ch parth. Ffurfweddwch nhw o ffeiliau a reolir gan fersiynau fel bod y rheolau’r un fath i bawb.

Trin rhybuddion fel gwallau a ratsio’r llinell sylfaen

Mae rhybudd nad yw’n methu’r adeiladwaith yn rhybudd a gaiff ei anwybyddu. Unwaith y bydd log yn llenwi â channoedd o rybuddion a oddefir, nid oes neb yn ei ddarllen, a’r un sy’n bwysig yn cuddio yn y sŵn. Mabwysiadwch bolisi trin-rhybuddion-fel-gwallau fel bod rhybudd newydd yn torri’r adeiladwaith ac yn cael ei drwsio yn yr eiliad rataf. Ar gronfa god etifeddol gyda miloedd o rybuddion presennol, ni allwch droi’r switsh hwnnw dros nos, felly defnyddiwch ratsiad: cofnodwch y cyfrif presennol fel llinell sylfaen, blociwch unrhyw newid sy’n ei gynyddu, a’i yrru i lawr dros amser. Ni all y llinell sylfaen ond gostwng. Mae hyn yn eich galluogi i droi rheol lem ymlaen heddiw heb lanhau enfawr ymlaen llaw, tra’n gwarantu na fydd y sefyllfa byth yn gwaethygu ac yn gwella’n gyson.

Weirio dadansoddiad i mewn i olygyddion a CI, gydag adborth cyflym

Mae dadansoddiad statig yn talu fwyaf pan fo’r adborth yn ddi-oed. Rhedwch yr un gwiriadau yn y golygydd, drwy’r Language Server Protocol neu rywbeth cyfatebol, fel bod datblygwr yn gweld y gwall wrth deipio, cyn iddo hyd yn oed gadw. Yna rhedwch yr un set union o reolau mewn integreiddio parhaus (CI) fel na chaiff dim ei uno heb basio, gan glymu hyn i biblinell pennod 8.1. Rhaid i’r ddau gytuno: os yw’r golygydd yn oddefgar a CI yn llym, neu’r gwrthwyneb, mae pobl yn colli ymddiriedaeth yn y ddau. Cadwch y dadansoddiad yn ddigon cyflym i redeg ar bob newid, storiwch ganlyniadau, a dadansoddwch yn unig yr hyn a newidiodd lle gallwch, fel bod y gwiriwr yn gymorth yn hytrach na threth. Pan fydd y golygydd a’r biblinell yn gorfodi’r un rheolau yr un ffordd, mae’r safon yn peidio â bod yn ddogfen y mae pobl yn ei hanghofio ac yn dod yn briodwedd o’r amgylchedd.

Cadw gwiriad ffurfiol ar gyfer y cod sy’n ei haeddu

Ar ben pellaf y sbectrwm mae gwiriad ffurfiol: profi’n fathemategol fod rhaglen yn bodloni manyleb union, nid dim ond ei bod yn pasio profion. Mae technegau’n amrywio o wirio modelau (archwilio holl gyflyrau system yn helaeth) i brofi damcaniaethau a mathau dibynnol (mathau sy’n ddigon mynegiannol i amgodio manylebau llawn). Dyma’r warant ddyfnaf sydd ar gael a’r ddrutaf i’w chynhyrchu, felly mae’n ennill ei lle dim ond lle mae diffyg yn drychinebus neu lle mae ardystiad yn ei fynnu: llyfrgelloedd cryptograffig, cod rheoli hedfan, hypervisor, protocol critigol. I’r rhan fwyaf o feddalwedd, y buddsoddiad cywir yw mathau cryf ynghyd â dadansoddwyr da, sy’n dal y rhan fwyaf o’r budd am ffracsiwn o’r gost. Byddwch yn ymwybodol bod dulliau ffurfiol (a gyflwynwyd ym mhennod 2.12) yn bodoli a lle mae’r llinell, fel eich bod yn estyn amdanynt yn fwriadol ar gyfer y cydran anghyffredin sydd eu hangen.

Cadw diffygiad yn onest

Nid oes yr un dadansoddwr yn berffaith, a’r ddisgyblaeth sy’n gwahanu teclyn a ymddiriedir ynddo oddi wrth un a anwybyddir yw sut y byddwch yn trin ei gamgymeriadau. Mae pob teclyn difrifol yn caniatáu i chi ddiffygio canfyddiad. Mynnwch fod pob diffygiad yn gul (un llinell neu un canfyddiad, byth ffeil neu reol gyfan), yn cario rheswm mewn sylw, ac yn weladwy mewn adolygiad fel unrhyw god arall. Analluogi cyffredinol ar frig ffeil yw sut mae gorchudd yn pydru’n dawel. Archwiliwch ddiffygiadau’n gyfnodol a thrinwch bentwr cynyddol ohonynt fel arwydd bod rheol wedi’i chalibro’n wael neu fod gan y cod broblem go iawn y mae rhywun yn ei chuddio. Mae diffygiad onest yn cadw’r teclyn yn hygred; mae diffygiad tawel, ysgubol yn ei droi’n theatr.

Cymhareb: manteision ac anfanteision

Dull	Manteision	Anfanteision
Teipio statig	Contractau a wirir gan beiriant; ailffactora diogel; offer cyfoethog	Mwy o seremoni ymlaen llaw; prototeipio cynnar arafach
Teipio dynamig	Cyflym i’w ysgrifennu; hyblyg; seremoni isel	Mae gwallau math yn ymddangos adeg rhedeg; ailffactora’n risglyd
Casgliad mathau	Diogelwch gyda chryno-deb; llai o sŵn anodi	Gall mathau a gasglwyd guddio bwriad os gorddefnyddir
Teipio graddol	Mabwysiadu cynyddrannol; gorchuddio cod critigol yn gyntaf	Mae ymylon heb eu teipio’n dal i ollwng; gwarantau rhannol
Leinwyr a dadansoddiad llif data	Dal gwallau nad yw mathau’n eu dal; rhad i’w rhedeg	Positifau ffug; sŵn os na ffurfweddir
Rhybuddion-fel-gwallau gyda ratsiad	Rhwystrir problemau newydd; ni all y llinell sylfaen ond gwella	Gall deimlo’n rwystrol; mae angen polisi diffygio
Gwiriad ffurfiol	Y warant gryfaf; yn profi priodweddau ar gyfer pob mewnbwn	Drud, arbenigol; anaml ei gyfiawnhau

Y tyndra sy’n dychwelyd byth a hefyd yw gwarantau yn erbyn ffrithiant. Mae pob gris tuag at deipio llymach a dadansoddiad dyfnach yn prynu i chi ddosbarth o wallau sy’n dod yn amhosibl, ac mae pob gris yn ychwanegu seremoni, amser rhedeg teclyn, a’r positif ffug achlysurol sy’n costio munudau i ddatblygwr. Datryswch hyn yn ôl y risg a’r hyd oes. Mae sgript un-tro neu sbeic am yr ochr ysgafn, gyflym, ddynamig. Mae llyfr cyfrifon taliadau, gwiriad caniatâd, neu system y bydd llywodraeth yn ei rhedeg am bymtheg mlynedd am fathau cryf, dadansoddwyr haenog, rhybuddion-fel-gwallau, ac, ar gyfer ei chraidd mwyaf peryglus, o bosibl prawf ffurfiol. Paru’r trylwyredd â chost bod yn anghywir, a gadewch i gasgliad a mabwysiadu graddol gadw’r ffrithiant yn fforddiadwy.

Cwestiynau i’w trafod gyda’ch tîm

Ble yn ein cronfa god y byddai system fathau wedi atal ein sawl digwyddiad cynhyrchiad diwethaf, ac a ydym yn gwybod? Mae’r rhan fwyaf o dimau’n dadlau am deipio yn yr haniaethol tra bo’r dystiolaeth yn eu hanes digwyddiadau eu hunain. Tynnwch y deg neu ugain diffyg cynhyrchiad diwethaf a’u didoli: faint oedd yn null lle disgwylid gwerth, siâp anghywir wedi’i basio ar draws ffin, achos heb ei drin, gwerth “stringly-typed” a lithrodd? Dyna’n union y diffygion y mae gwiriwr mathau a leiniwr yn eu dal am ddim. Os yw cyfran fawr o’ch digwyddiadau yn y bwced hwnnw, mae gennych achos pendant, wedi’i ddirwyo mewn arian, dros deipio cryfach yn y modiwlau lle digwyddasant. Os prin fod unrhyw un, mae’ch gwallau’n byw mewn mannau eraill (rhesymeg, cydredoliaeth, gofynion) ac efallai nad teipio trymach yw’ch symudiad mwyaf gwerthfawr. Y naill ffordd neu’r llall, rydych yn disodli barn â data.
Pe baem yn mabwysiadu teipio graddol, ble byddem yn dechrau, a beth fyddai “digon o’i wneud” yn ei olygu? Rhaglen yw troi gwiriwr ymlaen ar draws cronfa god ddynamig fawr, nid fflip o switsh, a’r dilyniannu sy’n penderfynu a yw’n llwyddo neu’n stolio. Trafodwch pa fodiwlau sy’n cario’r risg fwyaf (arian, dilysiad, y model data craidd) ac felly’n haeddu mathau’n gyntaf, yn erbyn pa rai sy’n ddigon sefydlog a risg-isel i’w gadael heb eu teipio am y tro. Cytunwch ar reol ar gyfer cod newydd (wedi’i deipio o’r dydd cyntaf) fel bod yr wyneb heb ei deipio’n peidio â thyfu tra byddwch yn cnoi drwy’r ôl-groniad. Diffiniwch darged: efallai pob llofnod swyddogaeth gyhoeddus wedi’i deipio, pob ffin wedi’i dilysu i fath, y gwiriwr yn rhedeg mewn modd llym ar y pecynnau critigol. Heb linell derfyn ddiffiniedig, mae teipio graddol yn dod yn barhaus ac wedi’i orchuddio’n rhannol, sef y gwaethaf o’r ddau fyd.
Beth yw ein polisi pan fo dadansoddwr statig yn anghywir, ac a yw hynny’n cadw’r teclyn yn hygred? Mae pob dadansoddwr yn cynhyrchu positifau ffug, a sut y byddwch yn eu trin sy’n penderfynu a yw’r teclyn yn aros yn ddefnyddiol neu’n cael ei analluogi mewn rhwystredigaeth. Trafodwch achosion penodol: pan fo canfyddiad yn bositif ffug go iawn, a yw’r diffygiad yn gul, wedi’i nodi â sylw sy’n rhoi rheswm, ac yn weladwy mewn adolygiad, neu a yw rhywun yn analluogi’r rheol gyfan ar gyfer y ystorfa gyfan? Edrychwch ar eich diffygiadau presennol: sawl un sydd, a ydynt yn cario cyfiawnhad, a phryd yr archwiliodd unrhyw un nhw ddiwethaf? Mae pentwr o ddiffygiadau eang, heb eu hesbonio yn golygu bod eich gorchudd yn dawel wag. Y nod yw disgyblaeth a rennir, a orfodir, sy’n cadw’r dadansoddwr yn hygred, fel bod ymddiriedaeth yn ei ganfyddiadau a gweithredu arnynt yn hytrach na’u tawelu’n reddfol.
Ar ba ieithoedd a dadansoddwyr ydym yn safoni, a sut ydym yn cadw un set o reolau wrth i’n stac ymrannu ar draws timau? Pan fo cannoedd o beirianwyr yn gweithio mewn sawl iaith, mae pob tîm yn crwydro at ei wiriwr ei hun, ei reolau leinio ei hun, a’i osodiad llymder ei hun yn dinistrio’r warant yn dawel, oherwydd bod contract a orfodir mewn un ystorfa yn ddim ond awgrym yn y nesaf. Mae’r tyniad cystadleuol yn real: mae safoni canolog yn rhoi peirianwyr cludadwy a thystiolaeth archwilio unffurf i chi, ond gall set o reolau a osodir o’r canol ymladd yn erbyn idiomau iaith neu arafu tîm a chanddo resymau da dros ei ffurfweddiad ei hun. Dewch ag rhestr o’r ieithoedd sydd mewn cynhyrchiad, y dadansoddwyr a’r fersiynau y mae pob tîm yn eu rhedeg, a chymhariaeth o’u setiau rheolau fel bod y crwydro’n weladwy yn hytrach na’i gymryd yn ganiataol. Mewn lleoliad menter neu lywodraeth, cysylltwch yr ateb â chaffael ac archwiliad: un ffurfweddiad a reolir gan fersiynau y mae pob ystorfa yn ei etifeddu yw’r hyn sy’n galluogi archwiliwr i gadarnhau bod yr un gwiriadau wedi rhedeg ym mhobman, a dyna’r hyn sy’n atal cyflenwr rhag anfon cod o dan reolau gwannach na’r rhai y mae’n rhaid i’ch staff eich hun eu bodloni.
Pa mor gyflym yw ein dadansoddiad, ac ar ba bwynt mae pobl yn dechrau mynd o’i gwmpas? Gwiriwr yw gwarant yn unig os yw’n rhedeg ar bob newid, a’r eiliad y mae’n gwneud y ddolen olygu-adeiladu’n boenus, mae peirianwyr yn dysgu ei sgipio, ei analluogi’n lleol, neu uno gyda hi’n goch gan addo trwsio’n hwyrach. Y tyndra yw dyfnder yn erbyn cyflymder: mae pas llif data neu ddiogelwch dyfnach yn dal gwallau y mae leiniwr cyflym yn eu colli, ond os yw’r gyfres lawn yn cymryd ugain munud mae pobl yn stopio aros amdani, ac nid yw gwiriad nad yw neb yn aros amdano’n amddiffyn dim. Dewch â’r rhifau go iawn i’r drafodaeth: oedi adborth y golygydd, amser wal-cloc CI ar gyfer y cam dadansoddi, cyfraddau taro’r storfa, pa mor aml y uneir adeiladweithiau gyda gwiriadau wedi’u sgipio neu eu diystyru, a faint o’r rhediad sy’n gynyddrannol yn hytrach na llawn. I sefydliad mawr neu gyhoeddus, ychwanegwch y bil cyfrifiadura a chost trwygyrch, oherwydd ar raddfa fflyd mae cam dadansoddi gorfodol araf yn linell gyllideb ac yn giw sy’n oedi pob rhyddhad, a’r trwsiad gonest fel arfer yw dadansoddiad cynyddrannol a storio yn hytrach na llacio’r rheolau’n dawel.
Pa dystiolaeth a wirir gan beiriant y gallwn ei chynhyrchu i archwiliwr mewn gwirionedd, a pha rai o’n hanfodion critigol y mae’n eu gorchuddio? Mewn systemau rheoledig a risg-uchel, pwynt teipio a dadansoddi statig yw prawf y gellir ei ddangos bod dosbarthiadau cyfan o ddiffyg yn amhosibl trwy adeiladwaith, y tu hwnt i’r gwallau bob dydd y mae’n eu hatal, ac mae’r hawliad hwnnw’n ddiwerth os na allwch ddangos pa anfonion a orfodir a lle. Y gymhareb yw cwmpas yn erbyn cost: mae profi mwy (dim byd yn null ym mhobman, mathau swm ar gyfer pob cyflwr cyfreithlon, gwiriad ffurfiol o’r cyfrifiad craidd) yn prynu tystiolaeth gryfach, ac eto mae pob cam i fyny mewn trylwyredd yn costio ymdrech anodi, amser arbenigwr, a chymhlethdod adeiladu nad oes ei angen efallai ar god risg-isel. Dewch â map o’ch modiwlau diogelwch-critigol i’r gwarantau y mae pob un yn eu cario ar hyn o bryd, y rhestr o ddiffygiadau agored gyda’u cyfiawnhad, ac unrhyw fylchau lle mae rheol critigol yn cael ei gorfodi gan gonfensiwn yn hytrach na’r crynhoydd. I fenter reoledig neu lywodraeth, fframiwch hyn fel tystiolaeth ardystio: dylai archwiliwr allu olrhain priodwedd ofynnol i fath neu brawf a wirir gan beiriant a gweld y log diffygio sy’n dogfennu pob eithriad, fel bod cydymffurfiaeth yn gorffwys ar arteffactau y mae’r gadwyn offer yn eu cynhyrchu yn hytrach nag adolygiad â llaw ar ôl y ffaith.

Lens sector

Cwmni newydd. Cyflymder sy’n ennill, felly estynnwch am y diogelwch rhataf nad yw’n eich arafu: iaith wedi’i theipio’n gryf neu wiriwr mathau mewn modd caniataol, ynghyd â leiniwr cyflym yn y golygydd, a theipiwch eich cod arian a dilysiad yn gyntaf. Sgipiwch wiriad ffurfiol a chyfresi llif data dyfn yn llwyr; maent yn costio amser nad oes gennych. Yr elw a ddymunwch yn gynnar yw ailffactora y gallwch ymddiried ynddo ar ddeng mil o linellau, felly trowch y gwiriwr ymlaen cyn i’r gronfa god fod yn rhy fawr i’w dofi.

Busnes bach. Heb arbenigwr dadansoddi statig ar y staff, ffafriwch iaith a chadwyn offer lle mae rhagosodiadau da wedi’u hadeiladu i mewn yn hytrach na chyfres y mae’n rhaid i chi ei thiwnio a gwarchod drosti. Prynwch y dadansoddiad wedi’i fewnadeiladu yn eich IDE a’ch CI wedi’i letya yn lle sefydlu’ch platfform eich hun, a chadwch y set reolau’n agos at safon y gymuned fel bod contractwr neu newydd-ddyfodiad yn ei hadnabod. Triniwch rybuddion-fel-gwallau a chraidd bach wedi’i deipio fel y symudiadau â’r trosoledd mwyaf y gall eich cyllideb gyfyngedig eu gwneud.

Menter. Llywodraethu ar draws llawer o dimau yw’r gwaith: un ffurfweddiad a reolir gan fersiynau y mae pob ystorfa’n ei etifeddu, rheolau union yr un fath yn y golygydd a’r biblinell, a llinell sylfaen wedi’i ratsio fel na all gorchudd unrhyw dîm ostwng yn dawel. Safonwch y dadansoddwyr, olrheiniwch orchudd mathau a chyfrifon diffygio fel metrigau portffolio, ac archwiliwch ddiffygiadau ar gadence sefydlog fel bod gwarantau a wirir gan beiriant yn aros yn ddigon unffurf i archwiliwr ddibynnu arnynt. Cyllidebwch y tîm platfform sy’n berchen ar y ffurfweddiad a rennir, oherwydd nid yw cysondeb ar draws miloedd o beirianwyr yn ei gynnal ei hun.

Llywodraeth. Caffael, tryloywder, a hydoedd oes hir sy’n dominyddu. Mynnwch mewn contractau bod cyflenwyr yn bodloni’r un rheolau dadansoddi â’ch staff eich hun a throsglwyddo’r ffurfweddiad a’r logiau diffygio fel danfoniadau, fel bod y warant yn goroesi newid gwerthwr. Ffafriwch dystiolaeth a wirir gan beiriant dros sicrwydd â llaw ar gyfer cymhwysedd a rhesymeg taliadau, cadwch wiriad ffurfiol ar gyfer y cyfrifiadau y byddai eu methiant yn gwadu budd-dal yn anghyfreithlon, a chadwch bob diffygiad wedi’i ddogfennu ar gyfer archwiliad dros y degawd neu ragor y bydd y system yn rhedeg.

Enghreifftiau

Cwmni newydd. Mae cwmni newydd chwe pherson yn adeiladu ei gynnyrch mewn iaith ddynamig er mwyn cyflymder, sy’n eu gwasanaethu’n dda nes bod ailffactora ar ddeng mil o linellau’n dechrau achosi gwallau math adeg rhedeg nad ydynt ond yn eu darganfod mewn cynhyrchiad. Maent yn mabwysiadu teipio graddol: maent yn troi gwiriwr mathau ymlaen mewn modd caniataol, yn ychwanegu awgrymiadau math at eu model parth craidd a chod taliadau’n gyntaf, ac yn gosod rheol bod pob modiwl newydd wedi’i deipio’n llawn. Maent yn weirio’r gwiriwr a leiniwr i mewn i’w golygydd a CI gyda’r un ffurfweddiad, ac yn trin rhybuddion newydd fel gwallau wrth ratsio’r rhai presennol i lawr. O fewn dau chwarter mae’r chwalfeydd o siapiau anghyson yn diflannu, mae ailffactora’n peidio â bod yn frawychus, ac mae awtogwblhau newydd-ddyfodiad mewn gwirionedd yn gwybod beth mae pob swyddogaeth yn ei ddychwelyd. Costiodd y buddsoddiad ychydig wythnosau-peiriannydd a chafodd wared ar ffynhonnell ailadroddus o wallau a welir gan gwsmeriaid.

Menter. Mae banc byd-eang yn safoni dadansoddiad statig ar draws miloedd o beirianwyr. Mae pob ystorfa’n etifeddu ffurfweddiad a rennir: gwiriwr mathau mewn modd llym, leiniwr, dadansoddwr llif data, a sganiwr SAST ar gyfer patrymau diogelwch, i gyd yn rhedeg yn y golygydd a’u gorfodi yn y biblinell fel na chaiff dim ei uno heb basio. Mae mathau parth yn gwneud cyflyrau anghyfreithlon yn amhosibl eu cynrychioli yn y cod sy’n symud arian: mae trafodiad wedi’i bostio ac un ar y gweill yn fathau gwahanol, mae arian cyfred wedi’i deipio fel na allwch adio doleri at ewros, ac mae mewnbynnau dilysedig yn fathau gwahanol i rai crai. Mae rhybuddion yn wallau, ac ni all llinell sylfaen pob tîm ond gostwng. Mae diffygiadau’n gofyn am gyfiawnhad ac fe’u harchwilir bob chwarter. Am fod y gwarantau’n cael eu gwirio gan beiriant ac yn unffurf, gall archwilwyr weld bod dosbarthiadau cyfan o ddiffyg yn amhosibl trwy adeiladwaith, ac mae peirianwyr yn symud yn hyderus ar draws gwasanaethau anghyfarwydd.

Llywodraeth. Mae awdurdod treth cenedlaethol yn moderneiddio system cyfrifo budd-daliadau y mae’n rhaid iddi fod yn gywir ac yn esboniadwy am flynyddoedd. Ysgrifennir y rhesymeg cymhwysedd craidd mewn iaith wedi’i theipio’n gryf lle mae’r model parth yn amgodio’r rheolau: mae statws ymgeisydd yn fath swm sy’n gorchuddio pob achos cyfreithlon, mae symiau ariannol yn fath pwrpasol na ellir ei gymysgu â chyfrifon, ac nid oes unrhyw werth a allai fod ar goll yn cael ei adael yn null moel. Mae dadansoddiad statig yn rhedeg yn CI fel giât, a gwirir y modiwl cyfrifo mwyaf diogelwch-critigol yn ychwanegol â dulliau ffurfiol i brofi bod anfonion allweddol yn dal ar gyfer pob mewnbwn, gan fodloni gofynion ardystio. Dogfennir pob diffygiad ar gyfer archwiliad. Pan fydd yr awduron gwreiddiol yn symud ymlaen, mae eu holynwyr yn etifeddu cod y mae’r crynhoydd yn gorfodi ei gontractau, fel y gallant ei newid yn ddiogel ddegawd yn ddiweddarach.

Achos busnes: cymhellion, ROI, a TCO

Newid yn y man y talwch am ddiffygion yw’r elw ar deipio a dadansoddiad statig. Mae diffyg a ddelir gan wiriwr mathau yn y golygydd yn costio eiliadau; mae’r un diffyg a ddelir mewn cynhyrchiad yn costio digwyddiad, ymchwiliad, posibl niwed i gwsmeriaid a chanfyddiad rheoleiddiol. Mae astudiaethau o economeg diffygion yn dangos yn gyson gost yn codi o urddiad maint ar bob cam y mae bwg yn goroesi, o awduro i adolygiad i brofi i gynhyrchiad. Mae dadansoddiad statig yn symud dosbarth cyfan o ddiffygion i’r cam rhataf, ar bob adeiladwaith, heb lafur fesul diffyg. Dyna gost sefydlu sefydlog, ar y cyfan un-tro, sy’n prynu ffrwd ddiddiwedd o ddiffygion a atalir, sy’n agos at y trosoledd gorau mewn peirianneg.

Mae’r costau’n real ond yn fach ac wedi’u llwytho ymlaen. Byddwch yn dewis ac yn ffurfweddu’r offer, yn talu peth seremoni mewn anodiadau (a esmwythir gan gasgliad), yn treulio amser peiriannydd yn mabwysiadu teipio graddol mewn cod etifeddol, ac yn derbyn positifau ffug achlysurol. Yn erbyn hynny, pwyswch gost berchnogaeth gyfan y dewis arall: pob bwg siâp-math sy’n cyrraedd cynhyrchiad, pob ailffactora risglyd a osgoir am nad oes dim yn gwarantu cywirdeb, pob sefydlu araf am nad yw’r cod yn dogfennu ei gontractau ei hun, ac mewn lleoliadau rheoledig pob archwiliad y mae’n rhaid ei fodloni drwy adolygiad â llaw yn hytrach na thystiolaeth a wirir gan beiriant. I wneud yr achos i arweinyddiaeth, cysylltwch ef â’r metrigau y maent eisoes yn eu tracio: cyfradd methiant newid, cyfradd dianc diffygion, amser cymedrig i adfer, a chyfran y digwyddiadau y gellir eu priodoli i wallau math a null y gellid eu hatal. Y graff sy’n argyhoeddi pobl yw eich hanes digwyddiadau eich hun wedi’i ddidoli yn ôl a fyddai gwiriwr wedi’i ddal.

Gwrth-batrymau a pheryglon

Y ddihangfa fel arferiad: bwrw i any, dynamic, neu’r cyfwerth heb ei deipio i dawelu’r gwiriwr, sy’n dileu’r warant yn union lle’r oedd ei fwyaf angen.
Popeth wedi’i deipio fel llinynnau: pasio llinynnau moel a mapiau heb eu teipio ar draws ffiniau yn lle modelu cyflyrau fel mathau go iawn, fel na all y crynhoydd helpu.
Null yn ddiofyn: gadael gwerthoedd yn null-adwy pan fo’r iaith yn cynnig mathau na ellir eu gwneud yn null a mathau dewisol, gan gadw’r camgymeriad biliwn doler yn fyw.
Rhybuddion nad ydynt byth yn methu: miloedd o rybuddion a oddefir lle mae’r un sy’n bwysig yn anweledig, am nad oes dim byth yn torri’r adeiladwaith.
Y golygydd a CI yn anghytuno: goddefgar yn lleol a llym yn y biblinell, neu’r gwrthwyneb, fel bod datblygwyr yn drwgdybio’r ddau ac undebau’n synnu pobl.
Diffygio cyffredinol: analluogi rheol neu ffeil gyfan yn lle un canfyddiad cyfiawnedig, gan wagio gorchudd yn dawel.
Theatr dadansoddi: rhedeg offer nad oes neb yn darllen na gweithredu ar eu canfyddiadau, fel bod yr adroddiadau’n cronni a’r gwerth yn sero.
Teipio popeth-neu-ddim byd: gwrthod dechrau am na allwch deipio popeth ar unwaith, gan wrthod yr enillion mawr o deipio’r cod critigol yn gyntaf.
Gwiriad ym mhobman: estyn am ddulliau ffurfiol ar god cyffredin, gan wario ymdrech arbenigwr prin lle byddai mathau cryf wedi bod yn ddigon.

Model aeddfedrwydd

Lefel 1, Cychwyn: Mae teipio a dadansoddi’n ad hoc ac fesul datblygwr. Nid oes gan god dynamig wiriwr, neu mae iaith statig yn rhedeg gyda rhybuddion yn cael eu hanwybyddu. Mae gwallau siâp-math (nullau, siapiau anghywir, achosion heb eu trin) yn cyrraedd cynhyrchiad yn rheolaidd, ac ofnir ailffactora am nad oes dim yn gwirio cywirdeb.
Lefel 2, Datblygu: Mae leiniwr, a lle bo’n berthnasol wiriwr mathau, yn rhedeg ar rai prosiectau, ond mae rheolau’n amrywio rhwng timau, nid yw rhybuddion yn methu’r adeiladwaith, ac mae dihangfeydd a diffygiadau eang yn gyffredin. Sylweddolir rhywfaint o fudd, ond mae gorchudd yn anghyson ac ymddiriedaeth yn yr offer yn glytiog.
Lefel 3, Safoni: Mae ffurfweddiad a rennir, a reolir gan fersiynau, yn gorfodi gwirio mathau a leinio yn y golygydd a CI gyda rheolau union yr un fath ar draws y sefydliad. Mae rhybuddion yn wallau gyda llinell sylfaen wedi’i ratsio, defnyddir null-adwyedd a mathau swm i wneud cyflyrau anghyfreithlon yn amhosibl eu cynrychioli wrth ffiniau, ac mae angen rheswm dogfenedig, y gellir ei adolygu, ar gyfer pob diffygiad.
Lefel 4, Rheoli: Mesurir a rheolir dadansoddiad yn erbyn llinellau sylfaen. Olrheinir gorchudd mathau ar fodiwlau critigol, cyfrifon rhybudd, cyfraddau positif ffug, cyfrifon diffygio, a chyfran y digwyddiadau cynhyrchiad y byddai gwiriwr wedi’u dal, i gyd yn erbyn targedau penodol. Mae’r metrigau’n gatio newid: ni all gorchudd ar y cod arian a dilysiad ostwng, mae cyfradd positif ffug gynyddol yn sbarduno ail-galibro rheolau, ac mae dangosfyrddau’n dangos a yw’r gwarantau’n dal go iawn yn hytrach na dim ond wedi’u ffurfweddu.
Lefel 5, Cerddorfa: Gwellir dadansoddiad yn barhaus a’i integreiddio ar draws y sefydliad. Mae teipio graddol wedi cyrraedd y modiwlau critigol, mae dadansoddwyr llif data a diogelwch yn rhedeg yn rheolaidd, mae rheolau’n addasu wrth i ieithoedd a bygythiadau esblygu, a chymhwysir gwiriad ffurfiol yn fwriadol ar y ychydig gydrannau y byddai eu methiant yn drychinebus. Mae’r offer, y metrigau, a’r set reolau’n bwydo’n ôl i mewn i ddylunio, recriwtio, a chaffael, fel bod y sefydliad cyfan yn tyfu’n gyson yn ddiogelach i’w newid.

Syniadau ar gyfer trafodaeth

Pa rai o’ch gwallau cynhyrchiad diweddar y byddai gwiriwr mathau neu leiniwr wedi’u dal, a pha gyfran o’r cyfanswm y maent yn ei gynrychioli?
Ble yn eich model parth y gallai math swm neu fath lapio dilysedig droi “ni ddylai hyn ddigwydd byth” adeg rhedeg yn “ni all hyn ddigwydd” adeg crynhoi?
Pe baech yn troi rhybuddion yn wallau yfory, faint fyddai’n torri’r adeiladwaith, a pha linell sylfaen a ratsiad fyddai’n eich galluogi i fabwysiadu’r polisi heb groesgad glanhau?
A yw’ch golygydd a’ch piblinell yn rhedeg union yr un rheolau, a sut y byddai datblygwr yn darganfod pe baent wedi crwydro ar wahân?
Faint o ddiffygiadau sy’n byw yn eich cronfa god ar hyn o bryd, sawl un sy’n cario cyfiawnhad, a phryd yr archwiliwyd nhw ddiwethaf?
A oes unrhyw gydran yn eich system y mae ei methiant yn ddigon trychinebus i gyfiawnhau gwiriad ffurfiol, a sut y byddech chi’n gwybod?

Casgliadau allweddol

Mae teipio a dadansoddiad statig yn gwthio dosbarth cyfan o ddiffygion i’r eiliad rataf i’w trwsio: wrth i chi ysgrifennu’r cod, ar bob adeiladwaith, heb lafur fesul diffyg.
Ffafriwch warantau y mae’r peiriant yn eu gwirio dros gonfensiynau y mae’n rhaid i bobl eu cofio, ac amgodiwch fwriad mewn mathau fel na ellir cynrychioli cyflyrau anghyfreithlon o gwbl.
Nid oes angen popeth neu ddim byd: mae teipio graddol yn eich galluogi i orchuddio’r cod critigol (arian, dilysiad, y model data) yn gyntaf tra bo’r gweddill yn dal i fyny.
Triniwch rybuddion fel gwallau gyda llinell sylfaen wedi’i ratsio, rhedwch reolau union yr un fath yn y golygydd a CI, a chadwch ddiffygiad yn gul, yn gyfiawnedig, ac wedi’i archwilio.
Parwch drylwyredd â risg: mathau cryf ynghyd â dadansoddwyr haenog ar gyfer y rhan fwyaf o systemau, a chadwch wiriad ffurfiol ar gyfer y cydran anghyffredin y byddai ei methiant yn drychinebus.

Cyfeiriadau a darllen pellach

Benjamin C. Pierce, Types and Programming Languages
Simon Peyton Jones (gol.), The Implementation of Functional Programming Languages
Flemming Nielson, Hanne Riis Nielson, a Chris Hankin, Principles of Program Analysis
Patrick Cousot a 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 a Chonsortiwm MISRA, 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