Operation: write



Implicit Arguments Off.



Section Write.



Variable s: SFSstate.



Next state definition



Local t [o:OBJECT; n:nat; buf:FILECONT] : SFSstate :=

   (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s)
          (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s)
          (secmat s) (write_files o n buf) (directories s)).



Operation definition



Inductive write
  [u:SUBJECT; o:OBJECT; n:nat; buf:FILECONT]: SFSstate -> Prop :=

  |WriteOK:
     (ObjType o)=File
     ->Cases (fsecmat (secmat s) o) of
        |None => False
        |(Some y) => (set_In u (ActWriters y))
     end -> (write u o n buf (t o n buf)).



End Write.