Termination checking

[levjj]

Check loops and recursive functions for termination. This requires an explicit annotation with a well founded measure such as "decreases" from LiquidHaskell or even a specified relation between iterations.

Examples:

let i = 0;
while (i < 23) {
  invariant(Number.isInteger(i) && i <= 23);
  decreases(23 - i); // Loop termination verified
  i++;
}

function even(n) {
  requires(Number.isInteger(n) && n >= 0);
  decreases(n); // Termination of recursive function verified
  if (n === 0) return true;
  if (n === 1) return false;
  return even(n - 2);
}