Здравствуйте, Pavel Dvorkin, Вы писали:

PD>Не согласен. Если есть способ избавиться от проблемы, то ИМХО решать ее не надо, а надо именно избавиться. Других проблем хватит, от которых избавиться так просто не удастся.

Проблемы возникают на разных уровнях. Для кого-то самая сложная проблема — продать программу. Для кого-то — разработать быстрый алгоритм. Для меня (на уровне языкостроения) важна проблема переполнения.

ARK>>Лично мне нравится такая цель — создание корректного ПО. Гарантированно корректного, а не с некоторой вероятностью. Под корректностью в данном контексте я понимаю отсутствие ошибок времени исполнения.
PD>А в том, что я предложил, именно эта цель и достигается.

Боюсь, что нет. Формальных гарантий ваш способ не дает.

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

Задача эта решается, и в первом посте темы приведен пример программного пакета, решающего ее (SPARK). Есть и другие разработки.

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

Вот мне и хочется корректности, но чтобы без очень больших усилий. С большими усилиями это уже сейчас реально.

PD>Мало ли какие абстрактные ситуации могут быть... Например, можно пообсуждать, как обеспечить работу программы при адресном пространстве в 64 Кбайта, каким оно и было во времена первых микропроцессоров. Тогда для того, чтобы программы уложить в эту память, придуманы были различные методики, о которых сейчас никто уже и не помнит, так как проблема самоликвидировалась. Нет ее, и решать незачем.

Проблема есть, просто она на практике не часто возникает.

Здравствуйте, AlexRK, Вы писали:

ARK>Боюсь, что нет. Формальных гарантий ваш способ не дает.

То есть ? Если результат заведомо укладывается в сетку — какие еще гарантии ?

ARK>Вот мне и хочется корректности, но чтобы без очень больших усилий. С большими усилиями это уже сейчас реально.

А можно поинтересоваться, что за реальная такая задача, что нужно эту проблему решать , и иначе ее решить нельзя ? Что из себя представляют эти целые числа, о чем речь ?

Здравствуйте, Pavel Dvorkin, Вы писали:

ARK>>Боюсь, что нет. Формальных гарантий ваш способ не дает.
PD>То есть ? Если результат заведомо укладывается в сетку — какие еще гарантии ?

В С++ (и всех остальных мейнстримовых языках) ответственность за "заведомо укладывается в сетку" лежит на программисте, а иногда даже и на пользователе.
Я хочу, чтобы эта ответственность лежала исключительно на компиляторе.

PD>А можно поинтересоваться, что за реальная такая задача, что нужно эту проблему решать , и иначе ее решить нельзя ? Что из себя представляют эти целые числа, о чем речь ?

Реальная задача — создание языка программирования, не допускающего создания программ, содержащих потенциальные арифметические переполнения.

A>>В C# поведение можно изменять опциями checked-unchecked:
A>>http://msdn.microsoft.com/en-us//library/a569z7k8.aspx
A>>Довольно удобно и наглядно, кстати.

ARK>Ну окей, будет либо как в С++, либо с проверками. C# я привел
ARK>просто в качестве примера подхода к "решению" проблемы переполнения
ARK>(на самом деле, никакое это не решение).

Тогда надо "проблему" более чётко сформулировать

Кстати, для C# есть ещё и контракты:
http://research.microsoft.com/en-us/projects/contracts/

Здравствуйте, andy1618, Вы писали:

A>Тогда надо "проблему" более чётко сформулировать

В принципе, я интересуюсь любой информацией на тему. Конкретные языки рояля не играют, главное — принятые там решения.

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

A>Кстати, для C# есть ещё и контракты:
A>http://research.microsoft.com/en-us/projects/contracts/

Да, я в курсе. Смесь compile-time (только примитивные случаи) и run-time проверок.

Здравствуйте, AlexRK, Вы писали:

ARK>Видимо, я хочу невозможного и только искусственный интеллект может помочь.

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

Здравствуйте, Erop, Вы писали:

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

Да, именно такой вариант применяется в статических анализаторах типа Frama-C или Perfect Developer — причем они сами расставляют эти assert'ы, а потом решатель теорем выводит, какие из них безопасны в рантайме, а какие нет.

В принципе, этот вариант неплох, но у него есть два серьезных недостатка.
Во-первых, это очень тяжелый процесс, конпеляция больших проектов С++ на фоне этого — сущая мелочь .
Во-вторых (и это даже главнее) — опять же выходит сильная зависимость от конкретной реализации метода.

Было так:

int foo()
{
  return 2000000000;
}

...

int i = foo();
int j = Int32.Parse(Console.ReadLine());

// i = i + j;  // тут анализатор предупреждает об опасности
// поэтому ставим иф
if (j < 100000)
  i = i + j;
else
  ...

Потом поменяли библиотечную функцию foo:

int foo()
{
  return Int32.MaxValue - 1;
}

...

int i = foo();
int j = Int32.Parse(Console.ReadLine());

if (j < 100000)
  i = i + j;  // опять наш код сломался, нужен уже более сильный иф
