LINUX.ORG.RU

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

 , refinement type, , ,


3

3

Я вот что подумал - почему вынесенные в заголовок штуки в основном применяются в ФП с жирным рантаймом 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 (всего исправлений: 2)
Ответ на: комментарий от pacer_gracyn

Это всё чушь нелепая запартная

Царь, у тебя есть высшее запартное математическое образование? Или опять полез не в свое царство?

anonymous
()
Ответ на: комментарий от AndreyKl

Тут тонкий момент в том что система типов в функциональных языках, она не с потолка.

Действительно.

По поводу которых довольно много известно хорошего (типа вот так точно можно, а вот так точно нельзя).

Нет, очевидно. В ФП системы типов нет - есть примитивный мусор. Там 2-3 типа и примитивный вывод.

Собственно из-за свой примитивности она и используется за партой. В нормальных языках есть мутации, а значит нужны мутации типов. Мутаций типов нет нигде.

В нормальных языках есть сложные условные конструкции, которые даже не выражения. Которые могут мутировать внешнее состояние, а значит и ты.

Т.е. flow-анализ для какой-нибудь сишки на порядок сложнее того же ФП-херни.

Есть системы верификации типа валгринда или рекламируемого тут часто для си++ чекера какого-то.

Система типов в С++ куда мощнее любой скриптухи, особенно хаскеля. Там уже есть завтипы. А значит какая угодно суперкомпиляция. Да и сам С++ состоит из суперкомпиляции на 99%.

Единственного чего в С++ - это ньютайпов. В связи с этим очень сложно аннотировать значения. Нужно костылять очень сильно, но в любом случае это в любом не работает.

Диспатч по чему угодно в С++ есть. Компилтайм логикой можно описывать отношения между типами. Точно так же как и сам диспатч. В типы можно записывать какую угодно информацию.

Проблема только одна - идентификация значений, т.е. отсутствие newtype, если автор это прям нужно - патч для шланга костылится за пару дней.

pacer_gracyn
()
Ответ на: комментарий от anonymous

Царь, у тебя есть высшее запартное математическое образование?

Я в яслях не образовываюсь.

Или опять полез не в свое царство?

С каких пор данная секта стала обладать монополией на это царство? Разве что в головах самих сектантов.

pacer_gracyn
()
Ответ на: комментарий от pacer_gracyn

Царь

Я

Вопросов больше не имею.

anonymous
()
Ответ на: комментарий от pacer_gracyn

Система типов в С++ куда мощнее любой скриптухи, особенно хаскеля. Там уже есть завтипы.

Шавка запартная, бегом мне побежала показывать, как пруфать что‐то на завтипах цепепе.

Покажи мне там: Π‐тип, Σ-тип, пропозициональное равенство. Можешь ещё унивалентность, если осилишь, петух.

Побежал, побежал, кал не растеряй.

anonymous
()
Ответ на: комментарий от anonymous

Шавка запартная, бегом мне побежала показывать, как пруфать что‐то на завтипах цепепе.

Шавка, побежала показывать как пруфвать что-то на завтипах в хаскеле и любой другой скриптухи.

К тому же, шавка, с чего ты взяла, что мне интересны какое-то твоё пруфанье запартное? С этим в школу, отребье.

Покажи мне там: Π‐тип, Σ-тип, пропозициональное равенство. Можешь ещё унивалентность, если осилишь, петух.

Шавка, со всей это чушнёй нелепой в школу. Это базворды для обезьян бездарных, которые кого-то за пределами твоей запарты не интересуют. Поэтому, падаль, зарылась бегом под шконку и не кукарекай.

anonymous
()
Ответ на: комментарий от anonymous

Шавка, побежала показывать как пруфвать что-то на завтипах в хаскеле и любой другой скриптухи.

А на хаскеле ничего толком и не попруфаешь, бездарность. Можно лишь немного костылей нагородить. На скриптухе — тем более.

К тому же, шавка, с чего ты взяла, что мне интересны какое-то твоё пруфанье запартное?

Потому что ты в математике — шлюха бездарная, но почему‐то очень важное мнение имеешь. Твой кукаретинг в сторону математики — беспруфное унылое говно тупого ПТУшника, который осилил математику на уровне квадратных уравнений. Побежал кал собирать за собой, псина тупая.

Заметим ещё, что ты, срущая под себя пыль, никаких пруфов не предоставила, поэтому твой кукаретинг — ещё беспруфный пук в воду тупого недоучки.

