-- C458A01.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. --* -- OBJECTIVES: -- -- (A) Check that the predicate of a quantified expression is evaluated in -- the order specified by the generalized iterator. -- -- (B) Check that result of a quantified expression with a -- generalized iterator is True if the predicate is True for -- all values if the quantifier is all and any value if the quantifier -- is some, and is False otherwise. -- -- (C) Check that evaluation of predicates of a quantified expression with -- a generalized iterator stops when the result is determined, -- and no extra evaluations occur. -- -- (D) Check that if the quantifier is all, the result of a quantified -- expression is True if there are no values in the domain. -- -- (E) Check that if the quantifier is some, the result of a quantified -- expression is False if there are no values in the domain. -- -- (F) Check that any exceptions propagated by the predicate of a -- quantified expression with a quantifier of all is propagated by the -- quantified expression. -- -- (G) Check that any exceptions propagated by the predicate of a -- quantified expression with a quantifier of some is propagated by the -- quantified expression. -- -- HISTORY: -- BJM 5/10/22 Created original test. -- RLB 6/30/22 Renamed foundation, test. Removed Ada 2022 features. --! with Report; use Report; with F458A00_Sparse_Arrays; procedure C458A01 is type Direction is (Forward, Backward); Test_Error : exception; package Sparse_Arrays is new F458A00_Sparse_Arrays (Sparse_Array_Index => Natural, Element_Type => Integer); subtype Sparse_Array_10 is Sparse_Arrays.Sparse_Array (Max_Elements => 10); function Test_Initialize return Sparse_Array_10 is The_Array : Sparse_Array_10 := Sparse_Arrays.Empty (Max_Elements => 10); begin Sparse_Arrays.Append (The_Array, Index => 100, New_Item => 1000); Sparse_Arrays.Append (The_Array, Index => 200, New_Item => 2000); Sparse_Arrays.Append (The_Array, Index => 300, New_Item => 3000); Sparse_Arrays.Append (The_Array, Index => 400, New_Item => 4000); Sparse_Arrays.Append (The_Array, Index => 500, New_Item => 5000); Sparse_Arrays.Append (The_Array, Index => 600, New_Item => 6000); Sparse_Arrays.Append (The_Array, Index => 700, New_Item => 7000); Sparse_Arrays.Append (The_Array, Index => 800, New_Item => 8000); Sparse_Arrays.Append (The_Array, Index => 900, New_Item => 9000); Sparse_Arrays.Append (The_Array, Index => 1000, New_Item => 10_000); return The_Array; end Test_Initialize; Test_Array : constant Sparse_Array_10 := Test_Initialize; Empty_Array : constant Sparse_Array_10 := Sparse_Arrays.Empty (Max_Elements => 10); TC_Last_Check : Sparse_Arrays.Storage_Index := 0; use type Sparse_Arrays.Count_Type; use type Sparse_Arrays.Cursor; function Succession_Check (Position : Sparse_Arrays.Cursor; Iteration : Direction; Result : Boolean; Propagate_Exception : Boolean := False) return Boolean is begin if Iteration = Forward then if TC_Last_Check + 1 /= Sparse_Arrays.Storage_Index_Of (Position) then Failed ("Expression evaluated out of order"); end if; if Test_Array (Position) /= Integer (TC_Last_Check + 1) * 1000 then Failed ("Unexpected array value, Index=" & Sparse_Arrays.Storage_Index'Image (TC_Last_Check + 1) & ", Value=" & Integer'Image (Test_Array (Position))); end if; else if TC_Last_Check - 1 /= Sparse_Arrays.Storage_Index_Of (Position) then Failed ("Expression evaluated out of order"); end if; if Test_Array (Position) /= Integer (TC_Last_Check - 1) * 1000 then Failed ("Unexpected array value, Index=" & Sparse_Arrays.Storage_Index'Image (TC_Last_Check - 1) & ", Value=" & Integer'Image (Test_Array (Position))); end if; end if; if Propagate_Exception then raise Test_Error with "Test Exception Propagation: " & Integer'Image (Test_Array (Position)); end if; TC_Last_Check := Sparse_Arrays.Storage_Index_Of (Position); return Result; end Succession_Check; begin -- C458001 Test ("C458A01", "Check that the predicate of a quantified expression " & "is evaluated in the order specified by the generalized iterator"); TC_Last_Check := 0; --Report.Comment ("Test 1"); Objective_A_Forward_All : -- Also partly satisfies Objective B declare Expression_Value : Boolean := False; begin -- Objective_A_Forward_All -- Forward iteration through all elements Expression_Value := (for all Position in Test_Array.Iterate => Succession_Check (Position, Forward, Result => True)); if not Expression_Value then Failed ("Wrong value for quantified expression - 1"); end if; if TC_Last_Check /= Test_Array.Length then Failed ("Unexpected value for last evaluated expression - 1"); end if; exception when others => Failed ("Unexpected exception raised - 1"); end Objective_A_Forward_All; --Report.Comment ("Test 2"); TC_Last_Check := Test_Array.Length + 1; Objective_A_Reverse_All : -- Also partly satisifies Objective B declare Expression_Value : Boolean := False; begin -- Objective_A_Reverse_All -- Reverse iteration through all elements Expression_Value := (for all Position in reverse Test_Array.Iterate => Succession_Check (Position, Backward, Result => True)); if not Expression_Value then Failed ("Wrong value for quantified expression - 2"); end if; if TC_Last_Check /= 1 then Failed ("Unexpected value for last evaluated expression - 2"); end if; exception when others => Failed ("Unexpected exception raised - 2"); end Objective_A_Reverse_All; --Report.Comment ("Test 3"); TC_Last_Check := 0; Objective_A_Forward_Some : -- Also partly satisifies Objective B declare Expression_Value : Boolean := False; begin -- Objective_A_Forward_Some -- Forward iteration to check one element exists Expression_Value := (for some Position in Test_Array.Iterate => Succession_Check (Position, Forward, Result => (Position = Test_Array.Last))); if not Expression_Value then Failed ("Wrong value for quantified expression - 3"); end if; if TC_Last_Check /= Test_Array.Length then Failed ("Unexpected value for last evaluated expression - 3"); end if; exception when others => Failed ("Unexpected exception raised - 3"); end Objective_A_Forward_Some; --Report.Comment ("Test 4"); TC_Last_Check := Test_Array.Length + 1; Objective_A_Reverse_Some : -- Also partly satisifies Objective B declare Expression_Value : Boolean := False; begin -- Objective_A_Reverse_Some -- Reverse iteration to check if one element exists Expression_Value := (for some Position in reverse Test_Array.Iterate => Succession_Check (Position, Backward, Result => (Position = Test_Array.First))); if not Expression_Value then Failed ("Wrong value for Quantified Expression - 4"); end if; if TC_Last_Check /= 1 then Failed ("Unexpected value for last evaluated expression - 4"); end if; exception when others => Failed ("Unexpected exception raised - 4"); end Objective_A_Reverse_Some; --Report.Comment ("Test 5"); TC_Last_Check := 0; Objective_C_Forward : declare Expression_Value : Boolean := False; begin -- Objective_C_Forward -- Forward iteration stopping on the second element Expression_Value := (for all Position in Test_Array.Iterate => Succession_Check (Position, Forward, Result => Position = Test_Array.First)); if Expression_Value then Failed ("Wrong value for quantified expression - 5"); end if; if TC_Last_Check < 2 then Failed ("Did not evaluate enough elements for False quantified expression" & " - 5"); elsif TC_Last_Check > 2 then Failed ("Evaluated too many elements for False quantified expression" & " - 5"); end if; exception when others => Failed ("Unexpected exception raised - 5"); end Objective_C_Forward; --Report.Comment ("Test 6"); TC_Last_Check := Test_Array.Length + 1; Objective_C_Reverse : declare Expression_Value : Boolean := False; begin -- Objective_C_Reverse -- Reverse iteration stopping on the 7th element. Expression_Value := (for all Position in reverse Test_Array.Iterate => Succession_Check (Position, Backward, Result => Sparse_Arrays.Storage_Index_Of (Position) > 7)); if Expression_Value then Failed ("Wrong value for quantified expression - 6"); end if; if TC_Last_Check < 7 then Failed ("Did not evaluate enough elements for False quantified expression" & " - 6"); elsif TC_Last_Check > 7 then Failed ("Evaluated too many elements for False quantified expression" & " - 6"); end if; exception when others => Failed ("Unexpected exception raised - 6"); end Objective_C_Reverse; --Report.Comment ("Test 7"); TC_Last_Check := 0; Objective_C_Forward_Middle : declare Expression_Value : Boolean := False; begin -- Objective_C_Forward_Middle -- Forward iteration to check one element exists, in this case -- the third element. Expression_Value := (for some Position in Test_Array.Iterate => Succession_Check (Position, Forward, Result => Sparse_Arrays.Storage_Index_Of (Position) = 3)); if not Expression_Value then Failed ("Wrong value for quantified expression - 7"); end if; if TC_Last_Check < 3 then Failed ("Did not evaluate enough elements for True quantified expression" & " - 7"); elsif TC_Last_Check > 3 then Failed ("Evaluated too many elements for True quantified expression" & " - 7"); end if; exception when others => Failed ("Unexpected exception raised - 7"); end Objective_C_Forward_Middle; --Report.Comment ("Test 8"); TC_Last_Check := Test_Array.Length + 1; Objective_C_Reverse_Middle : declare Expression_Value : Boolean := False; begin -- Objective_C_Reverse_Middle -- Reverse iteration to check if one element exists, in this case -- the sixth element. Expression_Value := (for some Position in reverse Test_Array.Iterate => Succession_Check (Position, Backward, Result => Sparse_Arrays.Storage_Index_Of (Position) = 6)); if not Expression_Value then Failed ("Wrong value for Quantified Expression - 8"); end if; if TC_Last_Check < 6 then Failed ("Did not evaluate enough elements for True quantified expression" & " - 8"); elsif TC_Last_Check > 6 then Failed ("Evaluated too many elements for True quantified expression" & " - 8"); end if; exception when others => Failed ("Unexpected exception raised - 8"); end Objective_C_Reverse_Middle; --Report.Comment ("Test 9"); TC_Last_Check := 0; Objective_B_Some_False_Forward : declare Expression_Value : Boolean := False; begin -- Objective_B_Some_False_Forward -- Forward iteration to check one element exists, but none do. Expression_Value := (for some Position in Test_Array.Iterate => Succession_Check (Position, Forward, Result => False)); if Expression_Value then Failed ("Wrong value for quantified expression - 9"); end if; if TC_Last_Check /= Test_Array.Length then Failed ("Unexpected value for last evaluated expression - 9"); end if; exception when others => Failed ("Unexpected exception raised - 9"); end Objective_B_Some_False_Forward; --Report.Comment ("Test 10"); TC_Last_Check := Test_Array.Length + 1; Objective_B_Some_False_Reverse : declare Expression_Value : Boolean := False; begin -- Objective_B_Some_False_Reverse -- Reverse iteration to check if one element exists, but none do. Expression_Value := (for some Position in reverse Test_Array.Iterate => Succession_Check (Position, Backward, Result => False)); if Expression_Value then Failed ("Wrong value for Quantified Expression - 10"); end if; if TC_Last_Check /= 1 then Failed ("Unexpected value for last evaluated expression - 10"); end if; exception when others => Failed ("Unexpected exception raised - 10"); end Objective_B_Some_False_Reverse; --Report.Comment ("Test 11"); TC_Last_Check := 0; Objective_B_All_False_Forward : declare Expression_Value : Boolean := False; begin -- Objective_B_All_False_Forward -- Forward iteration to check one element exists, but none do. Expression_Value := (for all Position in Test_Array.Iterate => Succession_Check (Position, Forward, Result => False)); if Expression_Value then Failed ("Wrong value for quantified expression - 11"); end if; if TC_Last_Check /= 1 then Failed ("Unexpected value for last evaluated expression - 11"); end if; exception when others => Failed ("Unexpected exception raised - 11"); end Objective_B_All_False_Forward; --Report.Comment ("Test 12"); TC_Last_Check := Test_Array.Length + 1; Objective_B_All_False_Reverse : declare Expression_Value : Boolean := False; begin -- Objective_B_All_False_Forward -- Forward iteration to check one element exists, but none do. Expression_Value := (for all Position in reverse Test_Array.Iterate => Succession_Check (Position, Backward, Result => False)); if Expression_Value then Failed ("Wrong value for quantified expression - 12"); end if; if TC_Last_Check /= Test_Array.Length then Failed ("Unexpected value for last evaluated expression - 12"); end if; exception when others => Failed ("Unexpected exception raised - 12"); end Objective_B_All_False_Reverse; --Report.Comment ("Test 13"); Objective_D_None_Forward : declare Expression_Value : Boolean := False; begin -- Objective_D_None_Forward -- Forward iteration to check one element exists, but none do. Expression_Value := (for all Position in Empty_Array.Iterate => Succession_Check (Position, Forward, Result => False)); if not Expression_Value then Failed ("Wrong value for quantified expression - 13"); end if; exception when others => Failed ("Unexpected exception raised - 13"); end Objective_D_None_Forward; --Report.Comment ("Test 14"); Objective_D_None_Reverse : declare Expression_Value : Boolean := False; begin -- Objective_D_None_Reverse -- Forward iteration to check one element exists, but none do. Expression_Value := (for all Position in reverse Empty_Array.Iterate => Succession_Check (Position, Backward, Result => False)); if not Expression_Value then Failed ("Wrong value for quantified expression - 14"); end if; exception when others => Failed ("Unexpected exception raised - 14"); end Objective_D_None_Reverse; --Report.Comment ("Test 15"); Objective_E_None_Forward : declare Expression_Value : Boolean := False; begin -- Objective_E_None_Forward -- Forward iteration to check one element exists, but none do. Expression_Value := (for some Position in Empty_Array.Iterate => Succession_Check (Position, Forward, Result => True)); if Expression_Value then Failed ("Wrong value for quantified expression - 15"); end if; exception when others => Failed ("Unexpected exception raised - 15"); end Objective_E_None_Forward; --Report.Comment ("Test 16"); Objective_E_None_Reverse : declare Expression_Value : Boolean := False; begin -- Objective_E_None_Reverse -- Forward iteration to check one element exists, but none do. Expression_Value := (for some Position in reverse Empty_Array.Iterate => Succession_Check (Position, Backward, Result => True)); if Expression_Value then Failed ("Wrong value for quantified expression - 16"); end if; exception when others => Failed ("Unexpected exception raised - 16"); end Objective_E_None_Reverse; --Report.Comment ("Test 17"); TC_Last_Check := 0; Objective_F_Forward_All : declare Expression_Value : Boolean := False; begin -- Objective_F_Forward_All -- Forward iteration until exception is raised Expression_Value := (for all Position in Test_Array.Iterate => Succession_Check (Position, Forward, Result => True, Propagate_Exception => Sparse_Arrays.Storage_Index_Of (Position) = 4)); Failed ("Exception not propagated - 17"); exception when Test_Error => if TC_Last_Check /= 3 then Failed ("Wrong number of iterations - 17"); end if; if Expression_Value then Failed ("Expression_Value should not have been modified - 17"); end if; when others => Failed ("Unexpected exception raised - 17"); end Objective_F_Forward_All; --Report.Comment ("Test 18"); TC_Last_Check := Test_Array.Length + 1; Objective_F_Reverse_All : declare Expression_Value : Boolean := False; begin -- Objective_F_Reverse_All -- Reverse iteration until exception is raised Expression_Value := (for all Position in reverse Test_Array.Iterate => Succession_Check (Position, Backward, Result => True, Propagate_Exception => Sparse_Arrays.Storage_Index_Of (Position) = 4)); Failed ("Exception not propagated - 18"); exception when Test_Error => if TC_Last_Check /= 5 then Failed ("Wrong number of iterations - 18"); end if; if Expression_Value then Failed ("Expression_Value should not have been modified - 18"); end if; when others => Failed ("Unexpected exception raised - 18"); end Objective_F_Reverse_All; --Report.Comment ("Test 19"); TC_Last_Check := 0; Objective_G_Forward_Some : declare Expression_Value : Boolean := False; begin -- Objective_G_Forward_Some -- Forward iteration until exception is raised Expression_Value := (for some Position in Test_Array.Iterate => Succession_Check (Position, Forward, Result => Sparse_Arrays.Storage_Index_Of (Position) > 4, Propagate_Exception => Sparse_Arrays.Storage_Index_Of (Position) = 4)); Failed ("Exception not propagated - 19"); exception when Test_Error => if TC_Last_Check /= 3 then Failed ("Wrong number of iterations - 19"); end if; if Expression_Value then Failed ("Expression_Value should not have been modified - 19"); end if; when others => Failed ("Unexpected exception raised - 19"); end Objective_G_Forward_Some; --Report.Comment ("Test 20"); TC_Last_Check := Test_Array.Length + 1; Objective_G_Reverse_Some : declare Expression_Value : Boolean := False; begin -- Objective_G_Reverse_Some -- Reverse iteration until exception is raised Expression_Value := (for some Position in reverse Test_Array.Iterate => Succession_Check (Position, Backward, Result => Sparse_Arrays.Storage_Index_Of (Position) < 4, Propagate_Exception => Sparse_Arrays.Storage_Index_Of (Position) = 4)); Failed ("Exception not propagated - 20"); exception when Test_Error => if TC_Last_Check /= 5 then Failed ("Wrong number of iterations - 20"); end if; if Expression_Value then Failed ("Expression_Value should not have been modified - 20"); end if; when others => Failed ("Unexpected exception raised - 20"); end Objective_G_Reverse_Some; Result; end C458A01;