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