Это базворды для обезьян бездарных, которые кого-то за пределами твоей запарты не интересуют.

Ещё раз, недоученная падаль: ты в математике — полное дно, ноль, zero, днище, DNIWE. Стоит тебе только сунуться туда, ты обсираешься на каждом шагу, беспруфно кукарекая. Обтекай.

anonymous
()
Ответ на: комментарий от anonymous

А на хаскеле ничего толком и не попруфаешь, бездарность. Можно лишь немного костылей нагородить. На скриптухе — тем более.

Шавка, ты же мне что-то блеяло в ответ на:

Система типов в С++ куда мощнее любой скриптухи, особенно хаскеля. Там уже есть завтипы.

Теперь оказывается на хаскеле ничего нет. Ты совсем поехавшая?

Потому что ты в математике — шлюха бездарная, но почему‐то очень важное мнение имеешь.

Во-первых, шлюха, какое отношение ты имеешь к математике и что вообще такое, шлюха, математика? На каком основании ты, говно бездарное, позволяешь себе блеять от имени этой математики? Блеять, шлюха, оправдания. Бегом.

Твой кукаретинг в сторону математики — беспруфное унылое говно тупого ПТУшника, который осилил математику на уровне квадратных уравнений. Побежал кал собирать за собой, псина тупая.

Падаль, я жопу вытирал тобою. Это первое. Второе - меня не интересует и не должно интересовать твоё запартное говно. Твоя задача, падаль. Сидеть за партой, жрать говно и молиться на то, что тебя подберёт хозяин.

Блеять ты о чём-то в принципе не можешь. Оправдываться, говно.

Ещё раз, недоученная падаль: ты в математике — полное дно, ноль, zero, днище, DNIWE. Стоит тебе только сунуться туда, ты обсираешься на каждом шагу, беспруфно кукарекая. Обтекай.

Т.е. падаль не имея ответа начало блеять херню? Шлюха, тебе не это приказано было блеять. Тебе нужно блеять за то, какое отношения твоя бездарная рожа имеет к математике, на каком основании ты блеешь от её имени, на каком основании ты блеешь что-то обо мне, шлюха?

Бегом, блеять, говно, за то где и как я обосрался. Живо, мразь.

anonymous
()
Ответ на: комментарий от anonymous

Шавка, ты же мне что-то блеяло в ответ на:

Падаль тупая, читать научись.

Какая же ты тупая бездарность.

Теперь оказывается на хаскеле ничего нет. Ты совсем поехавшая?

Я тебя ткнул носом в зависимые типы цепепе, чмо нулевое, про хаскель ты заговорил. Ты, тупое говно, переводишь стрелки на хаскель, когда твоё цепепе ничего не умеет.

Во-первых, шлюха, какое отношение ты имеешь к математике и что вообще такое, шлюха, математика?

Во-первых, говно, тебя вообще волновать не должно, какое я отношение имею к математике. Тебя должно лишь волновать, что ты не умеешь в математику и даже не знаешь, что это такое:

что вообще такое, шлюха, математика?

Но почему‐то имеет очень веское мнение о вещах вроде зависимых типов, петух.

Блеять, шлюха, оправдания. Бегом.

Приказывать своей собаке будешь, собака.

Падаль, я жопу вытирал тобою.

И это очевидная ложь, потому что ты обосранный всегда, следовательно, ты жопу никогда не вытираешь.

Второе - меня не интересует и не должно интересовать твоё запартное говно.

А меня не интересует, что не интересует тупую падаль вроде тебя. Мне только не нравится, что тупая падаль лезет туда, куда её не просили. Вылезай, падаль.

Т.е. падаль не имея ответа начало блеять херню?

Это ты, шлюховатая падаль, на запрос показать примеры использования завтипов внезапно пукнул, что пруфы не нужны, слившись окончательно. Говно, примеры показывай, иначе ты только беспруфное говно.

Тебе нужно блеять за то, какое отношения твоя бездарная рожа имеет к математике

Ещё раз, бездарное тупое чмо: про зависимые типы в цепе заговорил ты, но показал ты ничего. Своё отношение к математике показывать должен ты, ублюдок. Но ты ничего показать не можешь, ты полная бездарность.

Бегом, блеять, говно, за то где и как я обосрался.

Обосрался ты себе в штаны, но ты даже этого не можешь осознать.

anonymous
()
Ответ на: комментарий от anonymous

