-- RMIService extends BasicService implements RemoteService
     
-- import java.rmi.*;


package javacard::framework::service



context RMIService::RMIService(initialObject: Remote)
  pre : true
  post: (
           not excThrown(java::lang::Exception)
           and
           not (initialObject = null)
        )
        or
        (
           excThrown(java::lang::NullPointerException)
           and
           initialObject = null
        )



context RMIService::setInvokeInstructionByte(ins: JByte)
  pre : true
  post: true



context RMIService::processCommand(apdu: APDU): Boolean
  pre : true
  post: (
           not excThrown(java::lang::Exception)
           and
           (
              apdu.getCurrentState().asInt() = APDU.STATE_INITIAL
              or
              apdu.getCurrentState().asInt() = APDU.STATE_FULL_INCOMING
           )
        )
        or
        (
           excThrown(ServiceException)
           and
           (
              (
                 ServiceException.systemInstance.getReason().asInt()
                    = ServiceException.CANNOT_ACCESS_IN_COMMAND
                 and
                 apdu.getCurrentState().asInt() <> APDU.STATE_INITIAL
                 or
                 apdu.getCurrentState().asInt() <> APDU.STATE_FULL_INCOMING
              )
              or
              ServiceException.systemInstance.getReason().asInt()
                 = ServiceException.REMOTE_OBJECT_NOT_EXPORTED
           )
        )
        or
        excThrown(java::lang::SecurityException)



endpackage