-- abstract class Applet


package javacard::framework


-- static
context Applet::install(bArray: Sequence(JByte),
                        bOffset: JShort,
                        bLength: JByte)
  pre : bArray <> null
        and
        -- Should it not be bOffset.asInt() >= 0
        bOffset.asInt() > 0
        and
        bLength.asInt() > 0
        and
        bOffset.asInt()+bLength.asInt() <= bArray->size()
  post: not excThrown(java::lang::Exception)
        or
        excThrown(java::lang::Exception)


-- abstract
context Applet::process(apdu: APDU)
  pre : apdu <> null
        and
        apdu.getCurrentState().asInt() = APDU.STATE_INITIAL
  post: not excThrown(java::lang::Exception)
        or
        excThrown(java::lang::Exception)


context Applet::select(): Boolean
  pre : true  -- this applet has been selected by the JCRE
  post: not excThrown(java::lang::Exception)
        or
        excThrown(java::lang::Exception)


context Applet::deselect()
  pre : true  -- this applet is currently selected and
              -- will be imminently deselected
  post: not excThrown(java::lang::Exception)
        or
        excThrown(java::lang::Exception)


context Applet::getShareableInterfaceObject(clientAID: AID,
                                            parameter: JByte): Shareable
  pre : true
  post: not excThrown(java::lang::Exception)
        or
        excThrown(java::lang::Exception)


-- protected final
context Applet::register()
  pre : true
  post: not excThrown(java::lang::Exception)
        or
        (
           excThrown(SystemException)
           and
           SystemException.systemInstance.getReason().asInt()
              = SystemException.ILLEGAL_AID
        )


-- protected final
context Applet::register(bArray: Sequence(JByte),
                         bOffset: JShort,
                         bLength: JByte)
  pre : true
  post: if 
        (
           bLength.asInt() >= 5 
           and
           bLength.asInt() <= 16
           and
           bOffset.asInt() >= 0
           and
           bArray->notEmpty()
           and
           bOffset.asInt()+bLength.asInt() <= bArray->size()
        )
        then
        (
           not excThrown(java::lang::Exception)
           or
           excThrown(TransactionException)
        )
        endif
        and
        (
           not excThrown(java::lang::Exception)
           or
           (
              excThrown(java::lang::NullPointerException)
              and
              bArray = null
           )
           or
           (
              excThrown(java::lang::ArrayIndexOutOfBoundsException)
              and
              (
                 bOffset.asInt() < 0
                 or
                 bLength.asInt() < 0
                 or
                 bOffset.asInt()+bLength.asInt() > bArray->size()
              )
           )
           or
           (
              excThrown(SystemException)
              and
              (
                 (
                    SystemException.systemInstance.getReason().asInt()
                       = SystemException.ILLEGAL_AID
                    and
                    (
                       bLength.asInt() < 5
                       or
                       bLength.asInt() > 16
                    )
                 )
                 or
                 (
                    SystemException.systemInstance.getReason().asInt()
                       = SystemException.ILLEGAL_VALUE
                    -- and
                    -- (
                    --  the AID bytes in bArray are already in use
                    --  or
                    --  the RID portion of the AID bytes does not match
                    --  the RID portion of the Java Card name of the applet
                    --  or
                    --  a JCRE initiated install() method execution is not
                    --  in progress
                    -- )
                 )   
              )
           )
        )


-- protected final
context Applet::selectingApplet(): Boolean
  pre : true
  post: true


endpackage