валидация С++ невозможна?
Что ты имеешь ввиду? Сформулируй задачу в математических терминах, раз употребляешь выражения типа алгоритмически нераспознаваем.
Ну ладно, попробую 
Нет конечного автомата, который бы на правильный код на С++ на входе сказал, что он правильный, а на неправильный - что он неправильный.
Я слышал, что у всех плюсовых компиляторов есть некое "ядро" (в алгебраическом смысле
тексты из которого неправильны, но съедаются компиляторами, или наоборот, есть правильные, но вызывающие ошибку.
Нет конечного автомата, который бы на правильный код на С++ на входе сказал, что он правильный, а на неправильный - что он неправильный.
Я слышал, что у всех плюсовых компиляторов есть некое "ядро" (в алгебраическом смысле
тексты из которого неправильны, но съедаются компиляторами, или наоборот, есть правильные, но вызывающие ошибку.Что такое правильный?
Синтаксис можно проверить - это делают все компиляторы
А вот для выполнения программы "правильность" определить нетривиально.
Из общих соображений, если рассматривать абстрактный C++, то это эквивалентный машине тьюринга язык,
а для машины тьюринга принадлежность алгоритма к нетривиальному классу - алгоритмически неразрешима.
Если смотреть конкретную реализацию C++ на конкретной машине (конечный случай то уже здесь можно проверять многие
свойства, но за счет сложности по времени проверочных алгоритмов.
Так что все зависит от того, что такое ошибка. Вот зацикливающаяся программа - это ошибка?
Синтаксис можно проверить - это делают все компиляторы
А вот для выполнения программы "правильность" определить нетривиально.
Из общих соображений, если рассматривать абстрактный C++, то это эквивалентный машине тьюринга язык,
а для машины тьюринга принадлежность алгоритма к нетривиальному классу - алгоритмически неразрешима.
Если смотреть конкретную реализацию C++ на конкретной машине (конечный случай то уже здесь можно проверять многие
свойства, но за счет сложности по времени проверочных алгоритмов.
Так что все зависит от того, что такое ошибка. Вот зацикливающаяся программа - это ошибка?
Нет конечного автомата, который бы на правильный код на С++ на входе сказал, что он правильный, а на неправильный - что он неправильныйКонечный автомат --- штука весьма убогая. Скорее тут нужно ставить вопрос о существовании подобной машины Тьюринга.
А что, уже научились описывать семантику?
Или речь, всё-таки, идёт о грамматике?
Тогда почему не стековый автомат?
---
...Я работаю антинаучным аферистом...
Или речь, всё-таки, идёт о грамматике?
Тогда почему не стековый автомат?
---
...Я работаю антинаучным аферистом...
Я бы порекомендовал всем учавствующим в дискуссии (кроме бигмиха, пожалуй) почитать какую-нить книжку про "Формальные Языки" или "Формальные Грамматики" вместо того чтобы выставлять себя идиотами =)
Угу. Или Страуструпа. У него помнится в конце книги есть формальное описание с++.
причем здесь формальные языки, если речь шла про семантику?
или ты имеешь в виду ФА в широком смысле?
Кстати, если интересно. Есть различные тулы полуавтоматического вывода доказательств в формальных языках. У нас в лабе юзают один, называется B Toolkid кажется. Штука жутко дорогая, даже академическая лицензия. Если у языка есть формальная семантика, то можно отображать в B. Потом можно что-то доказывать с помощью тула. Обычно такие вещи применяются при разработке critical-safe систем (пример, система автоматического управления составом в каком-то Парижском метро).
Короче. Поскольку никто никогда не будет читать книжки мне придеццо самому написать небольшое разъяснение.
Формальный язык это некоторое множество слов состоящих из символов определенного алфавита. Если мы говорим о программах, то программа - это слово. Соответственно встает вопрос - принадлежит ли данное слово (программа) языку, то есть будет ли она компилироваццо на компиляторе, соответствующем стандарту.
Формальные языки достаточно логично делятся по описательной мощности (и сложности разбора соответственно).
1) Регулярные. Например, регекспы. Ну то есть любой регексп описывает некоторое множество слов. Проверяются конечным автоматом. Не допускают конструкций вида "произвольное количество открывающихся скобочек, затем точно такое же количество закрывающихся".
2) Контекстно-свободные. Допускают конструкции с требованием соответствия скобочек, но не допускают, например, требований вида "переменная должна быть объявлена перед использованием". Проверяются конечным автоматом со стеком.
3) Контекстно-зависимые. Например, С++ =). Проверяются машЫной Тьюринга или эквивалентным девайсом (конечный автомат с двумя стеками, нормальные алгоритмы Маркова)
4) Остальные. Поскольку понятие алгоритма в данный момент завязано на машину Тьюринга, то что с ними делать - не очень понятно.
Компилятор языка как правило состоит из трех частей: лексический анализатор, который регекспами разбивает входной поток на лексемы, затем синтаксический анализатор который чем-нить типа LALR спуска проверяет синтаксис и строит дерево, затем семантический анализатор написанный на полноценном языке (типа на С++) который проверяет, что, например, переменные объявляются до их использования. Потом еще можно код сгенерить.
Вроде как существуют компиляторы С++ в точности соответствующие стандарту.
Если предыдущий оратор понимал проверку семантики в более общем смысле, а не в устоявшемся среди компиляторописателей, то я, честно говоря, плохо себе представляю что это за более общий смысл.
Потому что вообще говоря описанием действия проги является сама прога. Ну то есть прога является описанием некоего алгоритма, и любое описание этого алгоритма является прогой. Так что проверять "правильность" алгоритма наверное можно или сравнивая два его описания на разных языках (плюсы и еще-что-нибудь-тормозное-зато-мощное-и-в-чем-легко-искать-ошибки, например или пытаясь на этапе компилирования проверить ассерты, то есть сравнивая полное описание (прогу) и некоторое урезанное (типа граничные значения переменных, а если решаем уравнение, то можно подставить в него ответ, например).
В любом случае это задача крайне сложная.
И в любом случае наличие в языке пойнтеров скорее всего переводит ее в разряд практически невозможных.
Формальный язык это некоторое множество слов состоящих из символов определенного алфавита. Если мы говорим о программах, то программа - это слово. Соответственно встает вопрос - принадлежит ли данное слово (программа) языку, то есть будет ли она компилироваццо на компиляторе, соответствующем стандарту.
Формальные языки достаточно логично делятся по описательной мощности (и сложности разбора соответственно).
1) Регулярные. Например, регекспы. Ну то есть любой регексп описывает некоторое множество слов. Проверяются конечным автоматом. Не допускают конструкций вида "произвольное количество открывающихся скобочек, затем точно такое же количество закрывающихся".
2) Контекстно-свободные. Допускают конструкции с требованием соответствия скобочек, но не допускают, например, требований вида "переменная должна быть объявлена перед использованием". Проверяются конечным автоматом со стеком.
3) Контекстно-зависимые. Например, С++ =). Проверяются машЫной Тьюринга или эквивалентным девайсом (конечный автомат с двумя стеками, нормальные алгоритмы Маркова)
4) Остальные. Поскольку понятие алгоритма в данный момент завязано на машину Тьюринга, то что с ними делать - не очень понятно.
Компилятор языка как правило состоит из трех частей: лексический анализатор, который регекспами разбивает входной поток на лексемы, затем синтаксический анализатор который чем-нить типа LALR спуска проверяет синтаксис и строит дерево, затем семантический анализатор написанный на полноценном языке (типа на С++) который проверяет, что, например, переменные объявляются до их использования. Потом еще можно код сгенерить.
Вроде как существуют компиляторы С++ в точности соответствующие стандарту.
Если предыдущий оратор понимал проверку семантики в более общем смысле, а не в устоявшемся среди компиляторописателей, то я, честно говоря, плохо себе представляю что это за более общий смысл.
Потому что вообще говоря описанием действия проги является сама прога. Ну то есть прога является описанием некоего алгоритма, и любое описание этого алгоритма является прогой. Так что проверять "правильность" алгоритма наверное можно или сравнивая два его описания на разных языках (плюсы и еще-что-нибудь-тормозное-зато-мощное-и-в-чем-легко-искать-ошибки, например или пытаясь на этапе компилирования проверить ассерты, то есть сравнивая полное описание (прогу) и некоторое урезанное (типа граничные значения переменных, а если решаем уравнение, то можно подставить в него ответ, например).
В любом случае это задача крайне сложная.
И в любом случае наличие в языке пойнтеров скорее всего переводит ее в разряд практически невозможных.
Не надо путать семантический разбор с семантикой языка. Формальным языком я называю язык, у которого семантика определена формально (можно в логике первого порядка). Говорить о семантике С++ нельзя, поскольку едва ли стандарт С++ можно назвать формальным определением семантики языка. Не знаю, что там в Страуструпе написано, думаю, что формальное определение синтаксиса. Но за семантику языка можно взять уже конкретную реализацию на конкретной платформе. Хотя встает вопрос о семантике стандартной библиотеки, ... Короче может это все и можно отобразить в B (теоретически это возможно т.к. В обладает той же выразимостью что и язык логики первого порядка). Но в итоге получиться что-то нереально сложное. Вообще локально можно наверно доказать, что в определенном месте проверка на условие не нужна, т.к. это условие всегда выполняется.
Но обычно поступают по-другому. Задача обычно стоит другая. Хотим получить правильную программу, т.е. формально надо проверить соответствие реализации заданной спецификации. Фактически спецификация задается на формальном языке более высокого уровня абстракции. Реализацию пишут не на С++, а на языке, который обладает формальной семантикой, который можно отображать в тот же В. Верификация на выполнение спецификации программы производится над реализацией в этом формальном языке (т.е. отображают спецификацию в В, отображают реализацию в В, доказывают что второе есть уточнение первого). Потом по этой реализации генерируется код хотя бы в том же С++. Генерация скорее всего автоматическая, хорошо отлажена и протестирована, возможно уже не на одном таком проекте. Тем более что ее реализация довольно плоская и состоит из слабо зависящих друг от друга кусков кода.
Такая метода вряд ли применима при написании обычных программ. Что-то не слышал, чтобы Виндовс или Линукс так разрабатывались. Хотя майкрософт использует формальмые методы при проверке кернеля и драйверов.
Но обычно поступают по-другому. Задача обычно стоит другая. Хотим получить правильную программу, т.е. формально надо проверить соответствие реализации заданной спецификации. Фактически спецификация задается на формальном языке более высокого уровня абстракции. Реализацию пишут не на С++, а на языке, который обладает формальной семантикой, который можно отображать в тот же В. Верификация на выполнение спецификации программы производится над реализацией в этом формальном языке (т.е. отображают спецификацию в В, отображают реализацию в В, доказывают что второе есть уточнение первого). Потом по этой реализации генерируется код хотя бы в том же С++. Генерация скорее всего автоматическая, хорошо отлажена и протестирована, возможно уже не на одном таком проекте. Тем более что ее реализация довольно плоская и состоит из слабо зависящих друг от друга кусков кода.
Такая метода вряд ли применима при написании обычных программ. Что-то не слышал, чтобы Виндовс или Линукс так разрабатывались. Хотя майкрософт использует формальмые методы при проверке кернеля и драйверов.
Короче может это все и можно отобразить в B (теоретически это возможно т.к. В обладает той же выразимостью что и язык логики первого порядка).
Язык C++, как и машина тьюринга, на сколько я знаю, в общем случае не
выражается в логиках первого порядка, иначе все было бы слишком просто
Фактически спецификация задается на формальном языке более высокого уровня абстракции.
А значит теряется описание того, что происходит на низких уровнях, часто программы бывают
дырявыми именно там.
Что-то не слышал, чтобы Виндовс или Линукс так разрабатывались. Хотя майкрософт использует формальмые методы при проверке кернеля и драйверов.
А у мелкомягких вроде как есть исследовательский отдел, который пишет проги на ML, которые при подготовке коммерческой версии конвертаются в С++.
Например, они работают над развитием языков VS...
Всем, кто всерьез интересуется такими вопросами, советую изучить ASML.
Вот ссылка для затравки.
Вот ссылка для затравки.
1) Регулярные. Например, регекспы. Ну то есть любой регексп описывает некоторое множество слов. Проверяются конечным автоматом. Не допускают конструкций вида "произвольное количество открывающихся скобочек, затем точно такое же количество закрывающихся".С каких пор нельзя 'x' в регекспе?
имеется ввиду, нельзя: "N оркрывающихся скобочек, потом N закрывающихся".
для любого N.
для любого N.
Ты не можешь написать выражение, сопоставляющееся с произвольным
количеством соответствующих друг другу открывающих и закрывающих
скобок.
---
...Я работаю антинаучным аферистом...
количеством соответствующих друг другу открывающих и закрывающих
скобок.
---
...Я работаю антинаучным аферистом...
Ты не можешь написать выражение, сопоставляющееся с произвольнымТак понятнее. Вернее "сопоставляющееся с произвольным выражением содержащим в себе произвольное количество соответствующих друг другу открывающих и закрывающих скобок".
количеством соответствующих друг другу открывающих и закрывающих
скобок.
По поводу контекстно-зависимых и КА с двумя стеками.
Я этого не встречал. Ссылку можешь кинуть?
---
...Я работаю...
Я этого не встречал. Ссылку можешь кинуть?
---
...Я работаю...
По поводу КЗ-языков - ищешь любую книжку про формальные грамматики.
А типа разве не очевидна эквивалентность машЫны тьюринга и двухстекового КА?
А типа разве не очевидна эквивалентность машЫны тьюринга и двухстекового КА?
Очевидно, что не любую, поскольку я этого не встречал.
Мне нет, но я этим не занимаюсь.
---
...Я работаю...
Мне нет, но я этим не занимаюсь.
---
...Я работаю...
Ладно, согласен, очевидно.
Я потом уже, на прогулке понял.
---
...Я работаю...
Я потом уже, на прогулке понял.
---
...Я работаю...
Оставить комментарий
margadon
правда ли, что это нельзя сделать с современным С++ (ну например стандарта ISO/IEC 14882)? То есть он алгоритмически нераспознаваем? Слухи такие я улавливал, а вот источников не видел.