Я вот что подумал - почему вынесенные в заголовок штуки в основном применяются в ФП с жирным рантаймом GC? Это ж вполне можно и в более нормальных языках заюзать.
Ну вот допустим будет некий язык с Си-подобным синтаксисом, пусть там пользователь вводит массив чисел с клавиатуры, ну как-то так
uint32_t a[100];
for (size_t i = 0; i < 100; i++)
{
if ( scanf("%" SCNu32 "\n", &a[i]) != 1)
{
exit(-1);
}
}
Вот после этого for цикла (если не произошло exit (-1)) в массиве a[100] образовались какие-то там данные, нам про них ничего в точности неизвестно, там пользователь что попало мог ввести.
Скажем, если мы после этого сделаем такое:
for (size_t i = 0; i < 100; i++)
{
printf("%" PRIu32 "\n", 100500 / a[i]);
}
a[i] может быть 0 и будет SIGFPE.А если например перед этим сделать нечто такое
for (size_t i = 0; i < 100; i++)
{
if(a[i] == 0)
{
a[i] = 1;
}
}
Надо значит цеплять какие-то условия к данным (массивам, переменным) т.е. отслеживать их историю эволюции, выводить на основе этого некие свойства.
Ну и это еще можно использовать для оптимизации, скажем если мы отсортировали некий массив, то потом если мы пытаемся его отсортировать второй раз подряд, то во-первых можно вывести предупреждение от компилятора «этот массив и так сортирован, нечего его сортировать» а во-вторых можно просто вызов сортировки выкинуть т.к. он ничего не делает. Ну и кроме того, есть алгоритмы которым обязательно сортированные данные нужны, например это алгоритм двоичного поиска. Можно на каком-то языке описать, что алгоритм двоичного поиска, если ему на вход подать сортированный массив, он там сможет найти некий элемент если он там точно есть и не найти если его нет. А если ему несортированный массив подать (т.е. для которого нет свойства что a[n] <= a[n+1] для всех n от 0 до размермассива) то тогда это уже неверно, т.е. должна быть ошибка компиляции, если мы не проверенные на сортированность данные пускаем на вход к двоичному поиску
Вообще, есть такой GNU экстеншен __builtin_unreachable() и им можно например такую ерунду вытворять https://godbolt.org/z/dN6ozS
#define ALWAYS_FALSE(a) if(a) __builtin_unreachable()
#define ALWAYS_TRUE(a) ALWAYS_FALSE(!(a))
unsigned div_eq(unsigned a, unsigned b)
{
ALWAYS_TRUE(a == b);
ALWAYS_TRUE(a != 0);
return a/b;
}
unsigned div(unsigned a, unsigned b)
{
return a/b;
}Ну и тут вариант div_eq оптимизируется до return 1; (шланг неосиливает) - но это все костыли. И язык аннотаций из Frama-C это тоже костыли - из них такую оптимзацию не сделать, это внешний костыль для проверки контрактов.
Почему нет нормального компилируемого в натив языка без жирного рантайма с GC, чтоб там можно было вот так специфицировать поведение функций, допустимые входные параметры, кванторы-шманторы там, чтоб это все проверялось и оптимизировалось на основе спецификации-контрактов? И чтоб с суперкомпиляцией!
