English: If the offset is greater than or equal to the size of the file, the status, NFS4_OK, is returned with a data length set to 0 (zero), and eof is set to TRUE.
Lexicon: A return B with C : return(E) WITH E.A WITH E.B WITH E.C
STL: ALWAYS ( offset >= get_size(file) -> return(E) WITH E.NFS4_OK WITH E.get_length(data)=0 WITH E.eof=TRUE
English: If the client specifies a count value of 0 (zero), the READ succeeds and returns 0 (zero) bytes of data (subject to access permissions checking).
Lexicon: subject to access permissions checking: read_perm_ok(E),return A: return(E) WITH E.A
STL: ALWAYS ( count = 0  AND read_perm_ok(cfh) -> return(E) WITH E.NFS4_OK WITH E.get_length(data)=0 WITH E.current_eof )
English: If the READ ended at the end-of-file (formally, in a correctly formed READ request, if offset + count is equal to the size of the file), or the READ request extends beyond the size of the file (if offset + count is greater than the size of the file), eof is returned as TRUE ; otherwise, it is FALSE.
Lexicon:
STL: ALWAYS ( offset+count==get_size(file) OR offset+count>get_size(file) -> return(E) WITH E.eof=True OR NOT ( offset+count==get_size(file) OR offset+count>get_size(file) ) -> return(E) WITH E.eof=FALSE )
English: If the current filehandle is not a regular file, an error will be returned to the client.
Lexicon: current filehandle:cfh, A is a regular file: is_regular(E) WITH E.A
STL:  Provide your reponse without using the word file.
user