ARK>>>На самом деле не такая и сложная, другой вопрос, что результаты будут весьма обескураживающими — на выходе всех путей большинство значений будет иметь громадные "потенциальные" диапазоны. CAB>>Посему простого обхода путей не достаточно, нужно ещё и трассировать их для всех возможных наборов входных значений программы, затем чтобы точно определить максимум необходимой памяти для каждого результата. ARK>Все пути по идее определяют и все входные значения.
В смысле?/Не понял.
ARK>[...]
С остальным согласен.
Между тем,что я думаю,тем,что я хочу сказать,тем,что я,как мне кажется,говорю,и тем,что вы хотите услышать,тем,что как вам кажется,вы слышите,тем,что вы понимаете,стоит десять вариантов возникновения непонимания.Но всё-таки давайте попробуем...(Э.Уэллс)
Здравствуйте, AlexRK, Вы писали:
ARK>Крутится мысль о выносе в сигнатуру функции некоторой дополнительной информации о числовых параметрах. Этакие "типы для числовых типов", но не просто диапазоны.
ARK>Может быть что-то вроде ARK>T foo(U parameter) where T : Integer, U : Integer, T > U
Это очень похоже на то, что сделано в ATS. Там вот такая сигнатура
fn search {n,m:nat | m <= n}
(str : string n, sub : string m) : [p:int | p <= n - m] int p = ...
гласит: функция search принимает две строки с натуральными длинами n и m, такие что m <= n, и возвращает целое число p такое, что p <= n-m. Проверяется это все в компайл-тайме, а на выходе генерится Си-код, где функция принимает два указателя и возвращает инт.
Подробнее: http://thedeemon.livejournal.com/41545.html
Здравствуйте, C.A.B, Вы писали:
ARK>>>>На самом деле не такая и сложная, другой вопрос, что результаты будут весьма обескураживающими — на выходе всех путей большинство значений будет иметь громадные "потенциальные" диапазоны. CAB>>>Посему простого обхода путей не достаточно, нужно ещё и трассировать их для всех возможных наборов входных значений программы, затем чтобы точно определить максимум необходимой памяти для каждого результата. ARK>>Все пути по идее определяют и все входные значения. CAB>В смысле?/Не понял.
Может это я чего не понял? Я имею в виду, что достаточно отслеживать все возможные пути прохождения целых значений в программе или отдельном модуле. И если там встретятся взаимодействия с внешним миром — ну что ж, учтем и их при вычислении размера.
Здравствуйте, D. Mon, Вы писали:
DM>Здравствуйте, AlexRK, Вы писали:
ARK>>Крутится мысль о выносе в сигнатуру функции некоторой дополнительной информации о числовых параметрах. Этакие "типы для числовых типов", но не просто диапазоны.
ARK>>Может быть что-то вроде ARK>>T foo(U parameter) where T : Integer, U : Integer, T > U
DM>Это очень похоже на то, что сделано в ATS. Там вот такая сигнатура DM>
DM>fn search {n,m:nat | m <= n}
DM> (str : string n, sub : string m) : [p:int | p <= n - m] int p = ...
DM>
DM>гласит: функция search принимает две строки с натуральными длинами n и m, такие что m <= n, и возвращает целое число p такое, что p <= n-m. Проверяется это все в компайл-тайме, а на выходе генерится Си-код, где функция принимает два указателя и возвращает инт. DM>Подробнее: DM>http://thedeemon.livejournal.com/41545.html
Да-да, помню ATS. Читал доки, хотя плотно не щупал. Действительно похоже, но, ИМХО, вариант из ATS все же не для мейнстрима. Сложно для программиста.
Здравствуйте, Sinix, Вы писали:
S>На практике придётся сильно менять язык/рантайм. Для начала: S>1. Покрытие контрактами входов-выходов с полноценным выводом ограничений. Для примера: S>Тут верификатор должен ругаться на A — именно он передаёт пустую строку куда попало. В текущей реализации CodeContracts статический верификатор ругается на B, который по сути работает посредником и никаких проверок в себе содержать не должен. S>Предлагаемое решение — копировать контракты в B() в продакшне по понятным причинам работать не будет.
По-моему, как раз этот вариант правильный. Контракты должны быть транзитивными.
S>2. Ко-/контравариантность контрактов по аналогии с генериками. Важно для верификации виртуальных вызовов.
Да, так в Eiffel сделано (только там run-time).
S>3. Или никакой рефлексии/dynamic, или отказываемся от условия "полностью статически верифицируемый код".
Run-time рефлексию и dynamic — безусловно в топку.
S>4. Инварианты для типов. В принципе, уже есть в CodeContracts:
Опять же, в Эйфеле это уже 20 лет назад было. Инварианты нужны, естественно.
S>5. Отказ от тру-параллельности, переход на модель акторов/coroutines аля Axum/Tpl DataFlow. В теории возможен и анализ разделяемого состояния как в CHESS, но на 100% верификацию это уже не катит.
Тут не копенгаген.
S>Разумеется, это не все условия, но объём работы (и возможные затыки) думаю, уже понятен.
ARK>Может это я чего не понял? Я имею в виду, что достаточно отслеживать все возможные пути прохождения целых значений в программе или отдельном модуле. И если там встретятся взаимодействия с внешним миром — ну что ж, учтем и их при вычислении размера.
Нужно отслеживать не только все возможные пути прохождения но и всё что происходит со значениями "по пути". Например:
def f(a:Int, b:Int) = { //у нас есть функция и мы знаем (каким-то образом) что всегда 'a' = 800..1000, 'b' = 800, потому для них нужно по 2 байта;
val c = a - b //здесь мы можем вычислить что всегда 'c' = 0..200, следовательно для 'с' достаточно 1 байта;
val d = c * 1000 //для 'd' уже нужно 3 байта;
... //и т.д.
}
Как-то так.
Между тем,что я думаю,тем,что я хочу сказать,тем,что я,как мне кажется,говорю,и тем,что вы хотите услышать,тем,что как вам кажется,вы слышите,тем,что вы понимаете,стоит десять вариантов возникновения непонимания.Но всё-таки давайте попробуем...(Э.Уэллс)
Здравствуйте, C.A.B, Вы писали:
ARK>>Может это я чего не понял? Я имею в виду, что достаточно отслеживать все возможные пути прохождения целых значений в программе или отдельном модуле. И если там встретятся взаимодействия с внешним миром — ну что ж, учтем и их при вычислении размера. CAB>Нужно отслеживать не только все возможные пути прохождения но и всё что происходит со значениями "по пути". Например:
Ну, я почему-то считал это само собой разумеющимся.
Здравствуйте, AlexRK, Вы писали:
S>>Тут верификатор должен ругаться на A — именно он передаёт пустую строку куда попало. В текущей реализации CodeContracts статический верификатор ругается на B, который по сути работает посредником и никаких проверок в себе содержать не должен. S>>Предлагаемое решение — копировать контракты в B() в продакшне по понятным причинам работать не будет.
ARK>По-моему, как раз этот вариант правильный. Контракты должны быть транзитивными.
Неа. 2-3 перегрузки метода, 1 хелпер, который просто вызывает штук 5 подобных методов — и мы захлебнёмся в тонне копипасты контрактов. Я не теоретезирую, именно что пробовали использовать CodeContracts в продакшне.
S>>5. Отказ от тру-параллельности, переход на модель акторов/coroutines аля Axum/Tpl DataFlow. В теории возможен и анализ разделяемого состояния как в CHESS, но на 100% верификацию это уже не катит.
ARK>Тут не копенгаген.
Смысл в следующем — или страшная магия, или требуем, чтобы данные не изменялись другими потоками во время работы метода. Иначе с верификацией начинаются очень большие проблемы, вплоть до перехода к проверкам на основе выборок, как в CHESS:
CHESS is a tool for finding and reproducing Heisenbugs in concurrent programs. CHESS repeatedly runs a concurrent test ensuring that every run takes a different interleaving. If an interleaving results in an error, CHESS can reproduce the interleaving for improved debugging.
Ну а переход от взаимодействия потоков через глобальные переменные к передаче состояния через входные-выходные параметры неизбежно требует своей инфраструктуры аля tasks/await в c#. Причём придётся научить анализатор понимать такие штуки.
S>>Разумеется, это не все условия, но объём работы (и возможные затыки) думаю, уже понятен. ARK>А что насчет переполнений?
А чем они принципиально отличаются от прочих ограничений? Прописываем диапазоны в контракте, если постусловия неразрешимы через SMT (как тут) — чекер предупредит.
Здравствуйте, Sinix, Вы писали:
S>Неа. 2-3 перегрузки метода, 1 хелпер, который просто вызывает штук 5 подобных методов — и мы захлебнёмся в тонне копипасты контрактов. Я не теоретезирую, именно что пробовали использовать CodeContracts в продакшне.
По-моему, все равно других вариантов нет. Иначе мы выставляем наружу зависимость от реализации. И как это может работать в условиях полиморфизма, когда мы вызываем вообще неизвестно какой метод?
ИМХО, единственный рабочий вариант — контракты на каждый метод, которые соблюдают и клиент, и поставщик.
Такие "не транзитивные" контракты можно применять только в рамках одного класса-модуля. Так же, как вывод типов обычно применяется только в рамках метода.
S>Ну а переход от взаимодействия потоков через глобальные переменные к передаче состояния через входные-выходные параметры неизбежно требует своей инфраструктуры аля tasks/await в c#. Причём придётся научить анализатор понимать такие штуки.
А, ну это да, я убежден, что глобального состояния быть не должно. Вообще нигде.
ARK>>А что насчет переполнений? S>А чем они принципиально отличаются от прочих ограничений? Прописываем диапазоны в контракте, если постусловия неразрешимы через SMT (как тут) — чекер предупредит.
В _принципе_ ничем, но, ИМХО, работать с диапазонами очень сложно. Нужна какая-то более простая технология. Пусть даже эта технология откинет 20% корректных программ, но позволит корректно и относительно легко создать оставшиеся 80%.
Здравствуйте, AlexRK, Вы писали:
ARK>По-моему, все равно других вариантов нет. Иначе мы выставляем наружу зависимость от реализации.
Не, тут у нас два варианта:
1. Совмещаем явные контракты с выводом контрактов по вызываемым методам. В предельной версии это позволяет вообще отказаться от ассертов в рантайме и от части тестов. В более-менее реальной — значительно снизить необходимость в тестах.
2. Или покрывать контрактами каждый метод, даже промежуточный, или смириться с неполной верификацией кода. Это по-моему вообще ошибка в логике: делаем больше работы, получаем меньший результат.
Кстати, а чем тут плоха зависимость от реализации, если:
1. Без контрактов она всё равно выстрелит, только в рантайме
2. При смене реализации компилятор подсветит места с потенциальными ошибками
3. Если нужна слабая связность — прячем реализацию за интерфейс и прописываем контракт в интерфейсе.
?
ARK>И как это может работать в условиях полиморфизма, когда мы вызываем вообще неизвестно какой метод?
Ко- и контра- вариантность контрактов. Наследник (реализация интерфейса, делегат — неважно) не может усиливать входной и ослаблять выходной контракты.
ARK>В _принципе_ ничем, но, ИМХО, работать с диапазонами очень сложно. Нужна какая-то более простая технология. Пусть даже эта технология откинет 20% корректных программ, но позволит корректно и относительно легко создать оставшиеся 80%.
Здравствуйте, Sinix, Вы писали:
S>1. Совмещаем явные контракты с выводом контрактов по вызываемым методам. В предельной версии это позволяет вообще отказаться от ассертов в рантайме и от части тестов. В более-менее реальной — значительно снизить необходимость в тестах. S>2. Или покрывать контрактами каждый метод, даже промежуточный, или смириться с неполной верификацией кода.
А чем плох вариант с явными контрактами на границах классов-модулей, и неявными внутри?
S>Это по-моему вообще ошибка в логике: делаем больше работы, получаем меньший результат.
Если такой перекос имеет место быть, то это, безусловно, неправильно.
S>Кстати, а чем тут плоха зависимость от реализации, если: S>1. Без контрактов она всё равно выстрелит, только в рантайме
Пардон, не понял. Зависимость выстрелит?
S>2. При смене реализации компилятор подсветит места с потенциальными ошибками
Вот не нравится мне это. Тогда понятие интерфейса совсем размывается.
S>3. Если нужна слабая связность — прячем реализацию за интерфейс и прописываем контракт в интерфейсе.
Ну, это как раз мой вариант.
ARK>>И как это может работать в условиях полиморфизма, когда мы вызываем вообще неизвестно какой метод? S>Ко- и контра- вариантность контрактов. Наследник (реализация интерфейса, делегат — неважно) не может усиливать входной и ослаблять выходной контракты.
Я к тому и клоню — потребуются явные контракты на интерфейсах.
Здравствуйте, AlexRK, Вы писали:
ARK>А чем плох вариант с явными контрактами на границах классов-модулей, и неявными внутри?
Тем, что надо отслеживать изменение контрактов и добавлять/убирать их при превращении метода в публичный.
Вручную — слишком много мороки.
С другой стороны, если это будет делаться автоматически, причём в отдельные файлы, чтоб не смешиваться с основным кодом — разница между двумя подходами исчезает.
Так что да, наверно лучше требовать явные контракты на границе модуля и хранить их в отдельных файлах.
Кстати, МС примерно так и делает с contract annotations, если не ошибаюсь
S>>Кстати, а чем тут плоха зависимость от реализации, если: S>>1. Без контрактов она всё равно выстрелит, только в рантайме
ARK> Пардон, не понял. Зависимость выстрелит?
Неа, нарушение контракта Если у нас код не нарушает контракт ни одной из реализаций, то, очевидно зависимость от реализации тут никак не проявляется.
S>>2. При смене реализации компилятор подсветит места с потенциальными ошибками ARK>Вот не нравится мне это. Тогда понятие интерфейса совсем размывается.
Есть немного. В принципе, ничего не мешает реализовать компромиссную стратегию — подсвечивать ошибку на границе модуля и даже сделать эту политику настраиваемой. Иначе у нас опять появляется необходимость в тестах для проверки корректности программы.
Здравствуйте, Sinix, Вы писали:
ARK>>А чем плох вариант с явными контрактами на границах классов-модулей, и неявными внутри? S>Тем, что надо отслеживать изменение контрактов и добавлять/убирать их при превращении метода в публичный. S>Вручную — слишком много мороки.
Черт его знает, может и так.
S>С другой стороны, если это будет делаться автоматически, причём в отдельные файлы, чтоб не смешиваться с основным кодом — разница между двумя подходами исчезает. S>Так что да, наверно лучше требовать явные контракты на границе модуля и хранить их в отдельных файлах. S>Кстати, МС примерно так и делает с contract annotations, если не ошибаюсь
С автоматическим подходом мне не нравится один момент. При таком подходе будет _очень_ сильная зависимость от реализации. Буквально поменяли "return 1" на "return 2" — и контракт изменился. А руками человек, скорее всего, написал бы что-то более осмысленное, исходя из семантики метода.
ARK>> Пардон, не понял. Зависимость выстрелит? S>Неа, нарушение контракта Если у нас код не нарушает контракт ни одной из реализаций, то, очевидно зависимость от реализации тут никак не проявляется.
А... ну это да. Но такие счастливые случаи вряд ли стоит рассматривать.
ARK>>Вот не нравится мне это. Тогда понятие интерфейса совсем размывается. S>Есть немного. В принципе, ничего не мешает реализовать компромиссную стратегию — подсвечивать ошибку на границе модуля и даже сделать эту политику настраиваемой. Иначе у нас опять появляется необходимость в тестах для проверки корректности программы.
Интерфейс — это абстрагирование от реализации. Содержит только существенные детали. Если мы будем автоматически выводить контракты из реализации, то, по сути, интерфейс вообще просто исчезает — точнее, начинает содержать все детали реализации. (По крайней мере, относящиеся к обсуждаемой теме, переполнениям и т.п.)
По хорошему нам бы не надо выносить в интерфейс ВСЁ — даже автоматически. Плохо это. Что-то надо безусловно вынести, иначе дополнительного контроля мы не получим, но не всё. А вопрос, что вынести и каким образом, — это и есть Святой Грааль.
Здравствуйте, AlexRK, Вы писали:
ARK>С автоматическим подходом мне не нравится один момент. При таком подходе будет _очень_ сильная зависимость от реализации. Буквально поменяли "return 1" на "return 2" — и контракт изменился. А руками человек, скорее всего, написал бы что-то более осмысленное, исходя из семантики метода.
Угу. Но автоматический вывод можно перекрыть явными условиями или в самом методе (например, Ensures(Return()>1), и тогда проверка остановится прямо на этих контрактах, или добавить этот же контракт где-то выше по стеку.
ARK>Интерфейс — это абстрагирование от реализации. Содержит только существенные детали. Если мы будем автоматически выводить контракты из реализации, то, по сути, интерфейс вообще просто исчезает — точнее, начинает содержать все детали реализации. (По крайней мере, относящиеся к обсуждаемой теме, переполнениям и т.п.)
Автоматические контракты ведь не отменяют возможность задать контракт вручную.
Вот и пусть "рукопашный" вариант отражается в документации, а "сгенеренный" — играет роль статических юнит-тестов. Тем более, что тесты тоже проверяют не столько контракт, сколько соответствие контракта и реализации.
Здравствуйте, Sinix, Вы писали:
S>Автоматические контракты ведь не отменяют возможность задать контракт вручную. S>Вот и пусть "рукопашный" вариант отражается в документации, а "сгенеренный" — играет роль статических юнит-тестов.
Это верно. Но мне кажется важным обстоятельство, что язык должен подталкивать и склонять к некоторому типу действий. В принципе, ООП может быть реализовано и на С, но язык этому не способствует. C# с ключевым словом readonly способствует созданию изменяемых переменных, а Ceylon с ключевым словом variable — наоборот. Языки равны по мощности, но приучают программиста к разным вещам.
Так вот, ИМХО, автоматический вывод контрактов совершенно не способствует созданию модульного, компонентного ПО. Если вообще не препятствует этому.
Здравствуйте, C.A.B, Вы писали:
CAB> Нужно отслеживать не только все возможные пути прохождения но и всё что происходит со значениями "по пути".
Не понимаю. Вот простенькая функция:
int fun(int m, int n) {
if (m == 0) {
return n + 1;
} else if (n == 0) {
return fun(m-1, 1);
} else {
return fun(m-1, fun(m, n-1));
}
}
Посчитай все пути прохождения с учётом того, что m,n не больше 5. Сколько нужно байт для хранения fun(4,4)?
Здравствуйте, ., Вы писали:
.>Здравствуйте, C.A.B, Вы писали:
CAB>> Нужно отслеживать не только все возможные пути прохождения но и всё что происходит со значениями "по пути". .>Не понимаю. Вот простенькая функция: .>Посчитай все пути прохождения с учётом того, что m,n не больше 5. Сколько нужно байт для хранения fun(4,4)?
Это функция Аккермана? В топку ее. И другие заковыристые функции тоже. Разумный анализатор дойдет до некоторого размера числа и дальше компилировать откажется.
Здравствуйте, ., Вы писали: .>Не понимаю. Вот простенькая функция: .>[...] .>Посчитай все пути прохождения с учётом того, что m,n не больше 5. Сколько нужно байт для хранения fun(4,4)?
Если функцию невозможно трассировать (по каким либо причинам) то и определить размер переменных не получится.
Между тем,что я думаю,тем,что я хочу сказать,тем,что я,как мне кажется,говорю,и тем,что вы хотите услышать,тем,что как вам кажется,вы слышите,тем,что вы понимаете,стоит десять вариантов возникновения непонимания.Но всё-таки давайте попробуем...(Э.Уэллс)
Здравствуйте, AlexRK, Вы писали:
CAB>>> Нужно отслеживать не только все возможные пути прохождения но и всё что происходит со значениями "по пути". .>>Не понимаю. Вот простенькая функция: .>>Посчитай все пути прохождения с учётом того, что m,n не больше 5. Сколько нужно байт для хранения fun(4,4)?
ARK>Это функция Аккермана? В топку ее. И другие заковыристые функции тоже. Разумный анализатор дойдет до некоторого размера числа и дальше компилировать откажется.
А не окажется ли такой анализатор на столько разумным, что будет отказываться компилировать что-то сложнее игрушечных демо-примеров?
но это не зря, хотя, может быть, невзначай
гÅрмония мира не знает границ — сейчас мы будем пить чай
Здравствуйте, ., Вы писали:
.>Здравствуйте, AlexRK, Вы писали:
CAB>>>> Нужно отслеживать не только все возможные пути прохождения но и всё что происходит со значениями "по пути". .>>>Не понимаю. Вот простенькая функция: .>>>Посчитай все пути прохождения с учётом того, что m,n не больше 5. Сколько нужно байт для хранения fun(4,4)?
ARK>>Это функция Аккермана? В топку ее. И другие заковыристые функции тоже. Разумный анализатор дойдет до некоторого размера числа и дальше компилировать откажется. .>А не окажется ли такой анализатор на столько разумным, что будет отказываться компилировать что-то сложнее игрушечных демо-примеров?
Однозначно на этот вопрос ответить, конечно, сложно. На мой взгляд, такого быть не должно. Существует достаточно сложное ПО, которое полностью верифицировано. Например вот: http://www.astree.ens.fr/ (раздел Industrial Applications).
Инварианты нужны, естественно.
