ghost code

[amarao]

А вот вам вкусного из реддитов.

Новое понятие "ghost code". Это код, который добавляется в программу каким-либо препроцессором/аугментатором/доказателем/ассистентом, который гарантировано уничтожается при компиляции, но который может добавлять утверждений для компилятора для валидации. Грубо говоря, способность компилятора выкидывать мёртвый код используется для того, чтобы записать набор желаемых свойств для объектов, которые заставляют компилятор больше работать и больше проверять.

Источник: https://www.reddit.com/r/rust/comments/1ainrpg/i_wrote_my_masters_thesis_about_rust_verification/

Comments

[sab123]

Было бы разумно вместо того явно предусмотреть в компиляторе прагмы для этих целей. Ну вот как скажем в Оракле можно задать опции для оптимизации запросов в виде специально сформатированных комментариев.

[amarao]

В расте такое есть и используется, хотя и не для целей ghost code (тут это понятие только что изобрели).

[anonim_legion]

Давно уже есть в Ada Spark, именно так оно там и называется.

https://docs.adacore.com/spark2014-docs/html/ug/en/source/specification_features.html#ghost-code

[amarao]

О, спасибо. И мне нравится, что у них показаны примеры. Я едва понял из описания о чём речь, а с примерами куда более понятно.