else
  ...

Здравствуйте, AlexRK, Вы писали:


ARK>А вот для абстрактных функций типа "сумма всех элементов массива целых чисел" — тут уже ни входные параметры, ни выходные ничего не значат. Но таких функций, думаю, не очень много.

Они могут быть шаблонными какими-то, и компилятор сможет подставить на вход и на выход какие-то внешние условия и как-то распространить их.

Здравствуйте, AlexRK, Вы писали:

ARK>Во-первых, это очень тяжелый процесс, конпеляция больших проектов С++ на фоне этого — сущая мелочь .
ARK>Во-вторых (и это даже главнее) — опять же выходит сильная зависимость от конкретной реализации метода.

Тут может тоже быть компромисс.
Главное отказаться от автоматической расстановки assert'ов. Пусть программист пишет из соображений своего понимания программы, а автомат показывает, где он может доказать assert статически, при предположении верности остальных, где не может, типа это нужно использовать, как аксиомы, а где теорема слишком сложна для автоматического вывода...

assert'ы тоже можно маркировать в коде какие мы подразумеваем, как вводные (аксиомы), какие, как теоремы, которые хорошо бы доказать, а какие как теоремы, которые доказать обязательно, типа критический участок ну и обработка провала в RT тоже может настраиваться...

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

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

на практике нужно обрабатывать довольно дикий и слабо ограниченный поток данных и/или событий.
Эти данные/события в процессе вычислений над ними будут с близкими к 100% шансами порождать (теоретически и иногда практически) возможные переполнения.

Здравствуйте, Erop, Вы писали:

E>Главное отказаться от автоматической расстановки assert'ов. Пусть программист пишет из соображений своего понимания программы, а автомат показывает, где он может доказать assert статически, при предположении верности остальных, где не может, типа это нужно использовать, как аксиомы, а где теорема слишком сложна для автоматического вывода...
E>assert'ы тоже можно маркировать в коде какие мы подразумеваем, как вводные (аксиомы), какие, как теоремы, которые хорошо бы доказать, а какие как теоремы, которые доказать обязательно, типа критический участок ну и обработка провала в RT тоже может настраиваться...

Такой вариант, конечно, возможен...

Но щас я думаю о чем-то "бескомпромиссном".

Крутится мысль о выносе в сигнатуру функции некоторой дополнительной информации о числовых параметрах. Этакие "типы для числовых типов", но не просто диапазоны.

Может быть что-то вроде

T foo(U parameter) where T : Integer, U : Integer, T > U

где "T > U" это выражение некоторого порядка над типами. Ну и какая-то простая алгебра над всем этим. Типа того, что одна функция "повышает порядок" значения, другая — понижает его, третья не меняет... И на основе этого какой-то простой value analysis для всех путей каждого значения... Хз, может это все утопия, конечно.

Здравствуйте, AlexRK, Вы писали:


ARK>где "T > U" это выражение некоторого порядка над типами. Ну и какая-то простая алгебра над всем этим. Типа того, что одна функция "повышает порядок" значения, другая — понижает его, третья не меняет... И на основе этого какой-то простой value analysis для всех путей каждого значения... Хз, может это все утопия, конечно.

Просто попробуй какие-нибудь реальные программы так разметить -- поймёшь насколько это жизненно или нет...

Здравствуйте, dilmah, Вы писали:

D>на практике нужно обрабатывать довольно дикий и слабо ограниченный поток данных и/или событий.
Не всегда.

D>Эти данные/события в процессе вычислений над ними будут с близкими к 100% шансами порождать (теоретически и иногда практически) возможные переполнения.
Это в ненадёжных программах так. В надёжных неудачные данные можно обрабатывать как-то особо. В любом случае запланированно обрабатывать особую ситуацию, намного надёжнее, чем в режиме "как получится, так и хорошо"

Здравствуйте, AlexRK, Вы писали:

ARK>Может быть есть иные подходы обработки переполнений? Хочется вариант с полной скоростью и полной надежностью, но не такой сложный в использовании, как контракты из SPARK.
Можно оставить как Python'е но сделать компилятор(jit) достаточно "умным" чтобы он, анализируя код, мог рассчитать сколько потребуется памяти для результата. Но это, мягко говоря, сложная задача
Ну а для идеального случая(просто, с полной скоростью и полной надежностью) думаю эта задача не разрешима, т.к. числа бесконечны, а память компьютера нет.

Здравствуйте, C.A.B, Вы писали:

CAB>Можно оставить как Python'е но сделать компилятор(jit) достаточно "умным" чтобы он, анализируя код, мог рассчитать сколько потребуется памяти для результата. Но это, мягко говоря, сложная задача

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

CAB>Ну а для идеального случая(просто, с полной скоростью и полной надежностью) думаю эта задача не разрешима, т.к. числа бесконечны, а память компьютера нет.

Разрешима, разрешима. Только сильно геморройно это.

Здравствуйте, Erop, Вы писали:

E>Здравствуйте, AlexRK, Вы писали:


