test/coq/pass/while_PP_terminating.sail


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

default Order dec

$include <prelude.sail>

function test n : int -> int = {
  i : int = 1;
  j : int = 1;
  while i < n do {
    j = i * j;
    i = i + 1
  };
  j
}

termination_measure test while n - i