diff --git a/gcc/ada/libgnat/a-strunb.adb b/gcc/ada/libgnat/a-strunb.adb
index c3d4c71271b..163906ed5cd 100644
--- a/gcc/ada/libgnat/a-strunb.adb
+++ b/gcc/ada/libgnat/a-strunb.adb
@@ -30,22 +30,21 @@
 ------------------------------------------------------------------------------
 
 with Ada.Strings.Fixed;
-with Ada.Strings.Search;
 with Ada.Unchecked_Deallocation;
 
 package body Ada.Strings.Unbounded is
 
-   function Sum (Left : Natural; Right : Integer) return Natural with Inline;
+   function Sum (Left, Right : Natural) return Natural with Inline;
    --  Returns summary of Left and Right, raise Constraint_Error on overflow
 
    function Mul (Left, Right : Natural) return Natural with Inline;
    --  Returns multiplication of Left and Right, raise Constraint_Error on
    --  overflow.
 
-   function Saturated_Sum (Left : Natural; Right : Integer) return Natural;
+   function Saturated_Sum (Left, Right : Natural) return Natural;
    --  Returns summary of Left and Right or Natural'Last on overflow
 
-   function Saturated_Mul (Left, Right : Natural) return Natural;
+   function Saturated_Mul (Left, Right : Positive) return Positive;
    --  Returns multiplication of Left and Right or Natural'Last on overflow
 
    ---------
@@ -67,8 +66,11 @@ package body Ada.Strings.Unbounded is
 
       Result.Reference (1 .. L_Length) :=
         Left.Reference (1 .. Left.Last);
-      Result.Reference (L_Length + 1 .. Result.Last) :=
-        Right.Reference (1 .. Right.Last);
+
+      if L_Length < Natural'Last then
+         Result.Reference (L_Length + 1 .. Result.Last) :=
+           Right.Reference (1 .. Right.Last);
+      end if;
 
       return Result;
    end "&";
@@ -86,7 +88,10 @@ package body Ada.Strings.Unbounded is
       Result.Reference := new String (1 .. Result.Last);
 
       Result.Reference (1 .. L_Length) := Left.Reference (1 .. Left.Last);
-      Result.Reference (L_Length + 1 .. Result.Last) := Right;
+
+      if L_Length < Natural'Last then
+         Result.Reference (L_Length + 1 .. Result.Last) := Right;
+      end if;
 
       return Result;
    end "&";
