LINUX.ORG.RU

Избранные сообщения Jini

refinement type, формальная верификация в нефункцональных языках?

Форум — Development

Я вот что подумал - почему вынесенные в заголовок штуки в основном применяются в ФП с жирным рантаймом 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;
    }
  }
То тогда норм. Вот я хочу, чтобы код в котором может возникнуть ошибка SIGFPE из-за поступления внешних непроверенных данных — вообще не компилировался.

Надо значит цеплять какие-то условия к данным (массивам, переменным) т.е. отслеживать их историю эволюции, выводить на основе этого некие свойства.

Ну и это еще можно использовать для оптимизации, скажем если мы отсортировали некий массив, то потом если мы пытаемся его отсортировать второй раз подряд, то во-первых можно вывести предупреждение от компилятора «этот массив и так сортирован, нечего его сортировать» а во-вторых можно просто вызов сортировки выкинуть т.к. он ничего не делает. Ну и кроме того, есть алгоритмы которым обязательно сортированные данные нужны, например это алгоритм двоичного поиска. Можно на каком-то языке описать, что алгоритм двоичного поиска, если ему на вход подать сортированный массив, он там сможет найти некий элемент если он там точно есть и не найти если его нет. А если ему несортированный массив подать (т.е. для которого нет свойства что 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, чтоб там можно было вот так специфицировать поведение функций, допустимые входные параметры, кванторы-шманторы там, чтоб это все проверялось и оптимизировалось на основе спецификации-контрактов? И чтоб с суперкомпиляцией!

 , , , ,

SZT ()

А есть нормальная и адекватная литература по структурам данных и алгоритмам

Форум — Development

Собственно потребовалось ручками реализовывать разные деревья, решил книжки посмотреть, а там непотребство пишут - даже на простых вещах обсираются по полной, как пример путают Tree Sort с поиском по BST дереву, хотя Tree Sort в общем случае вполне себе работает с данными, которые дублируются, т.к. работает с частично-упорядоченными бинарными деревьями, а не с BST деревьями, которые по определению полностью упорядоченные.

 , ,

peregrine ()

Композитор для Wayland на Common Lisp

Форум — Development

Сабж пока только работает на SBCL:

https://github.com/malcolmstill/ulubis

 , , ,

Oxdeadbeef ()

ИИ в стратегиях реального времени.

Форум — Development

Что учить что бы написать интеллект для ботов? Что то типа Red Alert 2 .

knotri ()