Я тебя ткнул носом в зависимые типы цепепе, чмо нулевое, про хаскель ты заговорил. Ты, тупое говно, переводишь стрелки на хаскель, когда твоё цепепе ничего не умеет.

переводишь стрелки на хаскель

Смотрим на потугу данной шлюхи:

Система типов в С++ куда мощнее любой скриптухи, особенно хаскеля. Там уже есть завтипы.

Шавка запартная, бегом мне побежала показывать, как пруфать что‐то на завтипах цепепе.

Т.е. шавка цитировало то, где уже был хаскель. Что же блеет теперь это говно?

переводишь стрелки на хаскель

Шлюха опущена.

Теперь по поводу «ничего не умеет». Шлюха не показало ничего, чего цпп не умеет. Шлюха непонтно зачем начало блеять про свои запартные пруфы. Я, конечно, понимаю, что падаль вчера об этом услышала за партой. Но меня это не волнует.

Завтипы никакого отношения к запартным пруфам не имеют. Запартные пруфы - это лишь загончик для бездарного запартного биомусора. Хотя данная шавка даже к этому загону отношения не имеет. К тому же даже про пруфы эта падаль не блеяла - она начала блеять базвордами услышанными запартой, с первой ссылки из гугла.

Это говно никакого отношения к завтипам так же не имеет. Шлюха обделалась.

Хотя после того как шлюха обделалась с хаскелем - обсуждать что-то далее не имеет смысла.

anonymous
()
Ответ на: комментарий от anonymous

Т.е. шавка цитировало то, где уже был хаскель.

Шавка запартная, бегом мне побежала показывать, как пруфать что‐то на завтипах цепепе.

Где ты тут слово «Haskell» увидел, говно? Я про цепепе говорил, бездарность запартная.

Шлюха не показало ничего, чего цпп не умеет.

Шлюха, сначала покажи, что цепепе умеет. Я вот не вижу Π-типа в цепепе. То, что ты, тупая шлюха, считаешь его баззвордом, говорит лишь о твоей тупости, необразованности и ограниченности.

Запартные пруфы - это лишь загончик для бездарного запартного биомусора.

То есть ты даже не знаешь, о чём говоришь, петух? Оправдываться побежал.

К тому же даже про пруфы эта падаль не блеяла

Шавка запартная, бегом мне побежала показывать, как пруфать что‐то на завтипах цепепе.

Жирным выделил для даунов. Падаль тупая, от онанизма ослеп уже?

Это говно никакого отношения к завтипам так же не имеет.

Π‐тип — одно из оснований нормальной системы с зависимыми типами. Ты, тупая шлюха, этого почему‐то не понимаешь.

Давай, покажи уже что‐то. Ты так ничего и не показал, петух, но всё беспруфно кукарекешь.

anonymous
()
Ответ на: комментарий от anonymous

Где ты тут слово «Haskell» увидел, говно? Я про цепепе говорил, бездарность запартная.

Шавка, чего же ты не полностью цитируешь? Бегом, падаль, побежала показывать то, что ты цитировала когда отвечала. И был ли там хаскель, либо нет.

Π‐тип — одно из оснований нормальной системы с зависимыми типами.

Смотрим, здесь уже шлюха пошла вилять жопой.

нормальной системы с зависимыми типами

Появился какой-то базворд «нормальной». Оказывается, всё это говно ненужно, но шлюха ищет пути к отступлению, называя всё, где нету этого примитивного мусора о котором он услышал в интернете - ненормыльным.

Уже можно фиксировать рожу у этой мрази в говне.

Π‐тип

Никаких «Π‐тип» не существует. Это мусорный базворд из скриптухи, где системы типов нету в принципе. Это говно не имеет никакого отношения к завтипам.

В общем, падаль. Бегом побежала блеять и показывать то, чего не умеет С++. И показывать не просто блеянием, а конкретно.

anonymous
()

Spark из Ada не на эту тему случаем?

dave ★★★★★
()
Ответ на: комментарий от x3al

Хаскель просто потому что для него есть суперкомпилятор. А так да.

AndreyKl ★★★★★
()
Ответ на: комментарий от SZT

По сути суперкомпиляция это ..

Вот тут у Романенко (одного из виднейших специалистов по суперкомпиляции, тоже сотрудник им. Келдыша) есть статьи. https://sergei-romanenko.github.io/scp-notes-ru/