ARK>>где "T > U" это выражение некоторого порядка над типами. Ну и какая-то простая алгебра над всем этим. Типа того, что одна функция "повышает порядок" значения, другая — понижает его, третья не меняет... И на основе этого какой-то простой value analysis для всех путей каждого значения... Хз, может это все утопия, конечно.

E>Просто попробуй какие-нибудь реальные программы так разметить -- поймёшь насколько это жизненно или нет...

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

Здравствуйте, AlexRK, Вы писали:

ARK>А еще лучше обсудить не существующие языки, а теоретические подходы к решению проблемы.

Ну тогда лучший путь — почитать научные публикации. Довольно неплохой список, кстати,
как раз приведён в той же самой ссылке на контракты:

A>>http://research.microsoft.com/en-us/projects/contracts/

Раздел "Publications" внизу. Кстати, судя по названиям конференций, этим плотно занимаются
уже не один десяток лет:
"Proceedings of the 14th Conference on Verification, Model Checking and Abstract Interpretation"
"Proceedings of the Verified Software: Theories, Tools, and Experiments"
"Proceedings of the 3rd workshop on Numerical and Symbolic Abstract Domains"
"Proceedings of the Conference on Formal Verification of Object-oriented Software"
"Proceedings of the 17th international conference on Static analysis"
и т.д.

CAB>>Можно оставить как Python'е но сделать компилятор(jit) достаточно "умным" чтобы он, анализируя код, мог рассчитать сколько потребуется памяти для результата.
ARK>На самом деле не такая и сложная, другой вопрос, что результаты будут весьма обескураживающими — на выходе всех путей большинство значений будет иметь громадные "потенциальные" диапазоны.
Посему простого обхода путей не достаточно, нужно ещё и трассировать их для всех возможных наборов входных значений программы, затем чтобы точно определить максимум необходимой памяти для каждого результата.

CAB>>Ну а для идеального случая(просто, с полной скоростью и полной надежностью) думаю эта задача не разрешима
ARK>Разрешима, разрешима.
Не думаю, так как в некоторых случаях не возможно заранее определить сколько памяти займёт значение, простой например: инкремент значение в while цикле проверяющем какое то внешнее условие(например нажатие anykey).

Здравствуйте, C.A.B, Вы писали:

ARK>>На самом деле не такая и сложная, другой вопрос, что результаты будут весьма обескураживающими — на выходе всех путей большинство значений будет иметь громадные "потенциальные" диапазоны.
CAB>Посему простого обхода путей не достаточно, нужно ещё и трассировать их для всех возможных наборов входных значений программы, затем чтобы точно определить максимум необходимой памяти для каждого результата.

Все пути по идее определяют и все входные значения.

CAB>>>Ну а для идеального случая(просто, с полной скоростью и полной надежностью) думаю эта задача не разрешима
ARK>>Разрешима, разрешима.
CAB>Не думаю, так как в некоторых случаях не возможно заранее определить сколько памяти займёт значение

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

CAB>простой например: инкремент значение в while цикле проверяющем какое то внешнее условие(например нажатие anykey)

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

Здравствуйте, AlexRK, Вы писали:

ARK>В принципе, я интересуюсь любой информацией на тему. Конкретные языки рояля не играют, главное — принятые там решения.

A>>Кстати, для C# есть ещё и контракты:
A>>http://research.microsoft.com/en-us/projects/contracts/
ARK>Да, я в курсе. Смесь compile-time (только примитивные случаи) и run-time проверок.
Под капотом полноценный Z3 smt solver. Он же используется в полностью верифицируемой Verve OS (pdf), так что в теории ограничений нет.

На практике придётся сильно менять язык/рантайм. Для начала:
1. Покрытие контрактами входов-выходов с полноценным выводом ограничений. Для примера:

        void A()
        {
            B("");
        }
        void B(string s)
        {
            C(s, 123);
        }
        void C(string s, int p)
        {
            Contract.NotNullOrEmpty(s);
            Contract.Ensures(p>=0);
        }

Тут верификатор должен ругаться на A — именно он передаёт пустую строку куда попало. В текущей реализации CodeContracts статический верификатор ругается на B, который по сути работает посредником и никаких проверок в себе содержать не должен.
Предлагаемое решение — копировать контракты в B() в продакшне по понятным причинам работать не будет.

2. Ко-/контравариантность контрактов по аналогии с генериками. Важно для верификации виртуальных вызовов.
3. Или никакой рефлексии/dynamic, или отказываемся от условия "полностью статически верифицируемый код".
4. Инварианты для типов. В принципе, уже есть в CodeContracts:

    struct NaturalNumber
    {
        [ContractInvariantMethod]
        protected void ObjectInvariant()
        {
            Contract.Ensures(this.Value>=0);
        }
        // ...
    }

5. Отказ от тру-параллельности, переход на модель акторов/coroutines аля Axum/Tpl DataFlow. В теории возможен и анализ разделяемого состояния как в CHESS, но на 100% верификацию это уже не катит.

Разумеется, это не все условия, но объём работы (и возможные затыки) думаю, уже понятен.