Снова о статической типизации

Запускал. Но результат 0 в коде неоднозначен: он трактуется и как «проверка пройдена» и как «ошибка при запуске с номером 0».

Программа проверки оказалась с ошибкой.

Большое спасибо за ответ. Всегда немного восхищался твоим умением быстро замечать опечатки/ошибки/неоднозначности.

Ниже краткий пересказ для интересующихся.
AndreyKl:

Тут есть ещё такой момент… Ты клянешься что код корректен?

monk:

Ага. Я его проверил:...
Запускал. Но результат 0 в коде неоднозначен: он трактуется и как «проверка пройдена» и как «ошибка при запуске с номером 0».
Программа проверки оказалась с ошибкой.

Я думал что плохой пример, но он по стечению обстоятельств оказался просто замечательным!

Очередной гипотетический Фобос направили в грунт, да только не в тот что надо, а на дно Земного океана те самые программисты «я клянусь у меня работает, я запускал и проверил», которые, к слову, сильно сомневались в ценности формальной верификации. А специалисты по формальной верификации на белом коне нашли ошибку даже в таком наидремучейшем лесу как функция Коллатца, который ни с каким проводником вообще не пройдёшь (хотя честно говоря ну вообще не чаяли).

Полный триумф технологии в отдельно взятой ветки дискуссии благодаря удачному примеру от monk! Спасибо большое ещё раз! (Без шуток, удачно вышло. Общая эрудированность оппонента и умение вести дискуссию и ставить острые и верные вопросы сыграли как нельзя лучше. Если б ты меня не допрашивал я б не полез туда, руки не поднимались в такие дебри.. там конечно один чёрт ничего не доказалось (и не докажется), но ошибка то нашлась!)

На этом я думаю данную ветку обсуждения можно завершить. Вернусь к мьютексам.

PS. Про «клянёшься» конечно был шуточный вопрос, как и ответ я думаю. Гипербола.

там конечно один чёрт ничего не доказалось (и не докажется), но ошибка то нашлась!

Там проверилось, что на 1…100000000000 f вернула значение, а не завершилась по таймауту.

Вот исправленная проверялка

(defconstant +N+ 100000000000)

