Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Доказательство корректности (часть 2)

Корректная функция — это функция, которая не может вызвать UB, если выполнены её предусловия безопасности.

Следствие: все функции, написанные на чистом безопасном Rust, корректны.

Доказательство:

  • Код на безопасном Rust не имеет предусловий безопасности.

  • Поэтому вызывающий код функций, написанных на чистом безопасном Rust, всегда тривиально выполняет пустой набор предусловий.

  • Код на безопасном Rust не может вызвать UB.

Ч.т.д.

  • Прочитайте следствие.

  • Объясните доказательство.

  • Переведите на неформальный язык: весь безопасный код на Rust «хороший». У него нет предусловий безопасности, о которых должен думать программист; он всегда играет по правилам и никогда не вызывает UB.