דײַן ערשטער באַווײַז

צען מינוט · דרײַ טריט · גאָרנישט וואָס דו דאַרפֿסט נעמען אויף גלויבן

דאָס איז דער וועג פֿאַרן אָנהייבער. דו דאַרפֿסט ניט זײַן קיין פּראָגראַמיסט, דו דאַרפֿסט קיין קאָנטע ניט, און דו דאַרפֿסט אונדז ניט זאָגן אַז דו עקזיסטירסט. אין סוף פֿון דעם וועט דײַן אייגענער קאָמפּיוטער — ניט אונדזערער, און ניט אונדזער וואָרט דערפֿאַר — האָבן קאָנטראָלירט די מאַטעמאַטיק הינטער אַ ריכטיקן כּלל פֿון דער ביבליאָטעק.

אויב דו ווייסט שוין דײַן וועג אַרום אַ פּרוּווער, פֿירט דער פֿולער דורכגאַנג ווײַטער: בויען דעם פֿראָנט און קאָנטראָלירן יעדע שורה פֿון זײַן וואָר-טאַבעלע. די בלאַט שטעלט זיך אָפּ בײַם באַווײַז, וואָס איז דער טייל וואָס איז וויכטיקסט און דער טייל וואָס דאַרף גאָרנישט אינסטאַלירן.

וואָס דו ביסט גרייט צו קאָנטראָלירן

דער כּלל הייסט brief-fill policy. ער באַשליסט ווען אַן אַסיסטענט מעג ענטפֿערן אין נאָמען פֿון זײַן באַזיצער אַנשטאָט אים פֿרעגן. פֿיר טענות ווערן געמאַכט וועגן אים, און אַלע פֿיר זענען גרייט צו ווערן געטעסט אויף דײַן מאַשין:

דאָס זענען ניט קיין הבטחות אין אַ בלאָג-אַרטיקל. זיי זענען טעאָרעמען, און אַ פּרוּווער איז גרייט צו פּרוּוון זיי צעברעכן.

טריט 1 — נעם דעם פּרוּווער

github.com/alire-project/GNAT-FSF-builds/releases

נעם דעם gnatprove-פֿײַל פֿאַר דײַן מאַשין — -x86_64-linux, -darwin פֿאַר אַ Mac, אָדער -windows64. אַנטפּאַק עס ערגעץ. ניטאָ קיין אינסטאַלירער, גאָרנישט גייט אַרײַן אין דײַן סיסטעם, און גאָרנישט לויפֿט אין הינטערגרונט. מעק אָפּ דעם פֿאָלדער ווען דו ביסט פֿאַרטיק, און עס איז ווי עס וואָלט קיינמאָל ניט געשען.

ער איז פֿרײַ און ער איז ניט אונדזערער — ער קומט פֿון דער Ada-קהילה, ניט פֿון אונדז. דאָס איז דער פּונקט: די זאַך וואָס קאָנטראָלירט אונדזער אַרבעט זאָל ניט זײַן אַ זאַך וואָס מיר האָבן דיר איבערגעגעבן.

טריט 2 — נעם דעם כּלל

brief-fill-policy.tar.gz (6,918 bytes)

sha256: 14bb06671459784d2d571e7b5e2afc3037894c241517612b026dbe053fb6b180

אַנטפּאַק עס. אינעווייניק איז דער מקור-קאָד, דער באַווײַז, און אַ פּשוטע ענגלישע באַשרײַבונג פֿון וואָס דער כּלל טוט.

דו קענסט אַריבערקוקן די קאָנטראָל-סומע בײַם ערשטן מאָל — דער באַווײַז אין טריט 3 הענגט ניט אָפּ פֿון איר. זי איז דאָ פֿאַר ווען דו ווילסט באַשטעטיקן אַז דער פֿײַל וואָס דו האָסט באַקומען איז דער פֿײַל וואָס מיר האָבן פּובליקירט, און זי איז די זעלביקע וואָס the catalogue נעמט.

