kouzdra (kouzdra) wrote,
kouzdra
kouzdra

здесь явно какая-то мудрость;

module Test

use import ref.Ref
use import int.Int

let  rev1 (n : int)  =
    let i = ref 0 in
    let j = ref n in
    while !i < !j do
         variant { !j - !i }
         invariant { 0  <= !i }
         invariant { !j <=  n }
         assert { 0 <= !j };
         assert { !i  <= n};
         i := !i + 1;
         j := !j - 1
     done
end


Оба инварианта при всей своей очевидности работают только будучи заявленными именно как инварианты - как просто условия (скажем assert) они не выводятся. механика этого понятна - но как-то не очень понятен смысл.

Разве что из чистоплюйства заставить формулировать такие условия явно/
Subscribe

  • "Вам Шура не завидно? Мне завидно"

    Ко Дню Победы, Илон Маск и компания SpaceX осуществили десятый повторный полет первой ступени. Ускоритель Falcon 9 Block 5 под номером B1051 поднялся…

  • "Иликой пабеды прозник"

    Щас subj положено плясать - хотя нынешняя россияния имеет к нему примерно столько же как и украиния. Эту войну выиграли совсем другие страны. И…

  • Вдогонку к предыдущему:

    Экспедицию Франклина на "Эребусе" и "Терроре" убил imho именно социальный распад группы - если бы не он - остальное все можно было бы пусть и с…

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 12 comments

  • "Вам Шура не завидно? Мне завидно"

    Ко Дню Победы, Илон Маск и компания SpaceX осуществили десятый повторный полет первой ступени. Ускоритель Falcon 9 Block 5 под номером B1051 поднялся…

  • "Иликой пабеды прозник"

    Щас subj положено плясать - хотя нынешняя россияния имеет к нему примерно столько же как и украиния. Эту войну выиграли совсем другие страны. И…

  • Вдогонку к предыдущему:

    Экспедицию Франклина на "Эребусе" и "Терроре" убил imho именно социальный распад группы - если бы не он - остальное все можно было бы пусть и с…