Eich prawf cyntaf

deg munud · tri cham · dim byd sy'n rhaid i chi ei dderbyn ar ffydd

Dyma lwybr y dechreuwr. Does dim rhaid i chi fod yn rhaglennwr, does dim rhaid i chi gael cyfrif, a does dim rhaid i chi ddweud wrthym eich bod yn bodoli. Ar ei ddiwedd bydd eich cyfrifiadur eich hun — nid ein un ni, ac nid ein gair ni amdano — wedi gwirio'r mathemateg y tu ôl i reol go iawn o'r llyfrgell.

Os ydych eisoes yn gwybod eich ffordd o gwmpas profwr, mae'r llwybr llawn yn mynd ymhellach: adeiladu'r ffrynt a gwirio pob rhes o'i dabl gwirionedd. Mae'r dudalen hon yn stopio wrth y prawf, sef y rhan sydd bwysicaf a'r rhan nad oes angen dim wedi'i osod ar ei chyfer.

Beth rydych ar fin ei wirio

Enw'r rheol yw brief-fill policy. Mae'n penderfynu pryd y caiff cynorthwyydd ateb ar ran ei berchennog yn hytrach na gofyn iddo. Gwneir pedwar honiad amdani, ac mae'r pedwar ar fin cael eu profi ar eich peiriant chi:

• nid yw byth yn llenwi ateb heb reol sy'n ei drwyddedu;
• os yw storfa'r rheolau ar goll, ni fydd dim yn mynd trwodd;
• nid yw byth yn dyfeisio unrhyw beth;
• nid yw byth yn gofyn i chi rywbeth y mae rheol eisoes yn ei ateb.

Nid addewidion mewn post blog yw'r rhain. Theoremau ydynt, ac mae profwr ar fin ceisio eu torri.

Cam 1 — cael y profwr

Mae'n rhad ac am ddim ac nid yw'n eiddo i ni — daw o gymuned Ada, nid oddi wrthym ni. Dyna'r pwynt: ni ddylai'r peth sy'n gwirio ein gwaith fod yn beth a roesom ni i chi.

Cam 2 — cael y rheol

Gallwch anwybyddu'r swm gwirio ar y tro cyntaf — nid yw'r prawf yng ngham 3 yn dibynnu arno. Mae yno ar gyfer pan fyddwch am gadarnhau mai'r ffeil a gawsoch chi yw'r ffeil a gyhoeddwyd gennym ni, a'i bod yr un ffeil ag y mae the catalogue yn ei henwi.

Cam 3 — gofynnwch i'ch cyfrifiadur ei wirio

Agorwch derfynell yn y ffolder wedi'i ddadbacio a rhedwch ddwy linell:

cd brief-fill-policy/core/src
gnatprove -P proof.gpr -f -U --level=2

Arhoswch. Pan fydd wedi gorffen, edrychwch am y ddau air hyn:

0 unproved

Dyna ni. Dyna'r ymarfer cyfan. Does dim byd arall angen ei osod, ac mae'r cam hwn yn gweithio ar beiriant plaen heb ddim byd arall arno — mae'r profwr a lwythoch i lawr yn cario popeth sydd angen ar y prawf.

Beth ddigwyddodd nawr

Cymerodd eich cyfrifiadur y pedwar honiad uchod, ceisiodd ddod o hyd i achos lle mae unrhyw un ohonynt yn methu, ac ni allai — oherwydd nid oes un yn bodoli. Nid “fe'i profwyd gennym ac roedd i weld yn iawn”. Nid “mae'r cynhaliwr yn dweud hynny”. Aeth peiriant na ellir ei berswadio i chwilio am wrtheiampl a daeth yn ôl yn waglaw.

Wnaethoch chi ddim ymddiried ynom ni i ddweud hynny wrthych. Fe wnaethoch chi ei wylio'n digwydd ar galedwedd sy'n eiddo i chi.

Dewisol — ei dorri'n fwriadol

Dyma'r rhan sy'n werth ei gwneud os oes gennych bum munud arall, achos nid yw gwiriad sydd ond byth yn dweud ie yn werth llawer.

Agorwch brief_fill_policy_pkg.ads mewn unrhyw olygydd testun a newidiwch y rheol fel bod storfa goll yn gadael i ateb fynd trwodd beth bynnag. Rhedwch yr un gorchymyn eto. Bydd yn gwrthod — a bydd yn enwi'r union theorem rydych newydd ei thorri.

Dyna'r gwrthodiad yw'r model diogelwch cyfan. Nid yw Ghillie'n gosod dim nad yw'n pasio hyn, felly'r hyn rydych newydd ei wneud â llaw yw'r hyn y mae'n ei wneud ar eich rhan bob tro.

Beth nad yw hyn yn ei brofi

Byddai'n well gennym ddweud hyn na'ch gadael i ddarganfod hynny nes ymlaen. Mae'r profion yn cwmpasu'r rheolau penderfynu — pwy sy'n cael gweld beth, beth sy'n cael gadael, beth y mae'n rhaid i ddanfoniad ei basio. Nid ydynt yn gwneud gweddill y feddalwedd yn hud, ac nid ydym yn honni eu bod. Yr onestrwydd hwnnw yw'r fargen, a dyna'r cyfan o'r fargen.

I ble nesaf

• Y llwybr llawn — adeiladu'r ffrynt a gwirio pob rhes o'i dabl gwirionedd wedi'i ddanfon.
• The catalogue — gweddill y silff, pob darn y gellir ei ail-ddeillio yr un ffordd.
• Ghillie — y cynorthwyydd y mae'r rheolau hyn yn ei wasanaethu.
• The Reef machine — pa galedwedd sydd ei angen arnoch os hoffech fynd ymhellach na'r dudalen hon.

Os na weithiodd, mae hynny'n ganfyddiad a hoffem glywed amdano. Mae gwrthodiad na allwch ei esbonio yn fwy diddorol i ni na llwyddiant.