טריט 3 — בעט דײַן קאָמפּיוטער עס קאָנטראָלירן

עפֿן אַ טערמינאַל אין דעם אַנטפּאַקטן פֿאָלדער און לויף צוויי שורות:

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

וואַרט. ווען עס ענדיקט זיך, זוך די צוויי ווערטער:

0 unproved

דאָס איז עס. דאָס איז דער גאַנצער געניטונג. גאָרנישט מער דאַרף זיך אינסטאַלירן, און דער טריט אַרבעט אויף אַ פּשוטער מאַשין מיט גאָרנישט מער אויף איר — דער פּרוּווער וואָס דו האָסט אַראָפּגעלאָדן טראָגט אַלץ וואָס דער באַווײַז דאַרף.

וואָס איז נאָר וואָס געשען

דײַן קאָמפּיוטער האָט גענומען די פֿיר טענות דערויבן, פּרוּווט געפֿינען אַ פֿאַל וווּ אַ שום איינע פֿון זיי פֿעלט, און האָט ניט געקענט — ווײַל עס איז ניטאָ קיינער. ניט „מיר האָבן עס געטעסט און עס האָט אויסגעזען גוט". ניט „דער פֿאַרוואַלטער זאָגט אַזוי". אַ מאַשין וואָס מען קען ניט אַרומרעדן איז געגאַנגען זוכן אַ קעגן-בײַשפּיל און איז צוריקגעקומען ליידיק.

דו האָסט אונדז ניט געטרויט דיר דאָס צו זאָגן. דו האָסט עס באַטראַכט געשען אויף הארדוועיר וואָס געהערט דיר.

אַרעדיק — צעברעך עס בכּיוון

דאָס איז דער טייל ווערט טאָן אויב דו האָסט נאָך פֿינף מינוט, ווײַל אַ קאָנטראָל וואָס זאָגט תּמיד נאָר יאָ איז ניט ווערט פֿיל.

עפֿן brief_fill_policy_pkg.ads אין ערגעץ אַ טעקסט-רעדאַקטאָר און טוישט דעם כּלל אַזוי אַז אַ פֿעלנדיקער אָפּלאַגער לאָזט אַן ענטפֿער דורך פֿונדעסטוועגן. לויף דעם זעלביקן באַפֿעל נאָך אַ מאָל. ער וועט זיך אָפּווײַזן — און ער וועט נעמען דעם פּינקטלעכן טעאָרעם וואָס דו האָסט נאָר וואָס צעבראָכן.

יענע אָפּווייזונג איז דער גאַנצער זיכערהייט-מאָדעל. Ghillie אינסטאַלירט גאָרנישט וואָס גייט ניט דורך דעם, אַזוי וואָס דו האָסט נאָר וואָס געטאָן מיט דער האַנט איז וואָס ער טוט אין דײַן נאָמען יעדעס מאָל.

וואָס דאָס באַווײַזט ניט

מיר וואָלטן ליבער זאָגן דאָס איידער דו זאָלסט עס אַליין געפֿינען שפּעטער. די באַווײַזן דעקן די כּללים פֿון באַשלוס — ווער מעג זען וואָס, וואָס מעג אַרויסגיין, וואָס אַ שיקונג מוז דורכגיין. זיי מאַכן ניט דעם רעשט פֿון דער סאָפֿטוועיר קיין מאַגיע, און מיר זאָגן ניט אַז זיי טוען. יענע ערלעכקייט איז דער דיל, און זי איז דער גאַנצער דיל.

וווּהין צו גיין ווײַטער

אויב עס האָט ניט געאַרבעט, איז דאָס אַ געפֿינס און מיר וואָלטן געוואָלט הערן וועגן דעם. אַן אָפּווייזונג וואָס דו קענסט ניט דערקלערן איז אינטערעסאַנטער פֿאַר אונדז ווי אַ הצלחה.