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