diff mbox series

[COMMITTED,17/26] ada: Add contracts to Ada.Strings.Unbounded and adapt implementation

Message ID 20240802071210.413366-17-poulhies@adacore.com
State New
Headers show
Series [COMMITTED,01/26] ada: Fix detection of suspicious loop patterns | expand

Commit Message

Marc Poulhiès Aug. 2, 2024, 7:11 a.m. UTC 
From: Yannick Moy <moy@adacore.com>

Add complete functional contracts to all subprograms in
Ada.Strings.Unbounded, except Count, following the specification from
Ada RM A.4.5. These contracts are similar to the contracts found in
Ada.Strings.Fixed and Ada.Strings.Bounded.

A difference is that type Unbounded_String is controlled, thus we avoid
performing copies of a parameter Source with Source'Old, and instead
apply 'Old attribute on the enclosing call, such as Length(Source)'Old.

As Unbounded_String is controlled, the implementation is not in SPARK.
Instead, we have separately proved a slightly different implementation
for which Unbounded_String is not controlled, against the same
specification. This ensures that the specification is consistent.

To minimize differences between this test from the SPARK testsuite and
the actual implementation (the one in a-strunb.adb), and to avoid
overflows in the actual implementation, some code is slightly rewritten.
Delete and Insert are modified to return the correct result in all
cases allowed by the standard.

The same contracts are added to the version in a-strunb__shared.ads and
similar implementation patches are applied to the body
a-strunb__shared.adb. In particular, tests are added to avoid overflows
on strings for which the last index is Natural'Last, and the computations
that involve Sum to guarantee that an exception is raised in case of
overflow are rewritten to guarantee correct detection and no intermediate
overflows (and such tests are applied consistently between the procedure
and the function when both exist).

gcc/ada/

	* libgnat/a-strunb.adb (Sum, Saturated_Sum, Saturated_Mul): Adapt
	function signatures to more precise types that allow proof.
	(function "&"): Conditionally assign a slice to avoid possible
	overflow which only occurs when the assignment is a noop (because
	the slice is empty in that case).
	(Append): Same.
	(function "*"): Retype K to avoid a possible overflow. Add early
	return on null length for proof.
	(Delete): Fix implementation to return the correct result in all
	cases allowed by the Ada standard.
	(Insert): Same. Also avoid possible overflows.
	(Length): Rewrite as expression function for proof.
	(Overwrite): Avoid possible overflows.
	(Slice): Same.
	(To_String): Rewrite as expression function for proof.
	* libgnat/a-strunb.ads: Extend Assertion_Policy to new contracts
	used. Add complete functional contracts to all subprograms of the
	public API except Count.
	* libgnat/a-strunb__shared.adb (Sum): Adapt function signature to
	more precise types that allow proof.
	(function "&"): Conditionally assign a slice to avoid possible
	overflow.
	(function "*"): Retype K to avoid a possible overflow.
	(Delete): Fix implementation to return the correct result in all
	cases allowed by the Ada standard.
	(Insert): Avoid possible overflows.
	(Overwrite): Avoid possible overflows.
	(Replace_Slice): Same.
	(Slice): Same.
	(To_String): Rewrite as expression function for proof.
	* libgnat/a-strunb__shared.ads: Extend Assertion_Policy to new
	contracts used. Add complete functional contracts to all
	subprograms of the public API except Count. Mark public part of
	spec as in SPARK.

Tested on x86_64-pc-linux-gnu, committed on master.

---
 gcc/ada/libgnat/a-strunb.adb         |  110 +--
 gcc/ada/libgnat/a-strunb.ads         | 1039 ++++++++++++++++++++++++--
 gcc/ada/libgnat/a-strunb__shared.adb |  150 ++--
 gcc/ada/libgnat/a-strunb__shared.ads | 1029 +++++++++++++++++++++++--
 4 files changed, 2068 insertions(+), 260 deletions(-)
diff mbox series

Patch

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;