May 15th, 2017

Gen.Turgidson

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

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) они не выводятся. механика этого понятна - но как-то не очень понятен смысл.

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