01: package src;
02:
03: /**
04: * @throughout self.empty = false implies (self.balance >= 0 and self.date <> null and self.transactionId > 0)
05: * @invariants self.empty = false implies (self.balance >= 0 and self.date <> null and self.transactionId > 0)
06: */
07: public class LogRecord {
08: private int balance = -1;
09: private SaleDate date = null;
10: private int transactionId = -1;
11: private boolean empty = true;
12:
13: public LogRecord() {
14: }
15:
16: /**
17: * @preconditions true
18: * @postconditions true
19: * @modifies self.balance, self.date, self.transactionId
20: */
21: public boolean setRecord(int balance, src.SaleDate date,
22: int transactionId) {
23: this .empty = false;
24: this .balance = balance;
25: this .date = date;
26: this .transactionId = transactionId;
27: // this.empty = false;
28: return true;
29: }
30:
31: public int getBalance() {
32: return balance;
33: }
34:
35: public SaleDate getSaleDate() {
36: return date;
37: }
38:
39: public int getTransactionId() {
40: return transactionId;
41: }
42: }
|