=====
>>> main.whiley
property read(int[] items, int i) -> (int v):
   return items[i]

public export method test():
   assert read([1,2,3],0) == 1
   assert read([1,2,3],1) == 2
   assert read([1,2,3],2) == 3   
---
E724 main.whiley 2,16
=====
>>> main.whiley 1:2
property read(int[] items, int i) -> (int v)
requires 0 < i && i < |items|:
---
E700 main.whiley 6,10:24
E716 main.whiley 0,0:0
=====
>>> main.whiley 2:3
requires 0 <= i && i <= |items|:
---