Axiom · dark

Керування потоком

Знайомі if/for/while без зайвої церемонії. Різниця в тому, що loop bounds і invariants можуть стати матеріалом для proof engine.

Цикл з доведеним bounds

Loop boundsAxiom

1sum(view<const i32> values) -> i64:2    i64 total = 03    for usize i = 0; i < values.size(); i = i + 1:4        total = total + values[i]5    RETURN total

Borrowed read-only sequence.

Акумулятор.

Loop condition гарантує i < size у тілі.

Тому values[i] не потребує runtime bounds check, якщо proof engine зберіг цей факт.

Повертаємо суму.

BREAK і CONTINUE

CONTINUE — запланованоCONTINUE наразі ще не існує в bootstrap compiler, але входить у target surface. Документація використовує його вже зараз, щоб майбутній control-flow був послідовним.

Target surfaceAxiom

1count_non_empty(view<const text> rows) -> usize:2    usize count = 03    for const text row in rows:4        if row.empty():5            CONTINUE6        count = count + 17    RETURN count

Range-style loop.

Перевіряємо поточний рядок.

CONTINUE переходить до наступної ітерації.

Виконується лише для непорожнього рядка.

Рекурсії немає

Пряма й непряма рекурсія заборонені. Compiler будує call graph і відхиляє цикл викликів. Для parser-ів, обходів дерев і state machines використовуйте явний stack/queue з bounded storage. Це не обмеження «бо так простіше компілятору»: воно робить worst-case stack usage аналізованим.

← Типи та ADT Контракти →