@@ -104,8 +109,11 @@ package body Ada.Strings.Unbounded is
       Result.Reference := new String (1 .. Result.Last);
 
       Result.Reference (1 .. Left'Length) := Left;
-      Result.Reference (Left'Length + 1 .. Result.Last) :=
-        Right.Reference (1 .. Right.Last);
+
+      if Left'Length < Natural'Last then
+         Result.Reference (Left'Length + 1 .. Result.Last) :=
+           Right.Reference (1 .. Right.Last);
+      end if;
 
       return Result;
    end "&";
@@ -170,17 +178,21 @@ package body Ada.Strings.Unbounded is
       Right : String) return Unbounded_String
    is
       Len    : constant Natural := Right'Length;
-      K      : Positive;
+      K      : Natural;
       Result : Unbounded_String;
 
    begin
+      if Len = 0 then
+         return Null_Unbounded_String;
+      end if;
+
       Result.Last := Mul (Left, Len);
 
       Result.Reference := new String (1 .. Result.Last);
 
-      K := 1;
+      K := 0;
       for J in 1 .. Left loop
-         Result.Reference (K .. K + Len - 1) := Right;
+         Result.Reference (K + 1 .. K + Len) := Right;
          K := K + Len;
       end loop;
 
@@ -192,17 +204,21 @@ package body Ada.Strings.Unbounded is
       Right : Unbounded_String) return Unbounded_String
    is
       Len    : constant Natural := Right.Last;
-      K      : Positive;
+      K      : Natural;
       Result : Unbounded_String;
 
    begin
+      if Len = 0 then
+         return Null_Unbounded_String;
+      end if;
+
       Result.Last := Mul (Left, Len);
 
       Result.Reference := new String (1 .. Result.Last);
 
-      K := 1;
+      K := 0;
       for J in 1 .. Left loop
-         Result.Reference (K .. K + Len - 1) :=
+         Result.Reference (K + 1 .. K + Len) :=
            Right.Reference (1 .. Right.Last);
          K := K + Len;
       end loop;
@@ -380,8 +396,12 @@ package body Ada.Strings.Unbounded is
    is
    begin
       Realloc_For_Chunk (Source, New_Item.Last);
-      Source.Reference (Source.Last + 1 .. Source.Last + New_Item.Last) :=
-        New_Item.Reference (1 .. New_Item.Last);
+
+      if Source.Last < Natural'Last then
+         Source.Reference (Source.Last + 1 .. Source.Last + New_Item.Last) :=
+           New_Item.Reference (1 .. New_Item.Last);
+      end if;
+
       Source.Last := Source.Last + New_Item.Last;
    end Append;
 
@@ -391,8 +411,12 @@ package body Ada.Strings.Unbounded is
    is
    begin
       Realloc_For_Chunk (Source, New_Item'Length);
-      Source.Reference (Source.Last + 1 .. Source.Last + New_Item'Length) :=
-        New_Item;
+
+      if Source.Last < Natural'Last then
+         Source.Reference (Source.Last + 1 .. Source.Last + New_Item'Length) :=
+           New_Item;
+      end if;
+
       Source.Last := Source.Last + New_Item'Length;
    end Append;
 
@@ -462,16 +486,20 @@ package body Ada.Strings.Unbounded is
       if From > Through then
          null;
 
-      elsif From < Source.Reference'First or else Through > Source.Last then
+      elsif From - 1 > Source.Last then
          raise Index_Error;
 
       else
          declare
-            Len : constant Natural := Through - From + 1;
+            Len : constant Natural :=
+              Natural'Min (Source.Last, Through) - From + 1;
 
          begin
-            Source.Reference (From .. Source.Last - Len) :=
-              Source.Reference (Through + 1 .. Source.Last);
+            if Through < Natural'Last then
+               Source.Reference (From .. Source.Last - Len) :=
+                 Source.Reference (Through + 1 .. Source.Last);
+            end if;
+
             Source.Last := Source.Last - Len;
          end;
       end if;
@@ -714,17 +742,19 @@ package body Ada.Strings.Unbounded is
       New_Item : String)
    is
    begin
-      if Before not in Source.Reference'First .. Source.Last + 1 then
+      if Before - 1 > Source.Last then
          raise Index_Error;
       end if;
 
       Realloc_For_Chunk (Source, New_Item'Length);
 
-      Source.Reference
-        (Before + New_Item'Length .. Source.Last + New_Item'Length) :=
-           Source.Reference (Before .. Source.Last);
+      if Before <= Source.Last then
+         Source.Reference
+           (Before + New_Item'Length .. Source.Last + New_Item'Length) :=
+             Source.Reference (Before .. Source.Last);
+      end if;
 
-      Source.Reference (Before .. Before + New_Item'Length - 1) := New_Item;
+      Source.Reference (Before .. Before - 1 + New_Item'Length) := New_Item;
       Source.Last := Source.Last + New_Item'Length;
    end Insert;
 
@@ -733,9 +763,7 @@ package body Ada.Strings.Unbounded is
    ------------
 
    function Length (Source : Unbounded_String) return Natural is
-   begin
-      return Source.Last;
-   end Length;
+     (Source.Last);
 
    ---------
    -- Mul --
@@ -769,8 +797,8 @@ package body Ada.Strings.Unbounded is
    is
       NL : constant Natural := New_Item'Length;
    begin
-      if Position <= Source.Last - NL + 1 then
-         Source.Reference (Position .. Position + NL - 1) := New_Item;
+      if Position - 1 <= Source.Last - NL then
+         Source.Reference (Position .. Position - 1 + NL) := New_Item;
       else
          declare
             Old : String_Access := Source.Reference;
@@ -897,7 +925,7 @@ package body Ada.Strings.Unbounded is
    -- Saturated_Mul --
    -------------------
 
-   function Saturated_Mul (Left, Right : Natural) return Natural is
+   function Saturated_Mul (Left, Right : Positive) return Positive is
    begin
       return Mul (Left, Right);
    exception
@@ -905,11 +933,11 @@ package body Ada.Strings.Unbounded is
          return Natural'Last;
    end Saturated_Mul;
 
-   -----------------
+   -------------------
    -- Saturated_Sum --
-   -----------------
+   -------------------
 
-   function Saturated_Sum (Left : Natural; Right : Integer) return Natural is
+   function Saturated_Sum (Left, Right : Natural) return Natural is
    begin
       return Sum (Left, Right);
    exception
@@ -945,7 +973,7 @@ package body Ada.Strings.Unbounded is
    begin
       --  Note: test of High > Length is in accordance with AI95-00128
 
-      if Low > Source.Last + 1 or else High > Source.Last then
+      if Low - 1 > Source.Last or else High > Source.Last then
          raise Index_Error;
       else
          return Source.Reference (Low .. High);
@@ -956,7 +984,7 @@ package body Ada.Strings.Unbounded is
    -- Sum --
    ---------
 
-   function Sum (Left : Natural; Right : Integer) return Natural is
+   function Sum (Left, Right : Natural) return Natural is
       pragma Unsuppress (Overflow_Check);
    begin
       return Left + Right;
@@ -993,9 +1021,7 @@ package body Ada.Strings.Unbounded is
    ---------------
 
    function To_String (Source : Unbounded_String) return String is
-   begin
-      return Source.Reference (1 .. Source.Last);
-   end To_String;
+     (Source.Reference (1 .. Source.Last));
 
    -------------------------
    -- To_Unbounded_String --
diff --git a/gcc/ada/libgnat/a-strunb.ads b/gcc/ada/libgnat/a-strunb.ads
index 385544ecb57..981f406a767 100644
--- a/gcc/ada/libgnat/a-strunb.ads
+++ b/gcc/ada/libgnat/a-strunb.ads
@@ -35,12 +35,18 @@
 
 --  Preconditions in this unit are meant for analysis only, not for run-time
 --  checking, so that the expected exceptions are raised. This is enforced by
---  setting the corresponding assertion policy to Ignore.
+--  setting the corresponding assertion policy to Ignore. Postconditions and
+--  contract cases should not be executed at runtime as well, in order not to
+--  slow down the execution of these functions.
 
-pragma Assertion_Policy (Pre => Ignore);
+pragma Assertion_Policy (Pre            => Ignore,
+                         Post           => Ignore,
+                         Contract_Cases => Ignore,
+                         Ghost          => Ignore);
 
-with Ada.Strings.Maps;
+with Ada.Strings.Maps; use type Ada.Strings.Maps.Character_Mapping_Function;
 with Ada.Finalization;
+with Ada.Strings.Search;
 private with Ada.Strings.Text_Buffers;
 
 --  The language-defined package Strings.Unbounded provides a private type
@@ -59,6 +65,13 @@ package Ada.Strings.Unbounded with
 is
    pragma Preelaborate;
 
+   --  Contracts may call function Length in the prefix of attribute reference
+   --  to Old as in Length (Source)'Old. Allow this use.
+
+   pragma Unevaluated_Use_Of_Old (Allow);
+
+   subtype String_1 is String (1 .. <>) with Ghost;  --  Type used in contracts
+
    type Unbounded_String is private with
      Default_Initial_Condition => Length (Unbounded_String) = 0;
    pragma Preelaborable_Initialization (Unbounded_String);
@@ -84,9 +97,10 @@ is
    --------------------------------------------------------
 
    function To_Unbounded_String
-     (Source : String)  return Unbounded_String
+     (Source : String) return Unbounded_String
    with
-     Post   => To_String (To_Unbounded_String'Result) = Source,
+     Post   => To_String (To_Unbounded_String'Result) = Source
+       and then Length (To_Unbounded_String'Result) = Source'Length,
      Global => null;
    --  Returns an Unbounded_String that represents Source
 
@@ -126,7 +140,8 @@ is
       New_Item : Unbounded_String)
    with
      Pre    => Length (New_Item) <= Natural'Last - Length (Source),
-     Post   => Length (Source) = Length (Source)'Old + Length (New_Item),
+     Post   =>
+       To_String (Source) = To_String (Source)'Old & To_String (New_Item),
      Global => null;
 
    procedure Append
@@ -134,7 +149,7 @@ is
       New_Item : String)
    with
      Pre    => New_Item'Length <= Natural'Last - Length (Source),
-     Post   => Length (Source) = Length (Source)'Old + New_Item'Length,
+     Post   => To_String (Source) = To_String (Source)'Old & New_Item,
      Global => null;
 
    procedure Append
@@ -142,7 +157,7 @@ is
       New_Item : Character)
    with
      Pre    => Length (Source) < Natural'Last,
-     Post   => Length (Source) = Length (Source)'Old + 1,
+     Post   => To_String (Source) = To_String (Source)'Old & New_Item,
      Global => null;
 
    --  For each of the Append procedures, the resulting string represented by
@@ -154,7 +169,7 @@ is
       Right : Unbounded_String) return Unbounded_String
    with
      Pre    => Length (Right) <= Natural'Last - Length (Left),
-     Post   => Length ("&"'Result) = Length (Left) + Length (Right),
+     Post   => To_String ("&"'Result) = To_String (Left) & To_String (Right),
      Global => null;
 
    function "&"
@@ -162,7 +177,7 @@ is
       Right : String) return Unbounded_String
    with
      Pre    => Right'Length <= Natural'Last - Length (Left),
-     Post   => Length ("&"'Result) = Length (Left) + Right'Length,
+     Post   => To_String ("&"'Result) = To_String (Left) & Right,
      Global => null;
 
    function "&"
@@ -170,7 +185,7 @@ is
       Right : Unbounded_String) return Unbounded_String
    with
      Pre    => Left'Length <= Natural'Last - Length (Right),
-     Post   => Length ("&"'Result) = Left'Length + Length (Right),
+     Post   => To_String ("&"'Result) = String_1 (Left) & To_String (Right),
      Global => null;
 
    function "&"
@@ -178,7 +193,7 @@ is
       Right : Character) return Unbounded_String
    with
      Pre    => Length (Left) < Natural'Last,
-     Post   => Length ("&"'Result) = Length (Left) + 1,
+     Post   => To_String ("&"'Result) = To_String (Left) & Right,
      Global => null;
 
    function "&"
@@ -186,7 +201,7 @@ is
       Right : Unbounded_String) return Unbounded_String
    with
      Pre    => Length (Right) < Natural'Last,
-     Post   => Length ("&"'Result) = Length (Right) + 1,
+     Post   => To_String ("&"'Result) = Left & To_String (Right),
      Global => null;
 
    --  Each of the "&" functions returns an Unbounded_String obtained by
@@ -211,7 +226,8 @@ is
       By     : Character)
    with
      Pre    => Index <= Length (Source),
-     Post   => Length (Source) = Length (Source)'Old,
+     Post   =>
+       To_String (Source) = (To_String (Source)'Old with delta Index => By),
      Global => null;
    --  Updates Source such that the character at position Index in the string
    --  represented by Source is By; propagates Index_Error if
@@ -223,7 +239,9 @@ is
       High   : Natural) return String
    with
      Pre    => Low - 1 <= Length (Source) and then High <= Length (Source),
-     Post   => Slice'Result'Length = Natural'Max (0, High - Low + 1),
+     Post   => Slice'Result'First = Low
+       and then Slice'Result'Last = High
+       and then Slice'Result = To_String (Source) (Low .. High),
      Global => null;
    --  Returns the slice at positions Low through High in the string
    --  represented by Source; propagates Index_Error if
@@ -237,7 +255,7 @@ is
    with
      Pre    => Low - 1 <= Length (Source) and then High <= Length (Source),
      Post   =>
-       Length (Unbounded_Slice'Result) = Natural'Max (0, High - Low + 1),
+       To_String (Unbounded_Slice'Result) = To_String (Source) (Low .. High),
      Global => null;
    pragma Ada_05 (Unbounded_Slice);
    --  Returns the slice at positions Low through High in the string
@@ -251,7 +269,7 @@ is
       High   : Natural)
    with
      Pre    => Low - 1 <= Length (Source) and then High <= Length (Source),
-     Post   => Length (Target) = Natural'Max (0, High - Low + 1),
+     Post   => To_String (Target) = To_String (Source) (Low .. High),
      Global => null;
    pragma Ada_05 (Unbounded_Slice);
    --  Sets Target to the Unbounded_String representing the slice at positions
@@ -283,72 +301,84 @@ is
      (Left  : Unbounded_String;
       Right : Unbounded_String) return Boolean
    with
+     Post   => "<"'Result = (To_String (Left) < To_String (Right)),
      Global => null;
 
    function "<"
      (Left  : Unbounded_String;
       Right : String) return Boolean
    with
+     Post   => "<"'Result = (To_String (Left) < Right),
      Global => null;
 
    function "<"
      (Left  : String;
       Right : Unbounded_String) return Boolean
    with
+     Post   => "<"'Result = (Left < To_String (Right)),
      Global => null;
 
    function "<="
      (Left  : Unbounded_String;
       Right : Unbounded_String) return Boolean
    with
+     Post   => "<="'Result = (To_String (Left) <= To_String (Right)),
      Global => null;
 
    function "<="
      (Left  : Unbounded_String;
       Right : String) return Boolean
    with
+     Post   => "<="'Result = (To_String (Left) <= Right),
      Global => null;
 
    function "<="
      (Left  : String;
       Right : Unbounded_String) return Boolean
    with
+     Post   => "<="'Result = (Left <= To_String (Right)),
      Global => null;
 
    function ">"
      (Left  : Unbounded_String;
       Right : Unbounded_String) return Boolean
    with
+     Post   => ">"'Result = (To_String (Left) > To_String (Right)),
      Global => null;
 
    function ">"
      (Left  : Unbounded_String;
       Right : String) return Boolean
    with
+     Post   => ">"'Result = (To_String (Left) > Right),
      Global => null;
 
    function ">"
      (Left  : String;
       Right : Unbounded_String) return Boolean
    with
+     Post   => ">"'Result = (Left > To_String (Right)),
      Global => null;
 
    function ">="
      (Left  : Unbounded_String;
       Right : Unbounded_String) return Boolean
    with
+     Post   => ">="'Result = (To_String (Left) >= To_String (Right)),
      Global => null;
 
    function ">="
      (Left  : Unbounded_String;
       Right : String) return Boolean
    with
+     Post   => ">="'Result = (To_String (Left) >= Right),
      Global => null;
 
    function ">="
      (Left  : String;
       Right : Unbounded_String) return Boolean
    with
+     Post   => ">="'Result = (Left >= To_String (Right)),
      Global => null;
 
    --  Each of the functions "=", "<", ">", "<=", and ">=" returns the same
@@ -365,8 +395,52 @@ is
       Going   : Direction := Forward;
       Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
    with
-     Pre    => Pattern'Length /= 0,
-     Global => null;
+     Pre            => Pattern'Length > 0,
+     Post           => Index'Result <= Length (Source),
+     Contract_Cases =>
+
+       --  If Source is the empty string, then 0 is returned
+
+       (Length (Source) = 0
+        =>
+          Index'Result = 0,
+
+        --  If some slice of Source matches Pattern, then a valid index is
+        --  returned.
+
+        Length (Source) > 0
+          and then
+            (for some J in 1 .. Length (Source) - (Pattern'Length - 1) =>
+               Search.Match (To_String (Source), Pattern, Mapping, J))
+        =>
+          --  The result is in the considered range of Source
+
+          Index'Result in 1 .. Length (Source) - (Pattern'Length - 1)
+
+            --  The slice beginning at the returned index matches Pattern
+
+            and then Search.Match
+              (To_String (Source), Pattern, Mapping, Index'Result)
+
+            --  The result is the smallest or largest index which satisfies
+            --  the matching, respectively when Going = Forward and Going =
+            --  Backward.
+
+            and then
+              (for all J in 1 .. Length (Source) =>
+                 (if (if Going = Forward
+                      then J <= Index'Result - 1
+                      else J - 1 in Index'Result
+                                    .. Length (Source) - Pattern'Length)
+                  then not (Search.Match
+                    (To_String (Source), Pattern, Mapping, J)))),
+
+        --  Otherwise, 0 is returned
+
+        others
+        =>
+          Index'Result = 0),
+     Global         => null;
 
    function Index
      (Source  : Unbounded_String;
@@ -374,8 +448,52 @@ is
       Going   : Direction := Forward;
       Mapping : Maps.Character_Mapping_Function) return Natural
    with
-     Pre    => Pattern'Length /= 0,
-     Global => null;
+     Pre            => Pattern'Length /= 0 and then Mapping /= null,
+     Post           => Index'Result <= Length (Source),
+     Contract_Cases =>
+
+       --  If Source is the empty string, then 0 is returned
+
+       (Length (Source) = 0
+        =>
+          Index'Result = 0,
+
+        --  If some slice of Source matches Pattern, then a valid index is
+        --  returned.
+
+        Length (Source) > 0
+          and then
+            (for some J in 1 .. Length (Source) - (Pattern'Length - 1) =>
+               Search.Match (To_String (Source), Pattern, Mapping, J))
+        =>
+          --  The result is in the considered range of Source
+
+          Index'Result in 1 .. Length (Source) - (Pattern'Length - 1)
+
+            --  The slice beginning at the returned index matches Pattern
+
+            and then Search.Match
+              (To_String (Source), Pattern, Mapping, Index'Result)
+
+            --  The result is the smallest or largest index which satisfies
+            --  the matching, respectively when Going = Forward and Going =
+            --  Backward.
+
+            and then
+              (for all J in 1 .. Length (Source) =>
+                 (if (if Going = Forward
+                      then J <= Index'Result - 1
+                      else J - 1 in Index'Result
+                                    .. Length (Source) - Pattern'Length)
+                  then not (Search.Match
+                    (To_String (Source), Pattern, Mapping, J)))),
+
+        --  Otherwise, 0 is returned
+
+        others
+        =>
+          Index'Result = 0),
+     Global         => null;
 
    function Index
      (Source : Unbounded_String;
@@ -383,7 +501,43 @@ is
       Test   : Membership := Inside;
       Going  : Direction  := Forward) return Natural
    with
-     Global => null;
+     Post           => Index'Result <= Length (Source),
+     Contract_Cases =>
+
+        --  If no character of Source satisfies the property Test on Set,
+        --  then 0 is returned.
+
+       ((for all C of To_String (Source) =>
+           (Test = Inside) /= Maps.Is_In (C, Set))
+        =>
+          Index'Result = 0,
+
+        --  Otherwise, an index in the range of Source is returned
+
+        others
+        =>
+          --  The result is in the range of Source
+
+          Index'Result in 1 .. Length (Source)
+
+            --  The character at the returned index satisfies the property
+            --  Test on Set.
+
+            and then
+              (Test = Inside) =
+                Maps.Is_In (Element (Source, Index'Result), Set)
+
+            --  The result is the smallest or largest index which satisfies
+            --  the property, respectively when Going = Forward and Going =
+            --  Backward.
+
+            and then
+              (for all J in 1 .. Length (Source) =>
+                 (if J /= Index'Result
+                       and then (J < Index'Result) = (Going = Forward)
+                  then (Test = Inside)
+                       /= Maps.Is_In (Element (Source, J), Set)))),
+     Global         => null;
 
    function Index
      (Source  : Unbounded_String;
@@ -392,9 +546,60 @@ is
       Going   : Direction := Forward;
       Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
    with
-     Pre    => (if Length (Source) /= 0 then From <= Length (Source))
-               and then Pattern'Length /= 0,
-     Global => null;
+     Pre            =>
+       (if Length (Source) /= 0 then From <= Length (Source))
+         and then Pattern'Length /= 0,
+     Post           => Index'Result <= Length (Source),
+     Contract_Cases =>
+
+       --  If Source is the empty string, then 0 is returned
+
+       (Length (Source) = 0
+        =>
+          Index'Result = 0,
+
+        --  If some slice of Source matches Pattern, then a valid index is
+        --  returned.
+
+        Length (Source) > 0
+          and then
+            (for some J in
+              (if Going = Forward then From else 1)
+               .. (if Going = Forward then Length (Source) else From)
+                - (Pattern'Length - 1) =>
+              Search.Match (To_String (Source), Pattern, Mapping, J))
+        =>
+          --  The result is in the considered range of Source
+
+          Index'Result in
+            (if Going = Forward then From else 1)
+            .. (if Going = Forward then Length (Source) else From)
+             - (Pattern'Length - 1)
+
+            --  The slice beginning at the returned index matches Pattern
+
+            and then Search.Match
+              (To_String (Source), Pattern, Mapping, Index'Result)
+
+            --  The result is the smallest or largest index which satisfies
+            --  the matching, respectively when Going = Forward and Going =
+            --  Backward.
+
+            and then
+              (for all J in 1 .. Length (Source) =>
+                 (if (if Going = Forward
+                      then J in From .. Index'Result - 1
+                      else J - 1 in Index'Result
+                                    .. From - Pattern'Length)
+                  then not (Search.Match
+                    (To_String (Source), Pattern, Mapping, J)))),
+
+        --  Otherwise, 0 is returned
+
+        others
+        =>
+          Index'Result = 0),
+     Global         => null;
    pragma Ada_05 (Index);
 
    function Index
@@ -404,9 +609,61 @@ is
       Going   : Direction := Forward;
       Mapping : Maps.Character_Mapping_Function) return Natural
    with
-     Pre    => (if Length (Source) /= 0 then From <= Length (Source))
-               and then Pattern'Length /= 0,
-     Global => null;
+     Pre            =>
+       (if Length (Source) /= 0 then From <= Length (Source))
+         and then Pattern'Length /= 0
+         and then Mapping /= null,
+     Post           => Index'Result <= Length (Source),
+     Contract_Cases =>
+
+       --  If Source is the empty string, then 0 is returned
+
+       (Length (Source) = 0
+        =>
+          Index'Result = 0,
+
+        --  If some slice of Source matches Pattern, then a valid index is
+        --  returned.
+
+        Length (Source) > 0
+          and then
+            (for some J in
+              (if Going = Forward then From else 1)
+               .. (if Going = Forward then Length (Source) else From)
+                - (Pattern'Length - 1) =>
+              Search.Match (To_String (Source), Pattern, Mapping, J))
+        =>
+          --  The result is in the considered range of Source
+
+          Index'Result in
+            (if Going = Forward then From else 1)
+            .. (if Going = Forward then Length (Source) else From)
+             - (Pattern'Length - 1)
+
+            --  The slice beginning at the returned index matches Pattern
+
+            and then Search.Match
+              (To_String (Source), Pattern, Mapping, Index'Result)
+
+            --  The result is the smallest or largest index which satisfies
+            --  the matching, respectively when Going = Forward and Going =
+            --  Backward.
+
+            and then
+              (for all J in 1 .. Length (Source) =>
+                 (if (if Going = Forward
+                      then J in From .. Index'Result - 1
+                      else J - 1 in Index'Result
+                                    .. From - Pattern'Length)
+                  then not (Search.Match
+                    (To_String (Source), Pattern, Mapping, J)))),
+
+        --  Otherwise, 0 is returned
+
+        others
+        =>
+          Index'Result = 0),
+     Global         => null;
    pragma Ada_05 (Index);
 
    function Index
@@ -416,23 +673,147 @@ is
       Test    : Membership := Inside;
       Going   : Direction := Forward) return Natural
    with
-     Pre    => (if Length (Source) /= 0 then From <= Length (Source)),
-     Global => null;
+     Pre            =>
+       (if Length (Source) /= 0 then From <= Length (Source)),
+     Post           => Index'Result <= Length (Source),
+     Contract_Cases =>
+
+        --  If Source is the empty string, or no character of the considered
+        --  slice of Source satisfies the property Test on Set, then 0 is
+        --  returned.
+
+       (Length (Source) = 0
+          or else
+            (for all J in 1 .. Length (Source) =>
+               (if J = From or else (J > From) = (Going = Forward) then
+                  (Test = Inside) /= Maps.Is_In (Element (Source, J), Set)))
+        =>
+          Index'Result = 0,
+
+        --  Otherwise, an index in the considered range of Source is
+        --  returned.
+
+        others
+        =>
+          --  The result is in the considered range of Source
+
+          Index'Result in 1 .. Length (Source)
+            and then
+              (Index'Result = From
+                 or else (Index'Result > From) = (Going = Forward))
+
+            --  The character at the returned index satisfies the property
+            --  Test on Set.
+
+            and then
+              (Test = Inside) =
+                Maps.Is_In (Element (Source, Index'Result), Set)
+
+            --  The result is the smallest or largest index which satisfies
+            --  the property, respectively when Going = Forward and Going =
+            --  Backward.
+
+            and then
+              (for all J in 1 .. Length (Source) =>
+                 (if J /= Index'Result
+                    and then (J < Index'Result) = (Going = Forward)
+                    and then (J = From
+                                or else (J > From) = (Going = Forward))
+                  then (Test = Inside)
+                       /= Maps.Is_In (Element (Source, J), Set)))),
+     Global         => null;
    pragma Ada_05 (Index);
 
    function Index_Non_Blank
      (Source : Unbounded_String;
       Going  : Direction := Forward) return Natural
    with
-     Global => null;
+     Post           => Index_Non_Blank'Result <= Length (Source),
+     Contract_Cases =>
+
+        --  If all characters of Source are Space characters, then 0 is
+        --  returned.
+
+       ((for all C of To_String (Source) => C = ' ')
+        =>
+          Index_Non_Blank'Result = 0,
+
+        --  Otherwise, an index in the range of Source is returned
+
+        others
+        =>
+          --  The result is in the range of Source
+
+          Index_Non_Blank'Result in 1 .. Length (Source)
+
+            --  The character at the returned index is not a Space character
+
+            and then Element (Source, Index_Non_Blank'Result) /= ' '
+
+            --  The result is the smallest or largest index which is not a
+            --  Space character, respectively when Going = Forward and Going
+            --  = Backward.
+
+            and then
+              (for all J in 1 .. Length (Source) =>
+                 (if J /= Index_Non_Blank'Result
+                       and then
+                         (J < Index_Non_Blank'Result) = (Going = Forward)
+                  then Element (Source, J) = ' '))),
+     Global         => null;
 
    function Index_Non_Blank
      (Source : Unbounded_String;
       From   : Positive;
       Going  : Direction := Forward) return Natural
    with
-     Pre    => (if Length (Source) /= 0 then From <= Length (Source)),
-     Global => null;
+     Pre            =>
+       (if Length (Source) /= 0 then From <= Length (Source)),
+     Post           => Index_Non_Blank'Result <= Length (Source),
+     Contract_Cases =>
+
+        --  If Source is the empty string, or all characters of the
+        --  considered slice of Source are Space characters, then 0
+        --  is returned.
+
+       (Length (Source) = 0
+          or else
+            (for all J in 1 .. Length (Source) =>
+               (if J = From or else (J > From) = (Going = Forward) then
+                  Element (Source, J) = ' '))
+        =>
+          Index_Non_Blank'Result = 0,
+
+        --  Otherwise, an index in the considered range of Source is
+        --  returned.
+
+        others
+        =>
+          --  The result is in the considered range of Source
+
+          Index_Non_Blank'Result in 1 .. Length (Source)
+            and then
+              (Index_Non_Blank'Result = From
+                 or else
+                   (Index_Non_Blank'Result > From) = (Going = Forward))
+
+            --  The character at the returned index is not a Space character
+
+            and then Element (Source, Index_Non_Blank'Result) /= ' '
+
+            --  The result is the smallest or largest index which isn't a
+            --  Space character, respectively when Going = Forward and Going
+            --  = Backward.
+
+            and then
+              (for all J in 1 .. Length (Source) =>
+                 (if J /= Index_Non_Blank'Result
+                    and then
+                      (J < Index_Non_Blank'Result) = (Going = Forward)
+                    and then (J = From
+                                or else (J > From) = (Going = Forward))
+                  then Element (Source, J) = ' '))),
+     Global         => null;
    pragma Ada_05 (Index_Non_Blank);
 
    function Count
@@ -448,7 +829,7 @@ is
       Pattern : String;
       Mapping : Maps.Character_Mapping_Function) return Natural
    with
-     Pre    => Pattern'Length /= 0,
+     Pre    => Pattern'Length /= 0 and then Mapping /= null,
      Global => null;
 
    function Count
@@ -465,8 +846,53 @@ is
       First  : out Positive;
       Last   : out Natural)
    with
-     Pre    => (if Length (Source) /= 0 then From <= Length (Source)),
-     Global => null;
+     Pre            =>
+       (if Length (Source) /= 0 then From <= Length (Source)),
+     Contract_Cases =>
+
+        --  If Source is the empty string, or if no character of the
+        --  considered slice of Source satisfies the property Test on
+        --  Set, then First is set to From and Last is set to 0.
+
+       (Length (Source) = 0
+          or else
+            (for all J in From .. Length (Source) =>
+               (Test = Inside) /= Maps.Is_In (Element (Source, J), Set))
+        =>
+          First = From and then Last = 0,
+
+        --  Otherwise, First and Last are set to valid indexes
+
+        others
+        =>
+          --  First and Last are in the considered range of Source
+
+          First in From .. Length (Source)
+            and then Last in First .. Length (Source)
+
+            --  No character between From and First satisfies the property
+            --  Test on Set.
+
+            and then
+              (for all J in From .. First - 1 =>
+                 (Test = Inside) /= Maps.Is_In (Element (Source, J), Set))
+
+            --  All characters between First and Last satisfy the property
+            --  Test on Set.
+
+            and then
+              (for all J in First .. Last =>
+                 (Test = Inside) = Maps.Is_In (Element (Source, J), Set))
+
+            --  If Last is not Source'Last, then the character at position
+            --  Last + 1 does not satify the property Test on Set.
+
+            and then
+              (if Last < Length (Source)
+               then
+                 (Test = Inside)
+                 /= Maps.Is_In (Element (Source, Last + 1), Set))),
+     Global         => null;
    pragma Ada_2012 (Find_Token);
 
    procedure Find_Token
@@ -476,7 +902,51 @@ is
       First  : out Positive;
       Last   : out Natural)
    with
-     Global => null;
+     Contract_Cases =>
+
+        --  If Source is the empty string, or if no character of the
+        --  considered slice of Source satisfies the property Test on
+        --  Set, then First is set to 1 and Last is set to 0.
+
+       (Length (Source) = 0
+          or else
+            (for all J in 1 .. Length (Source) =>
+               (Test = Inside) /= Maps.Is_In (Element (Source, J), Set))
+        =>
+          First = 1 and then Last = 0,
+
+        --  Otherwise, First and Last are set to valid indexes
+
+        others
+        =>
+          --  First and Last are in the considered range of Source
+
+          First in 1 .. Length (Source)
+            and then Last in First .. Length (Source)
+
+            --  No character between 1 and First satisfies the property Test
+            --  on Set.
+
+            and then
+              (for all J in 1 .. First - 1 =>
+                 (Test = Inside) /= Maps.Is_In (Element (Source, J), Set))
+
+            --  All characters between First and Last satisfy the property
+            --  Test on Set.
+
+            and then
+              (for all J in First .. Last =>
+                 (Test = Inside) = Maps.Is_In (Element (Source, J), Set))
+
+            --  If Last is not Source'Last, then the character at position
+            --  Last + 1 does not satify the property Test on Set.
+
+            and then
+              (if Last < Length (Source)
+               then
+                 (Test = Inside)
+                 /= Maps.Is_In (Element (Source, Last + 1), Set))),
+     Global         => null;
 
    --  Each of the search subprograms (Index, Index_Non_Blank, Count,
    --  Find_Token) has the same effect as the corresponding subprogram in
@@ -491,28 +961,44 @@ is
      (Source  : Unbounded_String;
       Mapping : Maps.Character_Mapping) return Unbounded_String
    with
-     Post   => Length (Translate'Result) = Length (Source),
+     Post   => Length (Translate'Result) = Length (Source)
+       and then
+         (for all K in 1 .. Length (Source) =>
+            Element (Translate'Result, K) =
+              Ada.Strings.Maps.Value (Mapping, Element (Source, K))),
      Global => null;
 
    procedure Translate
      (Source  : in out Unbounded_String;
       Mapping : Maps.Character_Mapping)
    with
-     Post   => Length (Source) = Length (Source)'Old,
+     Post   => Length (Source) = Length (Source)'Old
+       and then
+         (for all K in 1 .. Length (Source) =>
+            Element (Source, K) =
+              Ada.Strings.Maps.Value (Mapping, To_String (Source)'Old (K))),
      Global => null;
 
    function Translate
      (Source  : Unbounded_String;
       Mapping : Maps.Character_Mapping_Function) return Unbounded_String
    with
-     Post   => Length (Translate'Result) = Length (Source),
+     Pre    => Mapping /= null,
+     Post   => Length (Translate'Result) = Length (Source)
+       and then
+         (for all K in 1 .. Length (Source) =>
+            Element (Translate'Result, K) = Mapping (Element (Source, K))),
      Global => null;
 
    procedure Translate
      (Source  : in out Unbounded_String;
       Mapping : Maps.Character_Mapping_Function)
    with
-     Post   => Length (Source) = Length (Source)'Old,
+     Pre    => Mapping /= null,
+     Post   => Length (Source) = Length (Source)'Old
+       and then
+         (for all K in 1 .. Length (Source) =>
+            Element (Source, K) = Mapping (To_String (Source)'Old (K))),
      Global => null;
 
    --  The Translate function has an analogous effect to the corresponding
@@ -535,15 +1021,76 @@ is
          and then (if High >= Low
                    then Low - 1
                      <= Natural'Last - By'Length
-                      - Natural'Max (Length (Source) - High, 0)
+                      - Integer'Max (Length (Source) - High, 0)
                    else Length (Source) <= Natural'Last - By'Length),
      Contract_Cases =>
+
+        --  If High >= Low, when considering the application of To_String to
+        --  convert an Unbounded_String into String, then the returned string
+        --  comprises Source (Source'First .. Low - 1) & By
+        --  & Source(High + 1 .. Source'Last).
+
        (High >= Low =>
+
+          --  Length of the returned string
+
           Length (Replace_Slice'Result)
-        = Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0),
+          = Low - 1 + By'Length + Integer'Max (Length (Source) - High, 0)
+
+            --  Elements starting at Low are replaced by elements of By
+
+            and then
+              Slice (Replace_Slice'Result, 1, Low - 1) =
+                Slice (Source, 1, Low - 1)
+            and then
+              Slice (Replace_Slice'Result, Low, Low - 1 + By'Length) = By
+
+            --  When there are remaining characters after the replaced slice,
+            --  they are appended to the result.
+
+            and then
+              (if High < Length (Source)
+               then
+                 Slice (Replace_Slice'Result,
+                   Low + By'Length, Length (Replace_Slice'Result)) =
+                     Slice (Source, High + 1, Length (Source))),
+
+        --  If High < Low, then the returned string is
+        --  Insert (Source, Before => Low, New_Item => By).
+
         others      =>
-          Length (Replace_Slice'Result) = Length (Source)'Old + By'Length),
+
+          --  Length of the returned string
+
+          Length (Replace_Slice'Result) = Length (Source) + By'Length
+
+            --  Elements of By are inserted after the element at Low
+
+            and then
+              Slice (Replace_Slice'Result, 1, Low - 1) =
+                Slice (Source, 1, Low - 1)
+            and then
+              Slice (Replace_Slice'Result, Low, Low - 1 + By'Length) = By
+
+            --  When there are remaining characters after Low in Source, they
+            --  are appended to the result.
+
+            and then
+              (if Low < Length (Source)
+               then
+                Slice (Replace_Slice'Result,
+                  Low + By'Length, Length (Replace_Slice'Result)) =
+                    Slice (Source, Low, Length (Source)))),
      Global         => null;
+   --  If Low > Source'Last + 1, or High < Source'First - 1, then Index_Error
+   --  is propagated. Otherwise:
+   --
+   --  * If High >= Low, then the returned string comprises
+   --    Source (Source'First .. Low - 1)
+   --    & By & Source(High + 1 .. Source'Last), but with lower bound 1.
+   --
+   --  * If High < Low, then the returned string is
+   --    Insert (Source, Before => Low, New_Item => By).
 
    procedure Replace_Slice
      (Source : in out Unbounded_String;
@@ -559,11 +1106,61 @@ is
                       - Natural'Max (Length (Source) - High, 0)
                    else Length (Source) <= Natural'Last - By'Length),
      Contract_Cases =>
+
+        --  If High >= Low, when considering the application of To_String to
+        --  convert an Unbounded_String into String, then the returned string
+        --  comprises Source (Source'First .. Low - 1) & By
+        --  & Source(High + 1 .. Source'Last).
+
        (High >= Low =>
+
+          --  Length of the returned string
+
           Length (Source)
-        = Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0),
+          = Low - 1 + By'Length + Integer'Max (Length (Source)'Old - High, 0)
+
+            --  Elements starting at Low are replaced by elements of By
+
+            and then Slice (Source, 1, Low - 1) =
+              Slice (Source, 1, Low - 1)'Old
+            and then Slice (Source, Low, Low - 1 + By'Length) = By
+
+            --  When there are remaining characters after the replaced slice,
+            --  they are appended to the result.
+
+            and then
+              (if High < Length (Source)'Old
+               then Slice (Source, Low + By'Length, Length (Source)) =
+                 Slice (Source,
+                   --  Really "High + 1" but expressed with a conditional
+                   --  repeating the above test so that the call to Slice
+                   --  is valid on entry (under 'Old) even when the test
+                   --  evaluates to False.
+                   (if High < Length (Source) then High + 1 else 1),
+                   Length (Source))'Old),
+
+        --  If High < Low, then the returned string is
+        --  Insert (Source, Before => Low, New_Item => By).
+
         others      =>
-          Length (Source) = Length (Source)'Old + By'Length),
+
+          --  Length of the returned string
+
+          Length (Source) = Length (Source)'Old + By'Length
+
+            --  Elements of By are inserted after the element at Low
+
+            and then Slice (Source, 1, Low - 1) =
+              Slice (Source, 1, Low - 1)'Old
+            and then Slice (Source, Low, Low - 1 + By'Length) = By
+
+            --  When there are remaining characters after Low in Source, they
+            --  are appended to the result.
+
+            and then
+              (if Low < Length (Source)'Old
+               then Slice (Source, Low + By'Length, Length (Source)) =
+                 Slice (Source, Low, Length (Source))'Old)),
      Global         => null;
 
    function Insert
@@ -573,8 +1170,32 @@ is
    with
      Pre    => Before - 1 <= Length (Source)
                  and then New_Item'Length <= Natural'Last - Length (Source),
-     Post   => Length (Insert'Result) = Length (Source) + New_Item'Length,
+     Post   =>
+       --  Length of the returned string
+
+       Length (Insert'Result) = Length (Source) + New_Item'Length
+
+         --  Elements of New_Item are inserted after element at Before
+
+         and then
+           Slice (Insert'Result, 1, Before - 1) = Slice (Source, 1, Before - 1)
+         and then
+           Slice (Insert'Result, Before, Before - 1 + New_Item'Length)
+           = New_Item
+
+         --  When there are remaining characters after Before in Source, they
+         --  are appended to the returned string.
+
+         and then
+           (if Before <= Length (Source) then
+              Slice (Insert'Result, Before + New_Item'Length,
+                Length (Insert'Result)) =
+                  Slice (Source, Before, Length (Source))),
      Global => null;
+   --  Propagates Index_Error if Before is not in
+   --  Source'First .. Source'Last + 1; otherwise, returns
+   --  Source (Source'First .. Before - 1)
+   --  & New_Item & Source(Before..Source'Last), but with lower bound 1.
 
    procedure Insert
      (Source   : in out Unbounded_String;
@@ -583,7 +1204,25 @@ is
    with
      Pre    => Before - 1 <= Length (Source)
                  and then New_Item'Length <= Natural'Last - Length (Source),
-     Post   => Length (Source) = Length (Source)'Old + New_Item'Length,
+     Post   =>
+       --  Length of the returned string
+
+       Length (Source) = Length (Source)'Old + New_Item'Length
+
+         --  Elements of New_Item are inserted after element at Before
+
+         and then
+           Slice (Source, 1, Before - 1) = Slice (Source, 1, Before - 1)'Old
+         and then
+           Slice (Source, Before, Before - 1 + New_Item'Length) = New_Item
+
+         --  When there are remaining characters after Before in Source, they
+         --  are appended to the returned string.
+
+         and then
+           (if Before <= Length (Source)'Old then
+              Slice (Source, Before + New_Item'Length, Length (Source)) =
+                Slice (Source, Before, Length (Source))'Old),
      Global => null;
 
    function Overwrite
@@ -592,12 +1231,31 @@ is
       New_Item : String) return Unbounded_String
    with
      Pre    => Position - 1 <= Length (Source)
-                 and then (if New_Item'Length /= 0
-                           then
-                             New_Item'Length <= Natural'Last - (Position - 1)),
+                 and then New_Item'Length <= Natural'Last - (Position - 1),
      Post   =>
-       Length (Overwrite'Result)
-     = Natural'Max (Length (Source), Position - 1 + New_Item'Length),
+       --  Length of the returned string
+
+       Length (Overwrite'Result) =
+         Integer'Max (Length (Source), Position - 1 + New_Item'Length)
+
+         --  Elements after Position are replaced by elements of New_Item
+
+         and then
+           Slice (Overwrite'Result, 1, Position - 1) =
+             Slice (Source, 1, Position - 1)
+         and then
+           Slice (Overwrite'Result, Position, Position - 1 + New_Item'Length) =
+             New_Item
+         and then
+           (if Position - 1 + New_Item'Length < Length (Source) then
+
+              --  There are some unchanged characters of Source remaining
+              --  after New_Item.
+
+              Slice (Overwrite'Result,
+                Position + New_Item'Length, Length (Source)) =
+                  Slice (Source,
+                    Position + New_Item'Length, Length (Source))),
      Global => null;
 
    procedure Overwrite
@@ -606,13 +1264,36 @@ is
       New_Item : String)
    with
      Pre    => Position - 1 <= Length (Source)
-                 and then (if New_Item'Length /= 0
-                           then
-                             New_Item'Length <= Natural'Last - (Position - 1)),
+                 and then New_Item'Length <= Natural'Last - (Position - 1),
      Post   =>
-       Length (Source)
-     = Natural'Max (Length (Source)'Old, Position - 1 + New_Item'Length),
+       --  Length of the returned string
+
+       Length (Source) =
+         Integer'Max (Length (Source)'Old, Position - 1 + New_Item'Length)
+
+         --  Elements after Position are replaced by elements of New_Item
+
+         and then
+           Slice (Source, 1, Position - 1) = Slice (Source, 1, Position - 1)
+         and then
+           Slice (Source, Position, Position - 1 + New_Item'Length) = New_Item
+         and then
+           (if Position - 1 + New_Item'Length < Length (Source)'Old then
+
+              --  There are some unchanged characters of Source remaining
+              --  after New_Item.
 
+              Slice (Source,
+                Position + New_Item'Length, Length (Source)'Old) =
+                  Slice (Source,
+                    --  Really "Position + New_Item'Length" but expressed with
+                    --  a conditional repeating the above test so that the
+                    --  call to Slice is valid on entry (under 'Old) even
+                    --  when the test evaluates to False.
+                    (if Position - 1 + New_Item'Length < Length (Source)
+                     then Position + New_Item'Length
+                     else 1),
+                    Length (Source))'Old),
      Global => null;
 
    function Delete
@@ -620,12 +1301,19 @@ is
       From    : Positive;
       Through : Natural) return Unbounded_String
    with
-     Pre            => (if Through <= From then From - 1 <= Length (Source)),
+     Pre            => (if Through >= From then From - 1 <= Length (Source)),
      Contract_Cases =>
        (Through >= From =>
-          Length (Delete'Result) = Length (Source) - (Through - From + 1),
+          Length (Delete'Result) =
+            From - 1 + Natural'Max (Length (Source) - Through, 0)
+            and then
+              Slice (Delete'Result, 1, From - 1) = Slice (Source, 1, From - 1)
+            and then
+              (if Through < Length (Source) then
+                 Slice (Delete'Result, From, Length (Delete'Result)) =
+                   Slice (Source, Through + 1, Length (Source))),
         others          =>
-          Length (Delete'Result) = Length (Source)),
+             Delete'Result = Source),
      Global         => null;
 
    procedure Delete
@@ -633,82 +1321,255 @@ is
       From    : Positive;
       Through : Natural)
    with
-     Pre            => (if Through <= From then From - 1 <= Length (Source)),
+     Pre            => (if Through >= From then From - 1 <= Length (Source)),
      Contract_Cases =>
        (Through >= From =>
-          Length (Source) = Length (Source)'Old - (Through - From + 1),
+          Length (Source) =
+            From - 1 + Natural'Max (Length (Source)'Old - Through, 0)
+            and then
+              Slice (Source, 1, From - 1) =
+                To_String (Source)'Old (1 .. From - 1)
+            and then
+              (if Through < Length (Source) then
+                Slice (Source, From, Length (Source)) =
+                  To_String (Source)'Old (Through + 1 .. Length (Source)'Old)),
         others          =>
-          Length (Source) = Length (Source)'Old),
+          To_String (Source) = To_String (Source)'Old),
      Global         => null;
 
    function Trim
      (Source : Unbounded_String;
       Side   : Trim_End) return Unbounded_String
    with
-     Post   => Length (Trim'Result) <= Length (Source),
-     Global => null;
+     Contract_Cases =>
+       --  If all characters in Source are Space, the returned string is
+       --  empty.
+
+       ((for all C of To_String (Source) => C = ' ')
+        =>
+          Length (Trim'Result) = 0,
+
+        --  Otherwise, the returned string is a slice of Source
+
+        others
+        =>
+          (declare
+             Low  : constant Positive :=
+               (if Side = Right then 1
+                else Index_Non_Blank (Source, Forward));
+             High : constant Positive :=
+               (if Side = Left then Length (Source)
+                else Index_Non_Blank (Source, Backward));
+           begin
+             To_String (Trim'Result) = Slice (Source, Low, High))),
+     Global         => null;
 
    procedure Trim
      (Source : in out Unbounded_String;
       Side   : Trim_End)
    with
-     Post   => Length (Source) <= Length (Source)'Old,
-     Global => null;
+     Contract_Cases =>
+       --  If all characters in Source are Space, the returned string is
+       --  empty.
+
+       ((for all C of To_String (Source) => C = ' ')
+        =>
+          Length (Source) = 0,
+
+        --  Otherwise, the returned string is a slice of Source
+
+        others
+        =>
+          (declare
+             Low  : constant Positive :=
+               (if Side = Right then 1
+                else Index_Non_Blank (Source, Forward)'Old);
+             High : constant Positive :=
+               (if Side = Left then Length (Source)'Old
+                else Index_Non_Blank (Source, Backward)'Old);
+           begin
+             To_String (Source) = To_String (Source)'Old (Low .. High))),
+     Global         => null;
 
    function Trim
      (Source : Unbounded_String;
       Left   : Maps.Character_Set;
       Right  : Maps.Character_Set) return Unbounded_String
    with
-     Post   => Length (Trim'Result) <= Length (Source),
-     Global => null;
+     Contract_Cases =>
+       --  If all characters in Source are contained in one of the sets Left
+       --  or Right, then the returned string is empty.
+
+       ((for all C of To_String (Source) => Maps.Is_In (C, Left))
+          or else
+            (for all C of To_String (Source) => Maps.Is_In (C, Right))
+        =>
+          Length (Trim'Result) = 0,
+
+        --  Otherwise, the returned string is a slice of Source
+
+        others
+        =>
+          (declare
+             Low  : constant Positive :=
+               Index (Source, Left, Outside, Forward);
+             High : constant Positive :=
+               Index (Source, Right, Outside, Backward);
+           begin
+             To_String (Trim'Result) = Slice (Source, Low, High))),
+     Global         => null;
 
    procedure Trim
      (Source : in out Unbounded_String;
       Left   : Maps.Character_Set;
       Right  : Maps.Character_Set)
    with
-     Post   => Length (Source) <= Length (Source)'Old,
-     Global => null;
+     Contract_Cases =>
+       --  If all characters in Source are contained in one of the sets Left
+       --  or Right, then the returned string is empty.
+
+       ((for all C of To_String (Source) => Maps.Is_In (C, Left))
+          or else
+            (for all C of To_String (Source) => Maps.Is_In (C, Right))
+        =>
+          Length (Source) = 0,
+
+        --  Otherwise, the returned string is a slice of Source
+
+        others
+        =>
+          (declare
+             Low  : constant Positive :=
+               Index (Source, Left, Outside, Forward)'Old;
+             High : constant Positive :=
+               Index (Source, Right, Outside, Backward)'Old;
+           begin
+             To_String (Source) = To_String (Source)'Old (Low .. High))),
+     Global         => null;
 
    function Head
      (Source : Unbounded_String;
       Count  : Natural;
       Pad    : Character := Space) return Unbounded_String
    with
-     Post   => Length (Head'Result) = Count,
-     Global => null;
+     Post           => Length (Head'Result) = Count,
+     Contract_Cases =>
+       (Count <= Length (Source)
+        =>
+          --  Source is cut
+
+          To_String (Head'Result) = Slice (Source, 1, Count),
+
+        others
+        =>
+          --  Source is followed by Pad characters
+
+          Slice (Head'Result, 1, Length (Source)) = To_String (Source)
+            and then
+              Slice (Head'Result, Length (Source) + 1, Count) =
+                [1 .. Count - Length (Source) => Pad]),
+     Global         => null;
 
    procedure Head
      (Source : in out Unbounded_String;
       Count  : Natural;
       Pad    : Character := Space)
    with
-     Post   => Length (Source) = Count,
-     Global => null;
+     Post           => Length (Source) = Count,
+     Contract_Cases =>
+       (Count <= Length (Source)
+        =>
+          --  Source is cut
+
+          To_String (Source) = Slice (Source, 1, Count),
+
+        others
+        =>
+          --  Source is followed by Pad characters
+
+          Slice (Source, 1, Length (Source)'Old) = To_String (Source)'Old
+            and then
+              Slice (Source, Length (Source)'Old + 1, Count) =
+                [1 .. Count - Length (Source)'Old => Pad]),
+     Global         => null;
 
    function Tail
      (Source : Unbounded_String;
       Count  : Natural;
       Pad    : Character := Space) return Unbounded_String
    with
-     Post   => Length (Tail'Result) = Count,
-     Global => null;
+     Post           => Length (Tail'Result) = Count,
+     Contract_Cases =>
+       (Count = 0
+        =>
+          True,
+
+        (Count in 1 .. Length (Source))
+        =>
+          --  Source is cut
+
+          To_String (Tail'Result) =
+            Slice (Source, Length (Source) - Count + 1, Length (Source)),
+
+        others
+        =>
+          --  Source is preceded by Pad characters
+
+          (if Length (Source) = 0 then
+            To_String (Tail'Result) = [1 .. Count => Pad]
+          else
+            Slice (Tail'Result, 1, Count - Length (Source)) =
+              [1 .. Count - Length (Source) => Pad]
+              and then
+                Slice (Tail'Result, Count - Length (Source) + 1, Count) =
+                  To_String (Source))),
+     Global         => null;
 
    procedure Tail
      (Source : in out Unbounded_String;
       Count  : Natural;
       Pad    : Character := Space)
    with
-     Post   => Length (Source) = Count,
-     Global => null;
+     Post           => Length (Source) = Count,
+     Contract_Cases =>
+       (Count = 0
+        =>
+          True,
+
+        (Count in  1 .. Length (Source))
+        =>
+          --  Source is cut
+
+          To_String (Source) =
+            Slice (Source,
+              --  Really "Length (Source) - Count + 1" but expressed with a
+              --  conditional repeating the above guard so that the call to
+              --  Slice is valid on entry (under 'Old) even when the test
+              --  evaluates to False.
+              (if Count <= Length (Source) then Length (Source) - Count + 1
+               else 1),
+              Length (Source))'Old,
+
+        others
+        =>
+          --  Source is preceded by Pad characters
+
+          (if Length (Source)'Old = 0 then
+            To_String (Source) = [1 .. Count => Pad]
+          else
+            Slice (Source, 1, Count - Length (Source)'Old) =
+              [1 .. Count - Length (Source)'Old => Pad]
+              and then
+                Slice (Source, Count - Length (Source)'Old + 1, Count) =
+                  To_String (Source)'Old)),
+     Global         => null;
 
    function "*"
      (Left  : Natural;
       Right : Character) return Unbounded_String
    with
      Pre    => Left <= Natural'Last,
-     Post   => Length ("*"'Result) = Left,
+     Post   => To_String ("*"'Result) = [1 .. Left => Right],
      Global => null;
 
    function "*"
@@ -716,7 +1577,13 @@ is
       Right : String) return Unbounded_String
    with
      Pre    => (if Left /= 0 then Right'Length <= Natural'Last / Left),
-     Post   => Length ("*"'Result) = Left * Right'Length,
+     Post =>
+       Length ("*"'Result) = Left * Right'Length
+         and then
+           (if Right'Length > 0 then
+              (for all K in 1 .. Left * Right'Length =>
+                 Element ("*"'Result, K) =
+                   Right (Right'First + (K - 1) mod Right'Length))),
      Global => null;
 
    function "*"
@@ -724,7 +1591,13 @@ is
       Right : Unbounded_String) return Unbounded_String
    with
      Pre    => (if Left /= 0 then Length (Right) <= Natural'Last / Left),
-     Post   => Length ("*"'Result) = Left * Length (Right),
+     Post =>
+       Length ("*"'Result) = Left * Length (Right)
+         and then
+           (if Length (Right) > 0 then
+              (for all K in 1 .. Left * Length (Right) =>
+                 Element ("*"'Result, K) =
+                   Element (Right, 1 + (K - 1) mod Length (Right)))),
      Global => null;
 
    --  Each of the transformation functions (Replace_Slice, Insert, Overwrite,
diff --git a/gcc/ada/libgnat/a-strunb__shared.adb b/gcc/ada/libgnat/a-strunb__shared.adb
index ecc0e4af117..ef4f8c93bdb 100644
--- a/gcc/ada/libgnat/a-strunb__shared.adb
+++ b/gcc/ada/libgnat/a-strunb__shared.adb
@@ -29,7 +29,6 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
-with Ada.Strings.Search;
 with Ada.Unchecked_Deallocation;
 
 package body Ada.Strings.Unbounded is
@@ -58,7 +57,7 @@ package body Ada.Strings.Unbounded is
    --  Calculation takes into account alignment of the allocated memory
    --  segments to use memory effectively by Append/Insert/etc operations.
 
-   function Sum (Left : Natural; Right : Integer) return Natural with Inline;
+   function Sum (Left, Right : Natural) return Natural with Inline;
    --  Returns summary of Left and Right, raise Constraint_Error on overflow
 
    function Mul (Left, Right : Natural) return Natural with Inline;
@@ -165,7 +164,11 @@ package body Ada.Strings.Unbounded is
       else
          DR := Allocate (DL);
          DR.Data (1 .. Left'Length) := Left;
-         DR.Data (Left'Length + 1 .. DL) := RR.Data (1 .. RR.Last);
+
+         if Left'Length < Natural'Last then
+            DR.Data (Left'Length + 1 .. DL) := RR.Data (1 .. RR.Last);
+         end if;
+
          DR.Last := DL;
       end if;
 
@@ -243,7 +246,7 @@ package body Ada.Strings.Unbounded is
    is
       DL : constant Natural := Mul (Left, Right'Length);
       DR : Shared_String_Access;
-      K  : Positive;
+      K  : Natural;
 
    begin
       --  Result is an empty string, reuse shared empty string
@@ -255,10 +258,10 @@ package body Ada.Strings.Unbounded is
 
       else
          DR := Allocate (DL);
-         K := 1;
+         K := 0;
 
          for J in 1 .. Left loop
-            DR.Data (K .. K + Right'Length - 1) := Right;
+            DR.Data (K + 1 .. K + Right'Length) := Right;
             K := K + Right'Length;
          end loop;
 
@@ -275,7 +278,7 @@ package body Ada.Strings.Unbounded is
       RR : constant Shared_String_Access := Right.Reference;
       DL : constant Natural := Mul (Left, RR.Last);
       DR : Shared_String_Access;
-      K  : Positive;
+      K  : Natural;
 
    begin
       --  Result is an empty string, reuse shared empty string
@@ -293,10 +296,10 @@ package body Ada.Strings.Unbounded is
 
       else
          DR := Allocate (DL);
-         K := 1;
+         K := 0;
 
          for J in 1 .. Left loop
-            DR.Data (K .. K + RR.Last - 1) := RR.Data (1 .. RR.Last);
+            DR.Data (K + 1 .. K + RR.Last) := RR.Data (1 .. RR.Last);
             K := K + RR.Last;
          end loop;
 
@@ -703,15 +706,15 @@ package body Ada.Strings.Unbounded is
          Reference (SR);
          DR := SR;
 
-      --  Index is out of range
+      --  From is too large
 
-      elsif Through > SR.Last then
+      elsif From - 1 > SR.Last then
          raise Index_Error;
 
       --  Compute size of the result
 
       else
-         DL := SR.Last - (Through - From + 1);
+         DL := SR.Last - (Natural'Min (SR.Last, Through) - From + 1);
 
          --  Result is an empty string, reuse shared empty string
 
@@ -723,7 +726,11 @@ package body Ada.Strings.Unbounded is
          else
             DR := Allocate (DL);
             DR.Data (1 .. From - 1) := SR.Data (1 .. From - 1);
-            DR.Data (From .. DL) := SR.Data (Through + 1 .. SR.Last);
+
+            if Through < Natural'Last then
+               DR.Data (From .. DL) := SR.Data (Through + 1 .. SR.Last);
+            end if;
+
             DR.Last := DL;
          end if;
       end if;
@@ -746,13 +753,13 @@ package body Ada.Strings.Unbounded is
       if From > Through then
          null;
 
-      --  Through is outside of the range
+      --  From is too large
 
-      elsif Through > SR.Last then
+      elsif From - 1 > SR.Last then
          raise Index_Error;
 
       else
-         DL := SR.Last - (Through - From + 1);
+         DL := SR.Last - (Natural'Min (SR.Last, Through) - From + 1);
 
          --  Result is empty, reuse shared empty string
 
@@ -763,7 +770,10 @@ package body Ada.Strings.Unbounded is
          --  Try to reuse existing shared string
 
          elsif Can_Be_Reused (SR, DL) then
-            SR.Data (From .. DL) := SR.Data (Through + 1 .. SR.Last);
+            if Through < Natural'Last then
+               SR.Data (From .. DL) := SR.Data (Through + 1 .. SR.Last);
+            end if;
+
             SR.Last := DL;
 
          --  Otherwise, allocate new shared string
@@ -771,7 +781,11 @@ package body Ada.Strings.Unbounded is
          else
             DR := Allocate (DL);
             DR.Data (1 .. From - 1) := SR.Data (1 .. From - 1);
-            DR.Data (From .. DL) := SR.Data (Through + 1 .. SR.Last);
+
+            if Through < Natural'Last then
+               DR.Data (From .. DL) := SR.Data (Through + 1 .. SR.Last);
+            end if;
+
             DR.Last := DL;
             Source.Reference := DR;
             Unreference (SR);
@@ -1093,7 +1107,7 @@ package body Ada.Strings.Unbounded is
    begin
       --  Check index first
 
-      if Before > SR.Last + 1 then
+      if Before - 1 > SR.Last then
          raise Index_Error;
       end if;
 
@@ -1113,9 +1127,13 @@ package body Ada.Strings.Unbounded is
       else
          DR := Allocate (DL, DL / Growth_Factor);
          DR.Data (1 .. Before - 1) := SR.Data (1 .. Before - 1);
-         DR.Data (Before .. Before + New_Item'Length - 1) := New_Item;
-         DR.Data (Before + New_Item'Length .. DL) :=
-           SR.Data (Before .. SR.Last);
+         DR.Data (Before .. Before - 1 + New_Item'Length) := New_Item;
+
+         if Before <= SR.Last then
+            DR.Data (Before + New_Item'Length .. DL) :=
+              SR.Data (Before .. SR.Last);
+         end if;
+
          DR.Last := DL;
       end if;
 
@@ -1134,7 +1152,7 @@ package body Ada.Strings.Unbounded is
    begin
       --  Check bounds
 
-      if Before > SR.Last + 1 then
+      if Before - 1 > SR.Last then
          raise Index_Error;
       end if;
 
@@ -1152,9 +1170,12 @@ package body Ada.Strings.Unbounded is
       --  Try to reuse existing shared string first
 
       elsif Can_Be_Reused (SR, DL) then
-         SR.Data (Before + New_Item'Length .. DL) :=
-           SR.Data (Before .. SR.Last);
-         SR.Data (Before .. Before + New_Item'Length - 1) := New_Item;
+         if Before <= SR.Last then
+            SR.Data (Before + New_Item'Length .. DL) :=
+              SR.Data (Before .. SR.Last);
+         end if;
+
+         SR.Data (Before .. Before - 1 + New_Item'Length) := New_Item;
          SR.Last := DL;
 
       --  Otherwise, allocate new shared string and fill it
@@ -1162,9 +1183,13 @@ package body Ada.Strings.Unbounded is
       else
          DR := Allocate (DL, DL / Growth_Factor);
          DR.Data (1 .. Before - 1) := SR.Data (1 .. Before - 1);
-         DR.Data (Before .. Before + New_Item'Length - 1) := New_Item;
-         DR.Data (Before + New_Item'Length .. DL) :=
-           SR.Data (Before .. SR.Last);
+         DR.Data (Before .. Before - 1 + New_Item'Length) := New_Item;
+
+         if Before <= SR.Last then
+            DR.Data (Before + New_Item'Length .. DL) :=
+              SR.Data (Before .. SR.Last);
+         end if;
+
          DR.Last := DL;
          Source.Reference := DR;
          Unreference (SR);
@@ -1206,7 +1231,7 @@ package body Ada.Strings.Unbounded is
    begin
       --  Check bounds
 
-      if Position > SR.Last + 1 then
+      if Position - 1 > SR.Last then
          raise Index_Error;
       end if;
 
@@ -1228,9 +1253,13 @@ package body Ada.Strings.Unbounded is
       else
          DR := Allocate (DL);
          DR.Data (1 .. Position - 1) := SR.Data (1 .. Position - 1);
-         DR.Data (Position .. Position + New_Item'Length - 1) := New_Item;
-         DR.Data (Position + New_Item'Length .. DL) :=
-           SR.Data (Position + New_Item'Length .. SR.Last);
+         DR.Data (Position .. Position - 1 + New_Item'Length) := New_Item;
+
+         if Position <= SR.Last - New_Item'Length then
+            DR.Data (Position + New_Item'Length .. DL) :=
+              SR.Data (Position + New_Item'Length .. SR.Last);
+         end if;
+
          DR.Last := DL;
       end if;
 
@@ -1249,11 +1278,11 @@ package body Ada.Strings.Unbounded is
    begin
       --  Bounds check
 
-      if Position > SR.Last + 1 then
+      if Position - 1 > SR.Last then
          raise Index_Error;
       end if;
 
-      DL := Integer'Max (SR.Last, Position + New_Item'Length - 1);
+      DL := Integer'Max (SR.Last, Sum (Position - 1, New_Item'Length));
 
       --  Result is empty string, reuse empty shared string
 
@@ -1269,7 +1298,7 @@ package body Ada.Strings.Unbounded is
       --  Try to reuse existing shared string
 
       elsif Can_Be_Reused (SR, DL) then
-         SR.Data (Position .. Position + New_Item'Length - 1) := New_Item;
+         SR.Data (Position .. Position - 1 + New_Item'Length) := New_Item;
          SR.Last := DL;
 
       --  Otherwise allocate new shared string and fill it
@@ -1277,9 +1306,13 @@ package body Ada.Strings.Unbounded is
       else
          DR := Allocate (DL);
          DR.Data (1 .. Position - 1) := SR.Data (1 .. Position - 1);
-         DR.Data (Position .. Position + New_Item'Length - 1) := New_Item;
-         DR.Data (Position + New_Item'Length .. DL) :=
-           SR.Data (Position + New_Item'Length .. SR.Last);
+         DR.Data (Position .. Position - 1 + New_Item'Length) := New_Item;
+
+         if Position <= SR.Last - New_Item'Length then
+            DR.Data (Position + New_Item'Length .. DL) :=
+              SR.Data (Position + New_Item'Length .. SR.Last);
+         end if;
+
          DR.Last := DL;
          Source.Reference := DR;
          Unreference (SR);
@@ -1365,15 +1398,14 @@ package body Ada.Strings.Unbounded is
    begin
       --  Check bounds
 
-      if Low > SR.Last + 1 then
+      if Low - 1 > SR.Last then
          raise Index_Error;
       end if;
 
       --  Do replace operation when removed slice is not empty
 
       if High >= Low then
-         DL := Sum (SR.Last,
-                    By'Length + Low - Integer'Min (High, SR.Last) - 1);
+         DL := Sum (Low - 1 + Integer'Max (SR.Last - High, 0), By'Length);
          --  This is the number of characters remaining in the string after
          --  replacing the slice.
 
@@ -1387,8 +1419,13 @@ package body Ada.Strings.Unbounded is
          else
             DR := Allocate (DL);
             DR.Data (1 .. Low - 1) := SR.Data (1 .. Low - 1);
-            DR.Data (Low .. Low + By'Length - 1) := By;
-            DR.Data (Low + By'Length .. DL) := SR.Data (High + 1 .. SR.Last);
+            DR.Data (Low .. Low - 1 + By'Length) := By;
+
+            if High < SR.Last then
+               DR.Data (Low + By'Length .. DL) :=
+                 SR.Data (High + 1 .. SR.Last);
+            end if;
+
             DR.Last := DL;
          end if;
 
@@ -1414,14 +1451,14 @@ package body Ada.Strings.Unbounded is
    begin
       --  Bounds check
 
-      if Low > SR.Last + 1 then
+      if Low - 1 > SR.Last then
          raise Index_Error;
       end if;
 
       --  Do replace operation only when replaced slice is not empty
 
       if High >= Low then
-         DL := By'Length + SR.Last + Low - Integer'Min (High, SR.Last) - 1;
+         DL := Sum (Low - 1 + Integer'Max (SR.Last - High, 0), By'Length);
          --  This is the number of characters remaining in the string after
          --  replacing the slice.
 
@@ -1434,8 +1471,12 @@ package body Ada.Strings.Unbounded is
          --  Try to reuse existing shared string
 
          elsif Can_Be_Reused (SR, DL) then
-            SR.Data (Low + By'Length .. DL) := SR.Data (High + 1 .. SR.Last);
-            SR.Data (Low .. Low + By'Length - 1) := By;
+            if High < SR.Last then
+               SR.Data (Low + By'Length .. DL) :=
+                 SR.Data (High + 1 .. SR.Last);
+            end if;
+
+            SR.Data (Low .. Low - 1 + By'Length) := By;
             SR.Last := DL;
 
          --  Otherwise allocate new shared string and fill it
@@ -1443,8 +1484,13 @@ package body Ada.Strings.Unbounded is
          else
             DR := Allocate (DL);
             DR.Data (1 .. Low - 1) := SR.Data (1 .. Low - 1);
-            DR.Data (Low .. Low + By'Length - 1) := By;
-            DR.Data (Low + By'Length .. DL) := SR.Data (High + 1 .. SR.Last);
+            DR.Data (Low .. Low - 1 + By'Length) := By;
+
+            if High < SR.Last then
+               DR.Data (Low + By'Length .. DL) :=
+                 SR.Data (High + 1 .. SR.Last);
+            end if;
+
             DR.Last := DL;
             Source.Reference := DR;
             Unreference (SR);
@@ -1509,7 +1555,7 @@ package body Ada.Strings.Unbounded is
    begin
       --  Note: test of High > Length is in accordance with AI95-00128
 
-      if Low > SR.Last + 1 or else High > SR.Last then
+      if Low - 1 > SR.Last or else High > SR.Last then
          raise Index_Error;
 
       else
@@ -1521,7 +1567,7 @@ package body Ada.Strings.Unbounded is
    -- Sum --
    ---------
 
-   function Sum (Left : Natural; Right : Integer) return Natural is
+   function Sum (Left, Right : Natural) return Natural is
       pragma Unsuppress (Overflow_Check);
    begin
       return Left + Right;
diff --git a/gcc/ada/libgnat/a-strunb__shared.ads b/gcc/ada/libgnat/a-strunb__shared.ads
index 3a0411de5de..fa97680a7fa 100644
--- a/gcc/ada/libgnat/a-strunb__shared.ads
+++ b/gcc/ada/libgnat/a-strunb__shared.ads
@@ -35,9 +35,14 @@
 
 --  Preconditions in this unit are meant for analysis only, not for run-time
 --  checking, so that the expected exceptions are raised. This is enforced by
---  setting the corresponding assertion policy to Ignore.
+--  setting the corresponding assertion policy to Ignore. Postconditions and
+--  contract cases should not be executed at runtime as well, in order not to
+--  slow down the execution of these functions.
 
-pragma Assertion_Policy (Pre => Ignore);
+pragma Assertion_Policy (Pre            => Ignore,
+                         Post           => Ignore,
+                         Contract_Cases => Ignore,
+                         Ghost          => Ignore);
 
 --  This package provides an implementation of Ada.Strings.Unbounded that uses
 --  reference counts to implement copy on modification (rather than copy on
@@ -77,17 +82,26 @@ pragma Assertion_Policy (Pre => Ignore);
    --  make objects of Unbounded_String thread-safe: an instance cannot be
    --  accessed by several tasks simultaneously.
 
-with Ada.Strings.Maps;
+with Ada.Strings.Maps; use type Ada.Strings.Maps.Character_Mapping_Function;
 private with Ada.Finalization;
 private with System.Atomic_Counters;
+with Ada.Strings.Search;
 private with Ada.Strings.Text_Buffers;
 
 package Ada.Strings.Unbounded with
+  SPARK_Mode,
   Initial_Condition => Length (Null_Unbounded_String) = 0,
   Always_Terminates
 is
    pragma Preelaborate;
 
+   --  Contracts may call function Length in the prefix of attribute reference
+   --  to Old as in Length (Source)'Old. Allow this use.
+
+   pragma Unevaluated_Use_Of_Old (Allow);
+
+   subtype String_1 is String (1 .. <>) with Ghost;  --  Type used in contracts
+
    type Unbounded_String is private with
      Default_Initial_Condition => Length (Unbounded_String) = 0;
    pragma Preelaborable_Initialization (Unbounded_String);
@@ -99,7 +113,7 @@ is
 
    type String_Access is access all String;
 
-   procedure Free (X : in out String_Access);
+   procedure Free (X : in out String_Access) with SPARK_Mode => Off;
 
    --------------------------------------------------------
    -- Conversion, Concatenation, and Selection Functions --
@@ -108,7 +122,8 @@ is
    function To_Unbounded_String
      (Source : String)  return Unbounded_String
    with
-     Post   => To_String (To_Unbounded_String'Result) = Source,
+     Post   => To_String (To_Unbounded_String'Result) = Source
+       and then Length (To_Unbounded_String'Result) = Source'Length,
      Global => null;
 
    function To_Unbounded_String
@@ -136,7 +151,8 @@ is
       New_Item : Unbounded_String)
    with
      Pre    => Length (New_Item) <= Natural'Last - Length (Source),
-     Post   => Length (Source) = Length (Source)'Old + Length (New_Item),
+     Post   =>
+       To_String (Source) = To_String (Source)'Old & To_String (New_Item),
      Global => null;
 
    procedure Append
@@ -144,7 +160,7 @@ is
       New_Item : String)
    with
      Pre    => New_Item'Length <= Natural'Last - Length (Source),
-     Post   => Length (Source) = Length (Source)'Old + New_Item'Length,
+     Post   => To_String (Source) = To_String (Source)'Old & New_Item,
      Global => null;
 
    procedure Append
@@ -152,7 +168,7 @@ is
       New_Item : Character)
    with
      Pre    => Length (Source) < Natural'Last,
-     Post   => Length (Source) = Length (Source)'Old + 1,
+     Post   => To_String (Source) = To_String (Source)'Old & New_Item,
      Global => null;
 
    function "&"
@@ -160,7 +176,7 @@ is
       Right : Unbounded_String) return Unbounded_String
    with
      Pre    => Length (Right) <= Natural'Last - Length (Left),
-     Post   => Length ("&"'Result) = Length (Left) + Length (Right),
+     Post   => To_String ("&"'Result) = To_String (Left) & To_String (Right),
      Global => null;
 
    function "&"
@@ -168,7 +184,7 @@ is
       Right : String) return Unbounded_String
    with
      Pre    => Right'Length <= Natural'Last - Length (Left),
-     Post   => Length ("&"'Result) = Length (Left) + Right'Length,
+     Post   => To_String ("&"'Result) = To_String (Left) & Right,
      Global => null;
 
    function "&"
@@ -176,7 +192,7 @@ is
       Right : Unbounded_String) return Unbounded_String
    with
      Pre    => Left'Length <= Natural'Last - Length (Right),
-     Post   => Length ("&"'Result) = Left'Length + Length (Right),
+     Post   => To_String ("&"'Result) = String_1 (Left) & To_String (Right),
      Global => null;
 
    function "&"
@@ -184,7 +200,7 @@ is
       Right : Character) return Unbounded_String
    with
      Pre    => Length (Left) < Natural'Last,
-     Post   => Length ("&"'Result) = Length (Left) + 1,
+     Post   => To_String ("&"'Result) = To_String (Left) & Right,
      Global => null;
 
    function "&"
@@ -192,7 +208,7 @@ is
       Right : Unbounded_String) return Unbounded_String
    with
      Pre    => Length (Right) < Natural'Last,
-     Post   => Length ("&"'Result) = Length (Right) + 1,
+     Post   => To_String ("&"'Result) = Left & To_String (Right),
      Global => null;
 
    function Element
@@ -209,7 +225,8 @@ is
       By     : Character)
    with
      Pre    => Index <= Length (Source),
-     Post   => Length (Source) = Length (Source)'Old,
+     Post   =>
+       To_String (Source) = (To_String (Source)'Old with delta Index => By),
      Global => null;
 
    function Slice
@@ -218,7 +235,9 @@ is
       High   : Natural) return String
    with
      Pre    => Low - 1 <= Length (Source) and then High <= Length (Source),
-     Post   => Slice'Result'Length = Natural'Max (0, High - Low + 1),
+     Post   => Slice'Result'First = Low
+       and then Slice'Result'Last = High
+       and then Slice'Result = To_String (Source) (Low .. High),
      Global => null;
 
    function Unbounded_Slice
@@ -228,7 +247,7 @@ is
    with
      Pre    => Low - 1 <= Length (Source) and then High <= Length (Source),
      Post   =>
-       Length (Unbounded_Slice'Result) = Natural'Max (0, High - Low + 1),
+       To_String (Unbounded_Slice'Result) = To_String (Source) (Low .. High),
      Global => null;
    pragma Ada_05 (Unbounded_Slice);
 
@@ -239,7 +258,7 @@ is
       High   : Natural)
    with
      Pre    => Low - 1 <= Length (Source) and then High <= Length (Source),
-     Post   => Length (Target) = Natural'Max (0, High - Low + 1),
+     Post   => To_String (Target) = To_String (Source) (Low .. High),
      Global => null;
    pragma Ada_05 (Unbounded_Slice);
 
@@ -268,72 +287,84 @@ is
      (Left  : Unbounded_String;
       Right : Unbounded_String) return Boolean
    with
+     Post   => "<"'Result = (To_String (Left) < To_String (Right)),
      Global => null;
 
    function "<"
      (Left  : Unbounded_String;
       Right : String) return Boolean
    with
+     Post   => "<"'Result = (To_String (Left) < Right),
      Global => null;
 
    function "<"
      (Left  : String;
       Right : Unbounded_String) return Boolean
    with
+     Post   => "<"'Result = (Left < To_String (Right)),
      Global => null;
 
    function "<="
      (Left  : Unbounded_String;
       Right : Unbounded_String) return Boolean
    with
+     Post   => "<="'Result = (To_String (Left) <= To_String (Right)),
      Global => null;
 
    function "<="
      (Left  : Unbounded_String;
       Right : String) return Boolean
    with
+     Post   => "<="'Result = (To_String (Left) <= Right),
      Global => null;
 
    function "<="
      (Left  : String;
       Right : Unbounded_String) return Boolean
    with
+     Post   => "<="'Result = (Left <= To_String (Right)),
      Global => null;
 
    function ">"
      (Left  : Unbounded_String;
       Right : Unbounded_String) return Boolean
    with
+     Post   => ">"'Result = (To_String (Left) > To_String (Right)),
      Global => null;
 
    function ">"
      (Left  : Unbounded_String;
       Right : String) return Boolean
    with
+     Post   => ">"'Result = (To_String (Left) > Right),
      Global => null;
 
    function ">"
      (Left  : String;
       Right : Unbounded_String) return Boolean
    with
+     Post   => ">"'Result = (Left > To_String (Right)),
      Global => null;
 
    function ">="
      (Left  : Unbounded_String;
       Right : Unbounded_String) return Boolean
    with
+     Post   => ">="'Result = (To_String (Left) >= To_String (Right)),
      Global => null;
 
    function ">="
      (Left  : Unbounded_String;
       Right : String) return Boolean
    with
+     Post   => ">="'Result = (To_String (Left) >= Right),
      Global => null;
 
    function ">="
      (Left  : String;
       Right : Unbounded_String) return Boolean
    with
+     Post   => ">="'Result = (Left >= To_String (Right)),
      Global => null;
 
    ------------------------
@@ -346,8 +377,52 @@ is
       Going   : Direction := Forward;
       Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
    with
-     Pre    => Pattern'Length /= 0,
-     Global => null;
+     Pre            => Pattern'Length > 0,
+     Post           => Index'Result <= Length (Source),
+     Contract_Cases =>
+
+       --  If Source is the empty string, then 0 is returned
+
+       (Length (Source) = 0
+        =>
+          Index'Result = 0,
+
+        --  If some slice of Source matches Pattern, then a valid index is
+        --  returned.
+
+        Length (Source) > 0
+          and then
+            (for some J in 1 .. Length (Source) - (Pattern'Length - 1) =>
+               Search.Match (To_String (Source), Pattern, Mapping, J))
+        =>
+          --  The result is in the considered range of Source
+
+          Index'Result in 1 .. Length (Source) - (Pattern'Length - 1)
+
+            --  The slice beginning at the returned index matches Pattern
+
+            and then Search.Match
+              (To_String (Source), Pattern, Mapping, Index'Result)
+
+            --  The result is the smallest or largest index which satisfies
+            --  the matching, respectively when Going = Forward and Going =
+            --  Backward.
+
+            and then
+              (for all J in 1 .. Length (Source) =>
+                 (if (if Going = Forward
+                      then J <= Index'Result - 1
+                      else J - 1 in Index'Result
+                                    .. Length (Source) - Pattern'Length)
+                  then not (Search.Match
+                    (To_String (Source), Pattern, Mapping, J)))),
+
+        --  Otherwise, 0 is returned
+
+        others
+        =>
+          Index'Result = 0),
+     Global         => null;
 
    function Index
      (Source  : Unbounded_String;
@@ -355,8 +430,52 @@ is
       Going   : Direction := Forward;
       Mapping : Maps.Character_Mapping_Function) return Natural
    with
-     Pre    => Pattern'Length /= 0,
-     Global => null;
+     Pre            => Pattern'Length /= 0 and then Mapping /= null,
+     Post           => Index'Result <= Length (Source),
+     Contract_Cases =>
+
+       --  If Source is the empty string, then 0 is returned
+
+       (Length (Source) = 0
+        =>
+          Index'Result = 0,
+
+        --  If some slice of Source matches Pattern, then a valid index is
+        --  returned.
+
+        Length (Source) > 0
+          and then
+            (for some J in 1 .. Length (Source) - (Pattern'Length - 1) =>
+               Search.Match (To_String (Source), Pattern, Mapping, J))
+        =>
+          --  The result is in the considered range of Source
+
+          Index'Result in 1 .. Length (Source) - (Pattern'Length - 1)
+
+            --  The slice beginning at the returned index matches Pattern
+
+            and then Search.Match
+              (To_String (Source), Pattern, Mapping, Index'Result)
+
+            --  The result is the smallest or largest index which satisfies
+            --  the matching, respectively when Going = Forward and Going =
+            --  Backward.
+
+            and then
+              (for all J in 1 .. Length (Source) =>
+                 (if (if Going = Forward
+                      then J <= Index'Result - 1
+                      else J - 1 in Index'Result
+                                    .. Length (Source) - Pattern'Length)
+                  then not (Search.Match
+                    (To_String (Source), Pattern, Mapping, J)))),
+
+        --  Otherwise, 0 is returned
+
+        others
+        =>
+          Index'Result = 0),
+     Global         => null;
 
    function Index
      (Source : Unbounded_String;
@@ -364,7 +483,43 @@ is
       Test   : Membership := Inside;
       Going  : Direction  := Forward) return Natural
    with
-     Global => null;
+     Post           => Index'Result <= Length (Source),
+     Contract_Cases =>
+
+        --  If no character of Source satisfies the property Test on Set,
+        --  then 0 is returned.
+
+       ((for all C of To_String (Source) =>
+           (Test = Inside) /= Maps.Is_In (C, Set))
+        =>
+          Index'Result = 0,
+
+        --  Otherwise, an index in the range of Source is returned
+
+        others
+        =>
+          --  The result is in the range of Source
+
+          Index'Result in 1 .. Length (Source)
+
+            --  The character at the returned index satisfies the property
+            --  Test on Set.
+
+            and then
+              (Test = Inside) =
+                Maps.Is_In (Element (Source, Index'Result), Set)
+
+            --  The result is the smallest or largest index which satisfies
+            --  the property, respectively when Going = Forward and Going =
+            --  Backward.
+
+            and then
+              (for all J in 1 .. Length (Source) =>
+                 (if J /= Index'Result
+                       and then (J < Index'Result) = (Going = Forward)
+                  then (Test = Inside)
+                       /= Maps.Is_In (Element (Source, J), Set)))),
+     Global         => null;
 
    function Index
      (Source  : Unbounded_String;
@@ -373,9 +528,60 @@ is
       Going   : Direction := Forward;
       Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
    with
-     Pre    => (if Length (Source) /= 0 then From <= Length (Source))
-               and then Pattern'Length /= 0,
-     Global => null;
+     Pre            =>
+       (if Length (Source) /= 0 then From <= Length (Source))
+         and then Pattern'Length /= 0,
+     Post           => Index'Result <= Length (Source),
+     Contract_Cases =>
+
+       --  If Source is the empty string, then 0 is returned
+
+       (Length (Source) = 0
+        =>
+          Index'Result = 0,
+
+        --  If some slice of Source matches Pattern, then a valid index is
+        --  returned.
+
+        Length (Source) > 0
+          and then
+            (for some J in
+              (if Going = Forward then From else 1)
+               .. (if Going = Forward then Length (Source) else From)
+                - (Pattern'Length - 1) =>
+              Search.Match (To_String (Source), Pattern, Mapping, J))
+        =>
+          --  The result is in the considered range of Source
+
+          Index'Result in
+            (if Going = Forward then From else 1)
+            .. (if Going = Forward then Length (Source) else From)
+             - (Pattern'Length - 1)
+
+            --  The slice beginning at the returned index matches Pattern
+
+            and then Search.Match
+              (To_String (Source), Pattern, Mapping, Index'Result)
+
+            --  The result is the smallest or largest index which satisfies
+            --  the matching, respectively when Going = Forward and Going =
+            --  Backward.
+
+            and then
+              (for all J in 1 .. Length (Source) =>
+                 (if (if Going = Forward
+                      then J in From .. Index'Result - 1
+                      else J - 1 in Index'Result
+                                    .. From - Pattern'Length)
+                  then not (Search.Match
+                    (To_String (Source), Pattern, Mapping, J)))),
+
+        --  Otherwise, 0 is returned
+
+        others
+        =>
+          Index'Result = 0),
+     Global         => null;
    pragma Ada_05 (Index);
 
    function Index
@@ -385,9 +591,61 @@ is
       Going   : Direction := Forward;
       Mapping : Maps.Character_Mapping_Function) return Natural
    with
-     Pre    => (if Length (Source) /= 0 then From <= Length (Source))
-               and then Pattern'Length /= 0,
-     Global => null;
+     Pre            =>
+       (if Length (Source) /= 0 then From <= Length (Source))
+         and then Pattern'Length /= 0
+         and then Mapping /= null,
+     Post           => Index'Result <= Length (Source),
+     Contract_Cases =>
+
+       --  If Source is the empty string, then 0 is returned
+
+       (Length (Source) = 0
+        =>
+          Index'Result = 0,
+
+        --  If some slice of Source matches Pattern, then a valid index is
+        --  returned.
+
+        Length (Source) > 0
+          and then
+            (for some J in
+              (if Going = Forward then From else 1)
+               .. (if Going = Forward then Length (Source) else From)
+                - (Pattern'Length - 1) =>
+              Search.Match (To_String (Source), Pattern, Mapping, J))
+        =>
+          --  The result is in the considered range of Source
+
+          Index'Result in
+            (if Going = Forward then From else 1)
+            .. (if Going = Forward then Length (Source) else From)
+             - (Pattern'Length - 1)
+
+            --  The slice beginning at the returned index matches Pattern
+
+            and then Search.Match
+              (To_String (Source), Pattern, Mapping, Index'Result)
+
+            --  The result is the smallest or largest index which satisfies
+            --  the matching, respectively when Going = Forward and Going =
+            --  Backward.
+
+            and then
+              (for all J in 1 .. Length (Source) =>
+                 (if (if Going = Forward
+                      then J in From .. Index'Result - 1
+                      else J - 1 in Index'Result
+                                    .. From - Pattern'Length)
+                  then not (Search.Match
+                    (To_String (Source), Pattern, Mapping, J)))),
+
+        --  Otherwise, 0 is returned
+
+        others
+        =>
+          Index'Result = 0),
+     Global         => null;
    pragma Ada_05 (Index);
 
    function Index
@@ -397,23 +655,147 @@ is
       Test    : Membership := Inside;
       Going   : Direction := Forward) return Natural
    with
-     Pre    => (if Length (Source) /= 0 then From <= Length (Source)),
-     Global => null;
+     Pre            =>
+       (if Length (Source) /= 0 then From <= Length (Source)),
+     Post           => Index'Result <= Length (Source),
+     Contract_Cases =>
+
+        --  If Source is the empty string, or no character of the considered
+        --  slice of Source satisfies the property Test on Set, then 0 is
+        --  returned.
+
+       (Length (Source) = 0
+          or else
+            (for all J in 1 .. Length (Source) =>
+               (if J = From or else (J > From) = (Going = Forward) then
+                  (Test = Inside) /= Maps.Is_In (Element (Source, J), Set)))
+        =>
+          Index'Result = 0,
+
+        --  Otherwise, an index in the considered range of Source is
+        --  returned.
+
+        others
+        =>
+          --  The result is in the considered range of Source
+
+          Index'Result in 1 .. Length (Source)
+            and then
+              (Index'Result = From
+                 or else (Index'Result > From) = (Going = Forward))
+
+            --  The character at the returned index satisfies the property
+            --  Test on Set.
+
+            and then
+              (Test = Inside) =
+                Maps.Is_In (Element (Source, Index'Result), Set)
+
+            --  The result is the smallest or largest index which satisfies
+            --  the property, respectively when Going = Forward and Going =
+            --  Backward.
+
+            and then
+              (for all J in 1 .. Length (Source) =>
+                 (if J /= Index'Result
+                    and then (J < Index'Result) = (Going = Forward)
+                    and then (J = From
+                                or else (J > From) = (Going = Forward))
+                  then (Test = Inside)
+                       /= Maps.Is_In (Element (Source, J), Set)))),
+     Global         => null;
    pragma Ada_05 (Index);
 
    function Index_Non_Blank
      (Source : Unbounded_String;
       Going  : Direction := Forward) return Natural
    with
-     Global => null;
+     Post           => Index_Non_Blank'Result <= Length (Source),
+     Contract_Cases =>
+
+        --  If all characters of Source are Space characters, then 0 is
+        --  returned.
+
+       ((for all C of To_String (Source) => C = ' ')
+        =>
+          Index_Non_Blank'Result = 0,
+
+        --  Otherwise, an index in the range of Source is returned
+
+        others
+        =>
+          --  The result is in the range of Source
+
+          Index_Non_Blank'Result in 1 .. Length (Source)
+
+            --  The character at the returned index is not a Space character
+
+            and then Element (Source, Index_Non_Blank'Result) /= ' '
+
+            --  The result is the smallest or largest index which is not a
+            --  Space character, respectively when Going = Forward and Going
+            --  = Backward.
+
+            and then
+              (for all J in 1 .. Length (Source) =>
+                 (if J /= Index_Non_Blank'Result
+                       and then
+                         (J < Index_Non_Blank'Result) = (Going = Forward)
+                  then Element (Source, J) = ' '))),
+     Global         => null;
 
    function Index_Non_Blank
      (Source : Unbounded_String;
       From   : Positive;
       Going  : Direction := Forward) return Natural
    with
-     Pre    => (if Length (Source) /= 0 then From <= Length (Source)),
-     Global => null;
+     Pre            =>
+       (if Length (Source) /= 0 then From <= Length (Source)),
+     Post           => Index_Non_Blank'Result <= Length (Source),
+     Contract_Cases =>
+
+        --  If Source is the empty string, or all characters of the
+        --  considered slice of Source are Space characters, then 0
+        --  is returned.
+
+       (Length (Source) = 0
+          or else
+            (for all J in 1 .. Length (Source) =>
+               (if J = From or else (J > From) = (Going = Forward) then
+                  Element (Source, J) = ' '))
+        =>
+          Index_Non_Blank'Result = 0,
+
+        --  Otherwise, an index in the considered range of Source is
+        --  returned.
+
+        others
+        =>
+          --  The result is in the considered range of Source
+
+          Index_Non_Blank'Result in 1 .. Length (Source)
+            and then
+              (Index_Non_Blank'Result = From
+                 or else
+                   (Index_Non_Blank'Result > From) = (Going = Forward))
+
+            --  The character at the returned index is not a Space character
+
+            and then Element (Source, Index_Non_Blank'Result) /= ' '
+
+            --  The result is the smallest or largest index which isn't a
+            --  Space character, respectively when Going = Forward and Going
+            --  = Backward.
+
+            and then
+              (for all J in 1 .. Length (Source) =>
+                 (if J /= Index_Non_Blank'Result
+                    and then
+                      (J < Index_Non_Blank'Result) = (Going = Forward)
+                    and then (J = From
+                                or else (J > From) = (Going = Forward))
+                  then Element (Source, J) = ' '))),
+     Global         => null;
    pragma Ada_05 (Index_Non_Blank);
 
    function Count
@@ -429,7 +811,7 @@ is
       Pattern : String;
       Mapping : Maps.Character_Mapping_Function) return Natural
    with
-     Pre    => Pattern'Length /= 0,
+     Pre    => Pattern'Length /= 0 and then Mapping /= null,
      Global => null;
 
    function Count
@@ -446,8 +828,53 @@ is
       First  : out Positive;
       Last   : out Natural)
    with
-     Pre    => (if Length (Source) /= 0 then From <= Length (Source)),
-     Global => null;
+     Pre            =>
+       (if Length (Source) /= 0 then From <= Length (Source)),
+     Contract_Cases =>
+
+        --  If Source is the empty string, or if no character of the
+        --  considered slice of Source satisfies the property Test on
+        --  Set, then First is set to From and Last is set to 0.
+
+       (Length (Source) = 0
+          or else
+            (for all J in From .. Length (Source) =>
+               (Test = Inside) /= Maps.Is_In (Element (Source, J), Set))
+        =>
+          First = From and then Last = 0,
+
+        --  Otherwise, First and Last are set to valid indexes
+
+        others
+        =>
+          --  First and Last are in the considered range of Source
+
+          First in From .. Length (Source)
+            and then Last in First .. Length (Source)
+
+            --  No character between From and First satisfies the property
+            --  Test on Set.
+
+            and then
+              (for all J in From .. First - 1 =>
+                 (Test = Inside) /= Maps.Is_In (Element (Source, J), Set))
+
+            --  All characters between First and Last satisfy the property
+            --  Test on Set.
+
+            and then
+              (for all J in First .. Last =>
+                 (Test = Inside) = Maps.Is_In (Element (Source, J), Set))
+
+            --  If Last is not Source'Last, then the character at position
+            --  Last + 1 does not satify the property Test on Set.
+
+            and then
+              (if Last < Length (Source)
+               then
+                 (Test = Inside)
+                 /= Maps.Is_In (Element (Source, Last + 1), Set))),
+     Global         => null;
    pragma Ada_2012 (Find_Token);
 
    procedure Find_Token
@@ -457,7 +884,51 @@ is
       First  : out Positive;
       Last   : out Natural)
    with
-     Global => null;
+     Contract_Cases =>
+
+        --  If Source is the empty string, or if no character of the
+        --  considered slice of Source satisfies the property Test on
+        --  Set, then First is set to 1 and Last is set to 0.
+
+       (Length (Source) = 0
+          or else
+            (for all J in 1 .. Length (Source) =>
+               (Test = Inside) /= Maps.Is_In (Element (Source, J), Set))
+        =>
+          First = 1 and then Last = 0,
+
+        --  Otherwise, First and Last are set to valid indexes
+
+        others
+        =>
+          --  First and Last are in the considered range of Source
+
+          First in 1 .. Length (Source)
+            and then Last in First .. Length (Source)
+
+            --  No character between 1 and First satisfies the property Test
+            --  on Set.
+
+            and then
+              (for all J in 1 .. First - 1 =>
+                 (Test = Inside) /= Maps.Is_In (Element (Source, J), Set))
+
+            --  All characters between First and Last satisfy the property
+            --  Test on Set.
+
+            and then
+              (for all J in First .. Last =>
+                 (Test = Inside) = Maps.Is_In (Element (Source, J), Set))
+
+            --  If Last is not Source'Last, then the character at position
+            --  Last + 1 does not satify the property Test on Set.
+
+            and then
+              (if Last < Length (Source)
+               then
+                 (Test = Inside)
+                 /= Maps.Is_In (Element (Source, Last + 1), Set))),
+     Global         => null;
 
    ------------------------------------
    -- String Translation Subprograms --
@@ -467,28 +938,44 @@ is
      (Source  : Unbounded_String;
       Mapping : Maps.Character_Mapping) return Unbounded_String
    with
-     Post   => Length (Translate'Result) = Length (Source),
+     Post   => Length (Translate'Result) = Length (Source)
+       and then
+         (for all K in 1 .. Length (Source) =>
+            Element (Translate'Result, K) =
+              Ada.Strings.Maps.Value (Mapping, Element (Source, K))),
      Global => null;
 
    procedure Translate
      (Source  : in out Unbounded_String;
       Mapping : Maps.Character_Mapping)
    with
-     Post   => Length (Source) = Length (Source)'Old,
+     Post   => Length (Source) = Length (Source)'Old
+       and then
+         (for all K in 1 .. Length (Source) =>
+            Element (Source, K) =
+              Ada.Strings.Maps.Value (Mapping, To_String (Source)'Old (K))),
      Global => null;
 
    function Translate
      (Source  : Unbounded_String;
       Mapping : Maps.Character_Mapping_Function) return Unbounded_String
    with
-     Post   => Length (Translate'Result) = Length (Source),
+     Pre    => Mapping /= null,
+     Post   => Length (Translate'Result) = Length (Source)
+       and then
+         (for all K in 1 .. Length (Source) =>
+            Element (Translate'Result, K) = Mapping (Element (Source, K))),
      Global => null;
 
    procedure Translate
      (Source  : in out Unbounded_String;
       Mapping : Maps.Character_Mapping_Function)
    with
-     Post   => Length (Source) = Length (Source)'Old,
+     Pre    => Mapping /= null,
+     Post   => Length (Source) = Length (Source)'Old
+       and then
+         (for all K in 1 .. Length (Source) =>
+            Element (Source, K) = Mapping (To_String (Source)'Old (K))),
      Global => null;
 
    ---------------------------------------
@@ -506,14 +993,66 @@ is
          and then (if High >= Low
                    then Low - 1
                      <= Natural'Last - By'Length
-                      - Natural'Max (Length (Source) - High, 0)
+                      - Integer'Max (Length (Source) - High, 0)
                    else Length (Source) <= Natural'Last - By'Length),
      Contract_Cases =>
+
+        --  If High >= Low, when considering the application of To_String to
+        --  convert an Unbounded_String into String, then the returned string
+        --  comprises Source (Source'First .. Low - 1) & By
+        --  & Source(High + 1 .. Source'Last).
+
        (High >= Low =>
+
+          --  Length of the returned string
+
           Length (Replace_Slice'Result)
-        = Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0),
+          = Low - 1 + By'Length + Integer'Max (Length (Source) - High, 0)
+
+            --  Elements starting at Low are replaced by elements of By
+
+            and then
+              Slice (Replace_Slice'Result, 1, Low - 1) =
+                Slice (Source, 1, Low - 1)
+            and then
+              Slice (Replace_Slice'Result, Low, Low - 1 + By'Length) = By
+
+            --  When there are remaining characters after the replaced slice,
+            --  they are appended to the result.
+
+            and then
+              (if High < Length (Source)
+               then
+                 Slice (Replace_Slice'Result,
+                   Low + By'Length, Length (Replace_Slice'Result)) =
+                     Slice (Source, High + 1, Length (Source))),
+
+        --  If High < Low, then the returned string is
+        --  Insert (Source, Before => Low, New_Item => By).
+
         others      =>
-          Length (Replace_Slice'Result) = Length (Source)'Old + By'Length),
+
+          --  Length of the returned string
+
+          Length (Replace_Slice'Result) = Length (Source) + By'Length
+
+            --  Elements of By are inserted after the element at Low
+
+            and then
+              Slice (Replace_Slice'Result, 1, Low - 1) =
+                Slice (Source, 1, Low - 1)
+            and then
+              Slice (Replace_Slice'Result, Low, Low - 1 + By'Length) = By
+
+            --  When there are remaining characters after Low in Source, they
+            --  are appended to the result.
+
+            and then
+              (if Low < Length (Source)
+               then
+                Slice (Replace_Slice'Result,
+                  Low + By'Length, Length (Replace_Slice'Result)) =
+                    Slice (Source, Low, Length (Source)))),
      Global         => null;
 
    procedure Replace_Slice
@@ -530,11 +1069,61 @@ is
                       - Natural'Max (Length (Source) - High, 0)
                    else Length (Source) <= Natural'Last - By'Length),
      Contract_Cases =>
+
+        --  If High >= Low, when considering the application of To_String to
+        --  convert an Unbounded_String into String, then the returned string
+        --  comprises Source (Source'First .. Low - 1) & By
+        --  & Source(High + 1 .. Source'Last).
+
        (High >= Low =>
+
+          --  Length of the returned string
+
           Length (Source)
-        = Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0),
+          = Low - 1 + By'Length + Integer'Max (Length (Source)'Old - High, 0)
+
+            --  Elements starting at Low are replaced by elements of By
+
+            and then Slice (Source, 1, Low - 1) =
+              Slice (Source, 1, Low - 1)'Old
+            and then Slice (Source, Low, Low - 1 + By'Length) = By
+
+            --  When there are remaining characters after the replaced slice,
+            --  they are appended to the result.
+
+            and then
+              (if High < Length (Source)'Old
+               then Slice (Source, Low + By'Length, Length (Source)) =
+                 Slice (Source,
+                   --  Really "High + 1" but expressed with a conditional
+                   --  repeating the above test so that the call to Slice
+                   --  is valid on entry (under 'Old) even when the test
+                   --  evaluates to False.
+                   (if High < Length (Source) then High + 1 else 1),
+                   Length (Source))'Old),
+
+        --  If High < Low, then the returned string is
+        --  Insert (Source, Before => Low, New_Item => By).
+
         others      =>
-          Length (Source) = Length (Source)'Old + By'Length),
+
+          --  Length of the returned string
+
+          Length (Source) = Length (Source)'Old + By'Length
+
+            --  Elements of By are inserted after the element at Low
+
+            and then Slice (Source, 1, Low - 1) =
+              Slice (Source, 1, Low - 1)'Old
+            and then Slice (Source, Low, Low - 1 + By'Length) = By
+
+            --  When there are remaining characters after Low in Source, they
+            --  are appended to the result.
+
+            and then
+              (if Low < Length (Source)'Old
+               then Slice (Source, Low + By'Length, Length (Source)) =
+                 Slice (Source, Low, Length (Source))'Old)),
      Global         => null;
 
    function Insert
@@ -544,7 +1133,27 @@ is
    with
      Pre    => Before - 1 <= Length (Source)
                  and then New_Item'Length <= Natural'Last - Length (Source),
-     Post   => Length (Insert'Result) = Length (Source) + New_Item'Length,
+     Post   =>
+       --  Length of the returned string
+
+       Length (Insert'Result) = Length (Source) + New_Item'Length
+
+         --  Elements of New_Item are inserted after element at Before
+
+         and then
+           Slice (Insert'Result, 1, Before - 1) = Slice (Source, 1, Before - 1)
+         and then
+           Slice (Insert'Result, Before, Before - 1 + New_Item'Length)
+           = New_Item
+
+         --  When there are remaining characters after Before in Source, they
+         --  are appended to the returned string.
+
+         and then
+           (if Before <= Length (Source) then
+              Slice (Insert'Result, Before + New_Item'Length,
+                Length (Insert'Result)) =
+                  Slice (Source, Before, Length (Source))),
      Global => null;
 
    procedure Insert
@@ -554,7 +1163,25 @@ is
    with
      Pre    => Before - 1 <= Length (Source)
                  and then New_Item'Length <= Natural'Last - Length (Source),
-     Post   => Length (Source) = Length (Source)'Old + New_Item'Length,
+     Post   =>
+       --  Length of the returned string
+
+       Length (Source) = Length (Source)'Old + New_Item'Length
+
+         --  Elements of New_Item are inserted after element at Before
+
+         and then
+           Slice (Source, 1, Before - 1) = Slice (Source, 1, Before - 1)'Old
+         and then
+           Slice (Source, Before, Before - 1 + New_Item'Length) = New_Item
+
+         --  When there are remaining characters after Before in Source, they
+         --  are appended to the returned string.
+
+         and then
+           (if Before <= Length (Source)'Old then
+              Slice (Source, Before + New_Item'Length, Length (Source)) =
+                Slice (Source, Before, Length (Source))'Old),
      Global => null;
 
    function Overwrite
@@ -563,12 +1190,31 @@ is
       New_Item : String) return Unbounded_String
    with
      Pre    => Position - 1 <= Length (Source)
-                 and then (if New_Item'Length /= 0
-                           then
-                             New_Item'Length <= Natural'Last - (Position - 1)),
+                 and then New_Item'Length <= Natural'Last - (Position - 1),
      Post   =>
-       Length (Overwrite'Result)
-     = Natural'Max (Length (Source), Position - 1 + New_Item'Length),
+       --  Length of the returned string
+
+       Length (Overwrite'Result) =
+         Integer'Max (Length (Source), Position - 1 + New_Item'Length)
+
+         --  Elements after Position are replaced by elements of New_Item
+
+         and then
+           Slice (Overwrite'Result, 1, Position - 1) =
+             Slice (Source, 1, Position - 1)
+         and then
+           Slice (Overwrite'Result, Position, Position - 1 + New_Item'Length) =
+             New_Item
+         and then
+           (if Position - 1 + New_Item'Length < Length (Source) then
+
+              --  There are some unchanged characters of Source remaining
+              --  after New_Item.
+
+              Slice (Overwrite'Result,
+                Position + New_Item'Length, Length (Source)) =
+                  Slice (Source,
+                    Position + New_Item'Length, Length (Source))),
      Global => null;
 
    procedure Overwrite
@@ -577,13 +1223,36 @@ is
       New_Item : String)
    with
      Pre    => Position - 1 <= Length (Source)
-                 and then (if New_Item'Length /= 0
-                           then
-                             New_Item'Length <= Natural'Last - (Position - 1)),
+                 and then New_Item'Length <= Natural'Last - (Position - 1),
      Post   =>
-       Length (Source)
-     = Natural'Max (Length (Source)'Old, Position - 1 + New_Item'Length),
+       --  Length of the returned string
+
+       Length (Source) =
+         Integer'Max (Length (Source)'Old, Position - 1 + New_Item'Length)
+
+         --  Elements after Position are replaced by elements of New_Item
 
+         and then
+           Slice (Source, 1, Position - 1) = Slice (Source, 1, Position - 1)
+         and then
+           Slice (Source, Position, Position - 1 + New_Item'Length) = New_Item
+         and then
+           (if Position - 1 + New_Item'Length < Length (Source)'Old then
+
+              --  There are some unchanged characters of Source remaining
+              --  after New_Item.
+
+              Slice (Source,
+                Position + New_Item'Length, Length (Source)'Old) =
+                  Slice (Source,
+                    --  Really "Position + New_Item'Length" but expressed with
+                    --  a conditional repeating the above test so that the
+                    --  call to Slice is valid on entry (under 'Old) even
+                    --  when the test evaluates to False.
+                    (if Position - 1 + New_Item'Length < Length (Source)
+                     then Position + New_Item'Length
+                     else 1),
+                    Length (Source))'Old),
      Global => null;
 
    function Delete
@@ -591,12 +1260,19 @@ is
       From    : Positive;
       Through : Natural) return Unbounded_String
    with
-     Pre            => (if Through <= From then From - 1 <= Length (Source)),
+     Pre            => (if Through >= From then From - 1 <= Length (Source)),
      Contract_Cases =>
        (Through >= From =>
-          Length (Delete'Result) = Length (Source) - (Through - From + 1),
+          Length (Delete'Result) =
+            From - 1 + Natural'Max (Length (Source) - Through, 0)
+            and then
+              Slice (Delete'Result, 1, From - 1) = Slice (Source, 1, From - 1)
+            and then
+              (if Through < Length (Source) then
+                 Slice (Delete'Result, From, Length (Delete'Result)) =
+                   Slice (Source, Through + 1, Length (Source))),
         others          =>
-          Length (Delete'Result) = Length (Source)),
+             Delete'Result = Source),
      Global         => null;
 
    procedure Delete
@@ -604,82 +1280,255 @@ is
       From    : Positive;
       Through : Natural)
    with
-     Pre            => (if Through <= From then From - 1 <= Length (Source)),
+     Pre            => (if Through >= From then From - 1 <= Length (Source)),
      Contract_Cases =>
        (Through >= From =>
-          Length (Source) = Length (Source)'Old - (Through - From + 1),
+          Length (Source) =
+            From - 1 + Natural'Max (Length (Source)'Old - Through, 0)
+            and then
+              Slice (Source, 1, From - 1) =
+                To_String (Source)'Old (1 .. From - 1)
+            and then
+              (if Through < Length (Source) then
+                Slice (Source, From, Length (Source)) =
+                  To_String (Source)'Old (Through + 1 .. Length (Source)'Old)),
         others          =>
-          Length (Source) = Length (Source)'Old),
+          To_String (Source) = To_String (Source)'Old),
      Global         => null;
 
    function Trim
      (Source : Unbounded_String;
       Side   : Trim_End) return Unbounded_String
    with
-     Post   => Length (Trim'Result) <= Length (Source),
-     Global => null;
+     Contract_Cases =>
+       --  If all characters in Source are Space, the returned string is
+       --  empty.
+
+       ((for all C of To_String (Source) => C = ' ')
+        =>
+          Length (Trim'Result) = 0,
+
+        --  Otherwise, the returned string is a slice of Source
+
+        others
+        =>
+          (declare
+             Low  : constant Positive :=
+               (if Side = Right then 1
+                else Index_Non_Blank (Source, Forward));
+             High : constant Positive :=
+               (if Side = Left then Length (Source)
+                else Index_Non_Blank (Source, Backward));
+           begin
+             To_String (Trim'Result) = Slice (Source, Low, High))),
+     Global         => null;
 
    procedure Trim
      (Source : in out Unbounded_String;
       Side   : Trim_End)
    with
-     Post   => Length (Source) <= Length (Source)'Old,
-     Global => null;
+     Contract_Cases =>
+       --  If all characters in Source are Space, the returned string is
+       --  empty.
+
+       ((for all C of To_String (Source) => C = ' ')
+        =>
+          Length (Source) = 0,
+
+        --  Otherwise, the returned string is a slice of Source
+
+        others
+        =>
+          (declare
+             Low  : constant Positive :=
+               (if Side = Right then 1
+                else Index_Non_Blank (Source, Forward)'Old);
+             High : constant Positive :=
+               (if Side = Left then Length (Source)'Old
+                else Index_Non_Blank (Source, Backward)'Old);
+           begin
+             To_String (Source) = To_String (Source)'Old (Low .. High))),
+     Global         => null;
 
    function Trim
      (Source : Unbounded_String;
       Left   : Maps.Character_Set;
       Right  : Maps.Character_Set) return Unbounded_String
    with
-     Post   => Length (Trim'Result) <= Length (Source),
-     Global => null;
+     Contract_Cases =>
+       --  If all characters in Source are contained in one of the sets Left
+       --  or Right, then the returned string is empty.
+
+       ((for all C of To_String (Source) => Maps.Is_In (C, Left))
+          or else
+            (for all C of To_String (Source) => Maps.Is_In (C, Right))
+        =>
+          Length (Trim'Result) = 0,
+
+        --  Otherwise, the returned string is a slice of Source
+
+        others
+        =>
+          (declare
+             Low  : constant Positive :=
+               Index (Source, Left, Outside, Forward);
+             High : constant Positive :=
+               Index (Source, Right, Outside, Backward);
+           begin
+             To_String (Trim'Result) = Slice (Source, Low, High))),
+     Global         => null;
 
    procedure Trim
      (Source : in out Unbounded_String;
       Left   : Maps.Character_Set;
       Right  : Maps.Character_Set)
    with
-     Post   => Length (Source) <= Length (Source)'Old,
-     Global => null;
+     Contract_Cases =>
+       --  If all characters in Source are contained in one of the sets Left
+       --  or Right, then the returned string is empty.
+
+       ((for all C of To_String (Source) => Maps.Is_In (C, Left))
+          or else
+            (for all C of To_String (Source) => Maps.Is_In (C, Right))
+        =>
+          Length (Source) = 0,
+
+        --  Otherwise, the returned string is a slice of Source
+
+        others
+        =>
+          (declare
+             Low  : constant Positive :=
+               Index (Source, Left, Outside, Forward)'Old;
+             High : constant Positive :=
+               Index (Source, Right, Outside, Backward)'Old;
+           begin
+             To_String (Source) = To_String (Source)'Old (Low .. High))),
+     Global         => null;
 
    function Head
      (Source : Unbounded_String;
       Count  : Natural;
       Pad    : Character := Space) return Unbounded_String
    with
-     Post   => Length (Head'Result) = Count,
-     Global => null;
+     Post           => Length (Head'Result) = Count,
+     Contract_Cases =>
+       (Count <= Length (Source)
+        =>
+          --  Source is cut
+
+          To_String (Head'Result) = Slice (Source, 1, Count),
+
+        others
+        =>
+          --  Source is followed by Pad characters
+
+          Slice (Head'Result, 1, Length (Source)) = To_String (Source)
+            and then
+              Slice (Head'Result, Length (Source) + 1, Count) =
+                [1 .. Count - Length (Source) => Pad]),
+     Global         => null;
 
    procedure Head
      (Source : in out Unbounded_String;
       Count  : Natural;
       Pad    : Character := Space)
    with
-     Post   => Length (Source) = Count,
-     Global => null;
+     Post           => Length (Source) = Count,
+     Contract_Cases =>
+       (Count <= Length (Source)
+        =>
+          --  Source is cut
+
+          To_String (Source) = Slice (Source, 1, Count),
+
+        others
+        =>
+          --  Source is followed by Pad characters
+
+          Slice (Source, 1, Length (Source)'Old) = To_String (Source)'Old
+            and then
+              Slice (Source, Length (Source)'Old + 1, Count) =
+                [1 .. Count - Length (Source)'Old => Pad]),
+     Global         => null;
 
    function Tail
      (Source : Unbounded_String;
       Count  : Natural;
       Pad    : Character := Space) return Unbounded_String
    with
-     Post   => Length (Tail'Result) = Count,
-     Global => null;
+     Post           => Length (Tail'Result) = Count,
+     Contract_Cases =>
+       (Count = 0
+        =>
+          True,
+
+        (Count in 1 .. Length (Source))
+        =>
+          --  Source is cut
+
+          To_String (Tail'Result) =
+            Slice (Source, Length (Source) - Count + 1, Length (Source)),
+
+        others
+        =>
+          --  Source is preceded by Pad characters
+
+          (if Length (Source) = 0 then
+            To_String (Tail'Result) = [1 .. Count => Pad]
+          else
+            Slice (Tail'Result, 1, Count - Length (Source)) =
+              [1 .. Count - Length (Source) => Pad]
+              and then
+                Slice (Tail'Result, Count - Length (Source) + 1, Count) =
+                  To_String (Source))),
+     Global         => null;
 
    procedure Tail
      (Source : in out Unbounded_String;
       Count  : Natural;
       Pad    : Character := Space)
    with
-     Post   => Length (Source) = Count,
-     Global => null;
+     Post           => Length (Source) = Count,
+     Contract_Cases =>
+       (Count = 0
+        =>
+          True,
+
+        (Count in  1 .. Length (Source))
+        =>
+          --  Source is cut
+
+          To_String (Source) =
+            Slice (Source,
+              --  Really "Length (Source) - Count + 1" but expressed with a
+              --  conditional repeating the above guard so that the call to
+              --  Slice is valid on entry (under 'Old) even when the test
+              --  evaluates to False.
+              (if Count <= Length (Source) then Length (Source) - Count + 1
+               else 1),
+              Length (Source))'Old,
+
+        others
+        =>
+          --  Source is preceded by Pad characters
+
+          (if Length (Source)'Old = 0 then
+            To_String (Source) = [1 .. Count => Pad]
+          else
+            Slice (Source, 1, Count - Length (Source)'Old) =
+              [1 .. Count - Length (Source)'Old => Pad]
+              and then
+                Slice (Source, Count - Length (Source)'Old + 1, Count) =
+                  To_String (Source)'Old)),
+     Global         => null;
 
    function "*"
      (Left  : Natural;
       Right : Character) return Unbounded_String
    with
      Pre    => Left <= Natural'Last,
-     Post   => Length ("*"'Result) = Left,
+     Post   => To_String ("*"'Result) = [1 .. Left => Right],
      Global => null;
 
    function "*"
@@ -687,7 +1536,13 @@ is
       Right : String) return Unbounded_String
    with
      Pre    => (if Left /= 0 then Right'Length <= Natural'Last / Left),
-     Post   => Length ("*"'Result) = Left * Right'Length,
+     Post =>
+       Length ("*"'Result) = Left * Right'Length
+         and then
+           (if Right'Length > 0 then
+              (for all K in 1 .. Left * Right'Length =>
+                 Element ("*"'Result, K) =
+                   Right (Right'First + (K - 1) mod Right'Length))),
      Global => null;
 
    function "*"
@@ -695,10 +1550,18 @@ is
       Right : Unbounded_String) return Unbounded_String
    with
      Pre    => (if Left /= 0 then Length (Right) <= Natural'Last / Left),
-     Post   => Length ("*"'Result) = Left * Length (Right),
+     Post =>
+       Length ("*"'Result) = Left * Length (Right)
+         and then
+           (if Length (Right) > 0 then
+              (for all K in 1 .. Left * Length (Right) =>
+                 Element ("*"'Result, K) =
+                   Element (Right, 1 + (K - 1) mod Length (Right)))),
      Global => null;
 
 private
+   pragma SPARK_Mode (Off);  --  Controlled types are not in SPARK
+
    pragma Inline (Length);
 
    package AF renames Ada.Finalization;
