This small example of a database application demoes how formal verification and testing can be combined.
The functions and procedures which define the API of this database are all annotated with contracts (a precondition introduced by Pre and a postcondition introduced by Post) and formal test-cases (introduced by Test_Case).
-- identity.ads
package Identity is
-- A name is a non-null string of up to 255 characters
subtype Name_Len is Positive range 1 .. 255;
subtype Name is String (Name_Len);
No_Name : constant Name := Name'(others => ' ');
-- A unique identifier for a customer is a sequence of three numbers, each
-- one between 0 and 999.
type Num is range 0 .. 999;
type Num_Position is (Low, Mid, High);
type Id is array (Num_Position) of Num;
No_Id : constant Id := Id'(Low => 0, Mid => 0, High => 0);
end Identity;
-- money.ads
package Money is
-- An amount of mone is always qualified by the currency in which it is
-- expressed. None corresponds to the invalid currency.
type CUR is (None, Dollar, Euro, Linden, RMB, Yen, Your_Favorite_Currency);
-- Raw amounts of money range from 0 to 1 million units. The base type for
-- raw amounts safely allows adding or subtracting two amounts without any
-- possible overflow.
type Raw_Amount_Base is range -1_000_000 .. 2_000_000;
type Raw_Amount is new Raw_Amount_Base range 0 .. 1_000_000;
type Amount is record
Currency : CUR;
Raw : Raw_Amount;
end record;
No_Amount : constant Amount := Amount'(Currency => None,
Raw => 0);
function Is_Empty (A : Amount) return Boolean is (A.Raw = 0);
-- Basic arithmetic operations over amounts of money. All arguments should
-- be in the same currency, and the result is returned in this currency.
function "+" (A, B : Amount) return Amount
with
Pre => A.Currency = B.Currency and A.Raw + B.Raw <= Raw_Amount'Last,
Post => "+"'Result = Amount'(A.Currency, A.Raw + B.Raw);
function "-" (A, B : Amount) return Amount
with
Pre => A.Currency = B.Currency and B.Raw <= A.Raw,
Post => "-"'Result = Amount'(A.Currency, A.Raw - B.Raw);
end Money;
-- money.adb
package body Money is
function "+" (A, B : Amount) return Amount is
(Amount'(A.Currency, A.Raw + B.Raw));
function "-" (A, B : Amount) return Amount is
(Amount'(A.Currency, A.Raw - B.Raw));
end Money;
-- database.ads
with Identity;
with Money; use Money;
package Database is
-- Accounts are numbered from 0 (invalid account) to Max_Account_Num.
-- Valid accounts start at 1. Not all account numbers correspond to valid
-- accounts.
Max_Account_Num : constant := 200_000;
type Ext_Account_Num is range 0 .. Max_Account_Num;
subtype Account_Num is Ext_Account_Num range 1 .. Max_Account_Num;
No_Account_Num : constant Ext_Account_Num := 0;
-- Logical queries used in contracts
function Existing (Account : in Account_Num) return Boolean;
function Belongs_To
(Account : in Account_Num;
Customer : in Identity.Name;
Id : in Identity.Id) return Boolean;
function Num_Accounts return Natural;
function Max_Account_Reached return Boolean;
function Currency (Account : in Account_Num) return Money.CUR;
-- Basic account management facilities
function Balance (Account : in Account_Num) return Money.Amount
with
Pre => Existing (Account),
Test_Case => (Name => "existing account",
Mode => Nominal,
Ensures => Balance'Result.Currency = Currency (Account)),
Test_Case => (Name => "unknown account",
Mode => Robustness,
Requires => not Existing (Account),
Ensures => Balance'Result = No_Amount);
procedure Open
(Customer : in Identity.Name;
Id : in Identity.Id;
Cur : in Money.CUR;
Account : out Account_Num)
with
Pre => not Max_Account_Reached,
Post => Existing (Account)
and then Belongs_To (Account, Customer, Id)
and then Money.Is_Empty (Balance (Account)),
Test_Case => (Name => "first account",
Mode => Nominal,
Requires => Num_Accounts = 0,
Ensures => Num_Accounts = 1),
Test_Case => (Name => "common case",
Mode => Nominal,
Requires => Num_Accounts > 0,
Ensures => Num_Accounts = Num_Accounts'Old + 1),
Test_Case => (Name => "max account reached",
Mode => Robustness,
Requires => Max_Account_Reached,
Ensures => Account = Max_Account_Num);
procedure Close
(Customer : in Identity.Name;
Id : in Identity.Id;
Account : in Account_Num)
with
Pre => Existing (Account)
and then Belongs_To (Account, Customer, Id)
and then Money.Is_Empty (Balance (Account)),
Test_Case => (Name => "last account",
Mode => Nominal,
Requires => Num_Accounts = 1,
Ensures => Num_Accounts = 0),
Test_Case => (Name => "common case",
Mode => Nominal,
Requires => Num_Accounts > 1,
Ensures => Num_Accounts = Num_Accounts'Old - 1),
Test_Case => (Name => "non-null balance",
Mode => Robustness,
Requires => not Money.Is_Empty (Balance (Account)),
Ensures => Existing (Account) and then
Balance (Account) = Balance (Account)'Old);
procedure Deposit (Account : in Account_Num; Sum : in Money.Amount)
with
Pre => Existing (Account) and then
Currency (Account) = Sum.Currency and then
Balance (Account).Raw + Sum.Raw <= Money.Raw_Amount'Last,
Post => Balance (Account) = Balance (Account)'Old + Sum,
Test_Case => (Name => "common case",
Mode => Nominal),
Test_Case => (Name => "different currency",
Mode => Robustness,
Requires => Currency (Account) /= Sum.Currency,
Ensures => Balance (Account) = Balance (Account)'Old),
Test_Case => (Name => "too large",
Mode => Robustness,
Requires => Balance (Account).Raw + Sum.Raw >
Money.Raw_Amount'Last,
Ensures => Balance (Account) = Balance (Account)'Old);
procedure Withdraw (Account : in Account_Num; Sum : in Money.Amount)
with
Pre => Existing (Account) and then
Currency (Account) = Sum.Currency and then
Sum.Raw <= Balance (Account).Raw,
Post => Balance (Account) = Balance (Account)'Old - Sum,
Test_Case => (Name => "common case",
Mode => Nominal),
Test_Case => (Name => "different currency",
Mode => Robustness,
Requires => Currency (Account) /= Sum.Currency,
Ensures => Balance (Account) = Balance (Account)'Old),
Test_Case => (Name => "too large",
Mode => Robustness,
Requires => Sum.Raw > Balance (Account).Raw,
Ensures => Balance (Account) = Balance (Account)'Old);
end Database;
-- database.adb
with Identity;
use type Identity.Id;
package body Database is
--------------------
-- Local Packages --
--------------------
-- Availability of accounts is managed in a separate package, which offers
-- two procedures to reserve a previously unused account or to make one
-- available when not used anymore, and a function to query if there is at
-- least one account available.
package Availability is
type Account_Link is record
Available : Boolean;
Prev, Next : Ext_Account_Num;
end record;
type Account_Link_Data is array (Database.Account_Num) of Account_Link;
Links : Account_Link_Data;
First_Available : Ext_Account_Num := Account_Num'First;
function Some_Available return Boolean is
(First_Available /= No_Account_Num);
function Is_Available (Account : in Account_Num) return Boolean is
(Links (Account).Available);
procedure Reserve_First_Available (Account : out Account_Num)
with
Pre => Some_Available,
Post => not Is_Available (Account) and then
(for all Act in Account_Num =>
(if Act /= Account then
Links (Act).Available = Links'Old (Act).Available));
procedure Make_Available (Account : Account_Num)
with
Pre => not Is_Available (Account),
Post => Is_Available (Account) and then
(for all Act in Account_Num =>
(if Act /= Account then
Links (Act).Available = Links'Old (Act).Available));
function Num_Available return Natural;
end Availability;
-------------------------------
-- Local Types and Constants --
-------------------------------
-- An account relates an account number to an owner, whose name and id are
-- recorded.
type Account_Rec is record
Owner_Name : Identity.Name;
Owner_Id : Identity.Id;
Account : Ext_Account_Num;
end record;
No_Account_Rec : constant Account_Rec :=
Account_Rec'(Owner_Name => Identity.No_Name,
Owner_Id => Identity.No_Id,
Account => No_Account_Num);
-- The account balance relates an account number to an amount of money
type Account_Balance is record
Value : Money.Amount;
Account : Ext_Account_Num;
end record;
No_Account_Balance : constant Account_Balance :=
Account_Balance'(Value => Money.No_Amount,
Account => No_Account_Num);
type Account_Data is array (Account_Num) of Account_Rec;
type Account_Balance_Data is array (Account_Num) of Account_Balance;
---------------------
-- Local Variables --
---------------------
Accounts : Account_Data := Account_Data'(others => No_Account_Rec);
-- Database of account identity data
Accounts_Balance : Account_Balance_Data :=
Account_Balance_Data'(others => No_Account_Balance);
-- Database of account balance data
------------------
-- Availability --
------------------
package body Availability is
procedure Reserve_First_Available (Account : out Account_Num) is
begin
Account := First_Available;
Links (First_Available).Available := False;
First_Available := Links (First_Available).Next;
end Reserve_First_Available;
procedure Make_Available (Account : Account_Num) is
begin
-- Remove node Account from linked-list
if Links (Account).Prev /= No_Account_Num then
Links (Links (Account).Prev).Next := Links (Account).Next;
end if;
if Links (Account).Next /= No_Account_Num then
Links (Links (Account).Next).Prev := Links (Account).Prev;
end if;
-- Insert node Account into linked-list as first available node
if First_Available /= No_Account_Num then
Links (Account).Prev := Links (First_Available).Prev;
end if;
Links (Account).Next := First_Available;
Links (Account).Available := True;
First_Available := Account;
end Make_Available;
function Num_Available return Natural is
Count : Natural := 0;
begin
for I in Account_Num loop
pragma Assert (Count < Natural(I));
if Is_Available (I) then
Count := Count + 1;
end if;
end loop;
return Count;
end Num_Available;
procedure Initialize_Links is
Tmp_Prev : Ext_Account_Num;
Tmp_Next : Ext_Account_Num;
begin
for I in Account_Num loop
if I = Account_Num'First then
Tmp_Prev := No_Account_Num;
else
Tmp_Prev := I - 1;
end if;
if I = Account_Num'Last then
Tmp_Next := No_Account_Num;
else
Tmp_Next := I + 1;
end if;
Links (I) := Account_Link'(Available => True,
Prev => Tmp_Prev,
Next => Tmp_Next);
end loop;
end Initialize_Links;
begin
Initialize_Links;
end Availability;
-------------------------
-- Max_Account_Reached --
-------------------------
function Max_Account_Reached return Boolean is
(not Availability.Some_Available);
------------------
-- Num_Accounts --
------------------
function Num_Accounts return Natural is
begin
return Availability.Num_Available;
end Num_Accounts;
--------------
-- Existing --
--------------
function Existing (Account : in Account_Num) return Boolean is
(not Availability.Is_Available (Account));
----------------
-- Belongs_To --
----------------
function Belongs_To
(Account : in Account_Num;
Customer : in Identity.Name;
Id : in Identity.Id) return Boolean
is
(Accounts (Account) = Account_Rec'(Owner_Name => Customer,
Owner_Id => Id,
Account => Account));
-------------
-- Balance --
-------------
function Balance (Account : Account_Num) return Money.Amount is
(Accounts_Balance (Account).Value);
--------------
-- Currency --
--------------
function Currency (Account : in Account_Num) return Money.CUR is
(Accounts_Balance (Account).Value.Currency);
----------
-- Open --
----------
procedure Open
(Customer : in Identity.Name;
Id : in Identity.Id;
Cur : in Money.CUR;
Account : out Account_Num) is
begin
-- Defensive programming if precondition is not checked at run-time
if Max_Account_Reached then
Account := Max_Account_Num;
return;
end if;
Availability.Reserve_First_Available (Account);
Accounts (Account) := Account_Rec'(Owner_Name => Customer,
Owner_Id => Id,
Account => Account);
Accounts_Balance (Account) :=
Account_Balance'(Value => Money.Amount'(Currency => Cur,
Raw => 0),
Account => Account);
end Open;
-----------
-- Close --
-----------
procedure Close
(Customer : Identity.Name;
Id : Identity.Id;
Account : Account_Num) is
begin
-- Defensive programming if precondition is not checked at run-time
if Balance (Account).Raw /= 0 then
return;
end if;
-- Perform basic checks on name and identity of account owner. Only
-- delete the account if the checks are successful.
if Accounts (Account).Owner_Name = Customer
and then Accounts (Account).Owner_Id = Id
then
Accounts (Account) := No_Account_Rec;
Availability.Make_Available (Account);
end if;
end Close;
-------------
-- Deposit --
-------------
procedure Deposit (Account : Account_Num; Sum : Money.Amount) is
begin
-- Defensive programming if precondition is not checked at run-time
if Currency (Account) /= Sum.Currency
or else Balance (Account).Raw + Sum.Raw > Money.Raw_Amount'Last
then
return;
end if;
Accounts_Balance (Account).Value :=
Accounts_Balance (Account).Value + Sum;
end Deposit;
--------------
-- Withdraw --
--------------
procedure Withdraw (Account : in Account_Num; Sum : in Money.Amount) is
begin
-- Defensive programming if precondition is not checked at run-time
if Currency (Account) /= Sum.Currency
or else Sum.Raw > Balance (Account).Raw
then
return;
end if;
Accounts_Balance (Account).Value :=
Accounts_Balance (Account).Value - Sum;
end Withdraw;
end Database;
The tool GNATprove automatically proves that all subprograms are free from run-time error and respect their contracts. Here is the output of the analysis:
database.adb:105:21: (info) range check proved database.adb:106:10: (info) index check proved database.adb:107:29: (info) index check proved database.adb:114:13: (info) index check proved database.adb:115:13: (info) index check proved database.adb:115:20: (info) index check proved database.adb:115:50: (info) index check proved database.adb:117:13: (info) index check proved database.adb:118:13: (info) index check proved database.adb:118:20: (info) index check proved database.adb:118:50: (info) index check proved database.adb:124:13: (info) index check proved database.adb:124:37: (info) index check proved database.adb:126:10: (info) index check proved database.adb:127:10: (info) index check proved database.adb:128:29: (info) range check proved database.adb:132:29: (info) range check proved database.adb:135:13: (info) loop invariant initialization proved database.adb:135:13: (info) loop invariant preservation proved database.adb:136:30: (info) range check proved database.adb:137:31: (info) overflow check proved database.adb:137:31: (info) range check proved database.adb:147:31: (info) loop invariant initialization proved database.adb:147:31: (info) loop invariant preservation proved database.adb:151:30: (info) overflow check proved database.adb:151:30: (info) range check proved database.adb:156:30: (info) overflow check proved database.adb:156:30: (info) range check proved database.adb:158:13: (info) index check proved database.adb:200:7: (info) index check proved database.adb:202:55: (info) range check proved database.adb:208:8: (info) index check proved database.adb:215:8: (info) index check proved database.adb:230:21: (info) range check proved database.adb:234:19: (info) precondition proved database.adb:235:7: (info) index check proved database.adb:237:56: (info) range check proved database.adb:238:7: (info) index check proved database.adb:240:63: (info) range check proved database.adb:241:37: (info) range check proved database.adb:255:10: (info) precondition proved database.adb:262:10: (info) index check proved database.adb:263:18: (info) index check proved database.adb:265:10: (info) index check proved database.adb:266:22: (info) precondition proved database.adb:279:17: (info) precondition proved database.adb:279:39: (info) overflow check proved database.adb:284:7: (info) index check proved database.adb:285:42: (info) precondition proved database.adb:285:9: (info) index check proved database.adb:297:27: (info) precondition proved database.adb:302:7: (info) index check proved database.adb:303:42: (info) precondition proved database.adb:303:9: (info) index check proved database.adb:32:10: (info) index check proved database.adb:38:18: (info) postcondition proved database.adb:40:23: (info) index check proved database.adb:40:52: (info) index check proved database.adb:46:18: (info) postcondition proved database.adb:48:23: (info) index check proved database.adb:48:52: (info) index check proved database.ads:111:25: (info) precondition proved database.ads:112:14: (info) precondition proved database.ads:112:32: (info) postcondition proved database.ads:112:34: (info) precondition proved database.ads:112:56: (info) precondition proved database.ads:53:30: (info) postcondition proved database.ads:53:41: (info) precondition proved database.ads:74:41: (info) precondition proved database.ads:93:14: (info) precondition proved database.ads:93:36: (info) overflow check proved database.ads:94:14: (info) precondition proved database.ads:94:32: (info) postcondition proved database.ads:94:34: (info) precondition proved database.ads:94:56: (info) precondition proved money.adb:4:33: (info) overflow check proved money.adb:4:33: (info) range check proved money.adb:7:33: (info) overflow check proved money.adb:7:33: (info) range check proved money.ads:30:48: (info) overflow check proved money.ads:31:25: (info) postcondition proved money.ads:31:53: (info) overflow check proved money.ads:31:53: (info) range check proved money.ads:36:25: (info) postcondition proved money.ads:36:53: (info) overflow check proved money.ads:36:53: (info) range check proved