Контракти
Contracts — центральна частина Axiom. Це спосіб описати межі допустимого стану так, щоб compiler міг ними користуватися.
Уявіть типову backend-функцію: «offset має бути в buffer», «JSON response не більший за capacity», «після reserve місця вистачає». У Axiom ці речі не залишаються коментарями.
| Конструкція | Хто відповідає | Що означає |
|---|---|---|
require expr | caller | Передумова. Виклик законний лише коли умова доведена. |
ensure expr | callee | Післяумова: implementation має довести її для кожного return path. |
invariant expr | тип / loop | Властивість, яка повинна зберігатися. |
assert expr | compile time | Точка, де програміст вимагає доказ. |
runtime_assert expr | runtime | Свідомо залишена runtime-перевірка. |
assume expr | trusted boundary | Дуже обмежений спосіб сказати compiler-у «вважай це істинним»; це sus. |
Приклад: writer, який не переповнить buffer
1writer:2 view<u8> out3 usize used45 invariant used <= out.size()67 push(u8 value):8 require used < out.size()9 out[used] = value10 used = used + 111 ensure used <= out.size()12END writerMutable view на caller-owned storage.
Скільки байтів уже зайнято.
Інваріант об’єкта: used ніколи не виходить за capacity.
Caller повинен мати доказ, що є хоча б один вільний байт.
Індекс безпечний через require + invariant.
Збільшуємо used.
Implementation зобов’язаний довести, що invariant зберігся.
Runtime input не ламає модель
Якщо число приходить із мережі, compiler фізично не може знати його значення під час build. Тоді ви перевіряєте input один раз і після branch отримуєте доведений факт.
1set_page_size(u32 requested) -> result<u32, request_error>:2 if requested == 0 or requested > 100:3 RETURN error(invalid_page_size)4 assert requested >= 15 assert requested <= 1006 RETURN ok(requested)Runtime branch відсікає недопустимі дані.
Після branch analyzer уже має вивести цей факт; assert тут корисний як executable documentation/proof checkpoint.
У success path значення вже bounded 1..100.
Чому це схоже на SPARK
SPARK навчив інженерів мислити contracts як proof obligations, а не декоративні annotations. Axiom переносить цей принцип у компактніший surface syntax і поширює його на views, memory regions, parallel effects та bundle planning.