original.name="While_Valid_30"
======
>>> main.whiley
function duplicate(int n) -> (int r)
requires n >= 0
ensures r == 2*n:
//
int i = 0
int x = 0
while i < n where i <= n && x == 2*i:
x = x + 2
i = i + 1
return x
public export method test():
assume duplicate(0) == 0
assume duplicate(1) == 2
assume duplicate(2) == 4
assume duplicate(3) == 6
assume duplicate(4) == 8
assume duplicate(5) == 10
assume duplicate(6) == 12
assume duplicate(7) == 14
assume duplicate(8) == 16
assume duplicate(9) == 18
---