Let's get started...
Consider this basic model of a Bank:
package Bank is procedure Open_Account (Cash : Integer); procedure Deposit (Cash : Integer); procedure Withdraw (Cash : Integer); end Bank;
This bank maintains only one account that has to be open before doing any transation. The only client of this bank would be a main subprogram P that opens an account and operates several transactions:
with Bank; procedure P is begin Bank.Open_Account (100); Bank.Deposit (45); Bank.Withdraw (55); Bank.Deposit (80); end P;
The implementation of package Bank is straightforward; it also contains an additional transaction at elaboration time, that corresponds to a special offer of the bank (and one may already see that it will cause a problem):
package body Bank is Balance : Integer; procedure Open_Account (Cash : Integer) is begin Balance := Cash; end Open_Account; procedure Deposit (Cash : Integer) is begin Balance := Balance + Cash; end Deposit; procedure Withdraw (Cash : Integer) is begin Balance := Balance - Cash; end Withdraw; -- To celebrate the inauguration of the bank at elaboration time, your -- account is credited with $100. Special_Offer : constant Integer := 100; begin Deposit (Special_Offer); end Bank;
There is a implicit property that the account should be opened only once, and before any transaction takes place; would this special offer break this property? This is a good opportunity to see how GDB can help us in checking properties of this form and break whenever the property is violated at run time. To do so, one may use the script language of GDB along with breakpoint commands.
The first way to do so would be set breakpoints on the bank operations:
(gdb) break open_account Breakpoint 1 at 0x401592: file bank.adb, line 7. (gdb) break deposit Breakpoint 2 at 0x4015a2: file bank.adb, line 12. (gdb) break withdraw Breakpoint 3 at 0x4015b8: file bank.adb, line 17.
However, we would not like to stop on any transaction, but only on an invalid one. At each breakpoint, we would like to check if our invariants hold, continue if they do, stop with an error if they don't.
First, the properties that we want to check require to maintain a state: whether or not the account has been open. This may be represented by a GDB convenience variable that can be created as follows:
set variable $account_open := False
We can then attach a small program that will be executed each time the breakpoint is hit. e.g. for breakpoint 1 on open_account:
(gdb) commands 1 >if $account_open = True >echo error: account opened twice\n >else >set variable $account_open := True >printf "(info) account created with $%d\n", cash >continue >end >end
This command will resume the program if the account has not been opened yet, and will stop with an error message if we are trying to open it for the second time. The same kind of program may be used for withdraw and deposit:
(gdb) commands 2 >if $account_open = False >echo error: someone tries to deposit before opening an account\n >else >printf "(info) deposit: $%d\n", cash >continue >end >end (gdb) commands 3 >if $account_open = False >echo error: someone tries to withdraw before opening an account\n >else >printf "(info) withdrawal: $%d\n", cash >continue >end >end
Now let us run the program and look for invariant violations. One happens immediately:
Breakpoint 2, bank.deposit (cash=100) at bank.adb:12 12 Balance := Balance + Cash; error: someone tries to deposit before opening an account (gdb)
Indeed, the special offer is credited before the account is opened:
(gdb) up #1 0x004015da in
() at bank.adb:25 25 Deposit (Special_Offer);
Let us continue to find other violations. The program exits normally, meaning that no other violations were detected.
(gdb) c Continuing.
Breakpoint 1, bank.open_account (cash=100) at bank.adb:7 7 Balance := Cash; (info) account created with $100
Breakpoint 2, bank.deposit (cash=45) at bank.adb:12 12 Balance := Balance + Cash; (info) deposit: $45
Breakpoint 3, bank.withdraw (cash=55) at bank.adb:17 17 Balance := Balance - Cash; (info) withdrawal: $55
Breakpoint 2, bank.deposit (cash=80) at bank.adb:12 12 Balance := Balance + Cash; (info) deposit: $80 [Inferior 1 (process 7472) exited normally]
The script language of GDB provides various flow-control commands; you may find their full documentation in the section "Command files" in the GDB user's guide. We have seen that this language of GDB, along with convenience variables and breakpoint commands, provides a simple way to check some simple dynamic properties on a run. In order to check more elaborated properties, the full power of expression of the python interface should be used. This will be the subject of a forthcoming Gem.