Creusot 0.14.0: Qismən sıralama spesifikasiyaları, snapshot VC-ləri və rust-analyzer navigasiyası

Qismən sıralamalar

Creusot 0.14.0 Rust-ın formal verifikasiya alətinin buraxılışıdır. Buraxılış qeydlərində deyilir ki, qismən sıralamalar yeni funksiyaların kiçik hissəsidir, qalanı isə tam changelog-də verilib.

Əvvəlki versiyalar PartialOrd spesifikasiyasını tam sıralamalara qədər məhdudlaşdırırdı. 0.13.0 versiyasından bu məhdudiyyəti yüngülləşdirdilər ki, qismən sıralamalar da icazə verilsin. Əvvəlki tam sıralama trait-i OrdLogic cmp_log-a əsaslanırdı, cmp-in məntiqi analogu idi, bu isə Ordering qaytarırdı. Bu, nəticə ciddi şərtlər yaradırdı: istənilən iki element Less, Equal və ya Greater kimi müqayisə olunmalı idi.

Yeni ciddi qismən sıralama trait-i PartialOrdLogic əvəzinə lt_log-a əsaslanır, məntiqi müqayisə funksiyasına, refleksivlik və tranzitivlik qaydaları ilə. Sərtləşmə artıq ayrıca qaydadır OrdLogic-də, adı lt_log_total, bu isə self < other || self == other || other < self təmin edir. İnsanlar qeyd edirlər ki, mövcud sublardan heç biri zərər çəkməyib və avtomatik sublər dəyişikliklərə davam göstərib.

Snapshot-lər üçün verifikasiya şərtləri

Creusot indi snapshot-lər üçün verifikasiya şətləri generasiya edir, bunlar Rust proqramlarında quraşdırılmış məntiqi ifadələrdir. Bu, lemma funksiyalarının istifadəsini yaxşılaşdırır, idiomatik Creusot kimi verifikasiya alətlərində.

lemma məntiqi funksiya kimi yazıla bilər requires və ensures şərtləri ilə, bu, hyp(x) ifadəsinin concl(x)-i bütün x-lər üçün təmsil etdiyi mənasını verir. snapshot!-də lemma çağırışı indi assert-ə çevrilir ki, hyp(n) doğrudur və concl(n) doğrudur, konkret n arqumenti üçün ixtisaslaşdırılmış. Bu, subləri universal kvantor instansiyasına məcbur etmir.

Qeydlər bunu adi proqram lemma çağırışı ilə müqayisə edir. Həmin üsulun da requires və ensures şərtləri var, lakin o, Rust funksiyasını sürüdür və borrow checker-dən keçməlidir, bu da boilerplate tələb edə bilər, məqsəd yalnız faktları qeyd etməkdir. Snapshot-lər silinir, ona görə də onlar yalnız formal sübutlar üçün mövcuddur. snapshot! üçün verifikasiya şərtləri əvvəlcə generasiya edilmirdi, çünki soundness üçün lazım deyildi, buna baxmayaraq, spesifikasiya səhvlərini daha erkən aşkar etməyə kömək edir, məsələn, indeksləmə sərhədləri kənarı, və yeni texnikalar imkanı verir.

rust-analyzer dəstəyi

Go to definition indi Pearlite spesifikasiyalarında işləyir. Bunun üçün spesifikasiya makroları, məsələn requires, ensures, proof_assert! və snapshot!, rust-analyzer üçün genişləndirilib, normal kompilyasiya zamanı silinməsi əvəzinə. Creusot gid parametrlərini rust-analyzer üçün lazımi seçimlər üçün təqdim edir.

Genişləndirilmiş Pearlite kodu rustc üçün nəzərdə tutulmayıb, çünki o, tip yoxlayıcıdan keçir, lakin borrow checker-dən keçmir. Bu problem deyildi, çünki rust-analyzer borrow checking yerinə yetirmir. Qalan problem odur ki, Pearlite makrolarından alınan tokenlərin çox kobud span-ləri var idi. Nümunədə a + b AddLogic::add_logic(a, b)-ə genişlənir və bütün generasiya edilmiş tokenlər bütün ifadənin span-ına malik idi. Nəticədə, Go to definition bu ifadə dərinsindən istənilən yerdə creusot_std, logic, ops, AddLogic və add_logic üçün təriflər axtarırdı.

Düzəliş add_logic +-in span-ına verir, digər identifikatorlar isə rust-analyzer tərəfindən gözardı edilən sıfır genişlikli span-lərə malikdir. Sara Kinion bu təhlilin üzərinə götürülüb. İnsanlar deyirlər ki, nəticədə Creusot spesifikasiyalarında navigasiya daha səmərəlidir.

Suallar

Creusot haqqında sualları olan oxucular proyektin Zulip kanalına qoşula və ya Creusot repozitoriyasında discusiya və ya issue aça bilər.

Mənbələr: Lobsters