Sentez ve eşdeğerlik
Önemli hesaplamaların yapısını korurken amaçlanan sonuçların değişmediğini doğrulayın.
Hesaplamanın kendisini yeniden kurun#
Counterexample-Guided Inductive Synthesis, yani CEGIS, davranış ve karşı örneklerden yararlanarak alternatif bir hesaplama arar. Motorun uygun saf skaler bölgelerinde aday ifadeler farklı bir Boolean-aritmetik temel ve değerlendirme yapısıyla kurulur. Böylece yalnızca talimatlara ekleme yapmak yerine ifade grafiğinin kendisi değişebilir.
Karşı örnek, sonraki adayı geliştirir#
Aday, bölgesel dönüşüm doğrulamasına gönderilir. Doğrulayıcı adayın farklı sonuç verdiği bir girdi bulursa bu tanık sentez sürecine geri beslenir. Sonraki aday bu durumu da hesaba katmalıdır. Böylece bir formülü birkaç örnekten geçtiği için kabul etmek yerine açık sonuçları olan bir arama ve kanıt döngüsü oluşur.
Yalnızca kanıtlanan bölgesel dönüşüm kabul edilir#
Doğrulayıcı; PROVED, COUNTEREXAMPLE_FOUND, OUT_OF_SCOPE ve UNKNOWN_BUDGET_EXCEEDED sonuçlarını ayırır. Yalnızca PROVED kabul sonucudur. Çözücü bütçesinin tükenmesi başarıya dönüştürülmez; desteklenen anlamsal modelin dışındaki bir bölge, başka bir kapsamın kanıtını kullanamaz.
Doğrulayıcının karar kurallarını inceleyin. Bu şema bir çözücü çalıştırmaz.
R₀(x)R₁(x)Sonuçlar + trap davranışı + giriş ön koşulları
Aday, tanımlanan bölgesel model ve giriş ön koşulları kapsamında kabul edilir. Karar, uygulamanın tamamına değil, ilgili dönüşüme aittir.
Somut bir girdi farklılığı ortaya çıkarır. Aday reddedilir; tanık, sentez sürecine geri beslenir.
Bölge; desteklenen saflık, sahiplik, frame veya sınır yükümlülüklerini ihlal eder. Bu model kapsamında kabul edilemez.
Çözücü kanıta ulaşamadan bütçesini tüketmiştir. Sonuçsuz çalışma dönüşüme izin vermez ve başarılı kanıt olarak önbelleğe alınmaz.
Kanıtın kapsamı kesindir#
Bölgesel model, tanımlanan giriş ön koşulları ve frame yükümlülükleri altında tam 32/64 bit sonuçları ve trap davranışını karşılaştırır. İşaretli genişlikler, taşma ve sıfıra bölme bu sözleşmenin parçasıdır. Uygulama; eksik ön koşullar, farklı trap kanalları ve sonuçsuz çözücü çalışmaları için kanıt önbelleği davranışını da içeren regresyon senaryolarına sahiptir.
Bu, kabul edilen bölgesel dönüşümün kapsamı belirli bir doğruluk özelliğidir. Uygulamanın tamamının hatasız veya korumalı programın tersine mühendisliğe kapalı olduğunun kanıtı değildir. Uygulama doğrulaması ve güvenlik modeli ayrı sorumluluklar olarak kalır.