original.name="While_Valid_40"
======
>>> main.whiley
function contains(int[] items, int item) -> (bool r)
ensures r ==> some { i in 0 .. |items| | item == items[i] }:
//
int i = 0
//
while i < |items| where i >= 0:
if items[i] == item:
return true
i = i + 1
//
return false
public export method test():
int[] ls = [1,2,3,4]
assume contains(ls,0) == false
assume contains(ls,1) == true
assume contains(ls,2) == true
assume contains(ls,3) == true
assume contains(ls,4) == true
assume contains(ls,5) == false
---