-- interface Service


package javacard::framework::service



context Service::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 Service::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() = APDU::STATE_OUTGOING



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



endpackage