Від Axiom до Ada та SPARK
Після Axiom багато «дивних» ідей Ada перестають бути дивними: ranges, contracts, strong types і proof-oriented design мають одну мету — прибрати випадкові стани.
Axiom не копіює Ada syntax. Він намагається дати сучасному програмісту той самий рефлекс: спочатку сформулюй допустимий стан, потім пиши операцію.
| Axiom | Ada/SPARK ідея | Що спільного |
|---|---|---|
require | Precondition | Caller obligation |
ensure | Postcondition | Callee obligation |
invariant | Type/Loop invariant | Властивість зберігається |
| bounded values / contracts | Range / subtype constraints | Недопустимі значення відсікаються рано |
view + lifetime proof | accessibility/ownership discipline | Не дозволити dangling references |
| no recursion + memory reports | high-integrity resource reasoning | Bounded stack/resources |
| proof reports | GNATprove-style analysis | Діагностика як доказ, а не тільки warning |
Маленький приклад мислення
1percentage(i32 value) -> i32:2 require value >= 03 require value <= 1004 ensure result >= 05 ensure result <= 1006 RETURN valueТип i32 сам по собі занадто широкий для domain concept.
Передумови звужують допустимий domain.
Післяумови роблять гарантію функції доступною наступному caller-у.
Тіло тривіальне, але контракт формує semantic knowledge graph для решти програми.
Що читати далі в Ada
Коли вперше відкриєте Ada/SPARK, звертайте увагу не на багатослівний syntax, а на subtypes/ranges, contracts, tasking, strong typing, accessibility rules і GNATprove. Саме це — не «академічний шум», а інструменти для програм, де «майже завжди працює» недостатньо.
Кінцева ціль Axiom
Щоб web-розробник міг поступово дійти до драйвера, DSP, kernel або embedded-коду, не переходячи від безпечної високорівневої моделі до «тепер усе на pointer-ах і молитвах». Межі мають ставати нижчими, але правила — залишатися зрозумілими.