История изменений
Исправление AndreyKl, (текущая версия) :
И как сюда воткнуть утверждение типа «Для x от 0 до 1000 вернётся от 1 до 1001 и ошибки не будет»?
ну ты прям с места в карьер...
навскидку, если я верно понял что там как, наверное вот так примерно:
Lemma add_one_correct x : 0 <= x <= 1000 ->
exist res, 1 <= res <= 1001 /\ add_one _ [ x ] = M.return res.
Чтобы точнее сказать, это надо пойти поставить, скомпилировать.
Исходная версия AndreyKl, :
И как сюда воткнуть утверждение типа «Для x от 0 до 1000 вернётся от 1 до 1001 и ошибки не будет»?
ну ты прям с места в карьер...
навскидку, если я верно понял что там как, наверное вот так примерно:
Lemma add_one_correct x : 0 <= x <= 1000 ->
exist res, 1 <= res <= 1001 /\ add_one _ [ x ] = return res.
Чтобы точнее сказать, это надо пойти поставить, скомпилировать.