with Ada.Strings.Fixed;
function Contains3 (S : in String;
Ch : in Character) return Boolean
with
SPARK_Mode => On,
Pre => S'Length > 0,
Post => Contains3'Result = (for some I in S'Range => S (I) = Ch)
is
Search_String : String (1 .. 1) := (others => Ch);
Result_Index : Natural;
begin
-- An empty search string causes Index to raise Pattern_Error
-- A starting point for the search that is out of bounds raises Index_Error
pragma Assert (Search_String'Length > 0 and S'First in S'Range);
Result_Index := Ada.Strings.Fixed.Index (Source => S,
Pattern => Search_String,
From => S'First);
-- Index returns zero if it doesn't find the string or else it returns
-- a position in the string where the pattern starts
pragma Assume
(if Result_Index = 0 then
(for all J in S'Range => S (J) /= Ch)
else
(Result_Index in S'Range and then S (Result_Index) = Ch));
return Result_Index /= 0;
end Contains3;