01: package src;
02:
03: import javacard.framework.JCSystem;
04:
05: /**
06: * @throughout self.logFile.log.get(self.logFile.currentRecord).balance =
07: * self.balance
08: * @invariants self.logFile <> null
09: */
10: public class Client {
11:
12: LogFile logFile;// = new LogFile();
13: int balance = 1000;
14: SaleDate currentDate;
15:
16: public Client() {
17: }
18:
19: /**
20: * @preconditions self.logFile <> null and self.currentDate <> null and
21: * self.logFile.log <> null and self.logFile.logFileSize = 20 and
22: * self.logFile.log.length = self.logFile.logFileSize and
23: * self.logFile.currentRecord >=0 and self.logFile.currentRecord < self.logFile.logFileSize
24: * @postconditions true
25: */
26: public void processSale(int amount, int sellerId) {
27: JCSystem.beginTransaction();
28: balance -= amount;
29: if (balance < 0)
30: JCSystem.abortTransaction();
31: else {
32: logFile.addRecord(balance, currentDate, sellerId);
33: JCSystem.commitTransaction();
34: }
35: }
36: }
|