История изменений
Исправление hateyoufeel, (текущая версия) :
Теорема о неполноте о формулах (программах) в формальных системах (стандарте языка Си).
Повторюсь: Гёдель писал о том, что в любой самореферентной формальной системе будут либо правдивые утверждения, которые нельзя доказать (т.е. аксиомы), либо ложные утверждения, которые доказать можно (т.е. херота). Си здесь никаким боком не при делах.
Есть такие же без «проблемы остановки»?
Проблема останова является свойством любой Тьюринг-полной системы, но к UB отношения не имеет.
Самый (почти) простой и банальный пример Тьюринг-полного ЯП без UB: Brainfuck.
UB может быть бесконечным циклом.
Не может. Это вполне определённое поведение.
В моём примере выше бесконечный цикл появился в результате трансформаций кода компилятором, но точно так же так мог появиться любой другой дефект.
Как доказать, что программа завершиться, не имеет UB приводящий к бесконечному цику?
Причём здесь Си?
Исходная версия hateyoufeel, :
Теорема о неполноте о формулах (программах) в формальных системах (стандарте языка Си).
Повторюсь: Гёдель писал о том, что в любой самореферентной формальной системе будут либо правдивые утверждения, которые нельзя доказать (т.е. аксиомы), либо ложные утверждения, которые доказать можно (т.е. херота). Си здесь никаким боком не при делах.
Есть такие же без «проблемы остановки»?
Проблема останова является свойством любой Тьюринг-полной системы, но к UB отношения не имеет.
UB может быть бесконечным циклом.
Не может. Это вполне определённое поведение.
В моём примере выше бесконечный цикл появился в результате трансформаций кода компилятором, но точно так же так мог появиться любой другой дефект.
Как доказать, что программа завершиться, не имеет UB приводящий к бесконечному цику?
Причём здесь Си?