// This example shows (a) how contracts are written and used in DL, specifically
// for the transaction abort branch (note the prime symbold in setAcontract_tra)
// (b) that subsequent transactions are properly handled.
// For this example it is essential to use "... Using Method Contracts" strategy

\javaSource "code/";

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

\programVariables {
  MyClass self;
  int a;
}

\contracts {
  setAcontract {
    true -> \<{ self.setAtoZero()@MyClass; }\> (self.a = 0)
    \modifies { self.a }
  };

  setAcontract_tra {
    true -> \diamond_tra{ self.setAtoZero()@MyClass; }\endmodality (self.a' = 0)
    \modifies { self.a' } 
  };
}

\problem {
javacard.framework.JCSystem._transactionDepth = 0 &
!self = null ->
\<{
   self.a = 10;
   javacard.framework.JCSystem.beginTransaction();
      self.setAtoZero();
   javacard.framework.JCSystem.abortTransaction();
   self.a = 10;
   javacard.framework.JCSystem.beginTransaction();
      self.setAtoZero();
   javacard.framework.JCSystem.abortTransaction();
}\> (self.a = 10)

}