Некоторые из них обзорные. Например, вот эту я читал и понять не сложно.

https://sergei-romanenko.github.io/scp-notes-ru/01-what-is-scp.html

Более того у него есть маленькие суперкомпиляторы на идрисе, агде, и ещё чём то, емнип: https://github.com/sergei-romanenko

И кажется всё просто в суперкомпиляции. Но судя по тому что санки не осилили её для явы. И судя по тому что саймон джонс писал про написание суперкомпилятора для хаскеля, эта проста обманчива.

AndreyKl ★★★★★
()
Ответ на: комментарий от x3al

Не, частичные вычисления — это немного про другое.

если мне не изменяет память то кто то из корифеев суперкомпиляции писал как маркетинговый лозунг что то такое «суперкомпиляция = дефорестрация + частичные вычисления».

так что не совсем таки про другое :)

AndreyKl ★★★★★
()
Ответ на: комментарий от SZT

да, и говорят суперкомпилятор хаскеля работает просто жутко медленно. Просто жутко.

AndreyKl ★★★★★
()

Я вот что подумал - почему вынесенные в заголовок штуки в основном применяются в ФП с жирным рантаймом GC? Это ж вполне можно и в более нормальных языках заюзать.

например, Ада: range types, subtypes

anonymous
()

Можно на каком-то языке описать, что алгоритм двоичного поиска, если ему на вход подать сортированный массив, он там сможет найти некий элемент если он там точно есть и не найти если его нет. А если ему несортированный массив подать (т.е. для которого нет свойства что a[n] <= a[n+1] для всех n от 0 до размермассива) то тогда это уже неверно, т.е. должна быть ошибка компиляции, если мы не проверенные на сортированность данные пускаем на вход к двоичному поиску

контракты и контрактное программирование в той же Аде, GNAT компилятор (GCC)

anonymous
()
Ответ на: комментарий от anonymous

например, Ада: range types, subtypes

А оптимизировать на основе них оно умеет? Эти range types, subtypes надо руками всегда прописывать, или оно само может что-то выводить?

SZT ★★★★★
() автор топика

Почему нет нормального компилируемого в натив языка без жирного рантайма с GC, чтоб там можно было вот так специфицировать поведение функций, допустимые входные параметры, кванторы-шманторы там, чтоб это все проверялось и оптимизировалось на основе спецификации-контрактов?

есть, это Ada + SPARK (формально верифицируемое подмножество Ады)

И чтоб с суперкомпиляцией!

тут уже сложнее. бери Рефал (или здесь,IDE) (или сделай свой собственный), читай книжки и статьи Турчина , лекции и публикации, ещё, лекции по суперкомпиляции из блога, ещё sz презентации заметки,ещё,>> meta2012, meta2016 и закатывай солнце вручную.

вообще, кажется вот это

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

можно и на символах лиспа изобразить (и чтобы к значениям с тегированными типами прикреплять свойства через alist списки пар символ, значение)

соответственно вот это

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

реализовать через макрос, который пишет макрос и compiler macro.

как на это может выглядеть си, я не знаю.

но например отсюда на Idris: слайды гитхаб

вообще рекомендую перечитать все публикации Турчина и его учеников (Климова, Романенко).

anonymous
()
Ответ на: комментарий от SZT

руками надо прописывать диапазоны. умеет выводить что результат выражения получится в другом диапазоне. если выйдет за диапазон, бросит исключения. контракты могут быть не только в рантайме но и во время компиляции, что результат гарантированно будет в другом диапазоне.

складывать яблоки с апельсинами, например нельзя – это разные типы. но можно ввести подтип (количество в штуках), и приводить к одному подтипу. то есть: разные типы, разные операции; подтипы приводятся к нужному автоматически, одинаковые операции.

подтипы выводить и диапазоны приводить умеет (рантайм и компилятор Ады).

anonymous
()
Ответ на: комментарий от anonymous

вообще, кажется вот это

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

можно и на символах лиспа изобразить

или на зависимых типах (см. в слайдах про сравнение Idris и рефала)

также см. про linear typing и model checking.

anonymous
()
Ответ на: комментарий от SZT

в Аде есть ещё ASIS= Abstract Ada Syntax and Semantic Interface specification.

