История изменений
Исправление SZT, (текущая версия) :
Если руки все-таки дойдут — кастани :)
Пока покажу промежуточный результат. Я использовал нотацию от SMT-солвера alt-ergo https://paste.debian.net/hidden/ead1da5c/
Протестировать можно тут https://alt-ergo.ocamlpro.com/try.php только лучше поставить это через OPAM потому что так быстрее значительно. Не все те «юнит-тесты» завершаются успешно, но это обусловлено лишь исключительно тем, что солвер не может выбрать стратегию правильную и не пытается очень сильно «разворачивать» сдвиги. Там (если собрать себе этот alt-ergo на локалхост без жабаскриптов) есть возможность посмотреть то, каким образом доказывается верность утверждения
Немного о синтаксисе:
forall - квантор всеобщности. Есть еще квантор существования exists. Оператор -> — импликация. Есть встроенный тип int который принимает значения ... -4 -3 -2 -1 0 1 2 3 4 ... т.е. соответствует множеству целых чисел. Там уже есть встроенные операции умножения сложения деления и нахождения остатка от деления. Остальное должно быть самоочевидным.
через двоичные сдвиги я смогу нарезать инты большие чем или равные 0 на массив из 8-битных unsigned char. И еще нарезать для хранения самого «алфавита» брейнфака < > + - . , [ ]. В alt-ergo есть теория для массивов, но я массивы определю через неотрицательные инты, чтоб не возникало вопросов. Отдельным положительным интом будет хранится положение «указателя» на ленте с инструкциями, и еще одним - положение на ленте с ячейками памяти. Еще один инт будет нужен чтобы проматываться между скобочками [ ]. Далее, можно ввести понятия «шага» брейнфака, чтобы на каждом шаге инкрементировать некую переменную, и тогда можно будет попросить SMT солвер решить «а будет ли на таком-то шаге такое-то состояние у нашей брейнфак-машины?». Вообще это все очень напоминает какое-то функциональное программирование. Скоро доделаю
Исходная версия SZT, :
Если руки все-таки дойдут — кастани :)
Пока покажу промежуточный результат. Я использовал нотацию от SMT-солвера alt-ergo https://paste.debian.net/hidden/ead1da5c/
Протестировать можно тут https://alt-ergo.ocamlpro.com/try.php только лучше поставить это через OPAM потому что так быстрее значительно. Не все те «юнит-тесты» завершаются успешно, но это обусловлено лишь исключительно тем, что солвер не может выбрать стратегию правильную
Немного о синтаксисе:
forall - квантор всеобщности. Есть еще квантор существования exists. Оператор -> — импликация. Есть встроенный тип int который принимает значения ... -4 -3 -2 -1 0 1 2 3 4 ... т.е. соответствует множеству целых чисел. Там уже есть встроенные операции умножения сложения деления и нахождения остатка от деления. Остальное должно быть самоочевидным.
через двоичные сдвиги я смогу нарезать инты большие чем или равные 0 на массив из 8-битных unsigned char. И еще нарезать для хранения самого «алфавита» брейнфака < > + - . , [ ]. В alt-ergo есть теория для массивов, но я массивы определю через неотрицательные инты, чтоб не возникало вопросов. Отдельным положительным интом будет хранится положение «указателя» на ленте с инструкциями, и еще одним - положение на ленте с ячейками памяти. Еще один инт будет нужен чтобы проматываться между скобочками [ ]. Далее, можно ввести понятия «шага» брейнфака, чтобы на каждом шаге инкрементировать некую переменную, и тогда можно будет попросить SMT солвер решить «а будет ли на таком-то шаге такое-то состояние у нашей брейнфак-машины?». Вообще это все очень напоминает какое-то функциональное программирование. Скоро доделаю