ledger/
ledger.rs

1#![allow(dead_code)]
2#![allow(unused_imports)]
3
4use hegel::TestCase;
5use hegel::generators as gs;
6use hegel::stateful::{Variables, variables};
7use std::collections::HashMap;
8
9const LIMIT: i64 = 1000000;
10
11struct Ledger {
12    balances: HashMap<String, i64>,
13}
14
15impl Ledger {
16    fn new() -> Self {
17        Ledger {
18            balances: HashMap::new(),
19        }
20    }
21
22    fn credit(&mut self, account: String, amount: i64) {
23        let balance = self.balances.entry(account).or_insert(0);
24        *balance += amount;
25    }
26
27    fn debit(&mut self, account: String, amount: i64) {
28        let balance = self.balances.entry(account).or_insert(0);
29        *balance -= amount;
30    }
31
32    // Something here isn't quite right...
33    fn transfer(&mut self, from: String, to: String, amount: i64) {
34        let from_balance = *self.balances.get(&from).unwrap_or(&0);
35        if from != to && amount - from_balance <= 1 {
36            self.debit(from, amount);
37            self.credit(to, amount);
38        }
39    }
40}
41
42struct LedgerTest {
43    ledger: Ledger,
44    accounts: Variables<String>,
45}
46
47#[hegel::state_machine]
48impl LedgerTest {
49    #[rule]
50    fn create_account(&mut self, tc: TestCase) {
51        let account = tc.draw(gs::text().min_size(1));
52        tc.note(&format!("create account '{}'", account.clone()));
53        self.accounts.add(account);
54    }
55
56    #[rule]
57    fn credit(&mut self, tc: TestCase) {
58        let account = self.accounts.draw().clone();
59        let amount = tc.draw(gs::integers::<i64>().min_value(0).max_value(LIMIT));
60        tc.note(&format!("credit '{}' with {}", account.clone(), amount));
61        self.ledger.credit(account, amount);
62    }
63
64    #[rule]
65    fn transfer(&mut self, tc: TestCase) {
66        let from = self.accounts.draw().clone();
67        let to = self.accounts.draw().clone();
68        let amount = tc.draw(gs::integers::<i64>().min_value(0).max_value(LIMIT));
69        tc.note(&format!(
70            "transfer '{}' from {} to {}",
71            amount,
72            from.clone(),
73            to.clone()
74        ));
75        self.ledger.transfer(from, to, amount);
76    }
77
78    #[invariant]
79    fn nonnegative_balances(&mut self, _: TestCase) {
80        for (_account, balance) in &self.ledger.balances {
81            assert!(*balance >= 0);
82        }
83    }
84}
85
86#[hegel::test]
87fn test_ledger(tc: TestCase) {
88    let test = LedgerTest {
89        ledger: Ledger::new(),
90        accounts: variables(&tc),
91    };
92    hegel::stateful::run(test, tc);
93}
94
95fn main() {}
ledger/ledger.rs

ledger/
ledger.rs
