gnatprove_13.2.1_28fc3583/share/examples/spark/spark_book/Chapter-07/contains.adb

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
with Ada.Strings.Fixed;
function Contains (S  : in String;
                   Ch : in Character) return Boolean
   with SPARK_Mode => On
is
   Search_String : String (1 .. 1) := (others => Ch);
   Result_Index  : Natural;
begin
   Result_Index := Ada.Strings.Fixed.Index (Source  => S,
                                            Pattern => Search_String,
                                            From    => S'First);
   return Result_Index /= 0;
end Contains;