Add precondition in query i_th  Remove infix "@" which is deprecated now. Add invariant for values to show that it is always not Void. Add postcondition of add.
Add precondition in query i_th 
Remove infix "@" which is deprecated now.
Add invariant for values to show that it is always not Void.
Add postcondition of add.

git-svn-id: b8fc24f0e115b9c9c7e557c0b7b5b4cfa6bf3faf@22 387f9f67-f869-4f5a-9dd1-25509efca32b

Eiffel-World/ejson-svn