Example Packages

• Package Pair:
• pairpkg.ads and prettified
• pairpkg.adb and prettified
• pairclient.adb and prettified
• Comparable program in Java: PairClient.java


• Package Word:
• Word package specification: wordpgk.ads (and prettified)
• Client: simpleword.adb (prettified)
• Word package body: wordpkg.adb (and prettified)


• Package Bignum:
• Bignum specification: bignumpkg.ads (and prettified
• Bignum client 1: bignumget.adb (and prettified)
• Bignum client 2: bignumtest.adb (and prettified)
• Bignum implementation: bignumpkg.adb (and prettified)


• Integer Stack Package
• Integer Stack Client (and prettified)

    package intstackpkg is 
        type StackType is private;

        Stack_Is_Empty, Stack_Is_Full : Exception;

        function IsEmpty (S : StackType) return Boolean;
        function IsFull  (S : StackType) return Boolean;

        procedure Push (I : Integer; S : in out StackType);
        procedure Pop  (S : in out StackType);

        function  Top  (S : StackType) return Integer;
    private
        ...

• Integer Stack Specification (and prettified)
• Integer Stack Implementation (and prettified)

• Assume all operations are functions:
• top(s: Stack) return Integer
• pop(s: Stack) return Stack
• push(s: Stack; i: Integer) return Stack -- Returns new stack
• is_empty(s: Stack) return Boolean
• is_full(s: Stack) return Boolean
• Axioms define stack operations:
• top (push (s, x)) = ??
• pop (push (s, x)) = ??
• push (pop(s), top (s)) = ??
• is_empty (push (s, x)) = ??
• is_full (pop (s)) = ??