Operation: readdir



Section Readdir.



Variable s: SFSstate.



Operation definition

Inductive readdir
  [u:SUBJECT; o:OBJECT; n:nat] : SFSstate -> (Exc DIRCONT) -> Prop :=

  |ReaddirOK:
     (ObjType o)=Directory
     ->Cases (fsecmat (secmat s) o) of
        |None => False
        |(Some y) => (set_In u (ActReaders y))
       end -> (readdir u o n s
                       Cases (fsecmat (secmat s) o)
                             (fdirs (directories s) o) of
                        |None _ => (None DIRCONT)
                        |_ None => (None DIRCONT)
                        |(Some y)
                         (Some z) => (Some DIRCONT (take n z))
                       end).



End Readdir.