1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
|
import {toNullable} from 'fp-ts/lib/Option.js';
import {
Account,
Operation,
SimpleBank,
bankImplementationMatchesModel,
} from './bank.js';
import {
Gen,
Property,
choose,
elements,
forall,
frequency,
keyValueOf,
listOf,
mapOf1 as nonEmptyMap,
property,
} from './property.js';
import Prando from 'prando';
import {LevelBank} from './levelbank.js';
import {withTempFile} from './fs.js';
import {test, expect} from 'vitest';
const sampleAccounts: Account[] = [
'FR12345678901234',
'DE2345678901234',
'IT34567890123412',
];
const genAccount: Gen<Account> = elements(sampleAccounts);
const genBalance: Gen<number> = choose(0, 1000000);
const genAccounts: Gen<Map<Account, number>> = nonEmptyMap(
genAccount,
genBalance,
);
const genGetBalance: (accounts: Map<Account, number>) => Gen<Operation> =
(accounts: Map<Account, number>) => (rng: Prando) => (size: number) => {
const account = elements(Array.from(accounts.keys()))(rng)(size);
return {op: 'GetBalance', account};
};
const genDeposit: (accounts: Map<Account, number>) => Gen<Operation> =
(accounts: Map<Account, number>) => (rng: Prando) => (size: number) => {
const account = elements(Array.from(accounts.keys()))(rng)(size);
const gAmt = choose(1, 100000)(rng)(size);
return {op: 'Deposit', account, amount: gAmt};
};
const genWithdraw: (accounts: Map<Account, number>) => Gen<Operation> =
(accounts: Map<Account, number>) => (rng: Prando) => (size: number) => {
const account = elements(Array.from(accounts.keys()))(rng)(size);
const gAmt = choose(1, 100000)(rng)(size);
return {op: 'Withdraw', account, amount: gAmt};
};
const genOneOperation = (accounts: Map<Account, number>) =>
frequency([
[1, genGetBalance(accounts)],
[3, genDeposit(accounts)],
[3, genWithdraw(accounts)],
]);
const genOperations = (accounts: Map<Account, number>) =>
listOf(genOneOperation(accounts));
/// Using fake bank as a model to compare with real bank
const levelBankMatchFakeBank =
(initialAccounts: Map<Account, number>) =>
async (ops: Operation[]): Promise<boolean> => {
const fakeBank = new SimpleBank(initialAccounts);
const realBank = await withTempFile(filename => new LevelBank(filename))
.then(bank => bank.populateWith(initialAccounts))
.then(bank => bank);
for (const op of ops) {
switch (op.op) {
case 'GetBalance': {
const retrieved = await realBank.balance(op.account).then(toNullable);
const expected = await fakeBank.balance(op.account).then(toNullable);
if (retrieved !== expected) {
console.log(
`Balance mismatch for account ${op.account}: expected ${expected}, got ${retrieved}`,
);
return false;
}
break;
}
case 'Deposit': {
await realBank.deposit(op.account, op.amount);
await fakeBank.deposit(op.account, op.amount);
break;
}
case 'Withdraw': {
await realBank.withdraw(op.account, op.amount);
await fakeBank.withdraw(op.account, op.amount);
break;
}
}
}
// finally check all balances
for (const account of initialAccounts.keys()) {
const actual = await realBank.balance(account).then(toNullable);
const expected = await fakeBank.balance(account).then(toNullable);
if (actual !== expected) {
console.log(
`Final balance mismatch for account ${account}: expected ${expected}, got ${actual}`,
);
return false;
}
}
return true;
};
test('level-db bank conforms to model', async () => {
const prop = forall(genAccounts, async accounts => {
return property(genOperations(accounts), async ops => {
const levelBank = await withTempFile(
filename => new LevelBank(filename),
).then(bank => bank.populateWith(accounts));
return bankImplementationMatchesModel(accounts)(levelBank)(ops);
});
});
const result = await Property.run(prop);
console.log(result);
console.log(JSON.stringify(result.counterexample));
expect(result.result).toBe('OK');
});
//
//
//
//
//
//
test('in-mem bank conforms to model', async () => {
const prop = forall(genAccounts, async accounts => {
return property(genOperations(accounts), async ops => {
const simpleBank = new SimpleBank(accounts);
return bankImplementationMatchesModel(accounts)(simpleBank)(ops);
});
});
const result = await Property.run(prop);
console.log(result);
console.log(JSON.stringify(result.counterexample));
expect(result.result).toBe('OK');
});
//
//
//
//
//
//
test('can retrieve balance given account exists', async () => {
const prop = forall(genAccounts, async accounts => {
const api = new SimpleBank(accounts);
return property(keyValueOf(accounts), async ([accountNr, bal]) => {
const retrieved = toNullable(await api.balance(accountNr));
return Promise.resolve(retrieved === bal);
});
});
const result = await Property.run(prop);
expect(result.result).toBe('OK');
});
test('correctly update balance given a sequence of deposits and withdrawals', async () => {
const prop = forall(genAccounts, accounts => {
return property(genOperations(accounts), levelBankMatchFakeBank(accounts));
});
const result = await Property.run(prop);
console.log(result);
console.log(JSON.stringify(result.counterexample));
expect(result.result).toBe('OK');
});
|
