// This shows how creation of transient arrays is handled as opposed to 
// persitent arrays.

\javaSource "code/";

\withOptions transactions:transactionsOn,
             transactionAbort:abortOn,
	     intRules:arithmeticSemanticsIgnoringOF;

\programVariables {
  short[] a;
  short[] b;
}

\problem {
  \<{ 
    a = new short[2]; 
    b = javacard.framework.JCSystem.makeTransientShortArray((short)2, javacard.framework.JCSystem.CLEAR_ON_RESET); 
  }\> (!a.<transient> = b.<transient> & a.length = b.length)
}