Nov yog ib tsab xov xwm txhais lus . Tab sis ua ntej ntawd muaj ib qho kev qhia luv luv. Yuav ua li cas zombies tsim? Txhua tus tau pom lawv tus kheej hauv qhov xwm txheej uas lawv xav coj tus phooj ywg lossis cov npoj yaig mus rau lawv qib, tab sis nws tsis ua haujlwm. Tsis tas li ntawd, "nws tsis ua haujlwm" tsis yog rau koj, tab sis rau nws: ntawm ib sab ntawm qhov ntsuas muaj cov nyiaj hli ib txwm, cov haujlwm, thiab lwm yam, thiab lwm yam yog qhov xav tau. Kev xav yog qhov tsis kaj siab thiab mob. Nws sai sai tso tseg thiab txuas ntxiv sau code yam tsis siv nws lub hlwb txhua. Koj paub tias nws yuav siv zog npaum li cas los kov yeej kev cuam tshuam ntawm kev kawm tsis muaj peev xwm, thiab koj tsuas ua tsis tau. Qhov no yog li cas zombies tau tsim, uas zoo li yuav kho tau, tab sis zoo li tsis muaj leej twg yuav ua qhov no.
Thaum kuv pom li ntawd (yog, tus phooj ywg tib yam los ntawm phau ntawv kawm) thiab tsis yog muab ib daim ntawv qhia, tab sis ib tug nug-thiab- teb kev sib tham, kuv tau ceev faj me ntsis. Tsuas yog nyob rau hauv rooj plaub, Leslie yog tus kws tshawb fawb thoob ntiaj teb, tus sau cov lus qhuab qhia hauv kev faib xam, thiab koj kuj yuav paub nws los ntawm cov ntawv La hauv LaTeX - "Lamport TeX". Qhov kev ceeb toom thib ob yog nws qhov yuav tsum tau ua: txhua tus neeg tuaj yeem yuav tsum tau (dawb tag nrho) mloog ob peb ntawm nws cov lus ceeb toom ua ntej, tuaj nrog tsawg kawg ib nqe lus nug txog lawv, thiab tsuas yog tom qab ntawd tuaj. Kuv txiav txim siab pom dab tsi Lamport tau tshaj tawm nyob rau ntawd - thiab nws zoo heev! Qhov no yog raws nraim li ntawd, ib tug khawv koob txuas-cov tshuaj rau kho zombies. Kuv ceeb toom rau koj: cov ntawv nyeem yuav hlawv cov neeg uas nyiam cov txheej txheem nrawm nrawm thiab tsis nyiam sim qhov lawv tau sau.
Tom qab lub habrokat, kev txhais lus ntawm lub rooj sab laj yeej pib. Txaus siab rau kev nyeem ntawv!
Txawm koj ua haujlwm li cas los xij, koj ib txwm yuav tsum mus dhau peb kauj ruam:
- txiav txim siab seb lub hom phiaj koj xav ua kom tiav;
- txiav txim siab npaum li cas koj yuav ua tiav koj lub hom phiaj;
- ncav cuag koj lub hom phiaj.
Qhov no kuj siv tau rau programming. Thaum peb sau code, peb xav tau:
- txiav txim siab seb qhov kev zov me nyuam yuav tsum ua li cas;
- txiav txim siab raws nraim li cas nws yuav tsum ua nws txoj hauj lwm;
- sau tus lej tsim nyog.
Cov kauj ruam kawg, ntawm chav kawm, tseem ceeb heev, tab sis kuv yuav tsis tham txog nws hnub no. Hloov chaw, peb yuav tham txog thawj ob. Txhua tus programmer ua lawv ua ntej pib ua haujlwm. Koj tsis zaum sau ntawv tshwj tsis yog koj tau txiav txim siab qhov koj sau: browser lossis database. Ib lub tswv yim ntawm lub hom phiaj yuav tsum muaj tam sim no. Thiab koj twv yuav raug hu xav txog dab tsi raws nraim qhov kev pab cuam yuav ua, thiab tsis txhob sau nws haphazardly nyob rau hauv kev cia siab tias tus code nws tus kheej yuav ua li cas tig mus rau hauv ib tug browser.
Yuav ua li cas raws nraim qhov no pre-xav txog ntawm code tshwm sim? Peb yuav tsum siv zog npaum li cas rau qhov no? Nws tag nrho nyob ntawm seb qhov teeb meem nyuaj npaum li cas peb daws tau. Wb hais tias peb xav sau ib qho txhaum-tolerant faib system. Hauv qhov no, peb yuav tsum xav txog tej yam los ntawm kev ua tib zoo ua ntej zaum hauv qhov chaws. Yuav ua li cas yog tias peb tsuas yog xav tau nce tus lej sib txawv los ntawm 1? Thaum xub thawj siab ib muag, txhua yam ntawm no yog qhov tsis tseem ceeb thiab tsis xav tau kev xav, tab sis tom qab ntawd peb nco ntsoov tias qhov dej ntws tuaj yeem tshwm sim. Yog li ntawd, txawm nyob rau hauv thiaj li yuav to taub seb qhov teeb meem yog yooj yim los yog complex, koj yuav tsum xub xav.
Yog tias koj xav txog kev daws teeb meem ua ntej, koj tuaj yeem zam qhov yuam kev. Tab sis qhov no xav kom koj xav kom meej. Yuav kom ua tiav qhov no, koj yuav tsum sau koj cov kev xav. Kuv nyiam Dick Guindon cov lus hais: "Thaum koj sau, xwm qhia koj tias koj xav li cas." Yog koj tsis sau, koj tsuas xav tias koj tab tom xav. Thiab koj yuav tsum tau sau koj cov kev xav nyob rau hauv daim ntawv ntawm specifications.
Specifications ua haujlwm ntau, tshwj xeeb tshaj yog nyob rau hauv cov haujlwm loj. Tab sis kuv tsuas yog hais txog ib qho ntawm lawv: lawv pab peb xav kom meej. Kev xav kom meej yog qhov tseem ceeb thiab nyuaj heev, yog li peb xav tau kev pab ntawm no. Peb yuav tsum sau cov lus qhia tshwj xeeb hauv hom lus twg? Feem ntau, qhov no ib txwm yog thawj lo lus nug rau programmers: peb yuav sau hom lus dab tsi? Tsis muaj ib lo lus teb yog lawm: cov teeb meem peb daws muaj ntau haiv neeg. Rau qee tus neeg, TLA + yog hom lus tshwj xeeb uas kuv tau tsim. Rau lwm tus, nws yooj yim dua los siv Suav. Nws tag nrho nyob ntawm qhov xwm txheej.
Cov lus nug tseem ceeb tshaj yog: peb yuav ua li cas thiaj ua tiav kev xav kom meej? Teb: Peb yuav tsum xav zoo li cov kws tshawb fawb. Qhov no yog ib txoj kev xav uas tau ua haujlwm zoo nyob rau 500 xyoo dhau los. Hauv kev tshawb fawb peb tsim cov qauv lej ntawm kev muaj tiag. Astronomy yog kab tias thawj qhov kev tshawb fawb hauv kev nkag siab nruj ntawm lo lus. Nyob rau hauv cov qauv lej siv nyob rau hauv astronomy, lub cev xilethi-aus tshwm sim raws li cov ntsiab lus nrog huab hwm coj, txoj hauj lwm thiab lub zog, txawm hais tias qhov tseeb lawv yog cov khoom nyuaj heev nrog roob thiab dej hiav txwv, ebbs thiab ntws. Cov qauv no, zoo li lwm yam, tau tsim los daws qee yam teeb meem. Nws yog qhov zoo rau kev txiav txim siab qhov twg taw tes rau lub tsom iav yog tias koj xav nrhiav lub ntiaj teb. Tab sis yog tias koj xav kwv yees huab cua ntawm lub ntiaj teb no, tus qauv no yuav tsis ua haujlwm.
Kev ua lej tso cai rau peb los txiav txim qhov khoom ntawm tus qauv. Thiab kev tshawb fawb qhia tias cov khoom no cuam tshuam li cas rau kev muaj tiag. Cia peb tham txog peb txoj kev tshawb fawb, computer science. Qhov tseeb peb ua haujlwm nrog yog suav tshuab ntawm ntau hom: processors, game consoles, computers uas khiav cov kev pab cuam, thiab lwm yam. Kuv yuav tham txog kev ua tiav ib qho kev pab cuam ntawm lub computer, tab sis, los ntawm thiab loj, tag nrho cov lus xaus no siv rau txhua lub computer. Hauv peb txoj kev tshawb fawb peb siv ntau tus qauv sib txawv: lub tshuab Turing, ib nrab xaj cov txheej xwm, thiab ntau lwm yam.
Qhov kev pab cuam yog dab tsi? Qhov no yog txhua txoj cai uas tuaj yeem txiav txim siab ntawm nws tus kheej. Wb hais tias peb yuav tsum sau ib tug browser. Peb ua peb txoj haujlwm: tsim tus neeg siv qhov kev nthuav qhia ntawm qhov kev pab cuam, tom qab ntawd sau daim duab qhia qib siab ntawm qhov kev pab cuam, thiab thaum kawg sau cov lej. Thaum peb sau cov cai, peb paub tias peb yuav tsum tau sau ib tsab ntawv formatter. Ntawm no dua peb yuav tsum daws peb qhov teeb meem: txiav txim siab seb cov ntawv no yuav rov qab los; xaiv ib qho algorithm rau formatting; sau code. Txoj haujlwm no muaj nws tus kheej subtask: ntxig hyphens rau hauv cov lus kom raug. Peb kuj daws tau qhov kev ua haujlwm no hauv peb kauj ruam - raws li peb pom, lawv rov ua dua ntawm ntau qib.
Cia peb ua tib zoo saib thawj kauj ruam: qhov teeb meem twg qhov kev pab cuam daws teeb meem. Ntawm no peb feem ntau ua qauv ib qho kev pab cuam raws li kev ua haujlwm uas siv qee cov tswv yim thiab muab qee qhov tso tawm. Hauv kev ua lej, ib qho kev ua haujlwm feem ntau yog piav raws li kev txiav txim ntawm khub. Piv txwv li, kev ua haujlwm squaring rau cov lej ntuj tau piav qhia raws li qhov teeb tsa {<0,0>, <1,1>, <2,4>, <3,9>, β¦}. Lub ntsiab lus txhais ntawm qhov kev ua haujlwm no yog cov txheej txheem ntawm thawj lub ntsiab lus ntawm txhua khub, uas yog, tus lej ntuj. Txhawm rau txheeb xyuas qhov muaj nuj nqi, peb yuav tsum qhia nws cov npe thiab cov qauv.
Tab sis cov haujlwm hauv lej tsis zoo ib yam li cov haujlwm hauv cov lus programming. Kev ua lej yog qhov yooj yim dua. Txij li thaum kuv tsis muaj sij hawm rau cov piv txwv nyuaj, cia peb xav txog ib qho yooj yim: ib qho kev ua haujlwm hauv C lossis ib txoj kev zoo li qub hauv Java uas rov qab qhov sib faib loj tshaj ntawm ob tus lej. Hauv qhov tshwj xeeb ntawm txoj kev no peb yuav sau: xam GCD(M,N) rau kev sib cav M ΠΈ Nqhov twg GCD(M,N) - ib txoj haujlwm uas nws lub npe yog ib pawg ntawm cov lej ntawm cov lej, thiab tus nqi rov qab yog tus lej loj tshaj plaws uas muab faib los ntawm M ΠΈ N. Qhov kev muaj tiag piv rau tus qauv no li cas? Tus qauv ua haujlwm nrog cov lej, thiab hauv C lossis Java peb muaj 32-ntsis int. Cov qauv no tso cai rau peb txiav txim siab seb lub algorithm puas yog GCD, tab sis nws yuav tsis tiv thaiv overflow yuam kev. Qhov no yuav xav tau ib tug qauv complex, uas tsis muaj sij hawm.
Cia peb tham txog cov kev txwv ntawm kev ua haujlwm raws li tus qauv. Qee qhov kev pab cuam (xws li kev khiav hauj lwm systems) tsis tsuas yog xa rov qab tus nqi tshwj xeeb rau qee qhov kev sib cav; lawv tuaj yeem khiav tsis tu ncua. Tsis tas li ntawd, kev ua haujlwm raws li tus qauv tsis zoo rau cov kauj ruam thib ob: npaj yuav daws qhov teeb meem li cas. Quicksort thiab npuas txheeb suav tib lub luag haujlwm, tab sis lawv yog cov algorithms sib txawv kiag li. Yog li ntawd, los piav txog txoj hauv kev kom ua tiav lub hom phiaj ntawm qhov kev zov me nyuam, kuv siv lwm tus qauv, cia peb hu nws tus qauv coj tus cwj pwm. Qhov kev pab cuam yog sawv cev rau hauv nws raws li cov txheej txheem ntawm txhua tus cwj pwm siv tau, txhua tus ntawm cov uas, nyob rau hauv lem, yog ib theem ntawm cov xeev, thiab ib lub xeev yog lub luag hauj lwm ntawm qhov tseem ceeb rau variables.
Cia peb saib seb kauj ruam thib ob rau Euclidean algorithm yuav zoo li cas. Peb yuav tsum xam GCD(M, N). Peb pib M yuav ua li cas xthiab N yuav ua li cas y, ces rov rho cov me ntawm cov variables ntawm qhov loj kom txog rau thaum lawv sib npaug. Piv txwv li, yog tias M = 12thiab N = 18, peb tuaj yeem piav qhia txog tus cwj pwm hauv qab no:
[x = 12, y = 18] β [x = 12, y = 6] β [x = 6, y = 6]
Thiab yog tias M = 0 ΠΈ N = 0? Zero yog faib los ntawm txhua tus lej, yog li tsis muaj qhov sib faib loj tshaj plaws hauv qhov no. Hauv qhov xwm txheej no, peb yuav tsum rov qab mus rau thawj kauj ruam thiab nug: peb puas xav tau tiag tiag suav GCD rau cov lej tsis zoo? Yog tias qhov no tsis tsim nyog, ces koj tsuas yog yuav tsum tau hloov qhov specification.
Ib qho luv luv digression ntawm productivity yog nyob rau hauv kev txiav txim ntawm no. Nws yog feem ntau ntsuas nyob rau hauv tus naj npawb ntawm kab ntawm code sau ib hnub twg. Tab sis koj txoj haujlwm tseem ceeb dua yog tias koj tshem tawm qee cov kab, vim tias koj muaj chav tsawg dua rau cov kab. Thiab qhov yooj yim tshaj plaws kom tshem tau cov code yog thawj kauj ruam. Nws yog qhov ua tau tias koj tsuas yog tsis xav tau txhua lub tswb thiab xuav koj tab tom sim siv. Txoj kev ceev tshaj plaws los ua kom yooj yim rau qhov kev pab cuam thiab txuag lub sijhawm yog tsis ua tej yam uas yuav tsum tsis txhob ua. Cov kauj ruam thib ob muaj qhov thib ob siab tshaj lub sij hawm-txuag. Yog tias koj ntsuas cov khoom tsim tau raws li cov kab ntawv sau, ces xav txog yuav ua li cas ua tiav ib txoj haujlwm yuav ua rau koj tsawg tsim tau, vim tias koj tuaj yeem daws qhov teeb meem tib yam nrog tsawg code. Kuv tsis tuaj yeem muab cov txheeb cais tseeb ntawm no, vim tias kuv tsis muaj txoj hauv kev los suav cov kab uas kuv tsis tau sau vim lub sijhawm kuv siv rau qhov tshwj xeeb, uas yog, ntawm thawj thiab thib ob kauj ruam. Thiab peb tsis tuaj yeem ua qhov kev sim ntawm no, vim tias hauv kev sim peb tsis muaj cai ua kom tiav thawj kauj ruam; txoj haujlwm tau txiav txim ua ntej.
Nws yog ib qho yooj yim rau overlook ntau yam teeb meem nyob rau hauv tsis raws cai specifications. Tsis muaj dab tsi nyuaj txog kev sau cov lus tshwj xeeb rau kev ua haujlwm; Kuv yuav tsis tham txog qhov no. Hloov chaw, peb yuav tham txog kev sau cov lus qhia tshwj xeeb rau tus qauv coj cwj pwm. Muaj ib txoj kev xav uas hais tias txhua yam kev coj cwj pwm tuaj yeem piav qhia siv cov cuab yeej ruaj ntseg (kev nyab xeeb) thiab survivability zog (kev ua neej). Kev nyab xeeb txhais tau tias tsis muaj dab tsi phem yuav tshwm sim, qhov kev zov me nyuam yuav tsis muab cov lus teb tsis raug. Survivability txhais tau hais tias tsis ntev los yog tom qab ib yam dab tsi zoo yuav tshwm sim, piv txwv li qhov kev pab cuam yuav sai los yog tom qab muab cov lus teb raug. Raws li txoj cai, kev ruaj ntseg yog qhov taw qhia tseem ceeb dua; qhov yuam kev feem ntau tshwm sim ntawm no. Yog li ntawd, kom txuag tau sijhawm, kuv yuav tsis tham txog kev muaj sia nyob, txawm tias nws, ntawm chav kawm, kuj tseem ceeb.
Peb ua tiav kev nyab xeeb los ntawm thawj zaug qhia txog cov txheej txheem pib ua tau. Thiab qhov thib ob, kev sib raug zoo nrog txhua lub xeev tom ntej no rau txhua lub xeev. Cia peb coj zoo li cov kws tshawb fawb thiab txhais cov xeev ua lej. Cov txheej txheem thawj zaug tau piav qhia los ntawm cov qauv, piv txwv li, nyob rau hauv rooj plaub ntawm Euclidean algorithm: (x = M) β§ (y = N). Rau tej yam muaj nqis M ΠΈ N tsuas muaj ib lub xeev pib xwb. Kev sib raug zoo nrog lub xeev tom ntej no tau piav qhia los ntawm cov qauv uas qhov sib txawv ntawm lub xeev tom ntej tau sau nrog tus thawj, thiab cov kev hloov pauv ntawm lub xeev tam sim no tau sau tsis muaj prime. Nyob rau hauv cov ntaub ntawv ntawm Euclidean algorithm, peb yuav tau soj ntsuam nrog disjunction ntawm ob tug qauv, nyob rau hauv ib tug ntawm cov uas. x yog tus nqi loj tshaj plaws, thiab hauv qhov thib ob - y:
Hauv thawj kis, tus nqi tshiab ntawm y yog sib npaug rau tus nqi yav dhau los ntawm y, thiab peb tau txais tus nqi tshiab ntawm x los ntawm kev rho tawm qhov sib txawv me me ntawm qhov loj dua. Hauv qhov thib ob, peb ua qhov tsis sib xws.
Cia peb rov qab mus rau Euclidean algorithm. Xav tias dua M = 12, N = 18. Qhov no txhais tau ib lub xeev pib, (x = 12) β§ (y = 18). Peb mam li ntsaws cov nqi no rau hauv cov qauv saum toj no thiab tau txais:
Nov yog tib txoj kev daws teeb meem: x' = 18 - 12 β§ y' = 12, thiab peb tau txais tus cwj pwm: [x = 12, y = 18]. Ib yam li ntawd, peb tuaj yeem piav qhia txhua lub xeev hauv peb tus cwj pwm: [x = 12, y = 18] β [x = 12, y = 6] β [x = 6, y = 6].
Hauv lub xeev kawg [x = 6, y = 6] ob qho tib si ntawm cov lus qhia yuav tsis tseeb, yog li nws tsis muaj lub xeev tom ntej. Yog li, peb muaj cov lus qhia ua tiav ntawm theem thib ob - raws li peb pom, qhov no yog kev lej zoo tib yam, zoo li cov kws tshaj lij thiab cov kws tshawb fawb, thiab tsis txawv, zoo li hauv computer science.
Ob qho qauv no tuaj yeem muab tso ua ke rau hauv ib qho qauv ntawm lub cev logic. Nws yog elegant thiab yooj yim los piav, tab sis tsis muaj sij hawm rau nws tam sim no. Tej zaum peb yuav xav tau kev xav ntawm lub cev nkaus xwb rau cov cuab yeej ntawm kev muaj sia nyob; rau kev nyab xeeb nws tsis xav tau. Kuv tsis nyiam qhov kev xav ntawm lub cev xws li, nws tsis yog kev lej zoo tib yam, tab sis nyob rau hauv cov ntaub ntawv ntawm kev ua neej nws yog qhov tsim nyog phem.
Hauv Euclidean algorithm rau txhua tus nqi x ΠΈ y muaj tus nqi tshwj xeeb x' ΠΈ y', uas ua rau kev sib raug zoo nrog lub xeev tom ntej no muaj tseeb. Hauv lwm lo lus, Euclidean algorithm yog kev txiav txim siab. Txhawm rau ua tus qauv nondeterministic algorithm, lub xeev tam sim no yuav tsum muaj ntau lub xeev yav tom ntej, thiab txhua tus nqi ntawm qhov tsis sib xws yuav tsum muaj ntau yam txiaj ntsig ntawm qhov sib txawv ntawm qhov tseem ceeb xws li kev sib raug zoo rau lub xeev tom ntej yog qhov tseeb. Qhov no tsis yooj yim ua, tab sis kuv yuav tsis muab piv txwv tam sim no.
Txhawm rau ua ib qho cuab yeej ua haujlwm, koj xav tau lej lej. Yuav ua li cas thiaj ua tau ib qho kev qhia tshwj xeeb? Yuav kom ua tau li no peb yuav xav tau ib hom lus formal, piv txwv li. . Qhov tshwj xeeb ntawm Euclidean algorithm hauv hom lus no yuav zoo li no:
Lub cim kos npe sib npaug nrog daim duab peb sab txhais tau hais tias tus nqi rau sab laug ntawm daim paib txiav txim siab tias yuav sib npaug ntawm tus nqi mus rau sab xis ntawm daim paib. Nyob rau hauv qhov tseeb, ib tug specification yog ib tug txhais, nyob rau hauv peb rooj plaub ob txhais. Rau qhov tshwj xeeb hauv TLA + koj yuav tsum tau ntxiv cov lus tshaj tawm thiab qee cov lus sib dhos, xws li hauv cov swb saum toj no. Hauv ASCII nws yuav zoo li no:
Raws li koj tau pom, tsis muaj dab tsi nyuab. Cov lus qhia tshwj xeeb ntawm TLA + tuaj yeem txheeb xyuas tau, piv txwv li, nws muaj peev xwm hla txhua tus cwj pwm ua tau hauv tus qauv me me. Hauv peb cov ntaub ntawv, tus qauv no yuav yog qee yam muaj nuj nqis M ΠΈ N. Qhov no yog ib tug zoo heev thiab yooj yim kev txheeb xyuas txoj kev uas yog kiag li tsis siv neeg. Tsis tas li ntawd, nws muaj peev xwm sau cov ntaub ntawv pov thawj ntawm qhov tseeb thiab tshawb xyuas lawv cov tshuab, tab sis qhov no yuav siv sij hawm ntau, yog li yuav luag tsis muaj leej twg ua qhov no.
Lub ntsiab tsis zoo ntawm TLA + yog tias nws yog lej, thiab cov programmers thiab cov kws tshawb fawb hauv computer ntshai kev lej. Thaum xub thawj siab ib muag no suab zoo li ib tug tso dag, tab sis, hmoov tsis, kuv hais qhov no nyob rau hauv tag nrho cov loj. Ib tug npoj yaig ntawm kuv tsuas yog qhia kuv li cas nws sim piav qhia TLA + rau ntau tus tsim tawm. Thaum cov qauv tshwm sim ntawm qhov screen, lawv ob lub qhov muag tam sim ntawd ua glassy. Yog li yog tias TLA + txaus ntshai, koj tuaj yeem siv , yog hom khoom ua si programming lus. Ib qho kev qhia hauv PlusCal tuaj yeem yog ib qho kev qhia TLA +, uas yog, qhov tseem ceeb ntawm kev qhia lej. Tsis tas li ntawd, PlusCal muaj syntax rau non-deterministic algorithms. Vim tias PlusCal tuaj yeem sau ib qho kev qhia TLA +, nws yog qhov nthuav qhia ntau dua li cov lus programming tiag tiag. Tom ntej no, PlusCal tau muab tso ua ke rau hauv ib qho yooj yim nyeem TLA + specification. Qhov no tsis tau txhais hais tias, tau kawg, qhov nyuaj PlusCal specification yuav tig mus rau hauv ib qho yooj yim ntawm TLA + - tsuas yog tias cov ntawv xov xwm ntawm lawv pom tseeb, tsis muaj qhov nyuaj ntxiv yuav tshwm sim. Thaum kawg, qhov kev qhia tshwj xeeb no tuaj yeem txheeb xyuas tau siv TLA + cov cuab yeej. Feem ntau, PlusCal tuaj yeem pab kov yeej phobia ntawm kev ua lej; nws yooj yim to taub txawm rau cov programmers thiab cov kws tshawb fawb hauv computer. Kuv luam tawm algorithms rau qee lub sijhawm (kwv yees li 10 xyoo) yav dhau los.
Tej zaum ib tug neeg yuav tawm tsam tias TLA + thiab PlusCal yog lej, thiab lej tsuas yog ua haujlwm nrog cov qauv tsim. Hauv kev xyaum, koj xav tau hom lus tiag tiag nrog hom, txheej txheem, khoom, thiab lwm yam. Qhov no tsis yog lawm. Nov yog qhov Chris Newcomb, uas ua haujlwm ntawm Amazon, sau: "Peb tau siv TLA + ntawm kaum txoj haujlwm loj, thiab txhua qhov kev siv nws ua rau muaj qhov sib txawv tseem ceeb rau kev txhim kho vim tias peb tuaj yeem ntes cov kab txaus ntshai ua ntej lawv tsoo ntau lawm, thiab vim tias nws tau muab peb txoj kev nkag siab thiab kev ntseeg siab uas peb xav tau los ua kom nruj. kev ua tau zoo optimizations yam tsis muaj kev cuam tshuam qhov tseeb ntawm qhov kev pab cuam ". Koj tuaj yeem hnov ββββtias thaum siv txoj hauv kev peb tau txais cov cai tsis muaj txiaj ntsig - hauv kev xyaum, txhua yam yog qhov txawv. Tsis tas li ntawd, muaj kev nkag siab tias cov thawj coj tsis tuaj yeem ntseeg qhov kev xav tau ntawm cov txheej txheem raug cai, txawm tias cov programmers ntseeg tau tias lawv muaj txiaj ntsig. Thiab Newcomb sau: "Tam sim no cov thawj coj tau thawb txhua txoj hauv kev los sau cov lus qhia tshwj xeeb hauv TLA +, thiab tshwj xeeb faib sijhawm rau qhov no". Yog li thaum cov thawj coj pom tias TLA + ua haujlwm, lawv puag nws. Chris Newcomb tau sau qhov no txog rau lub hlis dhau los (Lub Kaum Hli 2014), tab sis tam sim no, raws li kuv paub, TLA + tau siv rau hauv 14 txoj haujlwm, tsis yog 10. Lwm qhov piv txwv cuam tshuam txog kev tsim ntawm XBox 360. Ib tug intern tuaj rau Charles Thacker thiab. sau specification rau lub cim xeeb system. Ua tsaug rau qhov kev qhia tshwj xeeb no, kab laum tau pom tias yuav tsis raug kuaj pom thiab yuav ua rau txhua tus XBox 360 tsoo tom qab plaub teev ntawm kev siv. Cov kws tshaj lij los ntawm IBM tau lees paub tias lawv qhov kev sim yuav tsis pom cov kab no.
Koj tuaj yeem nyeem ntxiv txog TLA + hauv Is Taws Nem, tab sis tam sim no cia peb tham txog cov ntsiab lus tsis raug cai. Peb tsis tshua tau sau cov kev pab cuam uas xam qhov sib faib tsawg tshaj plaws thiab cov zoo li. Ntau zaus peb sau cov kev pab cuam zoo li lub tshuab luam ntawv zoo nkauj uas kuv tau sau rau TLA +. Tom qab ua qhov yooj yim tshaj plaws, TLA + code yuav zoo li no:
Tab sis nyob rau hauv cov piv txwv saum toj no, tus neeg siv feem ntau yuav xav tau kev sib txuas thiab cov paib sib npaug sib npaug. Yog li qhov tseeb formatting yuav zoo li no:
Xav txog lwm cov piv txwv:
Ntawm no, ntawm qhov tsis sib xws, qhov sib npaug ntawm cov paib sib npaug, sib ntxiv thiab sib npaug hauv qhov chaw yog random, yog li kev ua haujlwm yooj yim yog txaus txaus. Feem ntau, tsis muaj qhov tseeb lej txhais ntawm qhov raug formatting, vim hais tias "yog" nyob rau hauv cov ntaub ntawv no txhais tau tias "qhov neeg siv xav tau," thiab qhov no tsis tuaj yeem txiav txim siab ua lej.
Nws yuav zoo li yog tias peb tsis muaj lub ntsiab lus ntawm qhov tseeb, ces qhov kev qhia tshwj xeeb tsis muaj txiaj ntsig. Tab sis qhov ntawd tsis muaj tseeb. Tsuas yog vim peb tsis paub tias qhov kev zov me nyuam yuav tsum ua dab tsi tsis tau txhais hais tias peb tsis tas yuav xav txog qhov nws yuav tsum ua haujlwm li cas - ntawm qhov tsis sib xws, peb yuav tsum siv zog ntau dua rau nws. Cov lus qhia tshwj xeeb yog qhov tseem ceeb ntawm no. Nws tsis tuaj yeem txiav txim siab qhov kev pom zoo rau cov qauv luam ntawv, tab sis qhov no tsis tau txhais hais tias peb yuav tsum tsis txhob ua txhua yam, thiab sau cov lej raws li cov kwj ntawm kev nco qab tsis yog qhov teeb meem. Kuv tau sau cov lus qhia txog rau txoj cai nrog cov lus txhais nyob rau hauv daim ntawv ntawm cov lus hauv Java file. Nov yog ib qho piv txwv ntawm ib txoj cai: a left-comment token is LeftComment aligned with its covering token. Txoj cai no yog sau rau hauv, cia peb hais, lej English: LeftComment aligned, left-comment ΠΈ covering token - Cov ntsiab lus nrog cov lus txhais. Qhov no yog li cas cov kws ua lej piav txog lej: lawv sau cov ntsiab lus ntawm cov ntsiab lus thiab, raws li lawv, tsim cov cai. Qhov txiaj ntsig ntawm qhov kev qhia tshwj xeeb no yog 850 txoj cai yooj yim dua rau kev nkag siab thiab debug dua 850 kab ntawm cov cai. Kuv yuav tsum hais tias kev sau cov cai no tsis yooj yim; nws siv sijhawm ntau heev los daws lawv. Kuv tau sau cov cai tshwj xeeb rau lub hom phiaj no uas qhia kuv tias txoj cai twg raug siv. Vim tias kuv tau sim rau txoj cai no nrog ob peb tus piv txwv, kuv tsis tas yuav debug XNUMX kab ntawm txoj cai, thiab cov kab no yooj yim zoo nkauj nrhiav. Java muaj cov cuab yeej zoo rau qhov no. Yog tias kuv nyuam qhuav sau tus lej, nws yuav siv sijhawm ntev dua thiab qhov formatting yuav tsis zoo.
Vim li cas ho tsis tuaj yeem siv cov lus qhia tshwj xeeb? Ntawm ib sab, kev ua kom raug tsis yog qhov tseem ceeb ntawm no. Ib daim ntawv luam tawm tau ua tiav yuav ua rau tsis txaus siab rau qee qhov, yog li kuv tsis tas yuav tau txais nws ua haujlwm kom raug hauv txhua qhov xwm txheej txawv. Qhov tseem ceeb tshaj yog qhov tseeb tias kuv tsis muaj cov cuab yeej tsim nyog. TLA + tus qauv kuaj xyuas tsis muaj txiaj ntsig ntawm no, yog li kuv yuav tsum tau sau cov piv txwv ntawm tes.
Cov kev qhia tshwj xeeb tau muab rau txhua qhov tshwj xeeb. Nws yog qib siab dua li code. Nws tuaj yeem siv tau hauv txhua hom lus. Tsis muaj cov cuab yeej lossis txoj hauv kev los sau nws. Tsis muaj chav kawm programming yuav pab koj sau cov lus qhia no. Thiab tsis muaj cov cuab yeej uas tuaj yeem ua rau qhov kev qhia tshwj xeeb no tsis tsim nyog, tshwj tsis yog tias koj tab tom sau hom lus tshwj xeeb rau kev sau cov txheej txheem luam tawm hauv TLA +. Thaum kawg, qhov kev qhia tshwj xeeb no tsis tau hais dab tsi txog qhov peb yuav sau tus lej li cas, nws tsuas yog hais tias tus lej ua li cas. Peb sau cov lus qhia tshwj xeeb los pab peb xav txog qhov teeb meem ua ntej peb pib xav txog cov cai.
Tab sis qhov kev qhia tshwj xeeb no kuj muaj cov yam ntxwv uas paub qhov txawv ntawm lwm qhov tshwj xeeb. 95% ntawm lwm cov kev qhia tshwj xeeb yog luv dua thiab yooj yim dua:
Tsis tas li ntawd, qhov kev qhia tshwj xeeb no yog cov txheej txheem kev cai. Qhov no feem ntau yog ib qho kev qhia tsis zoo. Kev nkag siab txog qhov tshwm sim ntawm cov txheej txheem kev cai yog qhov nyuaj heev, uas yog vim li cas kuv yuav tsum tau siv sijhawm ntau los kho lawv. Txawm li cas los xij, hauv qhov no kuv nrhiav tsis tau txoj hauv kev zoo dua.
Nws yog tsim nyog hais ob peb lo lus hais txog cov kev pab cuam uas khiav tsis tu ncua. Feem ntau lawv ua hauj lwm nyob rau hauv parallel, xws li kev khiav hauj lwm systems los yog faib systems. Tsawg tus neeg tuaj yeem nkag siab lawv hauv lawv lub siab lossis hauv daim ntawv, thiab kuv tsis yog ib tus ntawm lawv, txawm tias ib zaug kuv tuaj yeem ua tau. Yog li, peb xav tau cov cuab yeej uas yuav kuaj xyuas peb txoj haujlwm - piv txwv li, TLA + lossis PlusCal.
Vim li cas kuv thiaj li yuav tsum tau sau cov lus qhia tshwj xeeb yog tias kuv twb paub tias yuav ua li cas? Qhov tseeb, kuv tsuas xav tias kuv paub nws. Tsis tas li ntawd, nrog rau qhov tshwj xeeb hauv qhov chaw, tus neeg sab nraud tsis tas yuav saib mus rau hauv txoj cai kom nkag siab tias nws ua li cas. Kuv muaj txoj cai: yuav tsum tsis muaj kev cai dav dav. Muaj kev zam rau txoj cai no, qhov no tsuas yog txoj cai dav dav uas kuv ua raws: qhov tshwj xeeb ntawm qhov code yuav tsum qhia rau tib neeg txhua yam lawv xav paub thaum siv cov cai ntawd.
Yog li dab tsi raws nraim li programmers yuav tsum paub txog kev xav? Pib nrog, tib yam li rau txhua tus: yog tias koj tsis sau, ces nws tsuas yog zoo li koj uas koj xav. Tsis tas li ntawd, koj yuav tsum xav ua ntej koj code, uas txhais tau tias koj yuav tsum tau sau ua ntej koj code. Ib qho tshwj xeeb yog qhov peb sau ua ntej peb pib coding. Ib qho kev qhia tshwj xeeb yog xav tau rau txhua tus lej uas tuaj yeem siv lossis hloov tau los ntawm leej twg. Thiab qhov "ib tug" no yuav dhau los ua tus sau tus lej ib hlis tom qab nws tau sau. Ib qho kev qhia tshwj xeeb yog xav tau rau cov kev pab cuam loj thiab cov tshuab, rau cov chav kawm, rau txoj hauv kev, thiab qee zaum txawm rau cov ntu nyuaj ntawm ib txoj kev. Koj yuav tsum sau dab tsi ntawm tus lej? Koj yuav tsum piav qhia nws ua li cas, uas yog, ib yam dab tsi uas yuav pab tau rau txhua tus siv cov cai no. Qee zaum nws kuj tseem yuav tsim nyog los qhia meej tias qhov chaws ua tiav nws lub hom phiaj li cas. Yog tias peb mus dhau txoj kev no hauv chav kawm algorithms, ces peb hu nws ua algorithm. Yog hais tias nws yog ib yam dab tsi tshwj xeeb thiab tshiab, ces peb hu nws high-level tsim. Tsis muaj qhov sib txawv ntawm no: ob qho tib si yog cov qauv paub daws teeb ntawm qhov kev zov me nyuam.
Yuav ua li cas raws nraim koj yuav sau ib tug code specification? Qhov loj tshaj plaws: nws yuav tsum yog ib theem siab tshaj qhov chaws nws tus kheej. Nws yuav tsum piav qhia txog lub xeev thiab tus cwj pwm. Nws yuav tsum nruj raws li txoj haujlwm xav tau. Yog tias koj tab tom sau cov lus qhia txog yuav ua li cas los ua ib txoj haujlwm, ces nws tuaj yeem sau rau hauv pseudocode lossis siv PlusCal. Koj yuav tsum kawm sau cov lus qhia tshwj xeeb uas siv cov kev qhia tshwj xeeb. Qhov no yuav muab cov txuj ci tsim nyog rau koj uas tseem yuav pab nrog cov tsis raws cai. Koj kawm tau li cas los sau cov lus qhia tshwj xeeb? Thaum peb kawm txog qhov program, peb sau cov program thiab tom qab ntawd debuged lawv. Ib yam ntawm no: koj yuav tsum tau sau cov lus qhia tshwj xeeb, tshawb xyuas nrog tus qauv kuaj xyuas, thiab kho qhov yuam kev. TLA + tej zaum yuav tsis yog hom lus zoo tshaj plaws rau kev qhia tshwj xeeb, thiab lwm hom lus yuav zoo dua rau koj cov kev xav tau tshwj xeeb. Qhov zoo tshaj plaws ntawm TLA + yog tias nws ua haujlwm zoo ntawm kev qhia lej kev xav.
Yuav ua li cas txuas specification thiab code? Siv cov lus uas txuas cov ntsiab lus lej thiab lawv qhov kev siv. Yog tias koj ua haujlwm nrog cov duab kos, tom qab ntawd ntawm qib program koj yuav muaj arrays ntawm nodes thiab arrays ntawm kev sib txuas. Yog li koj yuav tsum sau cov duab raws nraim li cas los ntawm cov txheej txheem programming.
Nws yuav tsum tau muab sau tseg tias tsis muaj ib qho ntawm cov saum toj no siv rau cov txheej txheem ntawm kev sau code nws tus kheej. Thaum koj sau code, uas yog, ua qhov thib peb kauj ruam, koj kuj yuav tsum tau xav thiab xav los ntawm qhov kev pab cuam. Yog hais tias ib tug subtask hloov mus ua complex los yog tsis pom tseeb, koj yuav tsum tau sau ib tug specification rau nws. Tab sis kuv tsis tham txog tus lej nws tus kheej ntawm no. Koj tuaj yeem siv cov lus programming, txhua txoj kev, qhov no tsis yog hais txog lawv. Tsis tas li ntawd, tsis muaj ib qho ntawm cov saum toj no tshem tawm qhov yuav tsum tau sim thiab debug koj cov cai. Txawm hais tias tus qauv paub daws teeb yog sau kom raug, tej zaum yuav muaj kab laum hauv nws qhov kev siv.
Kev sau cov lus qhia tshwj xeeb yog ib kauj ruam ntxiv hauv cov txheej txheem coding. Ua tsaug rau nws, ntau qhov yuam kev tuaj yeem raug ntes nrog kev siv zog tsawg - peb paub qhov no los ntawm kev paub ntawm cov programmers los ntawm Amazon. Nrog specifications, qhov zoo ntawm cov kev pab cuam yuav siab dua. Yog li ntawd yog vim li cas peb thiaj li feem ntau mus tsis muaj lawv? Vim kev sau ntawv nyuaj. Tab sis kev sau ntawv yog qhov nyuaj, vim qhov no koj yuav tsum xav, thiab kev xav kuj nyuaj. Nws ib txwm yooj yim dua los ua piv txwv koj xav. Ib qho piv txwv tuaj yeem kos ntawm no nrog kev khiav - qhov tsawg koj khiav, qeeb koj khiav. Koj yuav tsum tau cob qhia koj cov leeg thiab xyaum sau ntawv. Nws yuav siv sij hawm xyaum.
Cov specification yuav tsis raug. Tej zaum koj yuav tau ua yuam kev nyob qhov twg, los yog cov kev cai yuav tau hloov, los yog yuav tsum tau txhim kho. Txhua tus lej uas leej twg siv yuav tsum tau hloov pauv, yog li sai lossis tom qab qhov kev qhia tshwj xeeb yuav tsis phim rau qhov program. Qhov zoo tshaj plaws, nyob rau hauv cov ntaub ntawv no, koj yuav tsum tau sau ib tug tshiab specification thiab tag rewrite code. Peb paub zoo tias tsis muaj leej twg ua li no. Hauv kev xyaum, peb kho qhov chaws thiab tej zaum hloov kho qhov tshwj xeeb. Yog tias qhov no yuav tshwm sim sai dua lossis tom qab, yog vim li cas thiaj sau cov lus qhia txhua? Ua ntej, rau tus neeg uas yuav hloov kho koj cov cai, txhua lo lus ntxiv hauv qhov tshwj xeeb yuav tsim nyog nws qhov hnyav hauv kub, thiab tus neeg no yuav yog koj. Kuv feem ntau ncaws kuv tus kheej rau qhov tsis meej txaus thaum kuv kho kuv cov cai. Thiab kuv sau ntau specifications tshaj li code. Yog li ntawd, thaum koj hloov kho cov cai, cov lus qhia ib txwm yuav tsum tau hloov kho. Thib ob, nrog rau txhua qhov kev hloov kho cov cai yuav tsis zoo, nws nyuaj rau kev nyeem thiab tswj. Qhov no yog qhov nce hauv entropy. Tab sis yog tias koj tsis pib nrog ib qho tshwj xeeb, ces txhua kab koj sau yuav yog ib qho kev hloov kho, thiab cov cai yuav loj heev thiab nyuaj nyeem los ntawm qhov pib.
Raws li hais , tsis muaj kev sib ntaus sib tua tau yeej raws li txoj kev npaj, thiab tsis muaj kev sib ntaus sib tua yeej tsis muaj phiaj xwm. Thiab nws paub ib yam dab tsi txog kev sib ntaus sib tua. Muaj kev xav tias kev sau cov lus qhia tshwj xeeb yog nkim sijhawm. Qee lub sij hawm qhov no yog qhov tseeb, thiab txoj haujlwm yooj yim heev uas tsis muaj lub ntsiab lus xav txog nws. Tab sis koj yuav tsum nco ntsoov tias thaum koj raug qhia kom tsis txhob sau cov lus qhia tshwj xeeb, nws txhais tau tias koj raug qhia kom tsis txhob xav. Thiab koj yuav tsum xav txog qhov no txhua lub sijhawm. Kev xav los ntawm ib txoj haujlwm tsis lav tias koj yuav tsis ua yuam kev. Raws li peb paub, tsis muaj leej twg tsim ib lub wand khawv koob, thiab programming yog ib txoj haujlwm nyuaj. Tab sis yog tias koj tsis xav txog txoj haujlwm, koj tau lees tias yuav ua yuam kev.
Koj tuaj yeem nyeem ntxiv txog TLA + thiab PlusCal ntawm lub vev xaib tshwj xeeb, koj tuaj yeem mus rau qhov ntawd los ntawm kuv qhov home page . Qhov ntawd yog txhua yam rau kuv, ua tsaug rau koj qhov kev mloog.
Thov nco ntsoov tias qhov no yog kev txhais lus. Thaum koj sau cov lus, nco ntsoov tias tus sau yuav tsis nyeem lawv. Yog tias koj xav tham nrog tus sau tiag tiag, nws yuav nyob ntawm Hydra 2019 lub rooj sib tham, uas yuav muaj rau Lub Xya Hli 11-12, 2019 hauv St. Daim pib tuaj yeem yuav .
Tau qhov twg los: www.hab.com