// This example shows how different combination of normal assignments and non
// atomic assignments affect the perservation of a strong invariant

\javaSource "code/";

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

\programVariables {
  MyClass self;
}

\problem {
javacard.framework.JCSystem._transactionDepth = 0 &
!self = null & !self.b = null & self.b.length = 2 
& self.b.<transient> = 0 & self.b[0] > 0 ->
\[[{
   self.b[0] = 1;
   javacard.framework.JCSystem.beginTransaction();
     // self.b[0] = -1;
     // for last arg. -5 and without the line above should NOT be provable
     // for last arg. -5 and with the line above should be provable
     // for last arg. 5 should be provable with and without the line above
     javacard.framework.Util.arrayFillNonAtomic(self.b, (short)0, (short)1, (byte)5);
     self.b[0] = -2;
   javacard.framework.JCSystem.abortTransaction();
}\]] (self.b[0] > 0)

}