-- CardRemoteObject implements Remote

-- import java.rmi.*;


package javacard::framework::service



context CardRemoteObject::CardRemoteObject()
  pre : true
  post: true



-- static
context CardRemoteObject::export(obj: Remote)
  pre : true
  post: not excThrown(java::lang::Exception)
        or
        excThrown(java::lang::SecurityException)



-- static
context CardRemoteObject::unexport(obj: Remote)
  pre : true
  post: not excThrown(java::lang::Exception)
        or
        excThrown(java::lang::SecurityException)



endpackage