Operation: read

Section Read.



Variable s: SFSstate.



Operation definition



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

  |ReadOK:
     (ObjType o)=File
     ->Cases (fsecmat (secmat s) o) of
        |None => False
        |(Some y) => (set_In u (ActReaders y))
       end -> (read u o n s
                    Cases (fsecmat (secmat s) o)
                          (ffiles (files s) o) of
                     |None _ => (None FILECONT)
                     |_ None => (None FILECONT)
                     |(Some y)
                      (Some z) => (Some FILECONT (take n z))
                    end).



End Read.