-- Dispatcher

-- import java.lang.*;
-- import javacard.framework.*;


package javacard::framework::service



context Dispatcher::Dispatcher(maxServices: JShort)
  pre : true
  post: not excThrown(java::lang::Exception)
	or
	(
	   excThrown(ServiceException)
	   and
	   ServiceException.systemInstance.getReason().asInt()
	      = ServiceException.ILLEGAL_PARAM
	   and
	   maxServices.asInt() < 0	            
	)



context Dispatcher::addService(service: Service, phase: JByte)
  pre : true
  post: not excThrown(java::lang::Exception)
	or
	(
	   excThrown(ServiceException)
	   and
	   (
	      (
	         ServiceException.systemInstance.getReason().asInt()
	            = ServiceException.ILLEGAL_PARAM
	         and
	         (
	            (
	               phase.asInt() <> Dispatcher.PROCESS_NONE
		       and
	               phase.asInt() <> Dispatcher.PROCESS_INPUT_DATA
		       and
	               phase.asInt() <> Dispatcher.PROCESS_COMMAND
		       and
	               phase.asInt() <> Dispatcher.PROCESS_OUTPUT_DATA
	            )
	            or
	            service = null
	         )
	      )
	      or
	      ServiceException.systemInstance.getReason().asInt()
	         = ServiceException.DISPATCH_TABLE_FULL            
	   )
        )



context Dispatcher::removeService(service: Service, phase: JByte)
  pre : true
  post: not excThrown(java::lang::Exception)
	or
	(
           excThrown(ServiceException)
	   and
	   ServiceException.systemInstance.getReason().asInt()
	      = ServiceException.ILLEGAL_PARAM
	   and
	   (
	      (
	         phase.asInt() <> Dispatcher.PROCESS_NONE
		 and
	         phase.asInt() <> Dispatcher.PROCESS_INPUT_DATA
		 and
	         phase.asInt() <> Dispatcher.PROCESS_COMMAND
		 and
	         phase.asInt() <> Dispatcher.PROCESS_OUTPUT_DATA
	      )
	      or
	      service = null
	   )           
	)



context Dispatcher::dispatch(command: APDU, phase: JByte): Exception
  pre : true
  post: not excThrown(java::lang::Exception)
	or
	(
	   excThrown(ServiceException)
	   and
	   ServiceException.systemInstance.getReason().asInt()
	      = ServiceException.ILLEGAL_PARAM
	   and
	   phase.asInt() <> Dispatcher.PROCESS_INPUT_DATA
           and
	   phase.asInt() <> Dispatcher.PROCESS_COMMAND
           and
	   phase.asInt() <> Dispatcher.PROCESS_OUTPUT_DATA           
	)



context Dispatcher::process(command: APDU)
  pre : true
  post: not excThrown(java::lang::Exception)
	or
	excThrown(javacard::framework::ISOException)



endpackage