Ніколи не використовуйте Float або Integer#
переклад статті Never use Float or Integer, Марк Гермелінг, 18 березня 2026 р.
Якщо ви писали на C або C++, то знаєте, як легко використовувати
int або float під час оголошення змінної. Вони є робочими конячками
числового програмування: універсальні, звичні та завжди доступні, коли
вони вам потрібні. Але ця універсальність має приховану ціну: компілятор
абсолютно не має уявлення про те, що означають ваші числа , а це
означає, що він не може допомогти вам, коли ви помилитеся.
Ада дотримується іншої філософії. Типи мають значення, і це може
запобігати помилкам. У цій публікації досліджується, чому майже ніколи
не слід використовувати вбудовані в Аду типи Float або
Integer безпосередньо, і що використовувати замість цього.
Під час проектування вбудованих або кіберстійких систем діапазони вхідних та вихідних сигналів зазвичай відомі. Датчики пропонують лише фіксований діапазон, а виконавчі механізми також обмежені. Включення цих діапазонів до типів вхідних та вихідних сигналів системи має великий сенс з інженерної точки зору та запобігає проблемам у джерелі.
Проблема з узагальненими типами#
Розглянемо просту систему керування польотом, написану на C. Ви відстежуєте швидкість та висоту літака:
float speed = 250.0;
float altitude = 35000.0;
// Somewhere later...
speed = altitude; // Ой. Компілятору байдуже.
Компілятор успішно компілюється. Зрештою, обидві змінні мають тип
float . Але ви щойно присвоїли висоту у футах швидкості у вузлах
— логічна катастрофа, яка може не проявитися, поки ваша програма не
запуститься у продакшені (або в повітрі).
Така ж пастка існує і з цілими числами:
int passengers = 180;
int fuel_kg = 42000;
fuel_kg = passengers; // Компілятор: мене влаштовує!
У C та C++ немає механізму для їх розрізнення. З точки зору системи типів, кількість пасажирів та завантаження палива — це одне й те саме: число.
Можна було б розробити власний тип за допомогою класу в C++, але це дуже складний підхід, який вимагає додаткової роботи від розробника. Те саме обмеження стосується і Rust.
Відповідь Ади: Визначте типи, що відображають вашу область знань#
Ада заохочує вас визначати окремий тип для кожного окремого поняття у вашій програмі. Це не просто псевдоніми чи визначення типів — це справді несумісні типи, і компілятор забезпечує цю несумісність.
type Speed_Knots is new Float;
type Altitude_Feet is new Float;
type Passenger_Count is new Integer;
type Fuel_Kg is new Integer;
Тепер спроба випадкового присвоєння, описаного вище, стає помилкою під час компіляції:
Speed : Speed_Knots := 250.0;
Altitude : Altitude_Feet := 35000.0;
Speed := Altitude; -- ПОМИЛКА:
-- очікувався тип Speed_Knots,
-- отримано Altitude_Feet
Компілятор виявив вашу помилку ще до того, як було виконано хоча б один рядок машинного коду. Це основна перевага системи типів Ada: чим точніше ви описуєте свої дані, тим краще компілятор може перевірити вашу логіку.
І типи — це лише початок#
Ця стаття продовжиться детальним описом переваг системи типів в Ada, а також інструкціями щодо того, як легко оцінити це у вашому поточному середовищі розробки, а також на Raspberry Pi Pico.
Після огляду системи типів ми коротко торкнемося додаткових розширених можливостей Ada для статичної (під час компіляції) перевірки відсутності помилок під час виконання, а також перевірки функціональної коректності за допомогою її підмножини мови SPARK.
Додавання обмежень діапазону#
Визначення іменованих типів — це лише початок. Ada також дозволяє вам безпосередньо додавати допустимі діапазони значень до ваших типів. Ці обмеження можна перевірити під час компіляції (коли значення є константою) або під час виконання (без необхідності додаткового коду з вашого боку):
type Speed_Knots is new Float range 0.0 .. 1000.0;
type Altitude_Feet is new Float range 0.0 .. 60_000.0;
type Passenger_Count is new Integer range 0 .. 853; -- Airbus A380 max
type Fuel_Kg is new Integer range 0 .. 320_000;
Тепер типи не просто виражають, що представляє значення, вони також
виражають, які значення є допустимими. Призначте значення
-50.0 Speed_Knots, і Ada викличе Constraint_Error . Немає
додаткової логіки перевірки, не потрібні модульні тести для покриття
цього випадку, і немає невизначеної поведінки, як це було б із
цілочисельним переповненням у C.
Порівняйте це з C, де від'ємна швидкість — це просто від'ємне число з плаваючою комою. Вам потрібно буде писати власні перевірки, пам'ятати про їх виклик усюди та сподіватися, що ніхто не введе шлях коду, який їх обійде.
Підтипи для спеціалізації без нових типів#
Іноді потрібно ще більше звузити тип, не створюючи повністю несумісного нового типу. Підтип Ada ідеально підходить для цього:
subtype Cruising_Speed is Speed_Knots range 400.0 .. 900.0;
subtype Low_Altitude is Altitude_Feet range 0.0 .. 10_000.0;
Cruising_Speed все ще є Speed_Knots , тому ви можете використовувати
їх взаємозамінно там, де очікується
Speed_Knots, але будь-яка спроба зберегти значення поза діапазоном
крейсерської швидкості буде перехоплена. Це корисно для вираження
різних «режимів» або «станів», у яких може перебувати значення,
без шкоди для сумісності типів.
Більш повний приклад#
Ось коротка програма на Ада, яка демонструє ці ідеї разом:
with Ada.Text_IO; use Ada.Text_IO;
procedure Flight_Data is
type Speed_Knots is new Float range 0.0 .. 1000.0;
type Altitude_Feet is new Float range 0.0 .. 60_000.0;
type Fuel_Kg is new Integer range 0 .. 320_000;
type Passenger_Count is new Integer range 0 .. 853;
subtype Cruising_Speed is Speed_Knots range 400.0 .. 900.0;
subtype Cruising_Altitude is Altitude_Feet range 25_000.0 .. 45_000.0;
Current_Speed : constant Cruising_Speed := 550.0;
Current_Altitude : constant Cruising_Altitude := 35_000.0;
On_Board : constant Passenger_Count := 312;
Fuel_Remaining : constant Fuel_Kg := 58_000;
begin
-- Це буде помилка компіляції:
-- Current_Speed := Current_Altitude;
-- Це призведе до Constraint_Error під час виконання:
-- Current_Speed := 1_200.0;
Put_Line ("Speed: " & Current_Speed'Image & " knots");
Put_Line ("Altitude: " & Current_Altitude'Image & " feet");
Put_Line ("Passengers: " & On_Board'Image);
Put_Line ("Fuel: " & Fuel_Remaining'Image & " kg");
end Flight_Data;
Кожна змінна має тип, який кодує як її значення, так і допустимий
діапазон. Майбутній розробник, який читає цей код, дізнається не лише
те, що Current_Speed — це число, а й те, що це швидкість, що
вимірюється у вузлах, і що вона має бути в межах від 400 до 900 вузлів.
А як щодо продуктивності?#
Розробників C та C++ часто турбує, чи вся ця перевірка типів впливає на продуктивність. Відповідь: майже ніколи.
Обмеження діапазону, які можна застосовувати під час компіляції, повністю виключаються — компілятор бачить, що константа підходить, і не генерує жодної перевірки. Обмеження на змінні вводять інструкцію порівняння, з якою сучасні процесори можуть обробляти дуже ефективно. Тим часом ви виключаєте цілі класи помилок, які в іншому випадку вимагали б дорогої перевірки під час виконання, захисних перевірок або, що ще гірше, сеансів налагодження.
Компілятори Ada, такі як GNAT, також можуть генерувати код з вимкненими
перевірками для релізних збірок ( -gnatp ). Однак, філософія Ada
загалом надає перевагу тому, щоб залишати їх увімкненими.
Спробуйте самі з Alire#
Найшвидший спосіб запустити ці приклади — за допомогою Alire (вимовляється як «а-лір»), сучасного менеджера пакетів та інструменту збірки Ada. Якщо ви використовували Cargo в Rust або npm в JavaScript, Alire буде вам знайомий.
Встановіть Alire, завантаживши бінарний файл для вашої платформи з alire.ada.dev. Він містить власний набір інструментів GNAT, тому вам не потрібно окремо встановлювати компілятор.
Після встановлення, створення та запуск нового проекту Ada здійснюється за допомогою трьох команд:
alr init --bin flight_data # створення нового проєкту
cd flight_data
alr run # збірка та запуск за один крок
Alire створює файл src/flight_data.adb — вставте туди процедуру
Flight_Data з наведеного вище прикладу, а потім запустіть alr run ,
щоб побачити її в дії. Щоб навмисно викликати Constraint_Error ,
розкоментуйте призначення out-of-range та перебудуйте; ви точно
побачите, де і чому сталася помилка.
Alire також надає вам доступ до повного Alire Index , курованого каталогу бібліотек Ada — від криптографії та мереж до вбудованих середовищ виконання. Потрібна бібліотека? Це просто:
alr with <crate-name>
Ось і все. Ніяких ручних прапорців лінкера, жодних шляхів до заголовків, яких потрібно було б переслідувати. Для розробника C++, який звик боротися з системами збірки, ця частина варта ціни, яку ви заплатили.
Запуск Ada на Raspberry Pi Pico#
Сувора типізація Ada так само корисна на мікроконтролері, як і на
настільному комп'ютері — можливо, навіть більше, оскільки немає
операційної системи, яка б виявляла помилки. Файл flight_data.adb з
наведеного вище прикладу працює на Pico без змін; відрізняється лише
конфігурація збірки.
Почніть з того ж проєкту, який ви створили раніше, а потім додайте набір інструментів ARM та пакет підтримки плати Pico:
cd flight_data
alr toolchain --select # виберіть arm-elf при запиті
alr with pico_bsp # завантажує the RP2040 HAL, BSP та light runtime
Потім відкрийте flight_data.gpr та додайте два рядки всередині
оголошення проекту, щоб вказати gprbuild орієнтуватися на ARM, а не на
хост-машину:
for Target use "arm-eabi";
for Runtime ("Ada") use "light-cortex-m0p";
Ваш вихідний файл взагалі не потрібно змінювати. Зберіть за допомогою:
alr build
Це створить файл flight_data.uf2 у вихідному каталозі збірки. Щоб
прошити його, утримуйте кнопку BOOTSEL на Pico під час підключення
його до USB — він монтується як пристрій масової пам'яті. Перетягніть
на нього файл .uf2 , і Pico перезавантажиться та запустить вашу
програму. Вихід Put_Line з'явиться на UART0 (виводи GP0/GP1), який
можна зчитати за допомогою будь-якого послідовного монітора зі швидкістю
115200 бод.
Щоб повернутися до нативної збірки, видаліть залежність pico_bsp та
відновіть нативний ланцюжок інструментів:
alr with --del pico_bsp
alr toolchain --select # виберіть gnat_native, коли буде запропоновано
Той самий вихідний файл, дві цілі.
Одна важлива відмінність від Ada для настільних комп'ютерів :
полегшене середовище виконання Pico не має поширення винятків. Порушення
діапазону, яке може викликати Constraint_Error на вашому ноутбуці,
натомість викличе жорстку перехоплення помилки на Pico — процесор
зупиниться. На практиці це нормально для вбудованого коду (контрольована
зупинка краща, ніж пошкоджений стан), але це варто знати під час
налагодження. Ви можете підключити налагоджувач через контакти SWD Pico
та Picoprobe, щоб точно перевірити, де сталася перехоплення.
SPARK: Коли компілятор підтверджує правильність вашої програми#
Суворі обмеження типізації та діапазону є потужними, але вони все ще залишають недоторканими категорію помилок: логічні помилки, які є абсолютно коректними з точки зору типів, але функціонально неправильними. Функція, яка повертає правильний тип, але неправильне значення, пройде повз компілятор.
Саме тут і з'являється SPARK . SPARK — це формально перевірена
підмножина Ada, що підтримується інструментом GNATprove (доступним
від Alire через alr з gnatprove). Окрім статичного доведення
правильності типів та діапазонів, SPARK може математично довести, що
ваша програма не може демонструвати певні класи помилок — переповнення
буфера, ділення на нуль, недійсний доступ до масивів, непередбачений
потік даних — без виконання коду.
Ключовим механізмом є контракти : передумови, постумови та інваріанти, які ви приєднуєте до своїх підпрограм і типів. Ось приклад flight-data, розширений за допомогою контракту SPARK:
procedure Set_Speed (S : in out Speed_Knots; New_Value : Speed_Knots)
with
Pre => New_Value >= 0.0 and New_Value <= 1000.0,
Post => S = New_Value;
GNATprove зчитує ці контракти та намагається довести — статично, під час збірки — що кожен сайт виклику задовольняє передумову, і що тіло підпрограми фактично гарантує постумову. Якщо він не може щось довести, він точно повідомляє, яка умова не виконала свою роботу та на якому рядку, надаючи вам точну ціль для виправлення коду або додавання відсутнього інваріанта.
Практичний результат полягає в тому, що програми SPARK можуть досягти рівнів гарантії програмного забезпечення, що вимагаються такими стандартами, як DO-178C (авіоніка), ISO 26262 (автомобільна промисловість), EN 50128 (залізничний транспорт) та IEC 61508 (функціональна безпека) — областями, де помилка під час виконання є не лише дорогою, але й потенційно фатальною. Європейська система керування поїздами, частини програмного забезпечення для польоту F-35 та критичні компоненти комерційних літаків працюють на перевіреній SPARK базі даних Ada, як і основні частини програмного забезпечення на системах на кристалах NVIDIA.
Для розробника на C або C++ ментальна модель така: SPARK бере дисципліну типів, описану в цій публікації, і розширює її аж до доказів коректності. Ви не просто повідомляєте компілятору, які у вас дані — ви повідомляєте йому, що має робити ваш код, і інструмент перевіряє, чи він це дійсно робить.
Гарною відправною точкою є документація SPARK на сайті learn.adacore.com , яка проходить верифікацію від простих доказів діапазону до повної функціональної коректності.
Зміна мислення#
Перехід від C або C++ до дисципліни типів Ada є радше концептуальною, ніж синтаксичною зміною. У C ви схильні думати: «Який правильний примітивний тип для зберігання цього?». В Ada ви думаєте: «Що це за значення, і які правила його керують?».
Щойно ви почнете визначати типи, що відображають вашу предметну область, відбувається щось дивовижне: ваш код стає самодокументованим, ваші інтерфейси стає важче використовувати неправильно, а ваш компілятор стає активним співавтором, а не пасивним перекладачем.
Тож наступного разу, коли у вас виникне спокуса написати:
Speed : Float := 0.0;
Запитайте себе, що насправді представляє цей Float , і дайте йому
назву.
Додаткова література#
Система типів Ади виходить навіть далі, ніж те, що розглядається тут. Далі варто дослідити такі теми:
Модулярні типи — цілі числа, що обтікають у певному степені двійки, ідеально підходять для маніпулювання бітами.
Типи з фіксованою комою — точна десяткова арифметика без несподіванок округлення, характерних для чисел з плаваючою комою.
Теговані типи — підхід Ади до об'єктно-орієнтованого програмування з повною безпекою типів.
Контракти Ada (
Pre,Post,Type_Invariant) — додавання формальних умов коректності безпосередньо до ваших типів та підпрограм.Узагальнені типи — узагальнені типи Ada дозволяють вам писати безпечні для типів, повторно використовувані алгоритми та структури даних, параметризовані для будь-якого типу, без шкоди для гарантій строгого типізації, описаних у цій публікації. Уявіть собі шаблони C++, але з чітко визначеною семантикою та без несподіванок у заголовкових файлах.
Найкраще почати з learn.adacore.com , який пропонує безкоштовні інтерактивні курси Ada, починаючи від вступу для початківців і закінчуючи поглибленими темами з формальної верифікації.