языки с логикой (проверкой условий)
Пользуйся asset.
Языки такие есть, но что ты с ними будешь делать?
Языки такие есть, но что ты с ними будешь делать?
см. Eiffel programming language, Design by Contract.
В D вроде тоже позаимствовали из Эйфеля.
Модификатор const в С++ ничего не утверждает. const параметры можно легко изменить с помощью приведения типов. Так что const - это просто защита от дурака.
Только Eiffel сам по себе ничего не проверяет, он лишь бросает исключение, если условия нарушаются. Языки, которые проверяют программу сами, никем не используются, ибо написание формальных доказательств для программ занимает о-о-очень много времени.
Не помню в модуле были инварианты или нет. В любом случае язык уже мёртвый считай.
В некотором смысле языки под jvm/.net обладают таким свойством. Потому что код скомпилирован в специальный ассемблер, который специально предназначен для отслеживания корректности. Например, ты можешь быть уверен, что вызываемая функция не изменит твою переменную, если ты ей не дал на неё ссылку (в отличие от С, в котором она может зафигачить нолик в произвольное место памяти). Ещё там есть достаточно развесистые методы для секьюрности: ты можешь ограничить права вызываемой функции на вызов других функций — то есть запретить пользоваться рефлекшеном, IO и всем таким. И даже в большей или меньшей степени защититься от того, что она вызовет твою функцию (которую тебе пришлось ей дать) и сможет получить доступ к ним через неё.
А логико/математические инварианты действительно почти никто сейчас не проверяет. Во-первых, потому что написание доказательства корректности функции вообще-то мало отличается от написания самой функции. Это ведь одно и то же, по сути. Чтобы доказать, что некая функция складывает два числа, тебе нужно написать другую функцию складывающую два числа и доказать их эквивалентность. Поэтому максимум, на который можно рассчитывать, это частичная проверка некоторых инвариантов, которые легко проверить. Но и это делать всем влом, потому что все интересные инварианты (типа, что функция когда-нибудь завершит выполнение) в общем случае алгоритмически неразрешимы.
Так что максимум ты можешь рассчитывать на ассерты в рантайме, может быть в удобной записи (когда-то видел библиотечку для шарпа, позволявшую помечать параметры специальными делегатами вроде [NotNull], что удобней проверки ручками).
А логико/математические инварианты действительно почти никто сейчас не проверяет. Во-первых, потому что написание доказательства корректности функции вообще-то мало отличается от написания самой функции. Это ведь одно и то же, по сути. Чтобы доказать, что некая функция складывает два числа, тебе нужно написать другую функцию складывающую два числа и доказать их эквивалентность. Поэтому максимум, на который можно рассчитывать, это частичная проверка некоторых инвариантов, которые легко проверить. Но и это делать всем влом, потому что все интересные инварианты (типа, что функция когда-нибудь завершит выполнение) в общем случае алгоритмически неразрешимы.
Так что максимум ты можешь рассчитывать на ассерты в рантайме, может быть в удобной записи (когда-то видел библиотечку для шарпа, позволявшую помечать параметры специальными делегатами вроде [NotNull], что удобней проверки ручками).
Только Eiffel сам по себе ничего не проверяет, он лишь бросает исключение, если условия нарушаются.не, не катит. Нжно на этапе компиляции.
Чтобы доказать, что некая функция складывает два числа, тебе нужно написать другую функцию складывающую два числа и доказать их эквивалентность.Не обязательно. Я это вижу так: про операцию + уже известно, что она складывает и более ничего не делает. Аналогично есть семантика и других базовых операций языка. Далее, утверждения про состояние переменных и про возвращаемое значение каким-то образом отражены в прототипах функций. Когда пишем в коде вызов, компилятор отслеживает состояние объектов (инварианты) аналогично тому, как он следит за типом переменных, только чуть более мудрено.
Но и это делать всем влом, потому что все интересные инварианты (типа, что функция когда-нибудь завершит выполнение) в общем случае алгоритмически неразрешимы.А тут задача и не ставится доказать корректность внешними по отношению к коду способами. Просто наряду с типами данных вводятся некие "свойства", которые приписываются объектам после выполнения операций над ними. Например, после a = b + 1 для формируется утверждение a > b. И аналогично для функций. Тогда появляется возможность контролировать семантику.
Да, какие-нибудь очень простые инварианты ты так можешь отследить. Если повезёт.
Если у тебя где-нибудь вызывается эта функция, причём в зависимости от результата изменяется или не изменяется какой-нибудь инвариант, то твоя гипотетическая проверялка ни за какое разумное время не сможет за этим инвариантом проследить. Если кажется, что она настолько умна и быстра, что сумеет соптимизировать вычисление до ~2^40 проверок и провести его, возьми какой-нибудь 128 битный лонг, там точно нет шансов.
Если тебе кажется, что подобные функции встречаются редко, а обычновстречающиеся твоя проверялка сумеет разрулить и проверить, подумай ещё раз.
#define LIMIT 2600000
for (long a = 2; a < LIMIT/2; a++)
{
for (long b = 2; b < LIMIT/2; b++)
{
for (long c = 2; c < LIMIT; c++)
{
if (a * a * a + b * b * b == c * c * c)
{
return 1;
}
}
}
}
return 0;
Если у тебя где-нибудь вызывается эта функция, причём в зависимости от результата изменяется или не изменяется какой-нибудь инвариант, то твоя гипотетическая проверялка ни за какое разумное время не сможет за этим инвариантом проследить. Если кажется, что она настолько умна и быстра, что сумеет соптимизировать вычисление до ~2^40 проверок и провести его, возьми какой-нибудь 128 битный лонг, там точно нет шансов.
Если тебе кажется, что подобные функции встречаются редко, а обычновстречающиеся твоя проверялка сумеет разрулить и проверить, подумай ещё раз.
Фишка в том, что фишка(тм) не должна пытаться разрулить код автоматически (также, как и gcc не делает сам const-кастинг, даже когда видит, что переменная только читается). Это _мы_ должны в теле функции построить утверждение о том, что все хорошо. Утверждение это, имхо, должно само являться переменной специального типа и строится аналогично тому, как строятся прочие объекты - в результате вызова функций (конструкторов) и применения операций. Утверждение также должно возвращаться из функции в числе прочих объектов. Например, функция сортировки возвращает пару: вектор и утверждение о его отсортированности. Вернуть просто вектор будет нельзя, так как формально тип возвращаемого значения - пара, где вторая компонента - утверждение вроде "i > j => a[i] > a[j]".
см. Eiffel programming language, Design by Contract.Спасибо, практически что надо. Неясно только пока, происходит ли проверка контракта на стадии компиляции или при выполнении. Кстати, там были ссылки на DbC in C++, но там все с помощью ASSERT-ов, т. е. на стадии выполнения.
Кстати, где-то слышал, что compile-time DbC можно смоделировать в C++ с помощью шаблонов и typedef-ов, но конкретно как - не помню.
Ты учти, что функция
Не всегда вовращает a+b даже при этих ограничениях - ибо многопоточность. Не забывай, что в любой функции, где есть цикл, тебе придется на формальном языке использовать индукцию. А что-либо доказать с действительными числами чрезвычайно сложно из-за погрешностей вычислений. Поэтому-то никто формальными доказательствами и не пользуется. Они могут иметь практическую пользу только если компьютер научится понимать научный текст на естественном языке и восстанавливать обоснование в простых шагах доказательств.
int f(int a,int b)не возвращает a+b. Пример - a=2000000000, b=2000000000. Поэтому тебе всегда придется писать ограничения на переменные. Так же не забывай, что метод
{
return a+b;
}
class test
{
int aa,bb;
int f(int a,int b)
{
aa=a;
bb=b;
return aa+bb;
}
}
Не всегда вовращает a+b даже при этих ограничениях - ибо многопоточность. Не забывай, что в любой функции, где есть цикл, тебе придется на формальном языке использовать индукцию. А что-либо доказать с действительными числами чрезвычайно сложно из-за погрешностей вычислений. Поэтому-то никто формальными доказательствами и не пользуется. Они могут иметь практическую пользу только если компьютер научится понимать научный текст на естественном языке и восстанавливать обоснование в простых шагах доказательств.
Любой язык со статической типизацией это позволяет
Другое дело, что ты задолбаешся программы в таком стиле писать.
Хотя в простых случаях, например, проверка списка на пустоту это не сложно.
тыц
Или там шняги для защиты от xss еще тыц
Другое дело, что ты задолбаешся программы в таком стиле писать.
Хотя в простых случаях, например, проверка списка на пустоту это не сложно.
тыц
Или там шняги для защиты от xss еще тыц
Это я понял прекрасно.
Я ж специально пример привёл (и да, я знаю, что это последняя теорема Ферма, она, кстати, решена) — как только у тебя появляется первая не примитивно-рекурсивная функция (если я ничего не путаю у тебя исчезает возможность автоматического нахождения доказательства любого инварианта, использующего возвращаемый ей результат, да и с автоматической проверкой будут сложности (в смысле, что это сложно да и с более простыми функциями могут возникнуть проблемы чисто с вычислительной сложностью.
Понимаешь, ты сейчас думаешь о линейных программах, типа взять число, прибавить другое число, вычесть третье... В таких можно отслеживать инварианты, без сомнений. Но первый же цикл даёт качественное изменение сложности, причём описанием часто повторяющихся паттернов тут не отделаешься, программы настолько разные, что неуниверсальная проверялка не имеет никакой практической ценности. Универсальная же невозможна, ограниченно-универсальная ограничена и дико сложна, сильно ограниченная бесполезна.
Вот, почитай-ка http://en.wikipedia.org/wiki/Curry-Howard_isomorphism
Например, функция сортировки возвращает пару: вектор и утверждение о его отсортированности.И вот мне очень интересно, как ты себе представляешь автоматическую проверку корректности этого утверждения? Прикинь, как это будет выглядеть. Единственное, что я могу представить — это программу на каком-нибудь хаскелле, в котором есть высокоуровневая операция конкатенации списков (и проверялка её понимает) и сама программа фактически выглядит как рекурсивное доказательство собственной корректности — но проверялка должна уметь такое понимать, а если твой язык не такой высокоуровневый (или ты не можешь себе позволить такую высокоуровневость то либо проверялка должна быть непредставимо умной, либо тебе придётся написать доказательство отдельно (а проверялка, опять же, будет достаточно умной, чтобы суметь его сопоставить самой программе).
Я ж специально пример привёл (и да, я знаю, что это последняя теорема Ферма, она, кстати, решена) — как только у тебя появляется первая не примитивно-рекурсивная функция (если я ничего не путаю у тебя исчезает возможность автоматического нахождения доказательства любого инварианта, использующего возвращаемый ей результат, да и с автоматической проверкой будут сложности (в смысле, что это сложно да и с более простыми функциями могут возникнуть проблемы чисто с вычислительной сложностью.
Понимаешь, ты сейчас думаешь о линейных программах, типа взять число, прибавить другое число, вычесть третье... В таких можно отслеживать инварианты, без сомнений. Но первый же цикл даёт качественное изменение сложности, причём описанием часто повторяющихся паттернов тут не отделаешься, программы настолько разные, что неуниверсальная проверялка не имеет никакой практической ценности. Универсальная же невозможна, ограниченно-универсальная ограничена и дико сложна, сильно ограниченная бесполезна.
Вот, почитай-ка http://en.wikipedia.org/wiki/Curry-Howard_isomorphism
Ты учти, что функция... не возвращает a+b. Пример - a=2000000000, b=2000000000. Поэтому тебе всегда придется писать ограничения на переменные.Разумеется, вычисление идет в целых по модулю 2^32 и т. п., причем, это "зашито" в семантику операции +.
Так же не забывай, что метод... Не всегда вовращает a+b даже при этих ограничениях - ибо многопоточностьДля глобальных переменных будут также глобальные утверждения. Вообе, утверждение может содержать имена любых переменных, которые есть в его области видимости. С многопоточностью - хуже. Если контекст разделяется между потоками, то на самом деле гарантировать состояние переменных нельзя, и тогда код должен быть заключен в некий unsycronized-блок, где нельзя работать с утверждениями о состоянии.
Не забывай, что в любой функции, где есть цикл, тебе придется на формальном языке использовать индукцию.Ну, видимо, оператор цикла как раз и должен генерить результирующее утверждение индукции, беря за базу то, что перед входом в цикл, и в качестве шага то, что внутри цикла. Но генерть он будет, конечно, не сам, а под нашим чутким руководством - мы говорим, что вот это утверждение следует вывести из цикла с такой-то инициализацией и таким-то шагом.
Любой язык со статической типизацией это позволяетЭто да, согласен. Придется помимо построения структур данных заниматься построением (выводом) утверждений, геморроя минимум в 2 раза больше. Но если сопоставить со временем тестирования и отловом багов, то... как знать.
Другое дело, что ты задолбаешся программы в таком стиле писать.
Вообще, идея, вокруг которой я кручусь - это сделать утверждения объектами в программе, т. е. завести для них примитивный тип данных (точнее, целое семейство). Тогда вывод - это просто построение объекта нужного типа, подобно тому, как, скажем, сортировка - это построение в памяти нужной структуры данных. Чтобы построить требуемое контрактом утверждение, просто напросто придется проделать правильные операции в правильном порядке (попутно построив нужную структуру данных в памяти, например, отсортировав вектор).
Слушай, но ты ведь реально общие слова говоришь.
Придумай условно формальный язык и покажи, как ты сумеешь применить его к функции, вычисляющей простоту числа (как тупым делением до корня из, так и решетом эратосфена).
Придумай условно формальный язык и покажи, как ты сумеешь применить его к функции, вычисляющей простоту числа (как тупым делением до корня из, так и решетом эратосфена).
Слушай, но ты ведь реально общие слова говоришьПока, к сожалению, более конкретного ничего не придумалось. Попробую как-нибудь разобрать парочку примеров реальных функций.
Вообще, идея, вокруг которой я кручусь - это сделать утверждения объектами в программе, т. е. завести для них примитивный тип данных (точнее, целое семейство). Тогда вывод - это просто построение объекта нужного типа, подобно тому, как, скажем, сортировка - это построение в памяти нужной структуры данных.Похоже на
http://en.wikipedia.org/wiki/Coq
Эту штуку иногда используют для формального доказательства нужных свойств алгоритмов и систем.
Оставить комментарий
Missi4ka
Существуют ли на сегодняшний день языки с автоматиеской проверкой семантики программы, то есть, скажем, чтобы в заголовке функции отмечалось, что если на входе имели a = b, то это же условие будет и после выхода. Аналогично модификатору const в c++, который утверждает: "все аргументы после возврата таке же, как до вызова".Почему вопрос ставится именно о вызове функций - потому что из всех операций именно вызов не предсказуем, так как происходит обращение к коду, написанному ранее и, возможно, хранящемуся уже в откомпилированном виде, так что проверить семантику по исходнику неинлайновой функции нельзя.