то есть:

  1. посредством ASIS (библиотеки на Аде) можно разбирать AST программ на Аде

  2. для рефлексии и кодогенерации годится не совсем, или совсем не годится. в основном, для того чтобы проверить например что определённый оператор в определённом блоке точно не встретится, если да – через прагму бросать ошибку времени компиляции

  3. это может быть в контрактах или в SPARK (формально верифицируемое подмножество Ады).

  4. есть libadalang на LLVM и проч., реализация Ады на LLVM а не только GNU GNAT. то есть, кодогенерировать в принципе возможно но более трудоёмко.

  5. ASIS не только про синтаксис, но и семантику. которую можно расширять, проверять на ошибки во время компиляции и самому задавать что считать ошибкой. то есть использовать в качестве трейта из D «этот код компилируется».

anonymous
()

кстати, через трейт «этот код компилируется» можно в D реализовать, только подумать надо с примерами.

anonymous
()
Ответ на: комментарий от anonymous

string mixin, template mixin в D позволяют сконструировать такой код и проверить трейтом, что компилируется без ошибок

ещё в Nim есть AST макросы (Nim с синтаксисом питона, семантикой паскаля +С++ компилируется в C, рантайм зависит от GC, но GC там вроде написан на самом Nim и можно заменить на стаб как в D или выкинуть и не использовать, переписав рантайм).

anonymous
()
Ответ на: комментарий от anonymous

отсюда:

 
The current implementation of Typed Assembly Language, TALx86, is based on Intel's IA32 architecture. This implementation extends the theoretical calculi described in our papers and provides support for sums, arrays, references, recursive types, subtyping, type tagging, and modules, among other features. Our distributions contain our Objective Caml source code and executables for the following: 
 
* TAL tools including a type-checker for the assembly language. 
* Popcorn: A prototype compiler for a safe C-like language. 
* SCHEME--: A prototype compiler for a subset of the scheme language (written in Popcorn). 

anonymous
()
Ответ на: комментарий от anonymous

также см. про linear typing

Linear TAL: A linearly typed variant of TAL that manages its own memory through linear alias tracking.

anonymous
()
Ответ на: комментарий от SZT

пропессор же

некий функциональный язык который непойми как в сишку оттранслируется

приплюснутую, ога.

дважды заслуженный

бложик фильтровать по HN

anonymous
()
Ответ на: комментарий от SZT

и доказывать, что программа никогда за лимиты не вылезет т.е. невозможность ситуации что malloc где-то вернет NULL

см. linear TAL про linear typing

anonymous
()
Ответ на: комментарий от SZT

Кстати можно и нейросетки к этому присобачить, чтоб они там доказательства придумывали и оптимизировали

и будут доказательства на 10500 страниц которые никто ниасилит

Синьити Мочидзуки машинно сгенерированный корчевателем :))

anonymous
()
Ответ на: комментарий от olelookoe

нет ровным счетом ни-че-го, кроме тех данных, которые мы верифицируем на этапе компиляции, и которыми манипулируем неизвестно зачем.

и метаданных. и интерфейсов. времени компиляции.

и если например побочные изменения конкретизировать через монады или коэффекты (дуальные к ним комонады и контексты), и потом задавать явно. то получим формально проверяемые окружения (контексты коэффектов), побочные эффекты (коэффекты), исчисления этих эффектов (комонады).

anonymous
()
Ответ на: комментарий от qulinxao3

ну например см. в EiffelStudio AutoTest визард который по контрактам автоматически генерирует тесты, ими затронутые.

вопрос цены

цена меньше, чем с полным деревом тестов – генерируется поддерево

anonymous
()
Ответ на: комментарий от anonymous

GADT in ATS

This example of GADT usage in ATS tries to implement a sprintf function that allows providing a format specification to sprintf which then processes it and accepts arguments of types as defined by the format specification.

anonymous
()
Ответ на: комментарий от anonymous

вообще на прологе легко пишется DCG парсер

anonymous
()

Кмк, эта проблема устраняется на этапе тестирования и зависит от полноты тестов, когда SIGFPE возникнет при подаче тестовых входных данных, перекрывающих данный случай.
Попытка уберечь скомпилированный код от потенциальных ошибок запретом компиляции всяких подозрительных случаев пахнет преждевременной оптимизацией и необходимостью в каком-то ИИ.
Потенциальный SIGFPE в подобном более сложном случае может быть перекрыт добрым десятком условных оберток и превращается в нагромождение вероятностей. А компилятор уже заранее обделается и убежит от твоего кода, так и не дав тебе узнать, что же случится на самом деле.

blexey ★★★★★
()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.