Erthygl gyfieithu yw hon . Ond cyn hynny ceir rhagymadrodd byr. Sut mae zombies yn cael eu ffurfio? Mae pawb wedi cael eu hunain mewn sefyllfa lle maen nhw eisiau dod â ffrind neu gydweithiwr i fyny i'w lefel nhw, ond nid yw'n gweithio allan. Ar ben hynny, "nid yw'n gweithio allan" nid cymaint i chi, ond iddo ef: ar un ochr i'r raddfa mae cyflog arferol, tasgau, ac yn y blaen, ac ar y llall mae angen meddwl. Mae meddwl yn annymunol ac yn boenus. Mae'n rhoi'r gorau iddi yn gyflym ac yn parhau i ysgrifennu cod heb ddefnyddio ei ymennydd o gwbl. Rydych chi'n sylweddoli faint o ymdrech y mae'n ei gymryd i oresgyn rhwystr diymadferthedd a ddysgwyd, ac yn syml, nid ydych chi'n ei wneud. Dyma sut mae zombies yn cael eu ffurfio, sy'n ymddangos yn bosibl eu gwella, ond mae'n ymddangos na fydd unrhyw un yn gwneud hyn.
Pan welais i hynny (ie, yr un ffrind yna o'r gwerslyfrau) ac nid yw'n rhoi adroddiad, ond yn sesiwn cwestiwn-ac-ateb, roeddwn ychydig yn wyliadwrus. Rhag ofn, mae Leslie yn wyddonydd byd-enwog, yn awdur gweithiau arloesol mewn cyfrifiadura dosranedig, ac efallai y byddwch hefyd yn ei adnabod wrth y llythrennau La yn LaTeX - “Lamport TeX”. Yr ail ffactor brawychus yw ei ofyniad: rhaid i bawb sy'n dod (yn hollol rhad ac am ddim) wrando ar un neu ddau o'i adroddiadau ymlaen llaw, dod o hyd i o leiaf un cwestiwn amdanynt, a dim ond wedyn dod. Penderfynais weld beth oedd Lamport yn darlledu yno - ac mae'n wych! Dyma'r union beth hwnnw, bilsen gyswllt hud ar gyfer trin zombies. Rwy'n eich rhybuddio: gall y testun losgi'n ddifrifol y rhai sy'n caru methodolegau hynod ystwyth ac nad ydyn nhw'n hoffi profi'r hyn maen nhw wedi'i ysgrifennu.
Ar ôl yr habrokat, mae cyfieithu'r seminar yn dechrau mewn gwirionedd. Mwynhewch ddarllen!
Pa bynnag dasg a gymerwch, mae angen i chi fynd trwy dri cham bob amser:
- penderfynu pa nod rydych am ei gyflawni;
- penderfynu sut yn union y byddwch yn cyrraedd eich nod;
- cyrraedd eich nod.
Mae hyn hefyd yn berthnasol i raglennu. Pan fyddwn yn ysgrifennu cod, mae angen:
- penderfynu beth yn union ddylai'r rhaglen ei wneud;
- penderfynu yn union sut y dylai gyflawni ei dasg;
- ysgrifennu'r cod priodol.
Mae’r cam olaf, wrth gwrs, yn bwysig iawn, ond ni siaradaf amdano heddiw. Yn hytrach, byddwn yn trafod y ddau gyntaf. Mae pob rhaglennydd yn eu perfformio cyn dechrau gweithio. Nid ydych yn eistedd i lawr i ysgrifennu oni bai eich bod wedi penderfynu beth rydych yn ei ysgrifennu: porwr neu gronfa ddata. Rhaid cael syniad sicr o'r nod yn bresennol. Ac rydych chi'n bendant yn meddwl beth yn union y bydd y rhaglen yn ei wneud, a pheidiwch â'i ysgrifennu ar hap yn y gobaith y bydd y cod ei hun rywsut yn troi'n borwr.
Sut yn union mae'r rhag-feddwl hwn am god yn digwydd? Faint o ymdrech y dylem ei roi i mewn i hyn? Mae'r cyfan yn dibynnu ar ba mor gymhleth yw'r broblem yr ydym yn ei datrys. Gadewch i ni ddweud ein bod am ysgrifennu system ddosbarthedig sy'n goddef diffygion. Yn yr achos hwn, dylem ystyried pethau'n ofalus cyn eistedd i lawr i god. Beth os oes angen i ni gynyddu newidyn cyfanrif o 1 yn unig? Ar yr olwg gyntaf, mae popeth yma yn ddibwys ac nid oes angen meddwl, ond yna cofiwn y gall gorlif ddigwydd. Felly, hyd yn oed er mwyn deall a yw problem yn syml neu'n gymhleth, mae angen i chi feddwl yn gyntaf.
Os meddyliwch am atebion posibl i broblem ymlaen llaw, gallwch osgoi camgymeriadau. Ond mae hyn yn ei gwneud yn ofynnol i'ch meddwl fod yn glir. I gyflawni hyn, mae angen i chi ysgrifennu eich meddyliau. Rwyf wrth fy modd â dyfyniad Dick Guindon: “Pan fyddwch chi'n ysgrifennu, mae natur yn dangos i chi pa mor flêr yw eich meddwl.” Os nad ydych yn ysgrifennu, dim ond meddwl eich bod yn meddwl yr ydych. Ac mae angen i chi ysgrifennu eich meddyliau ar ffurf manylebau.
Mae manylebau yn gwasanaethu llawer o swyddogaethau, yn enwedig mewn prosiectau mawr. Ond ni fyddaf ond yn siarad am un ohonynt: maent yn ein helpu i feddwl yn glir. Mae meddwl yn glir yn bwysig iawn ac yn eithaf anodd, felly mae angen unrhyw help arnom ni yma. Ym mha iaith y dylem ysgrifennu manylebau? Yn gyffredinol, dyma'r cwestiwn cyntaf i raglenwyr bob amser: ym mha iaith y byddwn yn ysgrifennu? Nid oes un ateb cywir: mae'r problemau rydyn ni'n eu datrys yn rhy amrywiol. I rai pobl, mae TLA+ yn iaith fanyleb a ddatblygais. I eraill, mae'n fwy cyfleus defnyddio Tsieinëeg. Mae'r cyfan yn dibynnu ar y sefyllfa.
Y cwestiwn pwysicaf yw: sut allwn ni gyflawni meddwl cliriach? Ateb: Rhaid inni feddwl fel gwyddonwyr. Mae hon yn ffordd o feddwl sydd wedi gweithio'n dda dros y 500 mlynedd diwethaf. Mewn gwyddoniaeth rydym yn adeiladu modelau mathemategol o realiti. Efallai mai seryddiaeth oedd y wyddoniaeth gyntaf yn ystyr gaeth y gair. Yn y model mathemategol a ddefnyddir mewn seryddiaeth, mae cyrff nefol yn ymddangos fel pwyntiau â màs, safle a momentwm, er eu bod mewn gwirionedd yn wrthrychau hynod gymhleth gyda mynyddoedd a chefnforoedd, trai a llifoedd. Crëwyd y model hwn, fel unrhyw un arall, i ddatrys rhai problemau. Mae'n wych ar gyfer penderfynu ble i bwyntio telesgop os ydych am ddod o hyd i blaned. Ond os ydych chi am ragweld y tywydd ar y blaned hon, ni fydd y model hwn yn gweithio.
Mae mathemateg yn ein galluogi i bennu priodweddau model. Ac mae gwyddoniaeth yn dangos sut mae'r priodweddau hyn yn berthnasol i realiti. Gadewch i ni siarad am ein gwyddoniaeth, cyfrifiadureg. Y realiti rydyn ni'n gweithio gyda hi yw systemau cyfrifiadurol o lawer o wahanol fathau: proseswyr, consolau gemau, cyfrifiaduron sy'n rhedeg rhaglenni, ac ati. Soniaf am weithredu rhaglen ar gyfrifiadur, ond, ar y cyfan, mae’r holl gasgliadau hyn yn berthnasol i unrhyw system gyfrifiadurol. Yn ein gwyddoniaeth rydym yn defnyddio llawer o wahanol fodelau: y peiriant Turing, setiau o ddigwyddiadau a archebwyd yn rhannol, a llawer o rai eraill.
Beth yw'r rhaglen? Dyma unrhyw god y gellir ei ystyried ar ei ben ei hun. Gadewch i ni ddweud bod angen i ni ysgrifennu porwr. Rydyn ni'n perfformio tair tasg: dylunio cyflwyniad y defnyddiwr o'r rhaglen, yna ysgrifennu diagram lefel uchel y rhaglen, ac yn olaf ysgrifennu'r cod. Wrth i ni ysgrifennu'r cod, rydyn ni'n sylweddoli bod angen i ni ysgrifennu fformatydd testun. Yma eto mae angen i ni ddatrys tair problem: penderfynu pa destun y bydd yr offeryn hwn yn ei ddychwelyd; dewis algorithm ar gyfer fformatio; ysgrifennu cod. Mae gan y dasg hon ei his-dasg ei hun: mewnosod cysylltnodau mewn geiriau yn gywir. Rydym hefyd yn datrys yr is-dasg hon mewn tri cham - fel y gwelwn, maent yn cael eu hailadrodd ar sawl lefel.
Gadewch i ni edrych yn agosach ar y cam cyntaf: pa broblem y mae'r rhaglen yn ei datrys. Yma rydym gan amlaf yn modelu rhaglen fel swyddogaeth sy'n cymryd rhywfaint o fewnbwn ac yn rhoi rhywfaint o allbwn. Mewn mathemateg, disgrifir ffwythiant fel arfer fel set drefnus o barau. Er enghraifft, disgrifir y ffwythiant sgwario ar gyfer rhifau naturiol fel y set {<0,0>, <1,1>, <2,4>, <3,9>, …}. Parth diffiniad swyddogaeth o'r fath yw set elfennau cyntaf pob pâr, hynny yw, rhifau naturiol. I ddiffinio swyddogaeth, mae angen i ni nodi ei barth a'i fformiwla.
Ond nid yw swyddogaethau mewn mathemateg yr un peth â swyddogaethau mewn ieithoedd rhaglennu. Mae'r mathemateg yn llawer symlach. Gan nad oes gennyf amser ar gyfer enghreifftiau cymhleth, gadewch i ni ystyried un syml: swyddogaeth yn C neu ddull statig yn Java sy'n dychwelyd y rhannydd cyffredin mwyaf o ddau gyfanrif. Ym manyleb y dull hwn byddwn yn ysgrifennu: cyfrifo GCD(M,N) am ddadleuon M и Nlle GCD(M,N) - swyddogaeth y mae ei parth yn set o barau o gyfanrifau, a'r gwerth dychwelyd yw'r cyfanrif mwyaf sy'n cael ei rannu â M и N. Sut mae realiti yn cymharu â'r model hwn? Mae'r model yn gweithredu gyda chyfanrifau, ac yn C neu Java mae gennym ni 32-bit int. Mae'r model hwn yn ein galluogi i benderfynu a yw'r algorithm yn gywir GCD, ond ni fydd yn atal gwallau gorlif. Byddai hyn yn gofyn am fodel mwy cymhleth, nad oes amser ar ei gyfer.
Gadewch i ni siarad am gyfyngiadau'r swyddogaeth fel model. Nid yw rhai rhaglenni (fel systemau gweithredu) yn dychwelyd gwerth penodol ar gyfer rhai dadleuon yn unig; gallant redeg yn barhaus. Yn ogystal, mae'r swyddogaeth fel model yn addas iawn ar gyfer yr ail gam: cynllunio sut i ddatrys y broblem. Mae trefn gyflym a swigen yn cyfrifo'r un swyddogaeth, ond maent yn algorithmau hollol wahanol. Felly, i ddisgrifio'r ffordd i gyflawni nod y rhaglen, rwy'n defnyddio model arall, gadewch i ni ei alw'n fodel ymddygiadol safonol. Cynrychiolir y rhaglen ynddi fel set o bob ymddygiad dilys, pob un ohonynt, yn ei dro, yn ddilyniant o wladwriaethau, a chyflwr yw'r aseiniad o werthoedd i newidynnau.
Gawn ni weld sut olwg fyddai ar yr ail gam ar gyfer yr algorithm Ewclidaidd. Mae angen i ni gyfrifo GCD(M, N). Rydym yn ymgychwyn M как xAc N как y, yna tynnwch y lleiaf o'r newidynnau hyn dro ar ôl tro o'r mwyaf nes eu bod yn hafal. Er enghraifft, os M = 12Ac N = 18, gallwn ddisgrifio'r ymddygiad canlynol:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
Ac os M = 0 и N = 0? Mae sero yn rhanadwy â phob rhif, felly nid oes unrhyw rannydd mwyaf yn yr achos hwn. Yn y sefyllfa hon, mae angen inni fynd yn ôl at y cam cyntaf a gofyn: a oes gwir angen inni gyfrifo GCD ar gyfer rhifau nad ydynt yn gadarnhaol? Os nad yw hyn yn angenrheidiol, yna does ond angen i chi newid y fanyleb.
Mae gwyriad byr ar gynhyrchiant mewn trefn yma. Mae'n aml yn cael ei fesur yn ôl nifer y llinellau cod a ysgrifennwyd bob dydd. Ond mae eich gwaith yn llawer mwy defnyddiol os byddwch chi'n cael gwared ar nifer benodol o linellau, oherwydd bod gennych chi lai o le i chwilod. Ac mae'r ffordd hawsaf i gael gwared ar god yn y cam cyntaf. Mae'n bosibl nad oes angen yr holl glychau a chwibanau rydych chi'n ceisio eu gweithredu. Y ffordd gyflymaf o symleiddio rhaglen ac arbed amser yw peidio â gwneud pethau na ddylid eu gwneud. Mae gan yr ail gam y potensial arbed amser uchaf ond un. Os ydych chi'n mesur cynhyrchiant yn nhermau llinellau a ysgrifennwyd, yna bydd meddwl am sut i gwblhau tasg yn eich gwneud chi llai cynhyrchiol, oherwydd gallwch chi ddatrys yr un broblem gyda llai o god. Ni allaf roi union ystadegau yma, oherwydd nid oes gennyf unrhyw ffordd i gyfrif nifer y llinellau na ysgrifennais oherwydd yr amser a dreuliais ar y fanyleb, hynny yw, ar y camau cyntaf a'r ail. Ac ni allwn wneud arbrawf yma ychwaith, oherwydd mewn arbrawf nid oes gennym yr hawl i gwblhau'r cam cyntaf; penderfynir ar y dasg ymlaen llaw.
Mae'n hawdd anwybyddu llawer o anawsterau mewn manylebau anffurfiol. Nid oes dim byd anodd ynglŷn ag ysgrifennu manylebau llym ar gyfer swyddogaethau; ni fyddaf yn trafod hyn. Yn lle hynny, byddwn yn siarad am ysgrifennu manylebau cryf ar gyfer ymddygiadau safonol. Mae yna theorem sy'n nodi y gellir disgrifio unrhyw set o ymddygiadau gan ddefnyddio'r eiddo diogelwch (diogelwch) ac eiddo goroesiad (bywder). Mae diogelwch yn golygu na fydd unrhyw beth drwg yn digwydd, ni fydd y rhaglen yn rhoi'r ateb anghywir. Mae goroesiad yn golygu y bydd rhywbeth da yn digwydd yn hwyr neu’n hwyrach, h.y. yn hwyr neu’n hwyrach bydd y rhaglen yn rhoi’r ateb cywir. Fel rheol, mae diogelwch yn ddangosydd pwysicach; mae gwallau yn digwydd amlaf yma. Felly, er mwyn arbed amser, ni siaradaf am oroesi, er ei fod, wrth gwrs, hefyd yn bwysig.
Rydym yn sicrhau diogelwch trwy nodi set o gyflyrau cychwynnol posibl yn gyntaf. Ac yn ail, perthynas â'r holl wladwriaethau nesaf posibl ar gyfer pob gwladwriaeth. Gadewch i ni ymddwyn fel gwyddonwyr a diffinio gwladwriaethau yn fathemategol. Disgrifir y set o gyflyrau cychwynnol gan y fformiwla, er enghraifft, yn achos yr algorithm Ewclidaidd: (x = M) ∧ (y = N). Ar gyfer gwerthoedd penodol M и N dim ond un cyflwr cychwynnol sydd. Disgrifir y berthynas â'r cyflwr nesaf gan fformiwla lle mae newidynnau'r cyflwr nesaf yn cael eu hysgrifennu â chysefin, ac mae newidynnau'r cyflwr presennol yn cael eu hysgrifennu heb gysefin. Yn achos yr algorithm Ewclidaidd, byddwn yn delio â datgysylltiad dwy fformiwla, ac yn un ohonynt x yw'r gwerth mwyaf, ac yn yr ail - y:
Yn yr achos cyntaf, mae gwerth newydd y yn hafal i werth blaenorol y, ac rydyn ni'n cael gwerth newydd x trwy dynnu'r newidyn llai o'r un mwy. Yn yr ail achos, rydym yn gwneud y gwrthwyneb.
Gadewch i ni ddychwelyd at yr algorithm Ewclidaidd. Tybiwch eto hyny M = 12, N = 18. Mae hyn yn diffinio cyflwr cychwynnol sengl, (x = 12) ∧ (y = 18). Yna byddwn yn plygio'r gwerthoedd hyn i'r fformiwla uchod ac yn cael:
Dyma'r unig ateb posib: x' = 18 - 12 ∧ y' = 12, a chawn yr ymddygiad: [x = 12, y = 18]. Yn yr un modd, gallwn ddisgrifio pob cyflwr yn ein hymddygiad: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
Yn y cyflwr diwethaf [x = 6, y = 6] bydd dwy ran y mynegiant yn ffug, felly nid oes ganddo gyflwr nesaf. Felly, mae gennym fanyleb gyflawn o'r ail gam - fel y gwelwn, mae hon yn fathemateg eithaf cyffredin, fel un peirianwyr a gwyddonwyr, ac nid yn rhyfedd, fel mewn cyfrifiadureg.
Gellir cyfuno'r ddwy fformiwla hyn yn un fformiwla o resymeg amseryddol. Mae'n gain ac yn hawdd ei esbonio, ond nid oes amser ar ei gyfer nawr. Efallai y bydd angen rhesymeg amserol arnom yn unig ar gyfer eiddo bywiogrwydd; er diogelwch nid oes ei angen. Dydw i ddim yn hoffi rhesymeg amserol fel y cyfryw, nid yw'n fathemateg eithaf cyffredin, ond yn achos bywiogrwydd mae'n ddrwg angenrheidiol.
Mewn algorithm Ewclidaidd ar gyfer pob gwerth x и y mae gwerthoedd unigryw x' и y', sy'n gwneud y berthynas â'r cyflwr nesaf yn wir. Mewn geiriau eraill, mae'r algorithm Ewclidaidd yn benderfynol. Er mwyn modelu algorithm anbenderfynol, mae'n rhaid i'r cyflwr presennol fod â chyflyrau posibl lluosog yn y dyfodol, a rhaid i bob gwerth o'r newidyn unprimed fod â gwerthoedd lluosog y newidyn preimio fel bod y berthynas â'r cyflwr nesaf yn wir. Nid yw hyn yn anodd ei wneud, ond ni roddaf enghreifftiau yn awr.
I wneud teclyn gweithio, mae angen mathemateg ffurfiol arnoch chi. Sut i wneud manyleb yn ffurfiol? I wneud hyn bydd angen iaith ffurfiol, e.e. . Bydd manyleb yr algorithm Ewclidaidd yn yr iaith hon yn edrych fel hyn:
Mae'r symbol arwydd cyfartal gyda thriongl yn golygu bod y gwerth i'r chwith o'r arwydd yn cael ei bennu i fod yn hafal i'r gwerth i'r dde o'r arwydd. Yn ei hanfod, diffiniad yw manyleb, dau ddiffiniad yn ein hachos ni. At y fanyleb yn TLA+ mae angen i chi ychwanegu datganiadau a rhywfaint o gystrawen, fel yn y sleid uchod. Yn ASCII byddai'n edrych fel hyn:
Fel y gallwch weld, dim byd cymhleth. Gellir gwirio’r fanyleb ar TLA+, h.y., mae’n bosibl osgoi pob ymddygiad posibl mewn model bach. Yn ein hachos ni, bydd y model hwn yn werthoedd penodol M и N. Mae hwn yn ddull dilysu effeithiol a syml iawn sy'n gwbl awtomatig. Yn ogystal, mae'n bosibl ysgrifennu proflenni ffurfiol o wirionedd a'u gwirio'n fecanyddol, ond mae hyn yn cymryd llawer o amser, felly nid oes bron neb yn gwneud hyn.
Prif anfantais TLA+ yw mai mathemateg ydyw, ac mae rhaglenwyr a gwyddonwyr cyfrifiadurol yn ofni mathemateg. Ar yr olwg gyntaf mae hyn yn swnio fel jôc, ond, yn anffodus, rwy'n dweud hyn yn ddifrifol iawn. Roedd cydweithiwr i mi yn dweud wrthyf sut y ceisiodd egluro TLA+ i sawl datblygwr. Cyn gynted ag yr ymddangosodd y fformiwlâu ar y sgrin, daeth eu llygaid yn wydr ar unwaith. Felly os yw TLA+ yn frawychus, gallwch chi ei ddefnyddio , yn fath o iaith raglennu tegan. Gall mynegiant yn PlusCal fod yn unrhyw fynegiad TLA+, hynny yw, yn y bôn unrhyw fynegiad mathemategol. Yn ogystal, mae gan PlusCal gystrawen ar gyfer algorithmau anbenderfynol. Oherwydd y gall PlusCal ysgrifennu unrhyw fynegiant TLA+, mae'n llawer mwy mynegiannol nag unrhyw iaith raglennu go iawn. Nesaf, mae PlusCal wedi'i grynhoi i fanyleb TLA+ hawdd ei darllen. Nid yw hyn yn golygu, wrth gwrs, y bydd y fanyleb PlusCal gymhleth yn troi'n un syml ar TLA+ - dim ond bod yr ohebiaeth rhyngddynt yn amlwg, ni fydd cymhlethdod ychwanegol yn ymddangos. Yn olaf, gellir gwirio'r fanyleb hon gan ddefnyddio offer TLA+. Yn gyffredinol, gall PlusCal helpu i oresgyn ffobia mathemateg; mae'n hawdd ei ddeall hyd yn oed i raglenwyr a gwyddonwyr cyfrifiadurol. Cyhoeddais algorithmau arno ers peth amser (tua 10 mlynedd) yn y gorffennol.
Efallai y bydd rhywun yn gwrthwynebu bod TLA+ a PlusCal yn fathemateg, a bod mathemateg yn gweithio gydag enghreifftiau cyfansoddiadol yn unig. Yn ymarferol, mae angen iaith go iawn gyda mathau, gweithdrefnau, gwrthrychau, ac ati. Mae hyn yn anghywir. Dyma beth mae Chris Newcomb, a oedd yn gweithio yn Amazon, yn ei ysgrifennu: “Rydym wedi defnyddio TLA+ ar ddeg prosiect mawr, ac ym mhob achos fe wnaeth ei ddefnydd wahaniaeth sylweddol i ddatblygiad oherwydd ein bod yn gallu dal bygiau peryglus cyn iddynt gyrraedd y cynhyrchiad, ac oherwydd ei fod wedi rhoi’r mewnwelediad a’r hyder yr oedd ei angen arnom i wneud yn ymosodol. optimeiddio perfformiad heb ddylanwadu ar wirionedd y rhaglen". Yn aml, gallwch chi glywed ein bod ni'n cael cod aneffeithlon wrth ddefnyddio dulliau ffurfiol - yn ymarferol, mae popeth yn union i'r gwrthwyneb. Yn ogystal, mae canfyddiad na all rheolwyr fod yn argyhoeddedig o'r angen am ddulliau ffurfiol, hyd yn oed os yw rhaglenwyr yn argyhoeddedig o'u defnyddioldeb. Ac mae Newcomb yn ysgrifennu: “Mae rheolwyr bellach yn gwthio ym mhob ffordd bosibl i ysgrifennu manylebau yn TLA+, ac yn neilltuo amser yn benodol ar gyfer hyn”. Felly pan fydd rheolwyr yn gweld bod TLA+ yn gweithio, maen nhw'n ei gofleidio. Ysgrifennodd Chris Newcomb hwn tua chwe mis yn ôl (Hydref 2014), ond nawr, hyd y gwn i, mae TLA+ yn cael ei ddefnyddio mewn 14 prosiect, nid 10. Mae enghraifft arall yn ymwneud â dyluniad yr XBox 360. Daeth intern i Charles Thacker a ysgrifennu manyleb ar gyfer y system cof. Diolch i'r fanyleb hon, canfuwyd nam na fyddai fel arall wedi'i ganfod ac a fyddai'n achosi i bob XBox 360 ddamwain ar ôl pedair awr o ddefnydd. Cadarnhaodd peirianwyr o IBM na fyddai eu profion wedi canfod y byg hwn.
Gallwch ddarllen mwy am TLA+ ar y Rhyngrwyd, ond nawr gadewch i ni siarad am fanylebau anffurfiol. Anaml y mae'n rhaid i ni ysgrifennu rhaglenni sy'n cyfrifo'r rhannydd lleiaf cyffredin ac yn y blaen. Yn llawer amlach rydyn ni'n ysgrifennu rhaglenni fel yr offeryn argraffydd bert a ysgrifennais ar gyfer TLA+. Ar ôl y prosesu symlaf, byddai'r cod TLA+ yn edrych fel hyn:
Ond yn yr enghraifft uchod, mae'n debyg bod y defnyddiwr eisiau i'r cysylltiad a'r arwyddion cyfartal gael eu halinio. Felly byddai'r fformatio cywir yn edrych yn debycach i hyn:
Gadewch i ni ystyried enghraifft arall:
Yma, i'r gwrthwyneb, roedd aliniad arwyddion cyfartal, adio a lluosi yn y ffynhonnell ar hap, felly mae'r prosesu symlaf yn ddigon eithaf. Yn gyffredinol, nid oes diffiniad mathemategol union o fformatio cywir, oherwydd mae "cywir" yn yr achos hwn yn golygu "yr hyn y mae'r defnyddiwr ei eisiau," ac ni ellir pennu hyn yn fathemategol.
Mae'n ymddangos, os nad oes gennym ddiffiniad o wirionedd, yna mae'r fanyleb yn ddiwerth. Ond nid yw hynny'n wir. Nid yw'r ffaith nad ydym yn gwybod beth ddylai rhaglen ei wneud yn golygu nad oes angen i ni feddwl sut y dylai weithio—i'r gwrthwyneb, dylem wario hyd yn oed mwy o ymdrech arni. Mae'r fanyleb yn arbennig o bwysig yma. Mae'n amhosibl pennu'r rhaglen optimaidd ar gyfer argraffu strwythuredig, ond nid yw hyn yn golygu na ddylem ymgymryd ag ef o gwbl, ac nid yw ysgrifennu cod fel ffrwd ymwybyddiaeth yn wir. Yn y diwedd, ysgrifennais fanyleb o chwe rheol gyda diffiniadau ar ffurf sylwadau mewn ffeil Java. Dyma enghraifft o un o'r rheolau: a left-comment token is LeftComment aligned with its covering token. Mae'r rheol hon wedi'i hysgrifennu mewn Saesneg mathemategol, gadewch i ni ddweud: LeftComment aligned, left-comment и covering token — termau gyda diffiniadau. Dyma sut mae mathemategwyr yn disgrifio mathemateg: maen nhw'n ysgrifennu diffiniadau o dermau ac, yn seiliedig arnyn nhw, yn creu rheolau. Mantais y fanyleb hon yw bod chwe rheol yn llawer haws i'w deall a'u dadfygio na 850 llinell o god. Rhaid imi ddweud nad oedd ysgrifennu'r rheolau hyn yn hawdd; cymerodd gryn dipyn o amser i'w dadfygio. Ysgrifennais god yn benodol at y diben hwn a ddywedodd wrthyf pa reol oedd yn cael ei defnyddio. Oherwydd i mi brofi'r chwe rheol hyn gydag ychydig o enghreifftiau, nid oedd yn rhaid i mi ddadfygio 850 llinell o god, ac roedd y bygiau'n eithaf hawdd dod o hyd iddynt. Mae gan Java offer gwych ar gyfer hyn. Pe bawn i newydd ysgrifennu'r cod, byddai wedi cymryd llawer mwy o amser i mi a byddai'r fformatio wedi bod o ansawdd gwaeth.
Pam na ellid defnyddio manyleb ffurfiol? Ar y naill law, nid yw gweithredu cywir yn rhy bwysig yma. Mae allbrint strwythuredig yn sicr o fod yn anfoddhaol i rai, felly nid oedd yn rhaid i mi ei gael i weithio'n gywir ym mhob sefyllfa anarferol. Yn bwysicach fyth yw'r ffaith nad oedd gennyf offer digonol. Mae'r gwiriwr model TLA+ yn ddiwerth yma, felly byddai'n rhaid i mi ysgrifennu'r enghreifftiau â llaw.
Mae gan y fanyleb a roddir nodweddion sy'n gyffredin i bob manyleb. Mae'n lefel uwch na chod. Gellir ei weithredu mewn unrhyw iaith. Nid oes unrhyw offer na dulliau ar gyfer ei ysgrifennu. Ni fydd unrhyw gwrs rhaglennu yn eich helpu i ysgrifennu'r fanyleb hon. Ac nid oes unrhyw offer a allai wneud y fanyleb hon yn ddiangen, oni bai wrth gwrs eich bod yn ysgrifennu iaith yn benodol ar gyfer ysgrifennu rhaglenni argraffu strwythuredig yn TLA+. Yn olaf, nid yw'r fanyleb hon yn dweud dim am sut yn union y byddwn yn ysgrifennu'r cod, mae'n nodi beth mae'r cod yn ei wneud. Rydym yn ysgrifennu manyleb i'n helpu i feddwl trwy'r broblem cyn i ni ddechrau meddwl am y cod.
Ond mae gan y fanyleb hon hefyd nodweddion sy'n ei gwahaniaethu oddi wrth fanylebau eraill. Mae 95% o fanylebau eraill yn llawer byrrach a symlach:
Ymhellach, mae'r fanyleb hon yn set o reolau. Mae hyn fel arfer yn arwydd o fanyleb wael. Mae deall canlyniadau set o reolau yn eithaf anodd, a dyna pam y bu'n rhaid i mi dreulio llawer o amser yn eu dadfygio. Fodd bynnag, yn yr achos hwn ni allwn ddod o hyd i ffordd well.
Mae'n werth dweud ychydig eiriau am raglenni sy'n rhedeg yn barhaus. Yn nodweddiadol maent yn gweithredu ochr yn ochr, megis systemau gweithredu neu systemau gwasgaredig. Ychydig iawn o bobl sy'n gallu eu deall yn eu meddyliau neu ar bapur, ac nid wyf yn un ohonynt, er fy mod unwaith yn gallu ei wneud. Felly, mae angen offer arnom a fydd yn gwirio ein gwaith - er enghraifft, TLA+ neu PlusCal.
Pam roedd angen i mi ysgrifennu manyleb os oeddwn eisoes yn gwybod beth ddylai'r cod ei wneud? Yn wir, dim ond roeddwn i'n meddwl fy mod yn ei wybod. Yn ogystal, gyda manyleb ar waith, nid oes angen i rywun o'r tu allan bellach edrych i mewn i'r cod i ddeall beth yn union y mae'n ei wneud. Mae gennyf reol: ni ddylai fod unrhyw reolau cyffredinol. Mae eithriad i'r rheol hon wrth gwrs, dyma'r unig reol gyffredinol rwy'n ei dilyn: dylai manyleb yr hyn y mae'r cod yn ei wneud ddweud wrth bobl bopeth sydd angen iddynt ei wybod wrth ddefnyddio'r cod hwnnw.
Felly beth yn union sydd angen i raglenwyr ei wybod am feddwl? I ddechrau, yr un peth ag ar gyfer pawb: os nad ydych chi'n ysgrifennu, yna dim ond i chi sy'n meddwl eich bod chi'n meddwl. Hefyd, mae angen i chi feddwl cyn codio, sy'n golygu bod angen i chi ysgrifennu cyn codio. Manyleb yw'r hyn rydyn ni'n ei ysgrifennu cyn i ni ddechrau codio. Mae angen manyleb ar gyfer unrhyw god y gall unrhyw un ei ddefnyddio neu ei newid. Ac fe all y “rhywun” hwn droi allan i fod yn awdur y cod fis ar ôl iddo gael ei ysgrifennu. Mae angen manyleb ar gyfer rhaglenni a systemau mawr, ar gyfer dosbarthiadau, ar gyfer dulliau, ac weithiau hyd yn oed ar gyfer adrannau cymhleth o un dull. Beth yn union ddylech chi ei ysgrifennu am y cod? Mae angen i chi ddisgrifio'r hyn y mae'n ei wneud, hynny yw, rhywbeth a all fod yn ddefnyddiol i unrhyw un sy'n defnyddio'r cod hwn. Weithiau gall fod angen nodi hefyd sut yn union y mae'r cod yn cyflawni ei nod. Pe baem yn mynd trwy'r dull hwn yn y cwrs algorithmau, yna rydym yn ei alw'n algorithm. Os yw'n rhywbeth mwy arbenigol a newydd, yna rydym yn ei alw'n ddyluniad lefel uchel. Nid oes gwahaniaeth ffurfiol yma: mae'r ddau yn fodelau haniaethol o'r rhaglen.
Sut yn union ddylech chi ysgrifennu manyleb cod? Y prif beth: dylai fod un lefel yn uwch na'r cod ei hun. Rhaid iddo ddisgrifio cyflyrau ac ymddygiadau. Dylai fod mor llym ag y mae'r dasg yn gofyn amdano. Os ydych chi'n ysgrifennu manyleb o sut i weithredu tasg, yna gellir ei hysgrifennu mewn ffuggod neu ddefnyddio PlusCal. Mae angen i chi ddysgu ysgrifennu manylebau gan ddefnyddio manylebau ffurfiol. Bydd hyn yn rhoi'r sgiliau angenrheidiol i chi a fydd hefyd yn helpu gyda rhai anffurfiol. Sut allwch chi ddysgu ysgrifennu manylebau ffurfiol? Pan ddysgon ni raglennu, fe wnaethon ni ysgrifennu rhaglenni ac yna eu dadfygio. Yr un peth yma: mae angen i chi ysgrifennu manyleb, ei wirio gyda gwiriwr model, a thrwsio'r gwallau. Efallai nad TLA+ yw’r iaith orau ar gyfer manyleb ffurfiol, ac mae’n debygol y byddai iaith arall yn fwy addas ar gyfer eich anghenion penodol. Y peth gwych am TLA+ yw ei fod yn gwneud gwaith gwych o addysgu meddwl mathemategol.
Sut i gysylltu manyleb a chod? Defnyddio sylwadau sy'n cysylltu cysyniadau mathemategol a'u gweithrediad. Os ydych yn gweithio gyda graffiau, yna ar lefel y rhaglen bydd gennych araeau o nodau ac araeau o ddolenni. Felly mae angen ichi ysgrifennu sut yn union y mae'r graff yn cael ei weithredu gan y strwythurau rhaglennu hyn.
Dylid nodi nad yw'r un o'r uchod yn berthnasol i'r broses o ysgrifennu cod ei hun. Pan fyddwch chi'n ysgrifennu cod, hynny yw, yn perfformio'r trydydd cam, mae angen i chi hefyd feddwl a meddwl trwy'r rhaglen. Os yw is-dasg yn troi allan i fod yn gymhleth neu ddim yn amlwg, mae angen i chi ysgrifennu manyleb ar ei gyfer. Ond dydw i ddim yn sôn am y cod ei hun yma. Gallwch ddefnyddio unrhyw iaith raglennu, unrhyw fethodoleg, nid yw hyn yn ymwneud â nhw. Hefyd, nid yw'r un o'r uchod yn dileu'r angen i brofi a dadfygio'ch cod. Hyd yn oed os yw'r model haniaethol wedi'i ysgrifennu'n gywir, efallai y bydd bygiau yn ei weithrediad.
Mae ysgrifennu manylebau yn gam ychwanegol yn y broses godio. Diolch iddo, gellir dal llawer o wallau gyda llai o ymdrech - gwyddom hyn o brofiad rhaglenwyr o Amazon. Gyda manylebau, mae ansawdd y rhaglenni'n dod yn uwch. Felly pam rydyn ni mor aml yn mynd hebddyn nhw? Achos mae ysgrifennu yn anodd. Ond mae ysgrifennu yn anodd, oherwydd ar gyfer hyn mae angen i chi feddwl, ac mae meddwl hefyd yn anodd. Mae bob amser yn haws esgus eich bod chi'n meddwl. Gellir llunio cyfatebiaeth yma gyda rhedeg - y lleiaf y byddwch chi'n rhedeg, yr arafaf y byddwch chi'n rhedeg. Mae angen i chi hyfforddi'ch cyhyrau ac ymarfer ysgrifennu. Mae'n cymryd ymarfer.
Gall y fanyleb fod yn anghywir. Efallai eich bod wedi gwneud camgymeriad yn rhywle, neu efallai bod y gofynion wedi newid, neu efallai y bydd angen gwella. Rhaid newid unrhyw god y mae unrhyw un yn ei ddefnyddio, felly yn hwyr neu'n hwyrach ni fydd y fanyleb yn cyd-fynd â'r rhaglen mwyach. Yn ddelfrydol, yn yr achos hwn, mae angen i chi ysgrifennu manyleb newydd ac ailysgrifennu'r cod yn llwyr. Gwyddom yn iawn nad oes neb yn gwneud hyn. Yn ymarferol, rydym yn clytio'r cod ac efallai'n diweddaru'r fanyleb. Os yw hyn yn sicr o ddigwydd yn hwyr neu'n hwyrach, yna pam ysgrifennu manylebau o gwbl? Yn gyntaf, ar gyfer y person a fydd yn golygu eich cod, bydd pob gair ychwanegol yn y fanyleb yn werth ei bwysau mewn aur, ac mae'n bosibl iawn mai chi yw'r person hwn. Rwy'n aml yn cicio fy hun am beidio â bod yn ddigon penodol pan fyddaf yn golygu fy nghod. Ac rwy'n ysgrifennu mwy o fanylebau na chod. Felly, pan fyddwch chi'n golygu'r cod, mae angen diweddaru'r fanyleb bob amser. Yn ail, gyda phob golygiad mae'r cod yn gwaethygu, mae'n dod yn fwy anodd ei ddarllen a'i gynnal. Mae hyn yn gynnydd mewn entropi. Ond os na ddechreuwch gyda manyleb, yna bydd pob llinell a ysgrifennwch yn olygiad, a bydd y cod yn swmpus ac yn anodd ei ddarllen o'r cychwyn cyntaf.
Fel y dywedwyd , ni enillwyd brwydr yn ol cynllun, ac ni enillwyd brwydr heb gynllun. Ac roedd yn gwybod rhywbeth am frwydrau. Mae yna farn bod ysgrifennu manylebau yn wastraff amser. Weithiau mae hyn yn wir, ac mae'r dasg mor syml fel nad oes pwrpas meddwl amdani. Ond dylech bob amser gofio, pan fyddwch chi'n cael eich cynghori i beidio ag ysgrifennu manylebau, mae'n golygu eich bod chi'n cael eich cynghori i beidio â meddwl. A dylech chi feddwl am hyn bob tro. Nid yw meddwl trwy dasg yn gwarantu na fyddwch yn gwneud camgymeriadau. Fel y gwyddom, ni dyfeisiodd neb ffon hud, ac mae rhaglennu yn dasg anodd. Ond os nad ydych chi'n meddwl trwy'r dasg, rydych chi'n sicr o wneud camgymeriadau.
Gallwch ddarllen mwy am TLA+ a PlusCal ar wefan arbennig, gallwch fynd yno o fy nhudalen gartref . Dyna i gyd i mi, diolch am eich sylw.
Cofiwch mai cyfieithiad yw hwn. Pan fyddwch yn ysgrifennu sylwadau, cofiwch na fydd yr awdur yn eu darllen. Os ydych chi wir eisiau sgwrsio â'r awdur, bydd yng nghynhadledd Hydra 2019, a gynhelir ar Orffennaf 11-12, 2019 yn St Petersburg. Gellir prynu tocynnau .
Ffynhonnell: hab.com