здесь явно какая-то мудрость;
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) они не выводятся. механика этого понятна - но как-то не очень понятен смысл.
Разве что из чистоплюйства заставить формулировать такие условия явно/