Действительно, для Z стоило бы сделать отдельный тип, потому что граничные условия будут другие. Видимо автор не стал копать слишком глубоко )
У него есть другая статья, где он написал Тетрис на Аде на встраиваемой платформы. Там он уже развернулся хорошо
In SPARK, things are more complicated: PID functions do some calculations over the inputs, like calculating the error between the measured angle and the desired one. We’ve seen that, without any information about input ranges, it’s very difficult to prove the absence of runtime errors on calculations, even over a basic one like an error calculation (Error = Desired – Measured). In other words, we can’t implement a general PID controller using the Ada Float type if we intend to prove it with SPARK.
The good practice here is to use Ada generics: by creating a generic PID package using input, output and PID coefficient ranges as parameters, SPARK will analyze each instance of the package with all information needed to prove the calculations done inside the PID functions.
Речь идет о следующем разделе, где он ограничивает нагрузку на двигатели. Он так и пишет, что для введения ограничений для типов данных лучше использовать обычный язык Ада (вход, выход и коэффициенты контроллера PID), а дальше уже работает система контрактов SPARK: доказать, что с учетом этих ограничений все остальное будет работать правильно.
Как я понял, SPARK работает на этапе сборки кода, и поскольку он полностью исключает ошибки времени выполнения, exceptions тогда действительно не нужны.
Но ладно, это его выбор :)
Существеннее другое, что в коде присутствует потенциально критическая ошибка, которую как раз можно было отловить средствами типизации.
Поглядите внимательно на следующие строки:
253 Rate_Change_Gy : T_Float_4 := Rad_Gy;
254 Rate_Change_Gz : T_Float_4 := Rad_Gy;
Функция вычисления скоростей изменений координат по осям. Начальная инициализация Gy и Gz делаются одним значением текущего роложения по оси Y. Это может так дрон крутануть, что мало не покажется :)
А если здесь для оси Z применить выделенный тип - то компилятор легко отследит подобную описку. Тем более, что это оправданно. X и Y могут меняться в пределах 0..2*Pi, а для Z вполне разумно сделать ограничение по отрицательным отклонениям, что бы дрон вверх ногами в землю не пошел.