-- F732B00.A -- -- Grant of Unlimited Rights -- -- The Ada Conformity Assessment Authority (ACAA) holds unlimited -- rights in the software and documentation contained herein. Unlimited -- rights are the same as those granted by the U.S. Government for older -- parts of the Ada Conformity Assessment Test Suite, and are defined -- in DFAR 252.227-7013(a)(19). By making this public release, the ACAA -- intends to confer upon all recipients unlimited rights equal to those -- held by the ACAA. These rights include rights to use, duplicate, -- release or disclose the released technical data and computer software -- in whole or in part, in any manner and for any purpose whatsoever, and -- to have or permit others to do so. -- -- DISCLAIMER -- -- ALL MATERIALS OR INFORMATION HEREIN RELEASED, MADE AVAILABLE OR -- DISCLOSED ARE AS IS. THE ACAA MAKES NO EXPRESS OR IMPLIED -- WARRANTY AS TO ANY MATTER WHATSOEVER, INCLUDING THE CONDITIONS OF THE -- SOFTWARE, DOCUMENTATION OR OTHER INFORMATION RELEASED, MADE AVAILABLE -- OR DISCLOSED, OR THE OWNERSHIP, MERCHANTABILITY, OR FITNESS FOR A -- PARTICULAR PURPOSE OF SAID MATERIAL. -- -- Notice -- -- The ACAA has created and maintains the Ada Conformity Assessment Test -- Suite for the purpose of conformity assessments conducted in accordance -- with the International Standard ISO/IEC 18009 - Ada: Conformity -- assessment of a language processor. This test suite should not be used -- to make claims of conformance unless used in accordance with -- ISO/IEC 18009 and any applicable ACAA procedures. --* -- -- FOUNDATION DESCRIPTION: -- This foundation provides the basis for testing aspect Type_Invariant -- on a private type and accesses to that private type. -- -- Note that a default-initialized object of type -- Change_Discriminated_Type will always fail an invariant check. We do -- this to test 7.3.2(10/4). -- -- This foundation is based on a package for generating "Diagrams" for -- bellringing. The type invariant is that each bell occurs once and only -- once. -- -- CHANGE HISTORY: -- 25 Dec 14 JAC Initial pre-release version. -- 20 Jan 15 JAC Second pre-release version. -- 09 Apr 15 RLB Fixed formatting problems; removed uses of Text_IO. -- 10 Apr 15 RLB Added operations on access-to-priv. -- --! package F732B00 is pragma Assertion_Policy (Check); Max_No_Of_Bells : constant := 16; No_Of_Bells : constant := 8; type Bell_Range_Type is range 1 .. Max_No_Of_Bells; type Change_Discriminated_Type (No_Of_Bells : Bell_Range_Type) is private with Type_Invariant => Each_Bell_Occurs_Once (Change_Discriminated_Type) and And_Only_Once (Change_Discriminated_Type); subtype Swappable_Bell_Range_Type is Bell_Range_Type range 1 .. No_Of_Bells - 1; subtype Number_Of_Pairs_To_Swap_Type is Bell_Range_Type range 1 .. No_Of_Bells / 2; type Pairs_To_Swap_Type is array (Number_Of_Pairs_To_Swap_Type range <>) of Swappable_Bell_Range_Type; type Bells_To_Swap_Type (Number_Of_Pairs_To_Swap : Number_Of_Pairs_To_Swap_Type) is record Pairs_To_Swap : Pairs_To_Swap_Type (1 .. Number_Of_Pairs_To_Swap); end record; function Each_Bell_Occurs_Once (Change : Change_Discriminated_Type) return Boolean; function And_Only_Once (Change : Change_Discriminated_Type) return Boolean; function Rounds_With_Default_Initialisation return Change_Discriminated_Type; function Rounds return Change_Discriminated_Type; function Invalid_Change return Change_Discriminated_Type; procedure Print_Change (Change : Change_Discriminated_Type); procedure Hunt_For_One_Change (Change : in out Change_Discriminated_Type; Tenor_Behind : in Boolean := True); function At_Lead_End (Change : in Change_Discriminated_Type) return Boolean; procedure Grandsire_Change (Change : in out Change_Discriminated_Type) with Pre => No_Of_Bells >= 5; procedure Invalid_Grandsire_Change (Change : in out Change_Discriminated_Type) with Pre => No_Of_Bells >= 5; function Swaps_Dont_Overlap (Bells_To_Swap : in Bells_To_Swap_Type) return Boolean; procedure Swap_Places (Change : in out Change_Discriminated_Type; Bells_To_Swap : in Bells_To_Swap_Type) with Pre => Swaps_Dont_Overlap (Bells_To_Swap); -- Operations to test access-to-private-with-invariants. Note that we -- try similar operations with an anonymous access type and with -- a named access type. type Access_to_Change is access all Change_Discriminated_Type; type Change_Kind is (Valid, Invalid); procedure Reset_Change (Change : not null access Change_Discriminated_Type; Kind : in Change_Kind); -- Adjust Change as specified by Kind. type Get_Change_Kind is (Param_Invalid, Result_Invalid, Result_is_Param, Result_Other_Valid); function Get_Change (Change : Access_to_Change; Kind : in Get_Change_Kind) return Access_to_Change; -- Get a Change value, what happens depends on Kind. function Create_Change (Kind : in Change_Kind) return not null access Change_Discriminated_Type; -- Create a Change value as specified by Kind. private type Change_Array_Type is array (Bell_Range_Type range <>) of Bell_Range_Type with Default_Component_Value => Bell_Range_Type'First; -- Note: Any default-initialized object will fail an invariant check, -- no matter where it is used. type Change_Discriminated_Type (No_Of_Bells : Bell_Range_Type) is record Change : Change_Array_Type (Bell_Range_Type range 1 .. No_Of_Bells); end record with Dynamic_Predicate => (for all Bell_Number in Bell_Range_Type range 1 .. No_Of_Bells => Change_Discriminated_Type.Change (Bell_Number) <= No_Of_Bells); end F732B00; with Report; package body F732B00 is pragma Assertion_Policy (Check); Change_Number : Natural := 0; function Each_Bell_Occurs_Once (Change : Change_Discriminated_Type) return Boolean is (for all Bell_Number in 1 .. Change.No_Of_Bells => (for some Bell in 1 .. Change.No_Of_Bells => Change.Change (Bell) = Bell_Number ) ); function And_Only_Once (Change : Change_Discriminated_Type) return Boolean is (not (for some Bell in 1 .. Change.No_Of_Bells -1 => (for some Other_Bell in Bell + 1 .. Change.No_Of_Bells => Change.Change (Bell) = Change.Change (Other_Bell) ) ) ); function Rounds_With_Default_Initialisation return Change_Discriminated_Type is -- Default initialisation checks the type invariant even within the -- package, RM 7.3.2(10/3) Change : Change_Discriminated_Type (No_Of_Bells); begin for Bell in 1 .. Change.No_Of_Bells loop Change.Change (Bell) := Bell; end loop; return Change; end Rounds_With_Default_Initialisation; function Rounds return Change_Discriminated_Type is -- Can knowingly set to something that breaches the type invariant, but -- can't use default initialisation as that still checks the type -- invariant, RM 7.3.2(10/3) doesn't exclude within the package. Change : Change_Discriminated_Type := (No_Of_Bells => No_Of_Bells, Change => (others => Bell_Range_Type'First)); begin for Bell in 1 .. Change.No_Of_Bells loop Change.Change (Bell) := Bell; end loop; return Change; end Rounds; function Invalid_Change return Change_Discriminated_Type is -- Can knowingly set to something that breaches the type invariant -- within the package. Change : constant Change_Discriminated_Type := (No_Of_Bells => No_Of_Bells, Change => (others => Bell_Range_Type'First)); begin return Change; end Invalid_Change; procedure Print_Change (Change : Change_Discriminated_Type) is Result : String (1 .. Natural(Change.No_Of_Bells*3)); begin for Place in 1 .. Change.No_Of_Bells loop if Change.Change (Place) < 10 then Result (Natural(Place*3-2)) := ' '; Result (Natural(Place*3-1)) := Character'Val(Change.Change (Place) + Character'Pos('0')); else Result (Natural(Place*3-2)) := '1'; Result (Natural(Place*3-1)) := Character'Val(Change.Change (Place) - 10 + Character'Pos('0')); end if; Result (Natural(Place*3)) := ' '; end loop; Report.Comment ("Change: " & Result); end Print_Change; procedure Swap_Bell_With_Following_Bell (Change : in out Change_Discriminated_Type; Bell_To_Swap : in Swappable_Bell_Range_Type) is Temp : Bell_Range_Type; begin Temp := Change.Change (Bell_To_Swap); Change.Change (Bell_To_Swap) := Change.Change (Bell_To_Swap + 1); Change.Change (Bell_To_Swap + 1) := Temp; end Swap_Bell_With_Following_Bell; procedure Hunt_For_One_Change (Change : in out Change_Discriminated_Type; Tenor_Behind : in Boolean := True) is Hunt_On_How_Many : constant Bell_Range_Type := (if Tenor_Behind then No_Of_Bells - 1 else No_Of_Bells); begin -- If Even Change_Number if Change_Number mod 2 = 0 then for Place in 1 .. Hunt_On_How_Many - 1 loop -- If Odd Place if Place mod 2 = 1 then Swap_Bell_With_Following_Bell (Change => Change, Bell_To_Swap => Place); end if; end loop; else -- Odd Change_Number for Place in 1 .. Hunt_On_How_Many - 1 loop -- If Even Place if Place mod 2 = 0 then Swap_Bell_With_Following_Bell (Change => Change, Bell_To_Swap => Place); end if; end loop; end if; Change_Number := Change_Number + 1; end Hunt_For_One_Change; function At_Lead_End (Change : in Change_Discriminated_Type) return Boolean is (Change.Change (1) = 1); procedure Grandsire_Change (Change : in out Change_Discriminated_Type) is begin Swap_Bell_With_Following_Bell (Change => Change, Bell_To_Swap => 1); for Place in Bell_Range_Type range 4 .. No_Of_Bells - 1 loop if Place mod 2 = 0 then Swap_Bell_With_Following_Bell (Change => Change, Bell_To_Swap => Place); end if; end loop; Change_Number := Change_Number + 1; end Grandsire_Change; procedure Broken_Swap_Bell_With_Following_Bell (Change : in out Change_Discriminated_Type; Bell_To_Swap : in Swappable_Bell_Range_Type) is Temp : Bell_Range_Type; begin Temp := Change.Change (Bell_To_Swap); Change.Change (Bell_To_Swap) := Change.Change (Bell_To_Swap + 1); -- Last line of swap missing. end Broken_Swap_Bell_With_Following_Bell; procedure Invalid_Grandsire_Change (Change : in out Change_Discriminated_Type) is -- A routine that uses a buggy Swap routine to make a mess. -- Note that the local broken swap does NOT check the invariant after -- each call; if we cleaned up the mess before the end of this routine, -- there would be no problem. begin Broken_Swap_Bell_With_Following_Bell (Change => Change, Bell_To_Swap => 1); for Place in Bell_Range_Type range 4 .. No_Of_Bells - 1 loop if Place mod 2 = 0 then Broken_Swap_Bell_With_Following_Bell (Change => Change, Bell_To_Swap => Place); end if; end loop; Change_Number := Change_Number + 1; end Invalid_Grandsire_Change; function Swaps_Dont_Overlap (Bells_To_Swap : in Bells_To_Swap_Type) return Boolean is (for all Pair_To_Swap in 1 .. Bells_To_Swap.Number_Of_Pairs_To_Swap - 1 => Bells_To_Swap.Pairs_To_Swap (Pair_To_Swap + 1) >= Bells_To_Swap.Pairs_To_Swap (Pair_To_Swap) + 2 ); procedure Swap_Places (Change : in out Change_Discriminated_Type; Bells_To_Swap : in Bells_To_Swap_Type) is begin for Pair_To_Swap in 1 .. Bells_To_Swap.Number_Of_Pairs_To_Swap loop Swap_Bell_With_Following_Bell (Change => Change, Bell_To_Swap => Bells_To_Swap.Pairs_To_Swap (Pair_To_Swap)); end loop; Change_Number := Change_Number + 1; end Swap_Places; procedure Reset_Change (Change : not null access Change_Discriminated_Type; Kind : in Change_Kind) is -- Adjust Change as specified by Kind. begin if Kind = Valid then Change.all := Rounds; else -- Kind = Invalid then -- Note: We can't call a public routine here, or that would make -- and fail the invariant check and we would not test our objectives. Change.Change := (others => Bell_Range_Type'First); end if; end Reset_Change; Temp : aliased Change_Discriminated_Type (No_Of_Bells) := Rounds; -- Have to initialize, else will fail invariant check. function Get_Change (Change : Access_to_Change; Kind : in Get_Change_Kind) return Access_to_Change is -- Get a Change value, what happens depends on Kind. begin if Kind = Param_Invalid then -- Note: We can't call a public routine here, or that would make -- and fail the invariant check and we would not test our objectives. Change.Change := (others => Bell_Range_Type'First); return null; elsif Kind = Result_Invalid then -- See note above. Temp.Change := (others => Bell_Range_Type'Last); return Temp'Access; elsif Kind = Result_is_Param then return Change; else --if Kind = Result_Other_Valid then Temp.Change := Rounds.Change; return Temp'Access; end if; end Get_Change; function Create_Change (Kind : in Change_Kind) return not null access Change_Discriminated_Type is -- Create a Change value as specified by Kind. begin if Kind = Valid then Temp.Change := Rounds.Change; return Temp'Access; else -- Kind = Invalid then -- Note: We can't call a public routine here, or that would make -- and fail the invariant check and we would not test our objectives. Temp.Change := (others => Bell_Range_Type'Last); return Temp'Access; end if; end Create_Change; end F732B00;