Stale translation: the English source changed after this draft. Treat the English edition as the authority.

यह पृष्ठ मशीन-जनित मसौदा है और अभी मानव समीक्षा नहीं हुई है। कोड उदाहरण, आदेश और पहचानकर्ता अंग्रेज़ी में रहते हैं।

परीक्षण और विश्वास#

मैं परीक्षण, स्थैतिक जाँच, और प्रमाण अलग करता हूँ। वे अलग प्रश्न उत्तर देते हैं।

शैडो#

शैडो फलन से जुड़ा निष्पादनीय परीक्षण है:

fn double(value: int) -> int {
    return (* value 2)
}

shadow double {
    assert (== (double 0) 0)
    assert (== (double 3) 6)
}

साधारण संकलन के दौरान मैं शैडो मेज़बान इंटरप्रेटर में चलाता हूँ। जनित मूल कार्यक्रमों में भी उनका शैडो हार्नेस होता है। शैडो जिन मामलों को चलाता है उनका परीक्षण करता है; यह हर इनपुट के लिए फलन सिद्ध नहीं करता।

कंपाइलर लागू करना और परियोजना नीति भिन्न हैं:

• कंपाइलर सामान्यतः लापता शैडो पर चेतावनी देता है।
• यह extern फलन, main, जनित लैम्ब्डा, GPU फलन, और extern कॉल करने वाले फलन छूट देता है।
• रिपॉज़िटरी नीति प्रत्येक जोड़े या बदले गैर-extern नामित फलन के लिए, जब परीक्षण हो सके, उपयोगी शैडो माँगती है।

प्रॉपर्टी परीक्षण और कवरेज#

प्रॉपर्टी परीक्षण जनित मानों का नमूना लेते हैं और विफलता सिकोड़ सकते हैं। नमूना पूर्ण सत्यापन नहीं है। कवरेज बताती है कौन सा कोड चला; यह सहीपन स्थापित नहीं करती।

संविदाएँ#

requires पूर्वशर्तें जाँचता है और ensures अपनी कार्यान्वित सीमा पर उत्तरशर्तें जाँचता है। सफल रनटाइम जाँच कहती है कि वह शर्त उस निष्पादन के लिए रही।

औपचारिक सत्यापन#

मेरा Coq विकास परिभाषित कोर मॉडल के लिए कथित मेटाथ्योरी सिद्ध करता है। यह हर बैकएंड, विदेशी कॉल, ऐलोकेटर, मॉड्यूल, या उपयोगकर्ता फलन स्वतः सिद्ध नहीं करता।

सीमा देखने के लिए ट्रस्ट रिपोर्ट उपयोग करें:

./bin/nanoc program.nano --trust-report

proved केवल जाँचे प्रमेय के उसके कथित मॉडल में कहें, tested केवल नामित परीक्षण द्वारा चलाए व्यवहार के लिए, और assumed बिना जाँच प्लेटफ़ॉर्म या विदेशी व्यवहार के लिए।

उपयोगी जाँच#

make test
make userguide-check
make check-stdlib-docs
python3 scripts/check_markdown_links.py