Operation: owner_close



Section Owner_Close.



Variable s: SFSstate.



Some preliminary definitions



Definition NEWRWOC
 [u:SUBJECT; o:OBJECT; y:ReadersWriters] : ReadersWriters :=
 (mkRW (set_remove SUBeq_dec u (ActReaders y))
       (set_remove SUBeq_dec u (ActWriters y))).



Local NEWSET
 [u:SUBJECT; o:OBJECT; y:ReadersWriters] :
 (set OBJECT*ReadersWriters) :=
  Cases (set_remove SUBeq_dec u (ActReaders y))
        (set_remove SUBeq_dec u (ActWriters y)) of
   |nil nil => (set_remove SECMATeq_dec (o,y) (secmat s))
   |_ _ => (set_add SECMATeq_dec
                        (o,(NEWRWOC u o y))
                        (set_remove SECMATeq_dec (o,y) (secmat s)))
  end.



Definition ownerclose_sm
 [u:SUBJECT; o:OBJECT]: (set OBJECT*ReadersWriters) :=

 Cases (fsecmat (secmat s) o) of
  |None => (secmat s)
  |(Some y) => (NEWSET u o y)
 end.



Next state definition



Local t [u:SUBJECT; o:OBJECT]: SFSstate :=

   (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s)
          (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s)
          (ownerclose_sm u o) (files s) (directories s)).



Operation definition

Inductive owner_close
  [owner,u:SUBJECT; o:OBJECT] : SFSstate -> Prop :=

  |Owner_CloseOK:
      Cases (fsecmat (secmat s) o) of
       |None => False
       |(Some y) => (set_In u
                             (set_union SUBeq_dec
                                        (ActReaders y) (ActWriters y)))
      end
      ->(ExecuterIsOwner s owner o)
      ->(owner_close owner u o (t u o)).



End Owner_Close.

Hints Unfold ownerclose_sm.