A Database Example

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
  • Categories

  • Open-DO Projects

  • Want to get involved?

  • Contact

    info @ open-do.org