-- BasicService implements Service

-- import javacard.framework.*;


package javacard::framework::service


context BasicService::BasicService()
  pre : true
  post: true



context BasicService::fail(apdu: APDU, sw: JShort): Boolean
  pre : true
  post: not excThrown(java::lang::Exception)
	or
	(
	   excThrown(ServiceException)
	   and
	   ServiceException.systemInstance.getReason().asInt()
	      = ServiceException::CANNOT_ACCESS_OUT_COMMAND
	   and
	   apdu.getCurrentState().asInt() < 0	            
	)



context BasicService::getCLA(apdu: APDU): JByte
  pre : true
  post: not excThrown(java::lang::Exception)
	and
	result.asInt() = apdu.getBuffer()->at(ISO7816.OFFSET_CLA).asInt()



context BasicService::getINS(apdu: APDU): JByte
  pre : true
  post: not excThrown(java::lang::Exception)
	and
	result.asInt() = apdu.getBuffer()->at(ISO7816.OFFSET_INS).asInt()



context BasicService::getP1(apdu: APDU): JByte
  pre : true
  post: (
           not excThrown(java::lang::Exception)
	   and
	   result.asInt() 
              = apdu.getBuffer()->at(ISO7816.OFFSET_P1).asInt()
        )
        or
	(
	   excThrown(ServiceException)
	   and
	   ServiceException.systemInstance.getReason().asInt()
	      = ServiceException.CANNOT_ACCESS_IN_COMMAND
	   and
	   apdu.getCurrentState().asInt() <> APDU::STATE_INITIAL
	   and
	   apdu.getCurrentState().asInt() <> APDU::STATE_FULL_INCOMING
	)



context BasicService::getP2(apdu: APDU): JByte
  pre : true
  post: (
           not excThrown(java::lang::Exception)
	   and
	   result.asInt() 
              = apdu.getBuffer()->at(ISO7816.OFFSET_P2).asInt()
        )
        or
	(
	   excThrown(ServiceException)
	   and
	   ServiceException.systemInstance.getReason().asInt()
	      = ServiceException.CANNOT_ACCESS_IN_COMMAND
	   and
	   apdu.getCurrentState().asInt() <> APDU::STATE_INITIAL
	   and
	   apdu.getCurrentState().asInt() <> APDU::STATE_FULL_INCOMING
	)



context BasicService::getOutputLength(apdu: APDU): JShort
  pre : true
  post: not excThrown(java::lang::Exception)
	or
	(
	   excThrown(ServiceException)
	   and
	   ServiceException.systemInstance.getReason().asInt()
	      = ServiceException.CANNOT_ACCESS_OUT_COMMAND
	   and
	   (
	      apdu.getCurrentState().asInt() < 0	 
	      or
	      self.isProcessed(apdu)
	   )           
	)



context BasicService::getStatusWord(apdu: APDU): JShort
  pre : true
  post: not excThrown(java::lang::Exception)
	or
	(
	   excThrown(ServiceException)
	   and
	   ServiceException.systemInstance.getReason().asInt()
	      = ServiceException.CANNOT_ACCESS_OUT_COMMAND
	   and
	   (
	      apdu.getCurrentState().asInt() < 0	 
	      or
	      self.isProcessed(apdu)
	   )           
	)



context BasicService::processDataIn(apdu: APDU): Boolean
  pre : apdu.getCurrentState().asInt() = APDU.STATE_INITIAL
	or
	apdu.getCurrentState().asInt() = APDU.STATE_FULL_INCOMING
  post: not excThrown(java::lang::Exception)
	and
	(
	   apdu.getCurrentState().asInt() = APDU.STATE_FULL_INCOMING
	   or
	   apdu.getCurrentState().asInt() = APDU.STATE_OUTGOING
	)



context BasicService::processCommand(apdu: APDU): Boolean
  pre : apdu.getCurrentState().asInt() = APDU.STATE_INITIAL
	or
	apdu.getCurrentState().asInt() = APDU.STATE_FULL_INCOMING
	or
	apdu.getCurrentState().asInt() = APDU.STATE_OUTGOING
  post: not excThrown(java::lang::Exception)
	and
	apdu.getCurrentState().asInt() = APDU.STATE_OUTGOING



context BasicService::processDataOut(apdu: APDU): Boolean
  pre : apdu.getCurrentState().asInt() = APDU.STATE_OUTGOING
  post: not excThrown(java::lang::Exception)
	and
	apdu.getCurrentState().asInt() = APDU.STATE_OUTGOING



context BasicService::receiveInData(apdu: APDU): JShort
  pre : true
  post: not excThrown(java::lang::Exception)
	or
	(
	   excThrown(ServiceException)
	   and
	   (
	      (
	         ServiceException.systemInstance.getReason().asInt()
	            = ServiceException.CANNOT_ACCESS_IN_COMMAND
	         and
	         apdu.getCurrentState().asInt() <> APDU::STATE_INITIAL
	         and
	         apdu.getCurrentState().asInt() 
                    <> APDU::STATE_FULL_INCOMING
	      )
	      or
	      ServiceException.systemInstance.getReason().asInt()
	         = ServiceException.COMMAND_DATA_TOO_LONG
	   )
	)



context BasicService::setProcessed(apdu: APDU)
  pre : true
  post: not excThrown(java::lang::Exception)
	or
	(
	   excThrown(ServiceException)
	   and
	   ServiceException.systemInstance.getReason().asInt()
	      = ServiceException.CANNOT_ACCESS_OUT_COMMAND
	   and
	   apdu.getCurrentState().asInt() < 0	            
	)



context BasicService::isProcessed(apdu: APDU): Boolean
  pre : true
  post: not excThrown(java::lang::Exception)



context BasicService::setOutputLength(apdu: APDU, length: JShort)
  pre : true
  post: not excThrown(java::lang::Exception)
	or
	(
	   excThrown(ServiceException)
	   and
	   ServiceException.systemInstance.getReason().asInt()
	      = ServiceException.ILLEGAL_PARAM	            
	)



context BasicService::getOutputLength(apdu: APDU): JShort
  pre : true
  post: not excThrown(java::lang::Exception)
	or
	(
	   excThrown(ServiceException)
	   and
	   ServiceException.systemInstance.getReason().asInt()
	      = ServiceException.CANNOT_ACCESS_OUT_COMMAND
	   and
	   (
	      apdu.getCurrentState().asInt() < 0	 
	      or
	      self.isProcessed(apdu)
	   )           
	)



context BasicService::setStatusWord(apdu: APDU, sw: JShort)
  pre : true
  post: not excThrown(java::lang::Exception)



context BasicService::succeed(apdu: APDU): Boolean
  pre : true
  post: not excThrown(java::lang::Exception)
	or
	(
	   excThrown(ServiceException)
	   and
	   ServiceException.systemInstance.getReason().asInt()
	      = ServiceException.CANNOT_ACCESS_OUT_COMMAND
	   and
	   apdu.getCurrentState().asInt() < 0	            
	)



context BasicService::succeedWithStatusWord(apdu: APDU, 
                                            sw: JShort): Boolean
  pre : true
  post: not excThrown(java::lang::Exception)
	or
	(
	   excThrown(ServiceException)
	   and
	   ServiceException.systemInstance.getReason().asInt()
	      = ServiceException.CANNOT_ACCESS_OUT_COMMAND
	   and
	   apdu.getCurrentState().asInt() < 0	            
	)



context BasicService::selectingApplet(): Boolean
  pre : true
  post: true



endpackage