(defun f (k n)
  (declare (type (integer 0 100000000000) k n))
  (cond
    ((= k 1) 1)
    ((zerop n) 'fail)
    ((zerop (rem k 2)) (f (/ k 2) (1- n)))
    (t (f (1+ (* 3 k)) (1- n)))))

(defun test ()
  (dotimes (n +N+)
    (when (> n 0)
      (if (eq (f n +N+) 'fail) (return n))))
  (return-from test 'ok))

(format t "~a" (test))

Кстати, что делать с доказательной проверкой, когда текст функции на Coq и текст изначальной проверяемой функции на Си++ или Ocaml не совпадают? Ведь тоже может получиться, что проверили не то, что дано, а то, что предположительно поняли.

Круто, должно работать. Но твой способ единственный в данном случае. Никуда не денешься, так тоже бывает.

Кстати, что делать с доказательной проверкой, когда текст функции на Coq и текст изначальной проверяемой функции на Си++ или Ocaml не совпадают? Ведь тоже может получиться, что проверили не то, что дано, а то, что предположительно поняли.

Заворачивать исходный текст в монаду в целью чтобы текст совпадал практически полностью.

Желательно иметь автоматическую трансляцию, как вот тут например https://github.com/formal-land/coq-of-rust

Желательно иметь автоматическую трансляцию

Какая она жуткая…

И в неё достаточно сложно втыкать дополнительные ограничения, которых нет в Rust, так как там нет зависимых типов. А если начинаем что-то втыкать в транслированный код, то автоматически теряем связь с изначальным.

По-моему, подход https://github.com/verus-lang/verus лучше.

Какая она жуткая…

Ну, я согласен что покрасивее - поприятнее. Но это не очень важно на самом деле. Иногда бывает прям сильно покрасивее получается. Но это вопрос уже конечно некоторых дополнительных усилий - чтобы было красиво.

И в неё достаточно сложно втыкать дополнительные ограничения, которых нет в Rust, так как там нет зависимых типов. А если начинаем что-то втыкать в транслированный код, то автоматически теряем связь с изначальным.

Это не так задумано.
У нас есть исходный код на Расте. Мы транслируем его в код на кок. Это наша модель. С большой долей уверенности можно говорит что она соотвествует оригинальному коду, так как

1) это бекэнд к оригинальному компилятору раста (т.е. парсинг и построение дерева выполняет rustc)

2) транслятор транслирует 99% примеров из rust by examples (т.е. тесты есть)

Имея эту модель, нужно просто писать про неё свои утверждения непосредственно в коке. Т.е. не нужно менять код модели, нужно писать утверждения o модели.

Т.е. например если у нас есть на расте функция (прошу прощения заранее, пример не компилировал, раст больше года не видел)

fn myfun(n) -> nat { return n + 1 }

Lemma myfun_correct n : myfun n = n + 1.

fn myfun(n) -> nat { return n + 1 }

Вот давай тогда прямо из примера, там именно это.

Rust:

fn add_one(x: u32) -> u32 {
    x + 1
}

Coq:

Definition add_one (τ : list Ty.t) (α : list Value.t) : M :=
  match τ, α with
  | [], [ x ] =>
    ltac:(M.monadic
      (let x := M.alloc (| x |) in
      BinOp.Panic.add (| M.read (| x |), Value.Integer Integer.U32 1 |)))
  | _, _ => M.impossible
  end.

И как сюда воткнуть утверждение типа «Для x от 0 до 1000 вернётся от 1 до 1001 и ошибки не будет»?

И как сюда воткнуть утверждение типа «Для x от 0 до 1000 вернётся от 1 до 1001 и ошибки не будет»?

ну ты прям с места в карьер...

навскидку, если я верно понял что там как, наверное вот так примерно:

Lemma add_one_correct x : 0 <= x <= 1000 ->
  exist res, 1 <= res <= 1001 /\ add_one _ [ x ] = M.return res.

навскидку, если я верно понял что там как, наверное вот так примерно:

То есть для каких-либо дополнительных утверждений о зависимостях параметров и результатов внутрь транслированного тела функции лезть не надо.

Хорошо, тогда всё не так страшно, как я предполагал. В минусе только то, что функция становится минимальной единицей: хочешь что-то утверждать про кусок кода в функции, выноси в отдельную. Впрочем, кому-то это, наоборот, в плюс.

Говоря кратко - в чуть более сложных случаях это сводится к очень интенсивному тестированию.

Эм, а как же Z3Prover которым код винды тестируют. Да, качество кода винды это довольно слабый пример, но все же.

Z3Prover - это smt солвер. Это способ ответа на вопрос «как решить уравнение». BMC (bounded model checking) - это способ ответа на вопрос «как построить уравнение».

PS. Это хоть и близкая мне тема, но не моя.

Ну да, там как раз представляют код в виде уравнения и суют параметры, а солвер говорит решаемо или не решаемо.

То есть для каких-либо дополнительных утверждений о зависимостях параметров и результатов внутрь транслированного тела функции лезть не надо.

Верно.

В минусе только то, что функция становится минимальной единицей: хочешь что-то утверждать про кусок кода в функции, выноси в отдельную.

В принципе можно вынести из тела функции кусок и сформулировать о нём утвреждение, почему нет. Потом это можно использовать для доказательства какого то утверждения о функции (частью тела которой является вынесенный код). Но это детали процесса, там как удобнее.

Ну да, там как раз представляют код в виде уравнения и суют параметры, а солвер говорит решаемо или не решаемо.

Да, верно. И вот можно создать уравнения которые полностью описывают систему (или нельзя.. не знаю точно). Но они обычно либо нерешаемы в принципе, либо за конечно время не решаются, либо решаются за конечное но очень большое.

Можно ограничить диапазоны переменных (собственно поэтому и bounded емнип). Тогда они решаются лучше. Чем меньше диапазон, тем быстрее, ясное дело.

Ну вот там нужно обычно найти баланс между надёжностью и собственно тем чтобы даже на больших компрьютерах дождаться какого то решения.

И вот можно создать уравнения которые полностью описывают систему (или нельзя.. не знаю точно).

нельзя. задача трех тел.

Ну у нас то система дискретная. Не дифурами описывается, а обычными линейными уравненияии или около того. При чем тут задача трёх тел?

вам везет. а в жизни все сложнее.

Да, верно. И вот можно создать уравнения которые полностью описывают систему (или нельзя.. не знаю точно). Но они обычно либо нерешаемы в принципе, либо за конечно время не решаются, либо решаются за конечное но очень большое.

Я как то сумбурно описываю, прошу прощения. По сути в этих моделях на сколько я помню (год назад смотрел) просто перебираются все возможные состояния переменных. Но у некоторых, вроде массивов, к примеру, диапазон приходится как то ограничивать в любом случае, поскольку возможных состояний может быть бесконечно много (ну или очень много на практике). Но даже ограничивая бесконечные состояния, мы получаем систему, не решаемую за разумное время. Поэтому диапазоны переменных ограничивают ещё больше. Поэтому bounded. Вроде суть такая.

вам везет. а в жизни все сложнее.

Ну, у дифурщиков и прочих матанщиков своя особая красота.

нельзя. задача трех тел.

Можно, но с допущениями. Там линейные уравнения, а взаимодействие между блоками кода считается по методу Рандеву (мгновенное) и тут самая большая засада в символьной алгебре доказательств, пол века над этим бьются, а воз и ныне там.

https://andreykl.github.io/mapcar/mutex.html

Там первые 185 строк - эмуляция монады IO.

Далее в модуле Program есть индуктивный тип t который содержит описание возможных состояний трёх мьютексов нашей программы и возможные переходы между ними. Плюс ещё одна операция - PutStrLn, очевидная, индифферентная к состояниям мьютексов, для разнообразия.

Примеры начинаются с 282 строки. Пример testOK - переключаем мьютексы правильно - всё получается. Пример justReturn5TestOK - без переключения мьютексов, всё работает. Пример testFailWrongOrder - пытаемся залочить первый мьютекс (успешно) и сразу разлочить его же (нарушение порядка, ошибка компиляции).

Запускаем внизу testOK.

wandrien, monk

пытаемся залочить первый мьютекс (успешно) и сразу разлочить его же (нарушение порядка, ошибка компиляции).

Но это должен быть корректный кейс.

В общем, немного не та задача решалась.

Но это должен быть корректный кейс.

гм.. не понял, поясни пжл.

а, понял.. да не, нормально всё. так по условиям: лочим только в порядке 1,2,3, разлочиваем только в порядке 2, 1, 3 (они там описаны).

Можно выбрать любой порядок лока/анлока. И не единственным образом, если нужно.

Вот тут я описывал:

Снова о статической типизации (комментарий)

Не должно быть двух независимых цепочек захвата мьютексов в рамках одного потока управления.

В цепочке не должно быть нарушения последовательности сортировки мьютексов.

Всё остальное возможно.

Вот тут я описывал:

Снова о статической типизации (комментарий)

Не должно быть двух независимых цепочек захвата мьютексов в рамках одного потока управления.

В цепочке не должно быть нарушения последовательности сортировки мьютексов.

Всё остальное возможно.

Я это описание как то пропустил.

У меня решается задача из ОП

Усложненный вариант задачи.
В программе имеются мьютексы m1, m2… mN.
Необходимо гарантировать, что при любом пути исполнения кода захват и освобождение мьютексов выполняется в фиксированной последовательности, что гарантирует отсутствие деадлоков для данного набора мьютексов.

Словосочетание «фиксированная последовательность» было понято именно как однозначно фиксированная, т.е. нет возможности заблокировать двумя разными способами.

Данный код по моему нельзя расширить до трактовки «в любой последовательности лишь бы больший номер после меньшего и разлочивать строго в обратной к залоченной».

Но в целом описанная задача тоже должна решаться. Не знаю, может вернусь к ней.

В некоторых языках можно написать операции суммирования, возвращающие число гарантированно того же диапазона, либо ошибку

Примерно об этом речь?

class Temperature():
    def __init__(self, num):
        if isinstance(num, int) and num >= 0:
            self.__num = num
        else:
            raise ValueError("Temperature value must be integer and not lower 0")