[Ada] Contracts written for the Ada.Strings.Bounded library

gcc/ada/

	* libgnat/a-strbou.adb: Turn SPARK_Mode on.
	* libgnat/a-strbou.ads: Write contracts.
	* libgnat/a-strfix.ads (Index): Fix grammar error in a comment.
	* libgnat/a-strsea.ads (Index): Likewise.
	* libgnat/a-strsup.adb: Rewrite the body to take into account
	the new definition of Super_String using Relaxed_Initialization
	and a predicate.
	(Super_Replicate, Super_Translate, Times): Added loop
	invariants, and ghost lemmas for Super_Replicate and Times.
	(Super_Trim): Rewrite the body using search functions to
	determine the cutting points.
	(Super_Element, Super_Length, Super_Slice, Super_To_String):
	Remove (now written as expression functions in a-strsup.ads).
	* libgnat/a-strsup.ads: Added contracts.
	(Super_Element, Super_Length, Super_Slice, Super_To_String):
	Rewrite as expression functions.

6 files changed, 4911 insertions, 723 deletions

diff --git a/gcc/ada/libgnat/a-strbou.adb b/gcc/ada/libgnat/a-strbou.adb
index 61b3d73..01a2002 100644
--- a/gcc/ada/libgnat/a-strbou.adb
+++ b/gcc/ada/libgnat/a-strbou.adb
@@ -29,7 +29,7 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
-package body Ada.Strings.Bounded is
+package body Ada.Strings.Bounded with SPARK_Mode is
 
    package body Generic_Bounded_Length is
 
diff --git a/gcc/ada/libgnat/a-strbou.ads b/gcc/ada/libgnat/a-strbou.ads
index f0cf7b2..b88e049 100644
--- a/gcc/ada/libgnat/a-strbou.ads
+++ b/gcc/ada/libgnat/a-strbou.ads
@@ -33,25 +33,33 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
---  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.
-
-pragma Assertion_Policy (Pre => Ignore);
-
-with Ada.Strings.Maps;
+with Ada.Strings.Maps; use type Ada.Strings.Maps.Character_Mapping_Function;
 with Ada.Strings.Superbounded;
+with Ada.Strings.Search;
 
-package Ada.Strings.Bounded is
+package Ada.Strings.Bounded with SPARK_Mode is
    pragma Preelaborate;
 
    generic
       Max : Positive;
       --  Maximum length of a Bounded_String
 
-   package Generic_Bounded_Length with
-     Initial_Condition => Length (Null_Bounded_String) = 0
+   package Generic_Bounded_Length with SPARK_Mode,
+     Initializes       => (Null_Bounded_String => Max,
+                           Max_Length          => Max),
+     Initial_Condition => Length (Null_Bounded_String) = 0,
+     Abstract_State    => null
    is
+      --  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.
+      --  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,
+                               Post           => Ignore,
+                               Contract_Cases => Ignore,
+                               Ghost          => Ignore);
 
       Max_Length : constant Positive := Max;
 
@@ -73,14 +81,24 @@ package Ada.Strings.Bounded is
         (Source : String;
          Drop   : Truncation := Error) return Bounded_String
       with
-        Pre    => (if Source'Length > Max_Length then Drop /= Error),
-        Post   =>
-          Length (To_Bounded_String'Result)
-        = Natural'Min (Max_Length, Source'Length),
-        Global => null;
+        Pre            => (if Source'Length > Max_Length then Drop /= Error),
+        Contract_Cases =>
+          (Source'Length <= Max_Length
+           =>
+             To_String (To_Bounded_String'Result) = Source,
+
+           Source'Length > Max_Length and then Drop = Left
+           =>
+             To_String (To_Bounded_String'Result) =
+               Source (Source'Last - Max_Length + 1 .. Source'Last),
+
+           others  --  Drop = Right
+           =>
+             To_String (To_Bounded_String'Result) =
+               Source (Source'First .. Source'First - 1 + Max_Length)),
+        Global         => Max_Length;
 
       function To_String (Source : Bounded_String) return String with
-        Post   => To_String'Result'Length = Length (Source),
         Global => null;
 
       procedure Set_Bounded_String
@@ -88,9 +106,22 @@ package Ada.Strings.Bounded is
          Source : String;
          Drop   : Truncation := Error)
       with
-        Pre    => (if Source'Length > Max_Length then Drop /= Error),
-        Post   => Length (Target) = Natural'Min (Max_Length, Source'Length),
-        Global => null;
+        Pre            => (if Source'Length > Max_Length then Drop /= Error),
+        Contract_Cases =>
+          (Source'Length <= Max_Length
+           =>
+             To_String (Target) = Source,
+
+           Source'Length > Max_Length and then Drop = Left
+           =>
+             To_String (Target) =
+               Source (Source'Last - Max_Length + 1 .. Source'Last),
+
+           others  --  Drop = Right
+           =>
+             To_String (Target) =
+               Source (Source'First .. Source'First - 1 + Max_Length)),
+        Global         => (Proof_In => Max_Length);
       pragma Ada_05 (Set_Bounded_String);
 
       function Append
@@ -98,138 +129,404 @@ package Ada.Strings.Bounded is
          Right : Bounded_String;
          Drop  : Truncation  := Error) return Bounded_String
       with
-        Pre    =>
+        Pre            =>
           (if Length (Left) > Max_Length - Length (Right)
            then Drop /= Error),
-        Post   =>
-          Length (Append'Result)
-        = Natural'Min (Max_Length, Length (Left) + Length (Right)),
-        Global => null;
+        Contract_Cases =>
+          (Length (Left) <= Max_Length - Length (Right)
+           =>
+             Length (Append'Result) = Length (Left) + Length (Right)
+               and then
+                 Slice (Append'Result, 1, Length (Left)) = To_String (Left)
+               and then
+                 (if Length (Right) > 0 then
+                    Slice (Append'Result,
+                      Length (Left) + 1, Length (Append'Result)) =
+                        To_String (Right)),
+
+           Length (Left) > Max_Length - Length (Right)
+             and then Drop = Strings.Left
+           =>
+             Length (Append'Result) = Max_Length
+               and then
+                 (if Length (Right) < Max_Length then
+                    Slice (Append'Result, 1, Max_Length - Length (Right)) =
+                      Slice (Left,
+                        Length (Left) - Max_Length + Length (Right) + 1,
+                        Length (Left)))
+               and then
+                 Slice (Append'Result,
+                   Max_Length - Length (Right) + 1, Max_Length) =
+                     To_String (Right),
+
+           others  --  Drop = Right
+           =>
+             Length (Append'Result) = Max_Length
+               and then
+                 Slice (Append'Result, 1, Length (Left)) = To_String (Left)
+               and then
+                 (if Length (Left) < Max_Length then
+                    Slice (Append'Result, Length (Left) + 1, Max_Length) =
+                      Slice (Right, 1, Max_Length - Length (Left)))),
+        Global         => (Proof_In => Max_Length);
 
       function Append
         (Left  : Bounded_String;
          Right : String;
          Drop  : Truncation := Error) return Bounded_String
       with
-        Pre    =>
+        Pre            =>
           (if Right'Length > Max_Length - Length (Left)
            then Drop /= Error),
-        Post   =>
-          Length (Append'Result)
-        = Natural'Min (Max_Length, Length (Left) + Right'Length),
-        Global => null;
+        Contract_Cases =>
+          (Length (Left) <= Max_Length - Right'Length
+           =>
+             Length (Append'Result) = Length (Left) + Right'Length
+               and then
+                 Slice (Append'Result, 1, Length (Left)) = To_String (Left)
+               and then
+                 (if Right'Length > 0 then
+                    Slice (Append'Result,
+                      Length (Left) + 1, Length (Append'Result)) =
+                        Right),
+
+           Length (Left) > Max_Length - Right'Length
+             and then Drop = Strings.Left
+           =>
+             Length (Append'Result) = Max_Length
+               and then
+                 (if Right'Length < Max_Length then
+
+                    --  The result is the end of Left followed by Right
+
+                    Slice (Append'Result, 1, Max_Length - Right'Length) =
+                      Slice (Left,
+                        Length (Left) - Max_Length + Right'Length + 1,
+                        Length (Left))
+                      and then
+                        Slice (Append'Result,
+                          Max_Length - Right'Length + 1, Max_Length) =
+                            Right
+                  else
+                    --  The result is the last Max_Length characters of Right
+
+                    To_String (Append'Result) =
+                      Right (Right'Last - Max_Length + 1 .. Right'Last)),
+
+           others  --  Drop = Right
+           =>
+             Length (Append'Result) = Max_Length
+               and then
+                 Slice (Append'Result, 1, Length (Left)) = To_String (Left)
+               and then
+                 (if Length (Left) < Max_Length then
+                    Slice (Append'Result, Length (Left) + 1, Max_Length) =
+                      Right (Right'First
+                        .. Max_Length - Length (Left) - 1 + Right'First))),
+        Global         => (Proof_In => Max_Length);
 
       function Append
         (Left  : String;
          Right : Bounded_String;
          Drop  : Truncation := Error) return Bounded_String
       with
-        Pre    =>
+        Pre            =>
           (if Left'Length > Max_Length - Length (Right)
            then Drop /= Error),
-        Post   =>
-          Length (Append'Result)
-        = Natural'Min (Max_Length, Left'Length + Length (Right)),
-        Global => null;
+        Contract_Cases =>
+          (Left'Length <= Max_Length - Length (Right)
+           =>
+             Length (Append'Result) = Left'Length + Length (Right)
+               and then Slice (Append'Result, 1, Left'Length) = Left
+               and then
+                 (if Length (Right) > 0 then
+                    Slice (Append'Result,
+                      Left'Length + 1, Length (Append'Result)) =
+                        To_String (Right)),
+
+           Left'Length > Max_Length - Length (Right)
+             and then Drop = Strings.Left
+           =>
+             Length (Append'Result) = Max_Length
+               and then
+                 (if Length (Right) < Max_Length then
+                    Slice (Append'Result, 1, Max_Length - Length (Right)) =
+                      Left (Left'Last - Max_Length + Length (Right) + 1
+                            .. Left'Last))
+               and then
+                 Slice (Append'Result,
+                   Max_Length - Length (Right) + 1, Max_Length) =
+                     To_String (Right),
+
+           others  --  Drop = Right
+           =>
+             Length (Append'Result) = Max_Length
+               and then
+                 (if Left'Length < Max_Length then
+
+                    --  The result is Left followed by the beginning of Right
+
+                    Slice (Append'Result, 1, Left'Length) = Left
+                      and then
+                        Slice (Append'Result, Left'Length + 1, Max_Length) =
+                          Slice (Right, 1, Max_Length - Left'Length)
+                  else
+                    --  The result is the first Max_Length characters of Left
+
+                    To_String (Append'Result) =
+                      Left (Left'First .. Max_Length - 1 + Left'First))),
+        Global         => (Proof_In => Max_Length);
 
       function Append
         (Left  : Bounded_String;
          Right : Character;
          Drop  : Truncation := Error) return Bounded_String
       with
-        Pre    => (if Length (Left) = Max_Length then Drop /= Error),
-        Post   =>
-          Length (Append'Result)
-        = Natural'Min (Max_Length, Length (Left) + 1),
-        Global => null;
+        Pre            => (if Length (Left) = Max_Length then Drop /= Error),
+        Contract_Cases =>
+          (Length (Left) < Max_Length
+           =>
+             Length (Append'Result) = Length (Left) + 1
+               and then
+                 Slice (Append'Result, 1, Length (Left)) = To_String (Left)
+               and then Element (Append'Result, Length (Left) + 1) = Right,
+
+           Length (Left) = Max_Length and then Drop = Strings.Right
+           =>
+             Length (Append'Result) = Max_Length
+               and then To_String (Append'Result) = To_String (Left),
+
+           others  --  Drop = Left
+           =>
+             Length (Append'Result) = Max_Length
+               and then
+                 Slice (Append'Result, 1, Max_Length - 1) =
+                   Slice (Left, 2, Max_Length)
+               and then Element (Append'Result, Max_Length) = Right),
+        Global         => (Proof_In => Max_Length);
 
       function Append
         (Left  : Character;
          Right : Bounded_String;
          Drop  : Truncation := Error) return Bounded_String
       with
-        Pre    => (if Length (Right) = Max_Length then Drop /= Error),
-        Post   =>
-          Length (Append'Result)
-        = Natural'Min (Max_Length, 1 + Length (Right)),
-        Global => null;
+        Pre            => (if Length (Right) = Max_Length then Drop /= Error),
+        Contract_Cases =>
+          (Length (Right) < Max_Length
+           =>
+             Length (Append'Result) = Length (Right) + 1
+               and then
+                 Slice (Append'Result, 2, Length (Right) + 1) =
+                   To_String (Right)
+               and then Element (Append'Result, 1) = Left,
+
+           Length (Right) = Max_Length and then Drop = Strings.Left
+           =>
+             Length (Append'Result) = Max_Length
+               and then To_String (Append'Result) = To_String (Right),
+
+           others  --  Drop = Right
+           =>
+             Length (Append'Result) = Max_Length
+               and then
+                 Slice (Append'Result, 2, Max_Length) =
+                   Slice (Right, 1, Max_Length - 1)
+               and then Element (Append'Result, 1) = Left),
+        Global         => (Proof_In => Max_Length);
 
       procedure Append
         (Source   : in out Bounded_String;
          New_Item : Bounded_String;
          Drop     : Truncation  := Error)
       with
-        Pre    =>
+        Pre            =>
           (if Length (Source) > Max_Length - Length (New_Item)
            then Drop /= Error),
-        Post   =>
-          Length (Source)
-        = Natural'Min (Max_Length, Length (Source)'Old + Length (New_Item)),
-        Global => null;
+        Contract_Cases =>
+          (Length (Source) <= Max_Length - Length (New_Item)
+           =>
+             Length (Source) = Length (Source'Old) + Length (New_Item)
+               and then
+                 Slice (Source, 1, Length (Source'Old)) =
+                   To_String (Source'Old)
+               and then
+                 (if Length (New_Item) > 0 then
+                    Slice (Source, Length (Source'Old) + 1, Length (Source)) =
+                      To_String (New_Item)),
+
+           Length (Source) > Max_Length - Length (New_Item)
+             and then Drop = Left
+           =>
+             Length (Source) = Max_Length
+               and then
+                 (if Length (New_Item) < Max_Length then
+                    Slice (Source, 1, Max_Length - Length (New_Item)) =
+                      Slice (Source'Old,
+                        Length (Source'Old) - Max_Length + Length (New_Item)
+                          + 1,
+                        Length (Source'Old)))
+               and then
+                 Slice (Source, Max_Length - Length (New_Item) + 1, Max_Length)
+                   = To_String (New_Item),
+
+           others  --  Drop = Right
+           =>
+             Length (Source) = Max_Length
+               and then
+                 Slice (Source, 1, Length (Source'Old)) =
+                   To_String (Source'Old)
+               and then
+                 (if Length (Source'Old) < Max_Length then
+                    Slice (Source, Length (Source'Old) + 1, Max_Length) =
+                      Slice (New_Item, 1, Max_Length - Length (Source'Old)))),
+        Global         => (Proof_In => Max_Length);
 
       procedure Append
         (Source   : in out Bounded_String;
          New_Item : String;
          Drop     : Truncation  := Error)
       with
-        Pre    =>
+        Pre            =>
           (if New_Item'Length > Max_Length - Length (Source)
            then Drop /= Error),
-        Post   =>
-          Length (Source)
-        = Natural'Min (Max_Length, Length (Source)'Old + New_Item'Length),
-        Global => null;
+        Contract_Cases =>
+          (Length (Source) <= Max_Length - New_Item'Length
+           =>
+             Length (Source) = Length (Source'Old) + New_Item'Length
+               and then
+                 Slice (Source, 1, Length (Source'Old)) =
+                   To_String (Source'Old)
+               and then
+                 (if New_Item'Length > 0 then
+                    Slice (Source, Length (Source'Old) + 1, Length (Source)) =
+                      New_Item),
+
+           Length (Source) > Max_Length - New_Item'Length
+             and then Drop = Left
+           =>
+             Length (Source) = Max_Length
+               and then
+                 (if New_Item'Length < Max_Length then
+
+                    --  The result is the end of Source followed by New_Item
+
+                    Slice (Source, 1, Max_Length - New_Item'Length) =
+                      Slice (Source'Old,
+                        Length (Source'Old) - Max_Length + New_Item'Length + 1,
+                        Length (Source'Old))
+                    and then
+                      Slice (Source,
+                        Max_Length - New_Item'Length + 1, Max_Length) =
+                          New_Item
+                  else
+                    --  The result is the last Max_Length characters of
+                    --  New_Item.
+
+                    To_String (Source) = New_Item
+                      (New_Item'Last - Max_Length + 1 .. New_Item'Last)),
+
+           others  --  Drop = Right
+           =>
+             Length (Source) = Max_Length
+               and then
+                 Slice (Source, 1, Length (Source'Old)) =
+                   To_String (Source'Old)
+               and then
+                 (if Length (Source'Old) < Max_Length then
+                    Slice (Source, Length (Source'Old) + 1, Max_Length) =
+                      New_Item (New_Item'First
+                        .. Max_Length - Length (Source'Old) - 1
+                          + New_Item'First))),
+        Global         => (Proof_In => Max_Length);
 
       procedure Append
         (Source   : in out Bounded_String;
          New_Item : Character;
          Drop     : Truncation  := Error)
       with
-        Pre    => (if Length (Source) = Max_Length then Drop /= Error),
-        Post   =>
-          Length (Source)
-        = Natural'Min (Max_Length, Length (Source)'Old + 1),
-        Global => null;
+        Pre            => (if Length (Source) = Max_Length then Drop /= Error),
+        Contract_Cases =>
+          (Length (Source) < Max_Length
+           =>
+             Length (Source) = Length (Source'Old) + 1
+               and then
+                 Slice (Source, 1, Length (Source'Old)) =
+                   To_String (Source'Old)
+               and then Element (Source, Length (Source'Old) + 1) = New_Item,
+
+           Length (Source) = Max_Length and then Drop = Right
+           =>
+             Length (Source) = Max_Length
+               and then To_String (Source) = To_String (Source'Old),
+
+           others  --  Drop = Left
+           =>
+             Length (Source) = Max_Length
+               and then
+                 Slice (Source, 1, Max_Length - 1) =
+                   Slice (Source'Old, 2, Max_Length)
+               and then Element (Source, Max_Length) = New_Item),
+        Global         => (Proof_In => Max_Length);
 
       function "&"
         (Left  : Bounded_String;
          Right : Bounded_String) return Bounded_String
       with
         Pre    => Length (Left) <= Max_Length - Length (Right),
-        Post   => Length ("&"'Result) = Length (Left) + Length (Right),
-        Global => null;
+        Post   => Length ("&"'Result) = Length (Left) + Length (Right)
+          and then Slice ("&"'Result, 1, Length (Left)) = To_String (Left)
+          and then
+            (if Length (Right) > 0 then
+               Slice ("&"'Result, Length (Left) + 1, Length ("&"'Result)) =
+                 To_String (Right)),
+        Global => (Proof_In => Max_Length);
 
       function "&"
         (Left  : Bounded_String;
          Right : String) return Bounded_String
       with
         Pre    => Right'Length <= Max_Length - Length (Left),
-        Post   => Length ("&"'Result) = Length (Left) + Right'Length,
-        Global => null;
+        Post   => Length ("&"'Result) = Length (Left) + Right'Length
+          and then Slice ("&"'Result, 1, Length (Left)) = To_String (Left)
+          and then
+            (if Right'Length > 0 then
+               Slice ("&"'Result, Length (Left) + 1, Length ("&"'Result)) =
+                 Right),
+        Global => (Proof_In => Max_Length);
 
       function "&"
         (Left  : String;
          Right : Bounded_String) return Bounded_String
       with
         Pre    => Left'Length <= Max_Length - Length (Right),
-        Post   => Length ("&"'Result) = Left'Length + Length (Right),
-        Global => null;
+        Post   => Length ("&"'Result) = Left'Length + Length (Right)
+          and then Slice ("&"'Result, 1, Left'Length) = Left
+          and then
+            (if Length (Right) > 0 then
+               Slice ("&"'Result, Left'Length + 1, Length ("&"'Result)) =
+                 To_String (Right)),
+        Global => (Proof_In => Max_Length);
 
       function "&"
         (Left  : Bounded_String;
          Right : Character) return Bounded_String
       with
         Pre    => Length (Left) < Max_Length,
-        Post   => Length ("&"'Result) = Length (Left) + 1,
-        Global => null;
+        Post   => Length ("&"'Result) = Length (Left) + 1
+          and then Slice ("&"'Result, 1, Length (Left)) = To_String (Left)
+          and then Element ("&"'Result, Length (Left) + 1) = Right,
+        Global => (Proof_In => Max_Length);
 
       function "&"
         (Left  : Character;
          Right : Bounded_String) return Bounded_String
       with
         Pre    => Length (Right) < Max_Length,
-        Post   => Length ("&"'Result) = 1 + Length (Right),
-        Global => null;
+        Post   => Length ("&"'Result) = 1 + Length (Right)
+          and then Element ("&"'Result, 1) = Left
+          and then
+            Slice ("&"'Result, 2, Length ("&"'Result)) = To_String (Right),
+        Global => (Proof_In => Max_Length);
 
       function Element
         (Source : Bounded_String;
@@ -244,7 +541,10 @@ package Ada.Strings.Bounded is
          By     : Character)
       with
         Pre    => Index <= Length (Source),
-        Post   => Length (Source) = Length (Source)'Old,
+        Post   => Length (Source) = Length (Source'Old)
+          and then (for all K in 1 .. Length (Source) =>
+                      Element (Source, K) =
+                        (if K = Index then By else Element (Source'Old, K))),
         Global => null;
 
       function Slice
@@ -253,7 +553,6 @@ package Ada.Strings.Bounded 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),
         Global => null;
 
       function Bounded_Slice
@@ -262,8 +561,7 @@ package Ada.Strings.Bounded is
          High   : Natural) return Bounded_String
        with
         Pre    => Low - 1 <= Length (Source) and then High <= Length (Source),
-        Post   =>
-          Length (Bounded_Slice'Result) = Natural'Max (0, High - Low + 1),
+        Post   => To_String (Bounded_Slice'Result) = Slice (Source, Low, High),
         Global => null;
       pragma Ada_05 (Bounded_Slice);
 
@@ -274,7 +572,7 @@ package Ada.Strings.Bounded 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) = Slice (Source, Low, High),
         Global => null;
       pragma Ada_05 (Bounded_Slice);
 
@@ -282,90 +580,105 @@ package Ada.Strings.Bounded is
         (Left  : Bounded_String;
          Right : Bounded_String) return Boolean
       with
+        Post   => "="'Result = (To_String (Left) = To_String (Right)),
         Global => null;
 
       function "="
         (Left  : Bounded_String;
          Right : String) return Boolean
       with
+        Post   => "="'Result = (To_String (Left) = Right),
         Global => null;
 
       function "="
         (Left  : String;
          Right : Bounded_String) return Boolean
       with
+        Post   => "="'Result = (Left = To_String (Right)),
         Global => null;
 
       function "<"
         (Left  : Bounded_String;
          Right : Bounded_String) return Boolean
       with
+        Post   => "<"'Result = (To_String (Left) < To_String (Right)),
         Global => null;
 
       function "<"
         (Left  : Bounded_String;
          Right : String) return Boolean
       with
+        Post   => "<"'Result = (To_String (Left) < Right),
         Global => null;
 
       function "<"
         (Left  : String;
          Right : Bounded_String) return Boolean
       with
+        Post   => "<"'Result = (Left < To_String (Right)),
         Global => null;
 
       function "<="
         (Left  : Bounded_String;
          Right : Bounded_String) return Boolean
       with
+        Post   => "<="'Result = (To_String (Left) <= To_String (Right)),
         Global => null;
 
       function "<="
         (Left  : Bounded_String;
          Right : String) return Boolean
       with
+        Post   => "<="'Result = (To_String (Left) <= Right),
         Global => null;
 
       function "<="
         (Left  : String;
          Right : Bounded_String) return Boolean
       with
+        Post   => "<="'Result = (Left <= To_String (Right)),
         Global => null;
 
       function ">"
         (Left  : Bounded_String;
          Right : Bounded_String) return Boolean
       with
+        Post   => ">"'Result = (To_String (Left) > To_String (Right)),
         Global => null;
 
       function ">"
         (Left  : Bounded_String;
          Right : String) return Boolean
       with
+        Post   => ">"'Result = (To_String (Left) > Right),
         Global => null;
 
       function ">"
         (Left  : String;
          Right : Bounded_String) return Boolean
       with
+        Post   => ">"'Result = (Left > To_String (Right)),
         Global => null;
 
       function ">="
         (Left  : Bounded_String;
          Right : Bounded_String) return Boolean
       with
+        Post   => ">="'Result = (To_String (Left) >= To_String (Right)),
         Global => null;
 
       function ">="
         (Left  : Bounded_String;
          Right : String) return Boolean
       with
+        Post   => ">="'Result = (To_String (Left) >= Right),
         Global => null;
 
       function ">="
         (Left  : String;
          Right : Bounded_String) return Boolean
       with
+        Post   => ">="'Result = (Left >= To_String (Right)),
         Global => null;
 
       ----------------------
@@ -378,8 +691,52 @@ package Ada.Strings.Bounded 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  : Bounded_String;
@@ -387,8 +744,52 @@ package Ada.Strings.Bounded 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 : Bounded_String;
@@ -396,7 +797,43 @@ package Ada.Strings.Bounded 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  : Bounded_String;
@@ -405,11 +842,60 @@ package Ada.Strings.Bounded 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
@@ -419,11 +905,61 @@ package Ada.Strings.Bounded 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
@@ -433,23 +969,147 @@ package Ada.Strings.Bounded 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 : Bounded_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 : Bounded_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
@@ -465,7 +1125,7 @@ package Ada.Strings.Bounded 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
@@ -482,8 +1142,53 @@ package Ada.Strings.Bounded 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
@@ -493,7 +1198,51 @@ package Ada.Strings.Bounded 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 --
@@ -503,28 +1252,44 @@ package Ada.Strings.Bounded is
         (Source  : Bounded_String;
          Mapping : Maps.Character_Mapping) return Bounded_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 Bounded_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, Element (Source'Old, K))),
         Global => null;
 
       function Translate
         (Source  : Bounded_String;
          Mapping : Maps.Character_Mapping_Function) return Bounded_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 Bounded_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 (Element (Source'Old, K))),
         Global => null;
 
       ---------------------------------------
@@ -541,23 +1306,128 @@ package Ada.Strings.Bounded is
         Pre            =>
           Low - 1 <= Length (Source)
             and then
-          (if Drop = Error
-           then (if High >= Low
-                 then Low - 1
-                   <= Max_Length - By'Length
-                    - Natural'Max (Length (Source) - High, 0)
-                 else Length (Source) <= Max_Length - By'Length)),
+              (if Drop = Error
+                 then (if High >= Low
+                         then Low - 1
+                           <= Max_Length - By'Length
+                            - Integer'Max (Length (Source) - High, 0)
+                         else Length (Source) <= Max_Length - By'Length)),
         Contract_Cases =>
-          (High >= Low =>
-             Length (Replace_Slice'Result)
-           = Natural'Min
-             (Max_Length,
-              Low - 1 + By'Length + Natural'Max (Length (Source) - High,
-                                                  0)),
-           others      =>
-             Length (Replace_Slice'Result)
-           = Natural'Min (Max_Length, Length (Source) + By'Length)),
-        Global         => null;
+          (Low - 1 <= Max_Length - By'Length
+             - Integer'Max (Length (Source) - Integer'Max (High, Low - 1), 0)
+           =>
+             --  Total length is lower than Max_Length: nothing is dropped
+
+             --  Note that if High < Low, the insertion is done before Low,
+             --  so in all cases the starting position of the slice of Source
+             --  remaining after the replaced Slice is Integer'Max (High + 1,
+             --  Low).
+
+             Length (Replace_Slice'Result) = Low - 1 + By'Length
+               + Integer'Max (Length (Source) - Integer'Max (High, Low - 1), 0)
+               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
+               and then
+                 (if Integer'Max (High, Low - 1) < Length (Source) then
+                    Slice (Replace_Slice'Result,
+                      Low + By'Length, Length (Replace_Slice'Result)) =
+                        Slice (Source,
+                          Integer'Max (High + 1, Low), Length (Source))),
+
+           Low - 1 > Max_Length - By'Length
+             - Integer'Max (Length (Source) - Integer'Max (High, Low - 1), 0)
+             and then Drop = Left
+           =>
+             --  Final_Slice is the length of the slice of Source remaining
+             --  after the replaced part.
+             (declare
+                Final_Slice : constant Natural :=
+                  Integer'Max
+                    (Length (Source) - Integer'Max (High, Low - 1), 0);
+              begin
+                --  The result is of maximal length and ends by the last
+                --  Final_Slice characters of Source.
+
+                Length (Replace_Slice'Result) = Max_Length
+                  and then
+                    (if Final_Slice > 0 then
+                       Slice (Replace_Slice'Result,
+                         Max_Length - Final_Slice + 1, Max_Length) =
+                           Slice (Source,
+                             Integer'Max (High + 1, Low), Length (Source)))
+
+                  --  Depending on when we reach Max_Length, either the first
+                  --  part of Source is fully dropped and By is partly dropped,
+                  --  or By is fully added and the first part of Source is
+                  --  partly dropped.
+
+                  and then
+                   (if Max_Length - Final_Slice - By'Length <= 0 then
+
+                      --  The first (possibly zero) characters of By are
+                      --  dropped.
+
+                      (if Final_Slice < Max_Length then
+                         Slice (Replace_Slice'Result,
+                           1, Max_Length - Final_Slice) =
+                             By (By'Last - Max_Length + Final_Slice + 1
+                                 .. By'Last))
+
+                    else  --  By is added to the result
+
+                      Slice (Replace_Slice'Result,
+                        Max_Length - Final_Slice - By'Length + 1,
+                        Max_Length - Final_Slice) =
+                          By
+
+                        --  The first characters of Source (1 .. Low - 1) are
+                        --  dropped.
+
+                        and then Slice (Replace_Slice'Result, 1,
+                          Max_Length - Final_Slice - By'Length) =
+                            Slice (Source,
+                              Low - Max_Length + Final_Slice + By'Length,
+                              Low - 1))),
+
+           others  --  Drop = Right
+           =>
+             --  The result is of maximal length and starts by the first Low -
+             --  1 characters of Source.
+
+             Length (Replace_Slice'Result) = Max_Length
+               and then
+                 Slice (Replace_Slice'Result, 1, Low - 1) =
+                   Slice (Source, 1, Low - 1)
+
+               --  Depending on when we reach Max_Length, either the last part
+               --  of Source is fully dropped and By is partly dropped, or By
+               --  is fully added and the last part of Source is partly
+               --  dropped.
+
+               and then
+                 (if Low - 1 >= Max_Length - By'Length then
+
+                    --  The last characters of By are dropped
+
+                    Slice (Replace_Slice'Result, Low, Max_Length) =
+                      By (By'First .. Max_Length - Low + By'First)
+
+                  else  --  By is fully added
+
+                    Slice (Replace_Slice'Result, Low, Low + By'Length - 1) = By
+
+                      --  Then Source starting from Integer'Max (High + 1, Low)
+                      --  is added but the last characters are dropped.
+
+                      and then Slice (Replace_Slice'Result,
+                        Low + By'Length, Max_Length) =
+                          Slice (Source, Integer'Max (High + 1, Low),
+                            Integer'Max (High + 1, Low) +
+                              (Max_Length - Low - By'Length)))),
+        Global         => (Proof_In => Max_Length);
 
       procedure Replace_Slice
         (Source   : in out Bounded_String;
@@ -569,23 +1439,120 @@ package Ada.Strings.Bounded is
         Pre            =>
           Low - 1 <= Length (Source)
             and then
-          (if Drop = Error
-           then (if High >= Low
-                 then Low - 1
-                   <= Max_Length - By'Length
-                    - Natural'Max (Length (Source) - High, 0)
-                 else Length (Source) <= Max_Length - By'Length)),
+              (if Drop = Error
+                 then (if High >= Low
+                         then Low - 1
+                           <= Max_Length - By'Length
+                            - Natural'Max (Length (Source) - High, 0)
+                         else Length (Source) <= Max_Length - By'Length)),
         Contract_Cases =>
-          (High >= Low =>
-            Length (Source)
-          = Natural'Min
-              (Max_Length,
-               Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High,
-                                                  0)),
-           others      =>
-             Length (Source)
-           = Natural'Min (Max_Length, Length (Source)'Old + By'Length)),
-        Global         => null;
+          (Low - 1 <= Max_Length - By'Length
+             - Integer'Max (Length (Source) - Integer'Max (High, Low - 1), 0)
+           =>
+             --  Total length is lower than Max_Length: nothing is dropped
+
+             --  Note that if High < Low, the insertion is done before Low,
+             --  so in all cases the starting position of the slice of Source
+             --  remaining after the replaced Slice is Integer'Max (High + 1,
+             --  Low).
+
+             Length (Source) = Low - 1 + By'Length + Integer'Max
+               (Length (Source'Old) - Integer'Max (High, Low - 1), 0)
+               and then
+                 Slice (Source, 1, Low - 1) = Slice (Source'Old, 1, Low - 1)
+               and then Slice (Source, Low, Low - 1 + By'Length) = By
+               and then
+                 (if Integer'Max (High, Low - 1) < Length (Source'Old) then
+                    Slice (Source, Low + By'Length, Length (Source)) =
+                      Slice (Source'Old,
+                        Integer'Max (High + 1, Low), Length (Source'Old))),
+
+           Low - 1 > Max_Length - By'Length
+             - Integer'Max (Length (Source) - Integer'Max (High, Low - 1), 0)
+             and then Drop = Left
+           =>
+             --  Final_Slice is the length of the slice of Source remaining
+             --  after the replaced part.
+             (declare
+                Final_Slice : constant Integer :=
+                  Integer'Max (0,
+                    Length (Source'Old) - Integer'Max (High, Low - 1));
+              begin
+                --  The result is of maximal length and ends by the last
+                --  Final_Slice characters of Source.
+
+                Length (Source) = Max_Length
+                  and then
+                    (if Final_Slice > 0 then
+                       Slice (Source,
+                         Max_Length - Final_Slice + 1, Max_Length) =
+                           Slice (Source'Old,
+                             Integer'Max (High + 1, Low), Length (Source'Old)))
+
+                  --  Depending on when we reach Max_Length, either the first
+                  --  part of Source is fully dropped and By is partly dropped,
+                  --  or By is fully added and the first part of Source is
+                  --  partly dropped.
+
+                  and then
+                    (if Max_Length - Final_Slice - By'Length <= 0 then
+
+                       --  The first characters of By are dropped
+
+                       (if Final_Slice < Max_Length then
+                          Slice (Source, 1, Max_Length - Final_Slice) =
+                            By (By'Last - Max_Length + Final_Slice + 1
+                                .. By'Last))
+
+                     else  --  By is added to the result
+
+                       Slice (Source,
+                         Max_Length - Final_Slice - By'Length + 1,
+                         Max_Length - Final_Slice) = By
+
+                         --  The first characters of Source (1 .. Low - 1) are
+                         --  dropped.
+
+                         and then Slice (Source, 1,
+                           Max_Length - Final_Slice - By'Length) =
+                             Slice (Source'Old,
+                               Low - Max_Length + Final_Slice + By'Length,
+                               Low - 1))),
+
+           others  --  Drop = Right
+           =>
+             --  The result is of maximal length and starts by the first Low -
+             --  1 characters of Source.
+
+             Length (Source) = Max_Length
+               and then
+                 Slice (Source, 1, Low - 1) = Slice (Source'Old, 1, Low - 1)
+
+               --  Depending on when we reach Max_Length, either the last part
+               --  of Source is fully dropped and By is partly dropped, or By
+               --  is fully added and the last part of Source is partly
+               --  dropped.
+
+               and then
+                 (if Low - 1 >= Max_Length - By'Length then
+
+                    --  The last characters of By are dropped
+
+                    Slice (Source, Low, Max_Length) =
+                      By (By'First .. Max_Length - Low + By'First)
+
+                  else  --  By is fully added
+
+                    Slice (Source, Low, Low + By'Length - 1) = By
+
+                      --  Then Source starting from Natural'Max (High + 1, Low)
+                      --  is added but the last characters are dropped.
+
+                      and then Slice (Source, Low + By'Length, Max_Length) =
+                        Slice (Source'Old, Integer'Max (High + 1, Low),
+                          Integer'Max (High + 1, Low) +
+                            (Max_Length - Low - By'Length)))),
+        Global         => (Proof_In => Max_Length);
 
       function Insert
         (Source   : Bounded_String;
@@ -593,14 +1560,114 @@ package Ada.Strings.Bounded is
          New_Item : String;
          Drop     : Truncation := Error) return Bounded_String
       with
-        Pre    =>
+        Pre            =>
           Before - 1 <= Length (Source)
             and then (if New_Item'Length > Max_Length - Length (Source)
                       then Drop /= Error),
-        Post   =>
-          Length (Insert'Result)
-        = Natural'Min (Max_Length, Length (Source) + New_Item'Length),
-        Global => null;
+        Contract_Cases =>
+          (Length (Source) <= Max_Length - New_Item'Length
+           =>
+             --  Total length is lower than Max_Length: nothing is dropped
+
+             Length (Insert'Result) = Length (Source) + New_Item'Length
+               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
+               and then
+                 (if Before <= Length (Source) then
+                    Slice (Insert'Result,
+                      Before + New_Item'Length, Length (Insert'Result)) =
+                        Slice (Source, Before, Length (Source))),
+
+           Length (Source) > Max_Length - New_Item'Length and then Drop = Left
+           =>
+             --  The result is of maximal length and ends by the last
+             --  characters of Source.
+
+             Length (Insert'Result) = Max_Length
+               and then
+                 (if Before <= Length (Source) then
+                    Slice (Insert'Result,
+                      Max_Length - Length (Source) + Before, Max_Length) =
+                        Slice (Source, Before, Length (Source)))
+
+               --  Depending on when we reach Max_Length, either the first part
+               --  of Source is fully dropped and New_Item is partly dropped,
+               --  or New_Item is fully added and the first part of Source is
+               --  partly dropped.
+
+               and then
+                 (if Max_Length - Length (Source) - 1 + Before
+                   < New_Item'Length
+                  then
+                    --  The first characters of New_Item are dropped
+
+                    (if Length (Source) - Before + 1 < Max_Length then
+                       Slice (Insert'Result,
+                         1, Max_Length - Length (Source) - 1 + Before) =
+                           New_Item
+                             (New_Item'Last - Max_Length + Length (Source)
+                               - Before + 2
+                              .. New_Item'Last))
+
+                  else  --  New_Item is added to the result
+
+                    Slice (Insert'Result,
+                      Max_Length - Length (Source) - New_Item'Length + Before,
+                      Max_Length - Length (Source) - 1 + Before) = New_Item
+
+                      --  The first characters of Source (1 .. Before - 1) are
+                      --  dropped.
+
+                      and then Slice (Insert'Result,
+                        1, Max_Length - Length (Source) - New_Item'Length
+                          - 1 + Before) =
+                            Slice (Source,
+                              Length (Source) - Max_Length + New_Item'Length
+                                + 1,
+                              Before - 1)),
+
+           others  --  Drop = Right
+           =>
+             --  The result is of maximal length and starts by the first
+             --  characters of Source.
+
+             Length (Insert'Result) = Max_Length
+               and then
+                 Slice (Insert'Result, 1, Before - 1) =
+                   Slice (Source, 1, Before - 1)
+
+               --  Depending on when we reach Max_Length, either the last part
+               --  of Source is fully dropped and New_Item is partly dropped,
+               --  or New_Item is fully added and the last part of Source is
+               --  partly dropped.
+
+               and then
+                 (if Before - 1 >= Max_Length - New_Item'Length then
+
+                    --  The last characters of New_Item are dropped
+
+                    Slice (Insert'Result, Before, Max_Length) =
+                      New_Item (New_Item'First
+                        .. Max_Length - Before + New_Item'First)
+
+                  else  --  New_Item is fully added
+
+                    Slice (Insert'Result,
+                      Before, Before + New_Item'Length - 1) =
+                        New_Item
+
+                      --  Then Source starting from Before is added but the
+                      --  last characters are dropped.
+
+                      and then Slice (Insert'Result,
+                        Before + New_Item'Length, Max_Length) =
+                          Slice (Source,
+                            Before, Max_Length - New_Item'Length))),
+        Global         => (Proof_In => Max_Length);
 
       procedure Insert
         (Source   : in out Bounded_String;
@@ -608,14 +1675,113 @@ package Ada.Strings.Bounded is
          New_Item : String;
          Drop     : Truncation := Error)
       with
-        Pre    =>
+        Pre            =>
           Before - 1 <= Length (Source)
             and then (if New_Item'Length > Max_Length - Length (Source)
                       then Drop /= Error),
-        Post   =>
-          Length (Source)
-        = Natural'Min (Max_Length, Length (Source)'Old + New_Item'Length),
-        Global => null;
+        Contract_Cases =>
+          (Length (Source) <= Max_Length - New_Item'Length
+           =>
+             --  Total length is lower than Max_Length: nothing is dropped
+
+             Length (Source) = Length (Source'Old) + New_Item'Length
+               and then
+                 Slice (Source, 1, Before - 1) =
+                   Slice (Source'Old, 1, Before - 1)
+               and then
+                 Slice (Source, Before, Before - 1 + New_Item'Length) =
+                   New_Item
+               and then
+                 (if Before <= Length (Source'Old) then
+                    Slice (Source, Before + New_Item'Length, Length (Source)) =
+                      Slice (Source'Old, Before, Length (Source'Old))),
+
+           Length (Source) > Max_Length - New_Item'Length and then Drop = Left
+           =>
+             --  The result is of maximal length and ends by the last
+             --  characters of Source.
+
+             Length (Source) = Max_Length
+               and then
+                 (if Before <= Length (Source'Old) then
+                    Slice (Source,
+                      Max_Length - Length (Source'Old) + Before, Max_Length) =
+                        Slice (Source'Old, Before, Length (Source'Old)))
+
+               --  Depending on when we reach Max_Length, either the first part
+               --  of Source is fully dropped and New_Item is partly dropped,
+               --  or New_Item is fully added and the first part of Source is
+               --  partly dropped.
+
+               and then
+                 (if Max_Length - Length (Source'Old) - 1 + Before
+                   < New_Item'Length
+                  then
+                    --  The first characters of New_Item are dropped
+
+                    (if Length (Source'Old) - Before + 1 < Max_Length then
+                       Slice (Source,
+                         1, Max_Length - Length (Source'Old) - 1 + Before) =
+                           New_Item
+                             (New_Item'Last - Max_Length + Length (Source'Old)
+                               - Before + 2
+                              .. New_Item'Last))
+
+                  else  --  New_Item is added to the result
+
+                    Slice (Source,
+                      Max_Length - Length (Source'Old) - New_Item'Length
+                        + Before,
+                      Max_Length - Length (Source'Old) - 1 + Before) = New_Item
+
+                      --  The first characters of Source (1 .. Before - 1) are
+                      --  dropped.
+
+                      and then Slice (Source, 1,
+                        Max_Length - Length (Source'Old) - New_Item'Length
+                          - 1 + Before) =
+                            Slice (Source'Old,
+                              Length (Source'Old)
+                                - Max_Length + New_Item'Length + 1,
+                              Before - 1)),
+
+           others  --  Drop = Right
+           =>
+             --  The result is of maximal length and starts by the first
+             --  characters of Source.
+
+             Length (Source) = Max_Length
+               and then
+                 Slice (Source, 1, Before - 1) =
+                   Slice (Source'Old, 1, Before - 1)
+
+               --  Depending on when we reach Max_Length, either the last part
+               --  of Source is fully dropped and New_Item is partly dropped,
+               --  or New_Item is fully added and the last part of Source is
+               --  partly dropped.
+
+               and then
+                 (if Before - 1 >= Max_Length - New_Item'Length then
+
+                    --  The last characters of New_Item are dropped
+
+                    Slice (Source, Before, Max_Length) =
+                      New_Item (New_Item'First
+                        .. Max_Length - Before + New_Item'First)
+
+                  else  --  New_Item is fully added
+
+                    Slice (Source, Before, Before + New_Item'Length - 1) =
+                      New_Item
+
+                      --  Then Source starting from Before is added but the
+                      --  last characters are dropped.
+
+                      and then
+                        Slice (Source, Before + New_Item'Length, Max_Length) =
+                          Slice (Source'Old,
+                            Before, Max_Length - New_Item'Length))),
+        Global         => (Proof_In => Max_Length);
 
       function Overwrite
         (Source   : Bounded_String;
@@ -623,16 +1789,86 @@ package Ada.Strings.Bounded is
          New_Item : String;
          Drop     : Truncation := Error) return Bounded_String
       with
-        Pre    =>
+        Pre            =>
           Position - 1 <= Length (Source)
             and then (if New_Item'Length > Max_Length - (Position - 1)
                       then Drop /= Error),
-        Post   =>
-          Length (Overwrite'Result)
-        = Natural'Max
-            (Length (Source),
-             Natural'Min (Max_Length, Position - 1 + New_Item'Length)),
-        Global => null;
+        Contract_Cases =>
+          (Position - 1 <= Max_Length - New_Item'Length
+           =>
+             --  The length is unchanged, unless New_Item overwrites further
+             --  than the end of Source. In this contract case, we suppose
+             --  New_Item doesn't overwrite further than Max_Length.
+
+             Length (Overwrite'Result) =
+               Integer'Max (Length (Source), Position - 1 + New_Item'Length)
+               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))),
+
+           Position - 1 > Max_Length - New_Item'Length and then Drop = Left
+           =>
+             Length (Overwrite'Result) = Max_Length
+
+               --  If a part of the result has to be dropped, it means New_Item
+               --  is overwriting further than the end of Source. Thus the
+               --  result is necessarily ending by New_Item. However, we don't
+               --  know whether New_Item covers all Max_Length characters or
+               --  some characters of Source are remaining at the left.
+
+               and then
+                 (if New_Item'Length > Max_Length then
+
+                    --  New_Item covers all Max_Length characters
+
+                    To_String (Overwrite'Result) =
+                      New_Item
+                        (New_Item'Last - Max_Length + 1 .. New_Item'Last)
+                  else
+                    --  New_Item fully appears at the end
+
+                    Slice (Overwrite'Result,
+                      Max_Length - New_Item'Length + 1, Max_Length) =
+                        New_Item
+
+                      --  The left of Source is cut
+
+                      and then
+                        Slice (Overwrite'Result,
+                          1, Max_Length - New_Item'Length) =
+                            Slice (Source,
+                              Position - Max_Length + New_Item'Length,
+                              Position - 1)),
+
+           others  --  Drop = Right
+           =>
+             --  The result is of maximal length and starts by the first
+             --  characters of Source.
+
+             Length (Overwrite'Result) = Max_Length
+               and then
+                 Slice (Overwrite'Result, 1, Position - 1) =
+                   Slice (Source, 1, Position - 1)
+
+               --  Then New_Item is written until Max_Length
+
+               and then Slice (Overwrite'Result, Position, Max_Length) =
+                 New_Item
+                   (New_Item'First .. Max_Length - Position + New_Item'First)),
+        Global         => (Proof_In => Max_Length);
 
       procedure Overwrite
         (Source    : in out Bounded_String;
@@ -640,16 +1876,85 @@ package Ada.Strings.Bounded is
          New_Item  : String;
          Drop      : Truncation := Error)
       with
-        Pre    =>
+        Pre            =>
           Position - 1 <= Length (Source)
             and then (if New_Item'Length > Max_Length - (Position - 1)
                       then Drop /= Error),
-        Post   =>
-          Length (Source)
-        = Natural'Max
-            (Length (Source)'Old,
-             Natural'Min (Max_Length, Position - 1 + New_Item'Length)),
-        Global => null;
+        Contract_Cases =>
+          (Position - 1 <= Max_Length - New_Item'Length
+           =>
+             --  The length of Source is unchanged, unless New_Item overwrites
+             --  further than the end of Source. In this contract case, we
+             --  suppose New_Item doesn't overwrite further than Max_Length.
+
+             Length (Source) = Integer'Max
+               (Length (Source'Old), Position - 1 + New_Item'Length)
+               and then
+                 Slice (Source, 1, Position - 1) =
+                   Slice (Source'Old, 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'Old,
+                          Position + New_Item'Length, Length (Source'Old))),
+
+           Position - 1 > Max_Length - New_Item'Length and then Drop = Left
+           =>
+             Length (Source) = Max_Length
+
+               --  If a part of the result has to be dropped, it means New_Item
+               --  is overwriting further than the end of Source. Thus the
+               --  result is necessarily ending by New_Item. However, we don't
+               --  know whether New_Item covers all Max_Length characters or
+               --  some characters of Source are remaining at the left.
+
+               and then
+                 (if New_Item'Length > Max_Length then
+
+                    --  New_Item covers all Max_Length characters
+
+                    To_String (Source) =
+                      New_Item
+                        (New_Item'Last - Max_Length + 1 .. New_Item'Last)
+                  else
+                    --  New_Item fully appears at the end
+
+                    Slice (Source,
+                      Max_Length - New_Item'Length + 1, Max_Length) =
+                        New_Item
+
+                      --  The left of Source is cut
+
+                      and then
+                        Slice (Source, 1, Max_Length - New_Item'Length) =
+                          Slice (Source'Old,
+                            Position - Max_Length + New_Item'Length,
+                            Position - 1)),
+
+           others  --  Drop = Right
+           =>
+             --  The result is of maximal length and starts by the first
+             --  characters of Source.
+
+             Length (Source) = Max_Length
+               and then
+                 Slice (Source, 1, Position - 1) =
+                   Slice (Source'Old, 1, Position - 1)
+
+               --  New_Item is written until Max_Length
+
+               and then Slice (Source, Position, Max_Length) =
+                 New_Item
+                   (New_Item'First .. Max_Length - Position + New_Item'First)),
+        Global         => (Proof_In => Max_Length);
 
       function Delete
         (Source  : Bounded_String;
@@ -657,13 +1962,20 @@ package Ada.Strings.Bounded is
          Through : Natural) return Bounded_String
       with
         Pre            =>
-          (if Through <= From then From - 1 <= Length (Source)),
+          (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
@@ -672,12 +1984,19 @@ package Ada.Strings.Bounded is
          Through : Natural)
       with
         Pre            =>
-          (if Through <= From then From - 1 <= Length (Source)),
+          (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) = Slice (Source'Old, 1, From - 1)
+               and then
+                 (if Through < Length (Source) then
+                    Slice (Source, From, Length (Source)) =
+                      Slice (Source'Old, Through + 1, Length (Source'Old))),
            others          =>
-             Length (Source) = Length (Source)'Old),
+             Source = Source'Old),
         Global         => null;
 
       ---------------------------------
@@ -688,31 +2007,111 @@ package Ada.Strings.Bounded is
         (Source : Bounded_String;
          Side   : Trim_End) return Bounded_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 Bounded_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'Old, Forward));
+                High : constant Positive :=
+                  (if Side = Left then Length (Source'Old)
+                   else Index_Non_Blank (Source'Old, Backward));
+              begin
+                To_String (Source) = Slice (Source'Old, Low, High))),
+        Global         => null;
 
       function Trim
         (Source : Bounded_String;
          Left   : Maps.Character_Set;
          Right  : Maps.Character_Set) return Bounded_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 Bounded_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'Old, Left, Outside, Forward);
+                High : constant Positive :=
+                  Index (Source'Old, Right, Outside, Backward);
+              begin
+                To_String (Source) = Slice (Source'Old, Low, High))),
+        Global         => null;
 
       function Head
         (Source : Bounded_String;
@@ -720,9 +2119,55 @@ package Ada.Strings.Bounded is
          Pad    : Character := Space;
          Drop   : Truncation := Error) return Bounded_String
       with
-        Pre    => (if Count > Max_Length then Drop /= Error),
-        Post   => Length (Head'Result) = Natural'Min (Max_Length, Count),
-        Global => null;
+        Pre            => (if Count > Max_Length then Drop /= Error),
+        Contract_Cases =>
+          (Count <= Length (Source)
+           =>
+             --  Source is cut
+
+             To_String (Head'Result) = Slice (Source, 1, Count),
+
+           Count > Length (Source) and then Count <= Max_Length
+           =>
+             --  Source is followed by Pad characters
+
+             Length (Head'Result) = Count
+               and then
+                 Slice (Head'Result, 1, Length (Source)) = To_String (Source)
+               and then
+                 Slice (Head'Result, Length (Source) + 1, Count) =
+                   (1 .. Count - Length (Source) => Pad),
+
+           Count > Max_Length and then Drop = Right
+           =>
+             --  Source is followed by Pad characters
+
+             Length (Head'Result) = Max_Length
+               and then
+                 Slice (Head'Result, 1, Length (Source)) = To_String (Source)
+               and then
+                 Slice (Head'Result, Length (Source) + 1, Max_Length) =
+                   (1 .. Max_Length - Length (Source) => Pad),
+
+           Count - Length (Source) > Max_Length and then Drop = Left
+           =>
+             --  Source is fully dropped at the left
+
+             To_String (Head'Result) = (1 .. Max_Length => Pad),
+
+           others
+           =>
+             --  Source is partly dropped at the left
+
+             Length (Head'Result) = Max_Length
+               and then
+                 Slice (Head'Result, 1, Max_Length - Count + Length (Source)) =
+                   Slice (Source, Count - Max_Length + 1, Length (Source))
+               and then
+                 Slice (Head'Result,
+                   Max_Length - Count + Length (Source) + 1, Max_Length) =
+                     (1 .. Count - Length (Source) => Pad)),
+        Global         => (Proof_In => Max_Length);
 
       procedure Head
         (Source : in out Bounded_String;
@@ -730,9 +2175,58 @@ package Ada.Strings.Bounded is
          Pad    : Character  := Space;
          Drop   : Truncation := Error)
       with
-        Pre    => (if Count > Max_Length then Drop /= Error),
-        Post   => Length (Source) = Natural'Min (Max_Length, Count),
-        Global => null;
+        Pre            => (if Count > Max_Length then Drop /= Error),
+        Contract_Cases =>
+          (Count <= Length (Source)
+           =>
+             --  Source is cut
+
+             To_String (Source) = Slice (Source'Old, 1, Count),
+
+           Count > Length (Source) and then Count <= Max_Length
+           =>
+             --  Source is followed by Pad characters
+
+             Length (Source) = Count
+               and then
+                 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),
+
+           Count > Max_Length and then Drop = Right
+           =>
+             --  Source is followed by Pad characters
+
+             Length (Source) = Max_Length
+               and then
+                 Slice (Source, 1, Length (Source'Old)) =
+                   To_String (Source'Old)
+               and then
+                 Slice (Source, Length (Source'Old) + 1, Max_Length) =
+                   (1 .. Max_Length - Length (Source'Old) => Pad),
+
+           Count - Length (Source) > Max_Length and then Drop = Left
+           =>
+             --  Source is fully dropped on the left
+
+             To_String (Source) = (1 .. Max_Length => Pad),
+
+           others
+           =>
+             --  Source is partly dropped on the left
+
+             Length (Source) = Max_Length
+               and then
+                 Slice (Source, 1, Max_Length - Count + Length (Source'Old)) =
+                   Slice (Source'Old,
+                     Count - Max_Length + 1, Length (Source'Old))
+               and then
+                 Slice (Source,
+                   Max_Length - Count + Length (Source'Old) + 1, Max_Length) =
+                     (1 .. Count - Length (Source'Old) => Pad)),
+        Global         => (Proof_In => Max_Length);
 
       function Tail
         (Source : Bounded_String;
@@ -740,9 +2234,61 @@ package Ada.Strings.Bounded is
          Pad    : Character  := Space;
          Drop   : Truncation := Error) return Bounded_String
       with
-        Pre    => (if Count > Max_Length then Drop /= Error),
-        Post   => Length (Tail'Result) = Natural'Min (Max_Length, Count),
-        Global => null;
+        Pre            => (if Count > Max_Length then Drop /= Error),
+        Contract_Cases =>
+          (Count < Length (Source)
+           =>
+             --  Source is cut
+
+             (if Count > 0 then
+                To_String (Tail'Result) =
+                  Slice (Source, Length (Source) - Count + 1, Length (Source))
+              else Length (Tail'Result) = 0),
+
+           Count >= Length (Source) and then Count < Max_Length
+           =>
+             --  Source is preceded by Pad characters
+
+             Length (Tail'Result) = Count
+               and then
+                 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),
+
+           Count >= Max_Length and then Drop = Left
+           =>
+             --  Source is preceded by Pad characters
+
+             Length (Tail'Result) = Max_Length
+               and then
+                 Slice (Tail'Result, 1, Max_Length - Length (Source)) =
+                   (1 .. Max_Length - Length (Source) => Pad)
+               and then
+                 (if Length (Source) > 0 then
+                    Slice (Tail'Result,
+                      Max_Length - Length (Source) + 1, Max_Length) =
+                        To_String (Source)),
+
+           Count - Length (Source) >= Max_Length and then Drop /= Left
+           =>
+             --  Source is fully dropped on the right
+
+             To_String (Tail'Result) = (1 .. Max_Length => Pad),
+
+           others
+           =>
+             --  Source is partly dropped on the right
+
+             Length (Tail'Result) = Max_Length
+               and then
+                 Slice (Tail'Result, 1, Count - Length (Source)) =
+                   (1 .. Count - Length (Source) => Pad)
+               and then
+                 Slice (Tail'Result, Count - Length (Source) + 1, Max_Length) =
+                   Slice (Source, 1, Max_Length - Count + Length (Source))),
+        Global         => (Proof_In => Max_Length);
 
       procedure Tail
         (Source : in out Bounded_String;
@@ -750,9 +2296,63 @@ package Ada.Strings.Bounded is
          Pad    : Character  := Space;
          Drop   : Truncation := Error)
       with
-        Pre    => (if Count > Max_Length then Drop /= Error),
-        Post   => Length (Source) = Natural'Min (Max_Length, Count),
-        Global => null;
+        Pre            => (if Count > Max_Length then Drop /= Error),
+        Contract_Cases =>
+          (Count < Length (Source)
+           =>
+             --  Source is cut
+
+             (if Count > 0 then
+                To_String (Source) =
+                  Slice (Source'Old,
+                    Length (Source'Old) - Count + 1, Length (Source'Old))
+              else Length (Source) = 0),
+
+           Count >= Length (Source) and then Count < Max_Length
+           =>
+             --  Source is preceded by Pad characters
+
+             Length (Source) = Count
+               and then
+                 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),
+
+           Count >= Max_Length and then Drop = Left
+           =>
+             --  Source is preceded by Pad characters
+
+             Length (Source) = Max_Length
+               and then
+                 Slice (Source, 1, Max_Length - Length (Source'Old)) =
+                   (1 .. Max_Length - Length (Source'Old) => Pad)
+               and then
+                 (if Length (Source'Old) > 0 then
+                    Slice (Source,
+                      Max_Length - Length (Source'Old) + 1, Max_Length) =
+                        To_String (Source'Old)),
+
+           Count - Length (Source) >= Max_Length and then Drop /= Left
+           =>
+             --  Source is fully dropped at the right
+
+             To_String (Source) = (1 .. Max_Length => Pad),
+
+           others
+           =>
+             --  Source is partly dropped at the right
+
+             Length (Source) = Max_Length
+               and then
+                 Slice (Source, 1, Count - Length (Source'Old)) =
+                   (1 .. Count - Length (Source'Old) => Pad)
+               and then
+                 Slice (Source, Count - Length (Source'Old) + 1, Max_Length) =
+                   Slice (Source'Old,
+                     1, Max_Length - Count + Length (Source'Old))),
+        Global         => (Proof_In => Max_Length);
 
       ------------------------------------
       -- String Constructor Subprograms --
@@ -763,24 +2363,36 @@ package Ada.Strings.Bounded is
          Right : Character) return Bounded_String
       with
         Pre    => Left <= Max_Length,
-        Post   => Length ("*"'Result) = Left,
-        Global => null;
+        Post   => To_String ("*"'Result) = (1 .. Left => Right),
+        Global => Max_Length;
 
       function "*"
         (Left  : Natural;
          Right : String) return Bounded_String
       with
         Pre    => (if Left /= 0 then Right'Length <= Max_Length / Left),
-        Post   => Length ("*"'Result) = Left * Right'Length,
-        Global => null;
+        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 => Max_Length;
 
       function "*"
         (Left  : Natural;
          Right : Bounded_String) return Bounded_String
       with
         Pre    => (if Left /= 0 then Length (Right) <= Max_Length / Left),
-        Post   => Length ("*"'Result) = Left * Length (Right),
-        Global => null;
+        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 => (Proof_In => Max_Length);
 
       function Replicate
         (Count : Natural;
@@ -789,37 +2401,80 @@ package Ada.Strings.Bounded is
       with
         Pre    => (if Count > Max_Length then Drop /= Error),
         Post   =>
-          Length (Replicate'Result)
-        = Natural'Min (Max_Length, Count),
-        Global => null;
+          To_String (Replicate'Result) =
+            (1 .. Natural'Min (Max_Length, Count) => Item),
+        Global => Max_Length;
 
       function Replicate
         (Count : Natural;
          Item  : String;
          Drop  : Truncation := Error) return Bounded_String
       with
-        Pre    =>
-          (if Item'Length /= 0
-             and then Count > Max_Length / Item'Length
+        Pre            =>
+          (if Count /= 0 and then Item'Length > Max_Length / Count
            then Drop /= Error),
-        Post   =>
-          Length (Replicate'Result)
-        = Natural'Min (Max_Length, Count * Item'Length),
-        Global => null;
+        Contract_Cases =>
+          (Count = 0 or else Item'Length <= Max_Length / Count
+           =>
+             Length (Replicate'Result) = Count * Item'Length
+               and then
+                 (if Item'Length > 0 then
+                    (for all K in 1 .. Count * Item'Length =>
+                       Element (Replicate'Result, K) =
+                         Item (Item'First + (K - 1) mod Item'Length))),
+           Count /= 0
+             and then Item'Length > Max_Length / Count
+             and then Drop = Right
+           =>
+             Length (Replicate'Result) = Max_Length
+               and then
+                 (for all K in 1 .. Max_Length =>
+                    Element (Replicate'Result, K) =
+                      Item (Item'First + (K - 1) mod Item'Length)),
+           others  --  Drop = Left
+           =>
+             Length (Replicate'Result) = Max_Length
+               and then
+                 (for all K in 1 .. Max_Length =>
+                    Element (Replicate'Result, K) =
+                      Item (Item'Last - (Max_Length - K) mod Item'Length))),
+        Global         => Max_Length;
 
       function Replicate
         (Count : Natural;
          Item  : Bounded_String;
          Drop  : Truncation := Error) return Bounded_String
       with
-        Pre    =>
-          (if Length (Item) /= 0
-             and then Count > Max_Length / Length (Item)
+        Pre            =>
+          (if Count /= 0 and then Length (Item) > Max_Length / Count
            then Drop /= Error),
-        Post   =>
-          Length (Replicate'Result)
-        = Natural'Min (Max_Length, Count * Length (Item)),
-        Global => null;
+        Contract_Cases =>
+          ((if Count /= 0 then Length (Item) <= Max_Length / Count)
+           =>
+             Length (Replicate'Result) = Count * Length (Item)
+               and then
+                 (if Length (Item) > 0 then
+                    (for all K in 1 .. Count * Length (Item) =>
+                       Element (Replicate'Result, K) =
+                         Element (Item, 1 + (K - 1) mod Length (Item)))),
+           Count /= 0
+             and then Length (Item) > Max_Length / Count
+             and then Drop = Right
+           =>
+             Length (Replicate'Result) = Max_Length
+               and then
+                 (for all K in 1 .. Max_Length =>
+                    Element (Replicate'Result, K) =
+                      Element (Item, 1 + (K - 1) mod Length (Item))),
+           others  --  Drop = Left
+           =>
+             Length (Replicate'Result) = Max_Length
+               and then
+                 (for all K in 1 .. Max_Length =>
+                    Element (Replicate'Result, K) =
+                      Element (Item,
+                        Length (Item) - (Max_Length - K) mod Length (Item)))),
+        Global         => (Proof_In => Max_Length);
 
    private
       --  Most of the implementation is in the separate non generic package
@@ -843,7 +2498,8 @@ package Ada.Strings.Bounded is
       --  the generic instantiation is compatible with the Super_String
       --  type declared in the Superbounded package.
 
-      function From_String (Source : String) return Bounded_String;
+      function From_String (Source : String) return Bounded_String
+      with Pre => Source'Length <= Max_Length;
       --  Private routine used only by Stream_Convert
 
       pragma Stream_Convert (Bounded_String, From_String, To_String);
diff --git a/gcc/ada/libgnat/a-strfix.ads b/gcc/ada/libgnat/a-strfix.ads
index 1a5ee94..168a8e0 100644
--- a/gcc/ada/libgnat/a-strfix.ads
+++ b/gcc/ada/libgnat/a-strfix.ads
@@ -382,7 +382,7 @@ package Ada.Strings.Fixed with SPARK_Mode is
         =>
           Index'Result = 0,
 
-        --  Otherwise, a index in the range of Source is returned
+        --  Otherwise, an index in the range of Source is returned
 
         others
         =>
@@ -392,7 +392,7 @@ package Ada.Strings.Fixed with SPARK_Mode is
           Index'Result in Source'Range
 
             --  The character at the returned index satisfies the property
-            --  Test on Set
+            --  Test on Set.
 
             and then
               (Test = Inside)
@@ -433,7 +433,7 @@ package Ada.Strings.Fixed with SPARK_Mode is
         =>
           Index'Result = 0,
 
-        --  Otherwise, a index in the considered range of Source is returned
+        --  Otherwise, an index in the considered range of Source is returned
 
         others
         =>
diff --git a/gcc/ada/libgnat/a-strsea.ads b/gcc/ada/libgnat/a-strsea.ads
index 4396747..f4e7d36 100644
--- a/gcc/ada/libgnat/a-strsea.ads
+++ b/gcc/ada/libgnat/a-strsea.ads
@@ -213,7 +213,7 @@ package Ada.Strings.Search with SPARK_Mode is
         =>
           Index'Result = 0,
 
-        --  Otherwise, a index in the range of Source is returned
+        --  Otherwise, an index in the range of Source is returned
 
         others =>
 
@@ -222,7 +222,7 @@ package Ada.Strings.Search with SPARK_Mode is
           Index'Result in Source'Range
 
             --  The character at the returned index satisfies the property
-            --  Test on Set
+            --  Test on Set.
 
             and then (Test = Inside)
               = Ada.Strings.Maps.Is_In (Source (Index'Result), Set)
@@ -377,7 +377,7 @@ package Ada.Strings.Search with SPARK_Mode is
         =>
           Index'Result = 0,
 
-        --  Otherwise, a index in the considered range of Source is returned
+        --  Otherwise, an index in the considered range of Source is returned
 
         others =>
 
diff --git a/gcc/ada/libgnat/a-strsup.adb b/gcc/ada/libgnat/a-strsup.adb
index 1e85cc2..a94d6ca 100644
--- a/gcc/ada/libgnat/a-strsup.adb
+++ b/gcc/ada/libgnat/a-strsup.adb
@@ -29,10 +29,17 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
-with Ada.Strings.Maps;   use Ada.Strings.Maps;
-with Ada.Strings.Search;
+--  Ghost code, loop invariants and assertions in this unit are meant for
+--  analysis only, not for run-time checking, as it would be too costly
+--  otherwise. This is enforced by setting the assertion policy to Ignore.
 
-package body Ada.Strings.Superbounded is
+pragma Assertion_Policy (Ghost          => Ignore,
+                         Loop_Invariant => Ignore,
+                         Assert         => Ignore);
+
+with Ada.Strings.Maps; use Ada.Strings.Maps;
+
+package body Ada.Strings.Superbounded with SPARK_Mode is
 
    ------------
    -- Concat --
@@ -53,9 +60,13 @@ package body Ada.Strings.Superbounded is
                raise Ada.Strings.Length_Error;
             end if;
 
-            Result.Current_Length := Nlen;
             Result.Data (1 .. Llen) := Left.Data (1 .. Llen);
-            Result.Data (Llen + 1 .. Nlen) := Right.Data (1 .. Rlen);
+
+            if Rlen > 0 then
+               Result.Data (Llen + 1 .. Nlen) := Right.Data (1 .. Rlen);
+            end if;
+
+            Result.Current_Length := Nlen;
          end;
       end return;
    end Concat;
@@ -74,9 +85,13 @@ package body Ada.Strings.Superbounded is
                raise Ada.Strings.Length_Error;
             end if;
 
-            Result.Current_Length := Nlen;
             Result.Data (1 .. Llen) := Left.Data (1 .. Llen);
-            Result.Data (Llen + 1 .. Nlen) := Right;
+
+            if Right'Length > 0 then
+               Result.Data (Llen + 1 .. Nlen) := Super_String_Data (Right);
+            end if;
+
+            Result.Current_Length := Nlen;
          end;
       end return;
    end Concat;
@@ -97,9 +112,13 @@ package body Ada.Strings.Superbounded is
                raise Ada.Strings.Length_Error;
             end if;
 
+            Result.Data (1 .. Llen) := Super_String_Data (Left);
+
+            if Rlen > 0 then
+               Result.Data (Llen + 1 .. Nlen) := Right.Data (1 .. Rlen);
+            end if;
+
             Result.Current_Length := Nlen;
-            Result.Data (1 .. Llen) := Left;
-            Result.Data (Llen + 1 .. Nlen) := Right.Data (1 .. Rlen);
          end;
       end return;
    end Concat;
@@ -117,9 +136,9 @@ package body Ada.Strings.Superbounded is
                raise Ada.Strings.Length_Error;
             end if;
 
-            Result.Current_Length := Llen + 1;
             Result.Data (1 .. Llen) := Left.Data (1 .. Llen);
-            Result.Data (Result.Current_Length) := Right;
+            Result.Data (Llen + 1) := Right;
+            Result.Current_Length := Llen + 1;
          end;
       end return;
    end Concat;
@@ -137,10 +156,9 @@ package body Ada.Strings.Superbounded is
                raise Ada.Strings.Length_Error;
             end if;
 
-            Result.Current_Length := Rlen + 1;
             Result.Data (1) := Left;
-            Result.Data (2 .. Result.Current_Length) :=
-              Right.Data (1 .. Rlen);
+            Result.Data (2 .. Rlen + 1) := Right.Data (1 .. Rlen);
+            Result.Current_Length := Rlen + 1;
          end;
       end return;
    end Concat;
@@ -154,9 +172,7 @@ package body Ada.Strings.Superbounded is
       Right : Super_String) return Boolean
    is
    begin
-      return Left.Current_Length = Right.Current_Length
-        and then Left.Data (1 .. Left.Current_Length) =
-                   Right.Data (1 .. Right.Current_Length);
+      return Super_To_String (Left) = Super_To_String (Right);
    end "=";
 
    function Equal
@@ -164,8 +180,7 @@ package body Ada.Strings.Superbounded is
       Right : String) return Boolean
    is
    begin
-      return Left.Current_Length = Right'Length
-        and then Left.Data (1 .. Left.Current_Length) = Right;
+      return Super_To_String (Left) = Right;
    end Equal;
 
    function Equal
@@ -173,8 +188,7 @@ package body Ada.Strings.Superbounded is
       Right : Super_String) return Boolean
    is
    begin
-      return Left'Length = Right.Current_Length
-        and then Left = Right.Data (1 .. Right.Current_Length);
+      return Left = Super_To_String (Right);
    end Equal;
 
    -------------
@@ -186,8 +200,7 @@ package body Ada.Strings.Superbounded is
       Right : Super_String) return Boolean
    is
    begin
-      return Left.Data (1 .. Left.Current_Length) >
-               Right.Data (1 .. Right.Current_Length);
+      return Super_To_String (Left) > Super_To_String (Right);
    end Greater;
 
    function Greater
@@ -195,7 +208,7 @@ package body Ada.Strings.Superbounded is
       Right : String) return Boolean
    is
    begin
-      return Left.Data (1 .. Left.Current_Length) > Right;
+      return Super_To_String (Left) > Right;
    end Greater;
 
    function Greater
@@ -203,7 +216,7 @@ package body Ada.Strings.Superbounded is
       Right : Super_String) return Boolean
    is
    begin
-      return Left > Right.Data (1 .. Right.Current_Length);
+      return Left > Super_To_String (Right);
    end Greater;
 
    ----------------------
@@ -215,8 +228,7 @@ package body Ada.Strings.Superbounded is
       Right : Super_String) return Boolean
    is
    begin
-      return Left.Data (1 .. Left.Current_Length) >=
-               Right.Data (1 .. Right.Current_Length);
+      return Super_To_String (Left) >= Super_To_String (Right);
    end Greater_Or_Equal;
 
    function Greater_Or_Equal
@@ -224,7 +236,7 @@ package body Ada.Strings.Superbounded is
       Right : String) return Boolean
    is
    begin
-      return Left.Data (1 .. Left.Current_Length) >= Right;
+      return Super_To_String (Left) >= Right;
    end Greater_Or_Equal;
 
    function Greater_Or_Equal
@@ -232,7 +244,7 @@ package body Ada.Strings.Superbounded is
       Right : Super_String) return Boolean
    is
    begin
-      return Left >= Right.Data (1 .. Right.Current_Length);
+      return Left >= Super_To_String (Right);
    end Greater_Or_Equal;
 
    ----------
@@ -244,8 +256,7 @@ package body Ada.Strings.Superbounded is
       Right : Super_String) return Boolean
    is
    begin
-      return Left.Data (1 .. Left.Current_Length) <
-               Right.Data (1 .. Right.Current_Length);
+      return Super_To_String (Left) < Super_To_String (Right);
    end Less;
 
    function Less
@@ -253,7 +264,7 @@ package body Ada.Strings.Superbounded is
       Right : String) return Boolean
    is
    begin
-      return Left.Data (1 .. Left.Current_Length) < Right;
+      return Super_To_String (Left) < Right;
    end Less;
 
    function Less
@@ -261,7 +272,7 @@ package body Ada.Strings.Superbounded is
       Right : Super_String) return Boolean
    is
    begin
-      return Left < Right.Data (1 .. Right.Current_Length);
+      return Left < Super_To_String (Right);
    end Less;
 
    -------------------
@@ -273,8 +284,7 @@ package body Ada.Strings.Superbounded is
       Right : Super_String) return Boolean
    is
    begin
-      return Left.Data (1 .. Left.Current_Length) <=
-               Right.Data (1 .. Right.Current_Length);
+      return Super_To_String (Left) <= Super_To_String (Right);
    end Less_Or_Equal;
 
    function Less_Or_Equal
@@ -282,7 +292,7 @@ package body Ada.Strings.Superbounded is
       Right : String) return Boolean
    is
    begin
-      return Left.Data (1 .. Left.Current_Length) <= Right;
+      return Super_To_String (Left) <= Right;
    end Less_Or_Equal;
 
    function Less_Or_Equal
@@ -290,7 +300,7 @@ package body Ada.Strings.Superbounded is
       Right : Super_String) return Boolean
    is
    begin
-      return Left <= Right.Data (1 .. Right.Current_Length);
+      return Left <= Super_To_String (Right);
    end Less_Or_Equal;
 
    ----------------------
@@ -307,20 +317,20 @@ package body Ada.Strings.Superbounded is
 
    begin
       if Slen <= Max_Length then
+         Target.Data (1 .. Slen) := Super_String_Data (Source);
          Target.Current_Length := Slen;
-         Target.Data (1 .. Slen) := Source;
 
       else
          case Drop is
             when Strings.Right =>
+               Target.Data (1 .. Max_Length) := Super_String_Data
+                 (Source (Source'First .. Source'First - 1 + Max_Length));
                Target.Current_Length := Max_Length;
-               Target.Data (1 .. Max_Length) :=
-                 Source (Source'First .. Source'First - 1 + Max_Length);
 
             when Strings.Left =>
+               Target.Data (1 .. Max_Length) := Super_String_Data
+                 (Source (Source'Last - (Max_Length - 1) .. Source'Last));
                Target.Current_Length := Max_Length;
-               Target.Data (1 .. Max_Length) :=
-                 Source (Source'Last - (Max_Length - 1) .. Source'Last);
 
             when Strings.Error =>
                raise Ada.Strings.Length_Error;
@@ -343,17 +353,18 @@ package body Ada.Strings.Superbounded is
       Result : Super_String (Max_Length);
       Llen   : constant Natural := Left.Current_Length;
       Rlen   : constant Natural := Right.Current_Length;
-      Nlen   : constant Natural := Llen + Rlen;
 
    begin
-      if Nlen <= Max_Length then
-         Result.Current_Length := Nlen;
+      if Llen <= Max_Length - Rlen then
          Result.Data (1 .. Llen) := Left.Data (1 .. Llen);
-         Result.Data (Llen + 1 .. Nlen) := Right.Data (1 .. Rlen);
 
-      else
-         Result.Current_Length := Max_Length;
+         if Rlen > 0 then
+            Result.Data (Llen + 1 .. Llen + Rlen) := Right.Data (1 .. Rlen);
+         end if;
+
+         Result.Current_Length := Llen + Rlen;
 
+      else
          case Drop is
             when Strings.Right =>
                if Llen >= Max_Length then -- only case is Llen = Max_Length
@@ -379,6 +390,8 @@ package body Ada.Strings.Superbounded is
             when Strings.Error =>
                raise Ada.Strings.Length_Error;
          end case;
+
+         Result.Current_Length := Max_Length;
       end if;
 
       return Result;
@@ -392,16 +405,15 @@ package body Ada.Strings.Superbounded is
       Max_Length : constant Positive := Source.Max_Length;
       Llen       : constant Natural := Source.Current_Length;
       Rlen       : constant Natural := New_Item.Current_Length;
-      Nlen       : constant Natural := Llen + Rlen;
 
    begin
-      if Nlen <= Max_Length then
-         Source.Current_Length := Nlen;
-         Source.Data (Llen + 1 .. Nlen) := New_Item.Data (1 .. Rlen);
+      if Llen <= Max_Length - Rlen then
+         if Rlen > 0 then
+            Source.Data (Llen + 1 .. Llen + Rlen) := New_Item.Data (1 .. Rlen);
+            Source.Current_Length := Llen + Rlen;
+         end if;
 
       else
-         Source.Current_Length := Max_Length;
-
          case Drop is
             when Strings.Right =>
                if Llen < Max_Length then
@@ -423,6 +435,8 @@ package body Ada.Strings.Superbounded is
             when Strings.Error =>
                raise Ada.Strings.Length_Error;
          end case;
+
+         Source.Current_Length := Max_Length;
       end if;
 
    end Super_Append;
@@ -438,17 +452,18 @@ package body Ada.Strings.Superbounded is
       Result : Super_String (Max_Length);
       Llen   : constant Natural := Left.Current_Length;
       Rlen   : constant Natural := Right'Length;
-      Nlen   : constant Natural := Llen + Rlen;
 
    begin
-      if Nlen <= Max_Length then
-         Result.Current_Length := Nlen;
+      if Llen <= Max_Length - Rlen then
          Result.Data (1 .. Llen) := Left.Data (1 .. Llen);
-         Result.Data (Llen + 1 .. Nlen) := Right;
 
-      else
-         Result.Current_Length := Max_Length;
+         if Rlen > 0 then
+            Result.Data (Llen + 1 .. Llen + Rlen) := Super_String_Data (Right);
+         end if;
+
+         Result.Current_Length := Llen + Rlen;
 
+      else
          case Drop is
             when Strings.Right =>
                if Llen >= Max_Length then -- only case is Llen = Max_Length
@@ -456,27 +471,29 @@ package body Ada.Strings.Superbounded is
 
                else
                   Result.Data (1 .. Llen) := Left.Data (1 .. Llen);
-                  Result.Data (Llen + 1 .. Max_Length) :=
-                    Right (Right'First .. Right'First - 1 +
-                             Max_Length - Llen);
+                  Result.Data (Llen + 1 .. Max_Length) := Super_String_Data
+                    (Right
+                       (Right'First .. Right'First - 1 - Llen + Max_Length));
 
                end if;
 
             when Strings.Left =>
                if Rlen >= Max_Length then
-                  Result.Data (1 .. Max_Length) :=
-                    Right (Right'Last - (Max_Length - 1) .. Right'Last);
+                  Result.Data (1 .. Max_Length) := Super_String_Data
+                    (Right (Right'Last - (Max_Length - 1) .. Right'Last));
 
                else
                   Result.Data (1 .. Max_Length - Rlen) :=
                     Left.Data (Llen - (Max_Length - Rlen - 1) .. Llen);
                   Result.Data (Max_Length - Rlen + 1 .. Max_Length) :=
-                    Right;
+                    Super_String_Data (Right);
                end if;
 
             when Strings.Error =>
                raise Ada.Strings.Length_Error;
          end case;
+
+         Result.Current_Length := Max_Length;
       end if;
 
       return Result;
@@ -490,40 +507,42 @@ package body Ada.Strings.Superbounded is
       Max_Length : constant Positive := Source.Max_Length;
       Llen   : constant Natural := Source.Current_Length;
       Rlen   : constant Natural := New_Item'Length;
-      Nlen   : constant Natural := Llen + Rlen;
 
    begin
-      if Nlen <= Max_Length then
-         Source.Current_Length := Nlen;
-         Source.Data (Llen + 1 .. Nlen) := New_Item;
+      if Llen <= Max_Length - Rlen then
+         if Rlen > 0 then
+            Source.Data (Llen + 1 .. Llen + Rlen) :=
+              Super_String_Data (New_Item);
+            Source.Current_Length := Llen + Rlen;
+         end if;
 
       else
-         Source.Current_Length := Max_Length;
-
          case Drop is
             when Strings.Right =>
                if Llen < Max_Length then
-                  Source.Data (Llen + 1 .. Max_Length) :=
-                    New_Item (New_Item'First ..
-                                New_Item'First - 1 + Max_Length - Llen);
+                  Source.Data (Llen + 1 .. Max_Length) := Super_String_Data
+                    (New_Item (New_Item'First ..
+                                New_Item'First - 1 - Llen + Max_Length));
                end if;
 
             when Strings.Left =>
                if Rlen >= Max_Length then
-                  Source.Data (1 .. Max_Length) :=
-                    New_Item (New_Item'Last - (Max_Length - 1) ..
-                                New_Item'Last);
+                  Source.Data (1 .. Max_Length) := Super_String_Data
+                    (New_Item (New_Item'Last - (Max_Length - 1) ..
+                                New_Item'Last));
 
                else
                   Source.Data (1 .. Max_Length - Rlen) :=
                     Source.Data (Llen - (Max_Length - Rlen - 1) .. Llen);
                   Source.Data (Max_Length - Rlen + 1 .. Max_Length) :=
-                    New_Item;
+                    Super_String_Data (New_Item);
                end if;
 
             when Strings.Error =>
                raise Ada.Strings.Length_Error;
          end case;
+
+         Source.Current_Length := Max_Length;
       end if;
 
    end Super_Append;
@@ -539,25 +558,25 @@ package body Ada.Strings.Superbounded is
       Result     : Super_String (Max_Length);
       Llen       : constant Natural := Left'Length;
       Rlen       : constant Natural := Right.Current_Length;
-      Nlen       : constant Natural := Llen + Rlen;
 
    begin
-      if Nlen <= Max_Length then
-         Result.Current_Length := Nlen;
-         Result.Data (1 .. Llen) := Left;
-         Result.Data (Llen + 1 .. Llen + Rlen) := Right.Data (1 .. Rlen);
+      if Llen <= Max_Length - Rlen then
+         Result.Data (1 .. Llen) := Super_String_Data (Left);
 
-      else
-         Result.Current_Length := Max_Length;
+         if Rlen > 0 then
+            Result.Data (Llen + 1 .. Llen + Rlen) := Right.Data (1 .. Rlen);
+         end if;
 
+         Result.Current_Length := Llen + Rlen;
+      else
          case Drop is
             when Strings.Right =>
                if Llen >= Max_Length then
-                  Result.Data (1 .. Max_Length) :=
-                    Left (Left'First .. Left'First + (Max_Length - 1));
+                  Result.Data (1 .. Max_Length) := Super_String_Data
+                    (Left (Left'First .. Left'First + (Max_Length - 1)));
 
                else
-                  Result.Data (1 .. Llen) := Left;
+                  Result.Data (1 .. Llen) := Super_String_Data (Left);
                   Result.Data (Llen + 1 .. Max_Length) :=
                     Right.Data (1 .. Max_Length - Llen);
                end if;
@@ -568,8 +587,8 @@ package body Ada.Strings.Superbounded is
                     Right.Data (Rlen - (Max_Length - 1) .. Rlen);
 
                else
-                  Result.Data (1 .. Max_Length - Rlen) :=
-                    Left (Left'Last - (Max_Length - Rlen - 1) .. Left'Last);
+                  Result.Data (1 .. Max_Length - Rlen) := Super_String_Data
+                    (Left (Left'Last - (Max_Length - Rlen - 1) .. Left'Last));
                   Result.Data (Max_Length - Rlen + 1 .. Max_Length) :=
                     Right.Data (1 .. Rlen);
                end if;
@@ -577,6 +596,8 @@ package body Ada.Strings.Superbounded is
             when Strings.Error =>
                raise Ada.Strings.Length_Error;
          end case;
+
+         Result.Current_Length := Max_Length;
       end if;
 
       return Result;
@@ -595,9 +616,9 @@ package body Ada.Strings.Superbounded is
 
    begin
       if Llen  < Max_Length then
-         Result.Current_Length := Llen + 1;
          Result.Data (1 .. Llen) := Left.Data (1 .. Llen);
          Result.Data (Llen + 1) := Right;
+         Result.Current_Length := Llen + 1;
          return Result;
 
       else
@@ -606,10 +627,10 @@ package body Ada.Strings.Superbounded is
                return Left;
 
             when Strings.Left =>
-               Result.Current_Length := Max_Length;
                Result.Data (1 .. Max_Length - 1) :=
                  Left.Data (2 .. Max_Length);
                Result.Data (Max_Length) := Right;
+               Result.Current_Length := Max_Length;
                return Result;
 
             when Strings.Error =>
@@ -628,12 +649,10 @@ package body Ada.Strings.Superbounded is
 
    begin
       if Llen  < Max_Length then
-         Source.Current_Length := Llen + 1;
          Source.Data (Llen + 1) := New_Item;
+         Source.Current_Length := Llen + 1;
 
       else
-         Source.Current_Length := Max_Length;
-
          case Drop is
             when Strings.Right =>
                null;
@@ -663,18 +682,18 @@ package body Ada.Strings.Superbounded is
 
    begin
       if Rlen < Max_Length then
-         Result.Current_Length := Rlen + 1;
          Result.Data (1) := Left;
          Result.Data (2 .. Rlen + 1) := Right.Data (1 .. Rlen);
+         Result.Current_Length := Rlen + 1;
          return Result;
 
       else
          case Drop is
             when Strings.Right =>
-               Result.Current_Length := Max_Length;
                Result.Data (1) := Left;
                Result.Data (2 .. Max_Length) :=
                  Right.Data (1 .. Max_Length - 1);
+               Result.Current_Length := Max_Length;
                return Result;
 
             when Strings.Left =>
@@ -696,9 +715,7 @@ package body Ada.Strings.Superbounded is
       Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
    is
    begin
-      return
-        Search.Count
-          (Source.Data (1 .. Source.Current_Length), Pattern, Mapping);
+      return Search.Count (Super_To_String (Source), Pattern, Mapping);
    end Super_Count;
 
    function Super_Count
@@ -707,9 +724,7 @@ package body Ada.Strings.Superbounded is
       Mapping : Maps.Character_Mapping_Function) return Natural
    is
    begin
-      return
-        Search.Count
-          (Source.Data (1 .. Source.Current_Length), Pattern, Mapping);
+      return Search.Count (Super_To_String (Source), Pattern, Mapping);
    end Super_Count;
 
    function Super_Count
@@ -717,7 +732,7 @@ package body Ada.Strings.Superbounded is
       Set    : Maps.Character_Set) return Natural
    is
    begin
-      return Search.Count (Source.Data (1 .. Source.Current_Length), Set);
+      return Search.Count (Super_To_String (Source), Set);
    end Super_Count;
 
    ------------------
@@ -737,19 +752,19 @@ package body Ada.Strings.Superbounded is
       if Num_Delete <= 0 then
          return Source;
 
-      elsif From > Slen + 1 then
+      elsif From - 1 > Slen then
          raise Ada.Strings.Index_Error;
 
       elsif Through >= Slen then
-         Result.Current_Length := From - 1;
          Result.Data (1 .. From - 1) := Source.Data (1 .. From - 1);
+         Result.Current_Length := From - 1;
          return Result;
 
       else
-         Result.Current_Length := Slen - Num_Delete;
          Result.Data (1 .. From - 1) := Source.Data (1 .. From - 1);
-         Result.Data (From .. Result.Current_Length) :=
+         Result.Data (From .. Slen - Num_Delete) :=
            Source.Data (Through + 1 .. Slen);
+         Result.Current_Length := Slen - Num_Delete;
          return Result;
       end if;
    end Super_Delete;
@@ -766,7 +781,7 @@ package body Ada.Strings.Superbounded is
       if Num_Delete <= 0 then
          return;
 
-      elsif From > Slen + 1 then
+      elsif From - 1 > Slen then
          raise Ada.Strings.Index_Error;
 
       elsif Through >= Slen then
@@ -779,22 +794,6 @@ package body Ada.Strings.Superbounded is
       end if;
    end Super_Delete;
 
-   -------------------
-   -- Super_Element --
-   -------------------
-
-   function Super_Element
-     (Source : Super_String;
-      Index  : Positive) return Character
-   is
-   begin
-      if Index <= Source.Current_Length then
-         return Source.Data (Index);
-      else
-         raise Strings.Index_Error;
-      end if;
-   end Super_Element;
-
    ----------------------
    -- Super_Find_Token --
    ----------------------
@@ -809,7 +808,7 @@ package body Ada.Strings.Superbounded is
    is
    begin
       Search.Find_Token
-        (Source.Data (From .. Source.Current_Length), Set, Test, First, Last);
+        (Super_To_String (Source), Set, From, Test, First, Last);
    end Super_Find_Token;
 
    procedure Super_Find_Token
@@ -820,8 +819,7 @@ package body Ada.Strings.Superbounded is
       Last   : out Natural)
    is
    begin
-      Search.Find_Token
-        (Source.Data (1 .. Source.Current_Length), Set, Test, First, Last);
+      Search.Find_Token (Super_To_String (Source), Set, Test, First, Last);
    end Super_Find_Token;
 
    ----------------
@@ -841,21 +839,22 @@ package body Ada.Strings.Superbounded is
 
    begin
       if Npad <= 0 then
-         Result.Current_Length := Count;
          Result.Data (1 .. Count) := Source.Data (1 .. Count);
+         Result.Current_Length := Count;
 
       elsif Count <= Max_Length then
-         Result.Current_Length := Count;
          Result.Data (1 .. Slen) := Source.Data (1 .. Slen);
          Result.Data (Slen + 1 .. Count) := (others => Pad);
+         Result.Current_Length := Count;
 
       else
-         Result.Current_Length := Max_Length;
-
          case Drop is
             when Strings.Right =>
                Result.Data (1 .. Slen) := Source.Data (1 .. Slen);
-               Result.Data (Slen + 1 .. Max_Length) := (others => Pad);
+
+               if Slen < Max_Length then
+                  Result.Data (Slen + 1 .. Max_Length) := (others => Pad);
+               end if;
 
             when Strings.Left =>
                if Npad >= Max_Length then
@@ -871,6 +870,8 @@ package body Ada.Strings.Superbounded is
             when Strings.Error =>
                raise Ada.Strings.Length_Error;
          end case;
+
+         Result.Current_Length := Max_Length;
       end if;
 
       return Result;
@@ -885,22 +886,22 @@ package body Ada.Strings.Superbounded is
       Max_Length : constant Positive := Source.Max_Length;
       Slen       : constant Natural  := Source.Current_Length;
       Npad       : constant Integer  := Count - Slen;
-      Temp       : String (1 .. Max_Length);
+      Temp       : Super_String_Data (1 .. Max_Length);
 
    begin
       if Npad <= 0 then
          Source.Current_Length := Count;
 
       elsif Count <= Max_Length then
-         Source.Current_Length := Count;
          Source.Data (Slen + 1 .. Count) := (others => Pad);
+         Source.Current_Length := Count;
 
       else
-         Source.Current_Length := Max_Length;
-
          case Drop is
             when Strings.Right =>
-               Source.Data (Slen + 1 .. Max_Length) := (others => Pad);
+               if Slen < Max_Length then
+                  Source.Data (Slen + 1 .. Max_Length) := (others => Pad);
+               end if;
 
             when Strings.Left =>
                if Npad > Max_Length then
@@ -910,15 +911,15 @@ package body Ada.Strings.Superbounded is
                   Temp := Source.Data;
                   Source.Data (1 .. Max_Length - Npad) :=
                     Temp (Count - Max_Length + 1 .. Slen);
-
-                  for J in Max_Length - Npad + 1 .. Max_Length loop
-                     Source.Data (J) := Pad;
-                  end loop;
+                  Source.Data (Max_Length - Npad + 1 .. Max_Length) :=
+                    (others => Pad);
                end if;
 
             when Strings.Error =>
                raise Ada.Strings.Length_Error;
          end case;
+
+         Source.Current_Length := Max_Length;
       end if;
    end Super_Head;
 
@@ -933,8 +934,7 @@ package body Ada.Strings.Superbounded is
       Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
    is
    begin
-      return Search.Index
-        (Source.Data (1 .. Source.Current_Length), Pattern, Going, Mapping);
+      return Search.Index (Super_To_String (Source), Pattern, Going, Mapping);
    end Super_Index;
 
    function Super_Index
@@ -944,8 +944,7 @@ package body Ada.Strings.Superbounded is
       Mapping : Maps.Character_Mapping_Function) return Natural
    is
    begin
-      return Search.Index
-        (Source.Data (1 .. Source.Current_Length), Pattern, Going, Mapping);
+      return Search.Index (Super_To_String (Source), Pattern, Going, Mapping);
    end Super_Index;
 
    function Super_Index
@@ -955,8 +954,7 @@ package body Ada.Strings.Superbounded is
       Going  : Strings.Direction  := Strings.Forward) return Natural
    is
    begin
-      return Search.Index
-        (Source.Data (1 .. Source.Current_Length), Set, Test, Going);
+      return Search.Index (Super_To_String (Source), Set, Test, Going);
    end Super_Index;
 
    function Super_Index
@@ -968,8 +966,7 @@ package body Ada.Strings.Superbounded is
    is
    begin
       return Search.Index
-        (Source.Data (1 .. Source.Current_Length),
-         Pattern, From, Going, Mapping);
+        (Super_To_String (Source), Pattern, From, Going, Mapping);
    end Super_Index;
 
    function Super_Index
@@ -981,8 +978,7 @@ package body Ada.Strings.Superbounded is
    is
    begin
       return Search.Index
-        (Source.Data (1 .. Source.Current_Length),
-         Pattern, From, Going, Mapping);
+        (Super_To_String (Source), Pattern, From, Going, Mapping);
    end Super_Index;
 
    function Super_Index
@@ -993,8 +989,15 @@ package body Ada.Strings.Superbounded is
       Going  : Direction := Forward) return Natural
    is
    begin
-      return Search.Index
-        (Source.Data (1 .. Source.Current_Length), Set, From, Test, Going);
+      return Result : Natural do
+         Result :=
+           Search.Index (Super_To_String (Source), Set, From, Test, Going);
+         pragma Assert
+           (if (for all J in 1 .. Super_Length (Source) =>
+                  (if J = From or else (J > From) = (Going = Forward) then
+                     (Test = Inside) /= Maps.Is_In (Source.Data (J), Set)))
+            then Result = 0);
+      end return;
    end Super_Index;
 
    ---------------------------
@@ -1006,9 +1009,7 @@ package body Ada.Strings.Superbounded is
       Going  : Strings.Direction := Strings.Forward) return Natural
    is
    begin
-      return
-        Search.Index_Non_Blank
-          (Source.Data (1 .. Source.Current_Length), Going);
+      return Search.Index_Non_Blank (Super_To_String (Source), Going);
    end Super_Index_Non_Blank;
 
    function Super_Index_Non_Blank
@@ -1017,9 +1018,7 @@ package body Ada.Strings.Superbounded is
       Going  : Direction := Forward) return Natural
    is
    begin
-      return
-        Search.Index_Non_Blank
-          (Source.Data (1 .. Source.Current_Length), From, Going);
+      return Search.Index_Non_Blank (Super_To_String (Source), From, Going);
    end Super_Index_Non_Blank;
 
    ------------------
@@ -1031,60 +1030,71 @@ package body Ada.Strings.Superbounded is
       Before   : Positive;
       New_Item : String;
       Drop     : Strings.Truncation := Strings.Error) return Super_String
+   with SPARK_Mode => Off
    is
       Max_Length : constant Positive := Source.Max_Length;
       Result     : Super_String (Max_Length);
       Slen       : constant Natural := Source.Current_Length;
       Nlen       : constant Natural := New_Item'Length;
-      Tlen       : constant Natural := Slen + Nlen;
       Blen       : constant Natural := Before - 1;
       Alen       : constant Integer := Slen - Blen;
-      Droplen    : constant Integer := Tlen - Max_Length;
+      Droplen    : constant Integer := Slen - Max_Length + Nlen;
 
-      --  Tlen is the length of the total string before possible truncation.
       --  Blen, Alen are the lengths of the before and after pieces of the
-      --  source string.
+      --  source string. The number of dropped characters is Natural'Max (0,
+      --  Droplen).
 
    begin
       if Alen < 0 then
          raise Ada.Strings.Index_Error;
 
       elsif Droplen <= 0 then
-         Result.Current_Length := Tlen;
          Result.Data (1 .. Blen) := Source.Data (1 .. Blen);
-         Result.Data (Before .. Before + Nlen - 1) := New_Item;
-         Result.Data (Before + Nlen .. Tlen) :=
-           Source.Data (Before .. Slen);
+         Result.Data (Before .. Before - 1 + Nlen) :=
+           Super_String_Data (New_Item);
 
-      else
-         Result.Current_Length := Max_Length;
+         if Before <= Slen then
+            Result.Data (Before + Nlen .. Slen + Nlen) :=
+              Source.Data (Before .. Slen);
+         end if;
 
+         Result.Current_Length := Slen + Nlen;
+
+      else
          case Drop is
             when Strings.Right =>
                Result.Data (1 .. Blen) := Source.Data (1 .. Blen);
 
-               if Droplen > Alen then
-                  Result.Data (Before .. Max_Length) :=
-                    New_Item (New_Item'First
-                                .. New_Item'First + Max_Length - Before);
+               if Droplen >= Alen then
+                  Result.Data (Before .. Max_Length) := Super_String_Data
+                    (New_Item (New_Item'First
+                               .. New_Item'First - Before + Max_Length));
+                  pragma Assert
+                    (String (Result.Data (Before .. Max_Length)) =
+                       New_Item (New_Item'First
+                                 .. New_Item'First - Before + Max_Length));
                else
-                  Result.Data (Before .. Before + Nlen - 1) := New_Item;
+                  Result.Data (Before .. Before - 1 + Nlen) :=
+                    Super_String_Data (New_Item);
                   Result.Data (Before + Nlen .. Max_Length) :=
                     Source.Data (Before .. Slen - Droplen);
                end if;
 
             when Strings.Left =>
-               Result.Data (Max_Length - (Alen - 1) .. Max_Length) :=
-                 Source.Data (Before .. Slen);
+               if Alen > 0 then
+                  Result.Data (Max_Length - (Alen - 1) .. Max_Length) :=
+                    Source.Data (Before .. Slen);
+               end if;
 
-               if Droplen >= Blen then
-                  Result.Data (1 .. Max_Length - Alen) :=
-                    New_Item (New_Item'Last - (Max_Length - Alen) + 1
-                                .. New_Item'Last);
+               if Droplen > Blen then
+                  if Alen < Max_Length then
+                     Result.Data (1 .. Max_Length - Alen) := Super_String_Data
+                       (New_Item (New_Item'Last - (Max_Length - Alen) + 1
+                                  .. New_Item'Last));
+                  end if;
                else
-                  Result.Data
-                    (Blen - Droplen + 1 .. Max_Length - Alen) :=
-                    New_Item;
+                  Result.Data (Blen - Droplen + 1 .. Max_Length - Alen) :=
+                    Super_String_Data (New_Item);
                   Result.Data (1 .. Blen - Droplen) :=
                     Source.Data (Droplen + 1 .. Blen);
                end if;
@@ -1092,6 +1102,8 @@ package body Ada.Strings.Superbounded is
             when Strings.Error =>
                raise Ada.Strings.Length_Error;
          end case;
+
+         Result.Current_Length := Max_Length;
       end if;
 
       return Result;
@@ -1111,15 +1123,6 @@ package body Ada.Strings.Superbounded is
       Source := Super_Insert (Source, Before, New_Item, Drop);
    end Super_Insert;
 
-   ------------------
-   -- Super_Length --
-   ------------------
-
-   function Super_Length (Source : Super_String) return Natural is
-   begin
-      return Source.Current_Length;
-   end Super_Length;
-
    ---------------------
    -- Super_Overwrite --
    ---------------------
@@ -1132,61 +1135,61 @@ package body Ada.Strings.Superbounded is
    is
       Max_Length : constant Positive := Source.Max_Length;
       Result     : Super_String (Max_Length);
-      Endpos     : constant Natural  := Position + New_Item'Length - 1;
       Slen       : constant Natural  := Source.Current_Length;
       Droplen    : Natural;
 
    begin
-      if Position > Slen + 1 then
+      if Position - 1 > Slen then
          raise Ada.Strings.Index_Error;
 
       elsif New_Item'Length = 0 then
          return Source;
 
-      elsif Endpos <= Slen then
-         Result.Current_Length := Source.Current_Length;
+      elsif Position - 1 <= Slen - New_Item'Length then
          Result.Data (1 .. Slen) := Source.Data (1 .. Slen);
-         Result.Data (Position .. Endpos) := New_Item;
+         Result.Data (Position .. Position - 1 + New_Item'Length) :=
+           Super_String_Data (New_Item);
+         Result.Current_Length := Source.Current_Length;
          return Result;
 
-      elsif Endpos <= Max_Length then
-         Result.Current_Length := Endpos;
+      elsif Position - 1 <= Max_Length - New_Item'Length then
          Result.Data (1 .. Position - 1) := Source.Data (1 .. Position - 1);
-         Result.Data (Position .. Endpos) := New_Item;
+         Result.Data (Position .. Position - 1 + New_Item'Length) :=
+           Super_String_Data (New_Item);
+         Result.Current_Length := Position - 1 + New_Item'Length;
          return Result;
 
       else
-         Result.Current_Length := Max_Length;
-         Droplen := Endpos - Max_Length;
+         Droplen := Position - 1 - Max_Length + New_Item'Length;
 
          case Drop is
             when Strings.Right =>
                Result.Data (1 .. Position - 1) :=
                  Source.Data (1 .. Position - 1);
 
-               Result.Data (Position .. Max_Length) :=
-                 New_Item (New_Item'First .. New_Item'Last - Droplen);
-               return Result;
+               Result.Data (Position .. Max_Length) := Super_String_Data
+                 (New_Item (New_Item'First .. New_Item'Last - Droplen));
 
             when Strings.Left =>
                if New_Item'Length >= Max_Length then
-                  Result.Data (1 .. Max_Length) :=
-                    New_Item (New_Item'Last - Max_Length + 1 ..
-                                New_Item'Last);
-                  return Result;
+                  Result.Data (1 .. Max_Length) := Super_String_Data
+                    (New_Item (New_Item'Last - Max_Length + 1 ..
+                                New_Item'Last));
 
                else
                   Result.Data (1 .. Max_Length - New_Item'Length) :=
                     Source.Data (Droplen + 1 .. Position - 1);
                   Result.Data
                     (Max_Length - New_Item'Length + 1 .. Max_Length) :=
-                    New_Item;
-                  return Result;
+                    Super_String_Data (New_Item);
                end if;
 
             when Strings.Error =>
                raise Ada.Strings.Length_Error;
          end case;
+
+         Result.Current_Length := Max_Length;
+         return Result;
       end if;
    end Super_Overwrite;
 
@@ -1195,50 +1198,52 @@ package body Ada.Strings.Superbounded is
       Position  : Positive;
       New_Item  : String;
       Drop      : Strings.Truncation := Strings.Error)
+   with SPARK_Mode => Off
    is
       Max_Length : constant Positive := Source.Max_Length;
-      Endpos     : constant Positive := Position + New_Item'Length - 1;
       Slen       : constant Natural  := Source.Current_Length;
       Droplen    : Natural;
 
    begin
-      if Position > Slen + 1 then
+      if Position - 1 > Slen then
          raise Ada.Strings.Index_Error;
 
-      elsif Endpos <= Slen then
-         Source.Data (Position .. Endpos) := New_Item;
+      elsif Position - 1 <= Slen - New_Item'Length then
+         Source.Data (Position .. Position - 1 + New_Item'Length) :=
+           Super_String_Data (New_Item);
 
-      elsif Endpos <= Max_Length then
-         Source.Data (Position .. Endpos) := New_Item;
-         Source.Current_Length := Endpos;
+      elsif Position - 1 <= Max_Length - New_Item'Length then
+         Source.Data (Position .. Position - 1 + New_Item'Length) :=
+           Super_String_Data (New_Item);
+         Source.Current_Length := Position - 1 + New_Item'Length;
 
       else
-         Source.Current_Length := Max_Length;
-         Droplen := Endpos - Max_Length;
+         Droplen := Position - 1 - Max_Length + New_Item'Length;
 
          case Drop is
             when Strings.Right =>
-               Source.Data (Position .. Max_Length) :=
-                 New_Item (New_Item'First .. New_Item'Last - Droplen);
+               Source.Data (Position .. Max_Length) := Super_String_Data
+                 (New_Item (New_Item'First .. New_Item'Last - Droplen));
 
             when Strings.Left =>
                if New_Item'Length > Max_Length then
-                  Source.Data (1 .. Max_Length) :=
-                    New_Item (New_Item'Last - Max_Length + 1 ..
-                                New_Item'Last);
+                  Source.Data (1 .. Max_Length) := Super_String_Data
+                    (New_Item
+                      (New_Item'Last - Max_Length + 1 .. New_Item'Last));
 
                else
                   Source.Data (1 .. Max_Length - New_Item'Length) :=
                     Source.Data (Droplen + 1 .. Position - 1);
-
                   Source.Data
                     (Max_Length - New_Item'Length + 1 .. Max_Length) :=
-                    New_Item;
+                    Super_String_Data (New_Item);
                end if;
 
             when Strings.Error =>
                raise Ada.Strings.Length_Error;
          end case;
+
+         Source.Current_Length := Max_Length;
       end if;
    end Super_Overwrite;
 
@@ -1269,12 +1274,13 @@ package body Ada.Strings.Superbounded is
       High   : Natural;
       By     : String;
       Drop   : Strings.Truncation := Strings.Error) return Super_String
+   with SPARK_Mode => Off
    is
       Max_Length : constant Positive := Source.Max_Length;
       Slen       : constant Natural  := Source.Current_Length;
 
    begin
-      if Low > Slen + 1 then
+      if Low - 1 > Slen then
          raise Strings.Index_Error;
 
       elsif High < Low then
@@ -1282,51 +1288,58 @@ package body Ada.Strings.Superbounded is
 
       else
          declare
-            Blen    : constant Natural := Natural'Max (0, Low - 1);
+            Blen    : constant Natural := Low - 1;
             Alen    : constant Natural := Natural'Max (0, Slen - High);
-            Tlen    : constant Natural := Blen + By'Length + Alen;
-            Droplen : constant Integer := Tlen - Max_Length;
+            Droplen : constant Integer := Blen + Alen - Max_Length + By'Length;
             Result  : Super_String (Max_Length);
 
-            --  Tlen is the total length of the result string before any
-            --  truncation. Blen and Alen are the lengths of the pieces
-            --  of the original string that end up in the result string
-            --  before and after the replaced slice.
+            --  Blen and Alen are the lengths of the pieces of the original
+            --  string that end up in the result string before and after the
+            --  replaced slice. The number of dropped characters is Natural'Max
+            --  (0, Droplen).
 
          begin
             if Droplen <= 0 then
-               Result.Current_Length := Tlen;
                Result.Data (1 .. Blen) := Source.Data (1 .. Blen);
-               Result.Data (Low .. Low + By'Length - 1) := By;
-               Result.Data (Low + By'Length .. Tlen) :=
-                 Source.Data (High + 1 .. Slen);
+               Result.Data (Low .. Blen + By'Length) :=
+                 Super_String_Data (By);
 
-            else
-               Result.Current_Length := Max_Length;
+               if Alen > 0 then
+                  Result.Data (Low + By'Length .. Blen + By'Length + Alen) :=
+                    Source.Data (High + 1 .. Slen);
+               end if;
 
+               Result.Current_Length := Blen + By'Length + Alen;
+
+            else
                case Drop is
                   when Strings.Right =>
                      Result.Data (1 .. Blen) := Source.Data (1 .. Blen);
 
-                     if Droplen > Alen then
-                        Result.Data (Low .. Max_Length) :=
-                          By (By'First .. By'First + Max_Length - Low);
+                     if Droplen >= Alen then
+                        Result.Data (Low .. Max_Length) := Super_String_Data
+                          (By (By'First .. By'First - Low + Max_Length));
                      else
-                        Result.Data (Low .. Low + By'Length - 1) := By;
+                        Result.Data (Low .. Low - 1 + By'Length) :=
+                          Super_String_Data (By);
                         Result.Data (Low + By'Length .. Max_Length) :=
                           Source.Data (High + 1 .. Slen - Droplen);
                      end if;
 
                   when Strings.Left =>
-                     Result.Data (Max_Length - (Alen - 1) .. Max_Length) :=
-                       Source.Data (High + 1 .. Slen);
+                     if Alen > 0 then
+                        Result.Data (Max_Length - (Alen - 1) .. Max_Length) :=
+                          Source.Data (High + 1 .. Slen);
+                     end if;
 
                      if Droplen >= Blen then
                         Result.Data (1 .. Max_Length - Alen) :=
-                          By (By'Last - (Max_Length - Alen) + 1 .. By'Last);
+                          Super_String_Data (By
+                            (By'Last - (Max_Length - Alen) + 1 .. By'Last));
                      else
                         Result.Data
-                          (Blen - Droplen + 1 .. Max_Length - Alen) := By;
+                          (Blen - Droplen + 1 .. Max_Length - Alen) :=
+                            Super_String_Data (By);
                         Result.Data (1 .. Blen - Droplen) :=
                           Source.Data (Droplen + 1 .. Blen);
                      end if;
@@ -1334,6 +1347,8 @@ package body Ada.Strings.Superbounded is
                   when Strings.Error =>
                      raise Ada.Strings.Length_Error;
                end case;
+
+               Result.Current_Length := Max_Length;
             end if;
 
             return Result;
@@ -1370,16 +1385,17 @@ package body Ada.Strings.Superbounded is
 
    begin
       if Count <= Max_Length then
+         Result.Data (1 .. Count) := (others => Item);
          Result.Current_Length := Count;
 
       elsif Drop = Strings.Error then
          raise Ada.Strings.Length_Error;
 
       else
+         Result.Data (1 .. Max_Length) := (others => Item);
          Result.Current_Length := Max_Length;
       end if;
 
-      Result.Data (1 .. Result.Current_Length) := (others => Item);
       return Result;
    end Super_Replicate;
 
@@ -1389,52 +1405,203 @@ package body Ada.Strings.Superbounded is
       Drop       : Truncation := Error;
       Max_Length : Positive) return Super_String
    is
-      Length : constant Integer := Count * Item'Length;
       Result : Super_String (Max_Length);
-      Indx   : Positive;
+      Indx   : Natural;
+      Ilen   : constant Natural := Item'Length;
+
+      --  Parts of the proof involving manipulations with the modulo operator
+      --  are complicated for the prover and can't be done automatically in
+      --  the global subprogram. That's why we isolate them in these two ghost
+      --  lemmas.
+
+      procedure Lemma_Mod (K : Natural; Q : Natural) with
+        Ghost,
+        Pre  => Ilen /= 0
+          and then Q mod Ilen = 0
+          and then K - Q in 0 .. Ilen - 1,
+        Post => K mod Ilen = K - Q;
+      --  Lemma_Mod is applied to an index considered in Lemma_Split to prove
+      --  that it has the right value modulo Item'Length.
+
+      procedure Lemma_Mod_Zero (X : Natural) with
+        Ghost,
+        Pre  => Ilen /= 0
+          and then X mod Ilen = 0
+          and then X <= Natural'Last - Ilen,
+        Post => (X + Ilen) mod Ilen = 0;
+      --  Lemma_Mod_Zero is applied to prove that the length of the range
+      --  of indexes considered in the loop, when dropping on the Left, is
+      --  a multiple of Item'Length.
+
+      procedure Lemma_Split (Going : Direction) with
+        Ghost,
+        Pre  =>
+          Ilen /= 0
+            and then Indx in 0 .. Max_Length - Ilen
+            and then
+              (if Going = Forward
+               then Indx mod Ilen = 0
+               else (Max_Length - Indx - Ilen) mod Ilen = 0)
+            and then Result.Data (Indx + 1 .. Indx + Ilen)'Initialized
+            and then String (Result.Data (Indx + 1 .. Indx + Ilen)) = Item,
+        Post =>
+          (if Going = Forward then
+             (for all J in Indx + 1 .. Indx + Ilen =>
+                Result.Data (J) = Item (Item'First + (J - 1) mod Ilen))
+           else
+             (for all J in Indx + 1 .. Indx + Ilen =>
+                Result.Data (J) =
+                  Item (Item'Last - (Max_Length - J) mod Ilen)));
+      --  Lemma_Split is used after Result.Data (Indx + 1 .. Indx + Ilen) is
+      --  updated to Item and concludes that the characters match for each
+      --  index when taken modulo Item'Length, as the considered slice starts
+      --  at index 1 (or ends at index Max_Length, if Going = Backward) modulo
+      --  Item'Length.
+
+      ---------------
+      -- Lemma_Mod --
+      ---------------
+
+      procedure Lemma_Mod (K : Natural; Q : Natural) is null;
+
+      --------------------
+      -- Lemma_Mod_Zero --
+      --------------------
+
+      procedure Lemma_Mod_Zero (X : Natural) is null;
+
+      -----------------
+      -- Lemma_Split --
+      -----------------
+
+      procedure Lemma_Split (Going : Direction) is
+      begin
+         if Going = Forward then
+            for K in Indx + 1 .. Indx + Ilen loop
+               Lemma_Mod (K - 1, Indx);
+               pragma Loop_Invariant
+                 (for all J in Indx + 1 .. K =>
+                    Result.Data (J) = Item (Item'First + (J - 1) mod Ilen));
+            end loop;
+         else
+            for K in Indx + 1 .. Indx + Ilen loop
+               Lemma_Mod (Max_Length - K, Max_Length - Indx - Ilen);
+               pragma Loop_Invariant
+                 (for all J in Indx + 1 .. K =>
+                    Result.Data (J) =
+                      Item (Item'Last - (Max_Length - J) mod Ilen));
+            end loop;
+         end if;
+      end Lemma_Split;
 
    begin
-      if Length <= Max_Length then
-         Result.Current_Length := Length;
-
-         if Length > 0 then
-            Indx := 1;
+      if Count = 0 or else Ilen <= Max_Length / Count then
+         if Count * Ilen > 0 then
+            Indx := 0;
 
             for J in 1 .. Count loop
-               Result.Data (Indx .. Indx + Item'Length - 1) := Item;
-               Indx := Indx + Item'Length;
+               Result.Data (Indx + 1 .. Indx + Ilen) :=
+                 Super_String_Data (Item);
+               pragma Assert
+                 (for all K in 1 .. Ilen =>
+                    Result.Data (Indx + K) = Item (Item'First - 1 + K));
+               pragma Assert
+                 (String (Result.Data (Indx + 1 .. Indx + Ilen)) = Item);
+               Lemma_Split (Forward);
+               Indx := Indx + Ilen;
+               pragma Loop_Invariant (Indx = J * Ilen);
+               pragma Loop_Invariant (Result.Data (1 .. Indx)'Initialized);
+               pragma Loop_Invariant
+                 (for all K in 1 .. Indx =>
+                    Result.Data (K) =
+                      Item (Item'First + (K - 1) mod Ilen));
             end loop;
          end if;
 
-      else
-         Result.Current_Length := Max_Length;
+         Result.Current_Length := Count * Ilen;
 
+      else
          case Drop is
             when Strings.Right =>
-               Indx := 1;
-
-               while Indx + Item'Length <= Max_Length + 1 loop
-                  Result.Data (Indx .. Indx + Item'Length - 1) := Item;
-                  Indx := Indx + Item'Length;
+               Indx := 0;
+
+               while Indx < Max_Length - Ilen loop
+                  Result.Data (Indx + 1 .. Indx + Ilen) :=
+                    Super_String_Data (Item);
+                  pragma Assert
+                    (for all K in 1 .. Ilen =>
+                       Result.Data (Indx + K) = Item (Item'First - 1 + K));
+                  pragma Assert
+                    (String (Result.Data (Indx + 1 .. Indx + Ilen)) = Item);
+                  Lemma_Split (Forward);
+                  Indx := Indx + Ilen;
+                  pragma Loop_Invariant (Indx mod Ilen = 0);
+                  pragma Loop_Invariant (Indx in 0 .. Max_Length - 1);
+                  pragma Loop_Invariant (Result.Data (1 .. Indx)'Initialized);
+                  pragma Loop_Invariant
+                    (for all K in 1 .. Indx =>
+                       Result.Data (K) =
+                         Item (Item'First + (K - 1) mod Ilen));
                end loop;
 
-               Result.Data (Indx .. Max_Length) :=
-                 Item (Item'First .. Item'First + Max_Length - Indx);
+               Result.Data (Indx + 1 .. Max_Length) := Super_String_Data
+                 (Item (Item'First .. Item'First + (Max_Length - Indx - 1)));
+               pragma Assert
+                 (for all J in Indx + 1 .. Max_Length =>
+                    Result.Data (J) = Item (Item'First - 1 - Indx + J));
+
+               for J in Indx + 1 .. Max_Length loop
+                  Lemma_Mod (J - 1, Indx);
+                  pragma Loop_Invariant
+                    (for all K in 1 .. J =>
+                       Result.Data (K) =
+                         Item (Item'First + (K - 1) mod Ilen));
+               end loop;
 
             when Strings.Left =>
                Indx := Max_Length;
 
-               while Indx - Item'Length >= 1 loop
-                  Result.Data (Indx - (Item'Length - 1) .. Indx) := Item;
-                  Indx := Indx - Item'Length;
+               while Indx > Ilen loop
+                  Indx := Indx - Ilen;
+                  Result.Data (Indx + 1 .. Indx + Ilen) :=
+                    Super_String_Data (Item);
+                  pragma Assert
+                    (for all K in 1 .. Ilen =>
+                       Result.Data (Indx + K) = Item (Item'First - 1 + K));
+                  pragma Assert
+                    (String (Result.Data (Indx + 1 .. Indx + Ilen)) = Item);
+                  Lemma_Split (Backward);
+                  Lemma_Mod_Zero (Max_Length - Indx - Ilen);
+                  pragma Loop_Invariant
+                    ((Max_Length - Indx) mod Ilen = 0);
+                  pragma Loop_Invariant (Indx in 1 .. Max_Length);
+                  pragma Loop_Invariant
+                    (Result.Data (Indx + 1 .. Max_Length)'Initialized);
+                  pragma Loop_Invariant
+                    (for all K in Indx + 1 .. Max_Length =>
+                       Result.Data (K) =
+                         Item (Item'Last - (Max_Length - K) mod Ilen));
                end loop;
 
                Result.Data (1 .. Indx) :=
-                 Item (Item'Last - Indx + 1 .. Item'Last);
+                 Super_String_Data (Item (Item'Last - Indx + 1 .. Item'Last));
+               pragma Assert
+                 (for all J in 1 .. Indx =>
+                    Result.Data (J) = Item (Item'Last - Indx + J));
+
+               for J in reverse 1 .. Indx loop
+                  Lemma_Mod (Max_Length - J, Max_Length - Indx);
+                  pragma Loop_Invariant
+                    (for all K in J .. Max_Length =>
+                       Result.Data (K) =
+                         Item (Item'Last - (Max_Length - K) mod Ilen));
+               end loop;
 
             when Strings.Error =>
                raise Ada.Strings.Length_Error;
          end case;
+
+         Result.Current_Length := Max_Length;
       end if;
 
       return Result;
@@ -1447,11 +1614,7 @@ package body Ada.Strings.Superbounded is
    is
    begin
       return
-        Super_Replicate
-          (Count,
-           Item.Data (1 .. Item.Current_Length),
-           Drop,
-           Item.Max_Length);
+        Super_Replicate (Count, Super_To_String (Item), Drop, Item.Max_Length);
    end Super_Replicate;
 
    -----------------
@@ -1461,42 +1624,20 @@ package body Ada.Strings.Superbounded is
    function Super_Slice
      (Source : Super_String;
       Low    : Positive;
-      High   : Natural) return String
-   is
-   begin
-      --  Note: test of High > Length is in accordance with AI95-00128
-
-      return R : String (Low .. High) do
-         if Low > Source.Current_Length + 1
-           or else High > Source.Current_Length
-         then
-            raise Index_Error;
-         end if;
-
-         --  Note: in this case, superflat bounds are not a problem, we just
-         --  get the null string in accordance with normal Ada slice rules.
-
-         R := Source.Data (Low .. High);
-      end return;
-   end Super_Slice;
-
-   function Super_Slice
-     (Source : Super_String;
-      Low    : Positive;
       High   : Natural) return Super_String
    is
    begin
       return Result : Super_String (Source.Max_Length) do
-         if Low > Source.Current_Length + 1
+         if Low - 1 > Source.Current_Length
            or else High > Source.Current_Length
          then
             raise Index_Error;
          end if;
 
-         --  Note: the Max operation here deals with the superflat case
-
-         Result.Current_Length := Integer'Max (0, High - Low + 1);
-         Result.Data (1 .. Result.Current_Length) := Source.Data (Low .. High);
+         if High >= Low then
+            Result.Data (1 .. High - Low + 1) := Source.Data (Low .. High);
+            Result.Current_Length := High - Low + 1;
+         end if;
       end return;
    end Super_Slice;
 
@@ -1507,16 +1648,18 @@ package body Ada.Strings.Superbounded is
       High   : Natural)
    is
    begin
-      if Low > Source.Current_Length + 1
+      if Low - 1 > Source.Current_Length
         or else High > Source.Current_Length
       then
          raise Index_Error;
       end if;
 
-      --  Note: the Max operation here deals with the superflat case
-
-      Target.Current_Length := Integer'Max (0, High - Low + 1);
-      Target.Data (1 .. Target.Current_Length) := Source.Data (Low .. High);
+      if High >= Low then
+         Target.Data (1 .. High - Low + 1) := Source.Data (Low .. High);
+         Target.Current_Length := High - Low + 1;
+      else
+         Target.Current_Length := 0;
+      end if;
    end Super_Slice;
 
    ----------------
@@ -1536,18 +1679,22 @@ package body Ada.Strings.Superbounded is
 
    begin
       if Npad <= 0 then
-         Result.Current_Length := Count;
-         Result.Data (1 .. Count) :=
-           Source.Data (Slen - (Count - 1) .. Slen);
+         if Count > 0 then
+            Result.Data (1 .. Count) :=
+              Source.Data (Slen - (Count - 1) .. Slen);
+            Result.Current_Length := Count;
+         end if;
 
       elsif Count <= Max_Length then
-         Result.Current_Length := Count;
          Result.Data (1 .. Npad) := (others => Pad);
-         Result.Data (Npad + 1 .. Count) := Source.Data (1 .. Slen);
 
-      else
-         Result.Current_Length := Max_Length;
+         if Slen > 0 then
+            Result.Data (Npad + 1 .. Count) := Source.Data (1 .. Slen);
+         end if;
+
+         Result.Current_Length := Count;
 
+      else
          case Drop is
             when Strings.Right =>
                if Npad >= Max_Length then
@@ -1567,6 +1714,8 @@ package body Ada.Strings.Superbounded is
             when Strings.Error =>
                raise Ada.Strings.Length_Error;
          end case;
+
+         Result.Current_Length := Max_Length;
       end if;
 
       return Result;
@@ -1582,22 +1731,27 @@ package body Ada.Strings.Superbounded is
       Slen       : constant Natural  := Source.Current_Length;
       Npad       : constant Integer  := Count - Slen;
 
-      Temp : constant String (1 .. Max_Length) := Source.Data;
+      Temp : constant Super_String_Data (1 .. Max_Length) := Source.Data;
 
    begin
       if Npad <= 0 then
          Source.Current_Length := Count;
-         Source.Data (1 .. Count) :=
-           Temp (Slen - (Count - 1) .. Slen);
+
+         if Count > 0 then
+            Source.Data (1 .. Count) :=
+              Temp (Slen - (Count - 1) .. Slen);
+         end if;
 
       elsif Count <= Max_Length then
-         Source.Current_Length := Count;
          Source.Data (1 .. Npad) := (others => Pad);
-         Source.Data (Npad + 1 .. Count) := Temp (1 .. Slen);
 
-      else
-         Source.Current_Length := Max_Length;
+         if Slen > 0 then
+            Source.Data (Npad + 1 .. Count) := Temp (1 .. Slen);
+         end if;
 
+         Source.Current_Length := Count;
+
+      else
          case Drop is
             when Strings.Right =>
                if Npad >= Max_Length then
@@ -1610,31 +1764,19 @@ package body Ada.Strings.Superbounded is
                end if;
 
             when Strings.Left =>
-               for J in 1 .. Max_Length - Slen loop
-                  Source.Data (J) := Pad;
-               end loop;
-
+               Source.Data (1 .. Max_Length - Slen) := (others => Pad);
                Source.Data (Max_Length - Slen + 1 .. Max_Length) :=
                  Temp (1 .. Slen);
 
             when Strings.Error =>
                raise Ada.Strings.Length_Error;
          end case;
+
+         Source.Current_Length := Max_Length;
       end if;
    end Super_Tail;
 
    ---------------------
-   -- Super_To_String --
-   ---------------------
-
-   function Super_To_String (Source : Super_String) return String is
-   begin
-      return R : String (1 .. Source.Current_Length) do
-         R := Source.Data (1 .. Source.Current_Length);
-      end return;
-   end Super_To_String;
-
-   ---------------------
    -- Super_Translate --
    ---------------------
 
@@ -1645,12 +1787,15 @@ package body Ada.Strings.Superbounded is
       Result : Super_String (Source.Max_Length);
 
    begin
-      Result.Current_Length := Source.Current_Length;
-
       for J in 1 .. Source.Current_Length loop
          Result.Data (J) := Value (Mapping, Source.Data (J));
+         pragma Loop_Invariant (Result.Data (1 .. J)'Initialized);
+         pragma Loop_Invariant
+           (for all K in 1 .. J =>
+              Result.Data (K) = Value (Mapping, Source.Data (K)));
       end loop;
 
+      Result.Current_Length := Source.Current_Length;
       return Result;
    end Super_Translate;
 
@@ -1661,6 +1806,9 @@ package body Ada.Strings.Superbounded is
    begin
       for J in 1 .. Source.Current_Length loop
          Source.Data (J) := Value (Mapping, Source.Data (J));
+         pragma Loop_Invariant
+           (for all K in 1 .. J =>
+              Source.Data (K) = Value (Mapping, Source'Loop_Entry.Data (K)));
       end loop;
    end Super_Translate;
 
@@ -1671,12 +1819,15 @@ package body Ada.Strings.Superbounded is
       Result : Super_String (Source.Max_Length);
 
    begin
-      Result.Current_Length := Source.Current_Length;
-
       for J in 1 .. Source.Current_Length loop
          Result.Data (J) := Mapping.all (Source.Data (J));
+         pragma Loop_Invariant (Result.Data (1 .. J)'Initialized);
+         pragma Loop_Invariant
+           (for all K in 1 .. J =>
+              Result.Data (K) = Mapping (Source.Data (K)));
       end loop;
 
+      Result.Current_Length := Source.Current_Length;
       return Result;
    end Super_Translate;
 
@@ -1687,6 +1838,9 @@ package body Ada.Strings.Superbounded is
    begin
       for J in 1 .. Source.Current_Length loop
          Source.Data (J) := Mapping.all (Source.Data (J));
+         pragma Loop_Invariant
+           (for all K in 1 .. J =>
+              Source.Data (K) = Mapping (Source'Loop_Entry.Data (K)));
       end loop;
    end Super_Translate;
 
@@ -1699,24 +1853,62 @@ package body Ada.Strings.Superbounded is
       Side   : Trim_End) return Super_String
    is
       Result : Super_String (Source.Max_Length);
-      Last   : Natural := Source.Current_Length;
-      First  : Positive := 1;
+      Last   : constant Natural := Source.Current_Length;
 
    begin
-      if Side = Left or else Side = Both then
-         while First <= Last and then Source.Data (First) = ' ' loop
-            First := First + 1;
-         end loop;
-      end if;
+      case Side is
+         when Strings.Left =>
+            declare
+               Low : constant Natural :=
+                 Super_Index_Non_Blank (Source, Forward);
+            begin
+               --  All blanks case
 
-      if Side = Right or else Side = Both then
-         while Last >= First and then Source.Data (Last) = ' ' loop
-            Last := Last - 1;
-         end loop;
-      end if;
+               if Low = 0 then
+                  return Result;
+               end if;
+
+               Result.Data (1 .. Last - Low + 1) := Source.Data (Low .. Last);
+               Result.Current_Length := Last - Low + 1;
+            end;
+
+         when Strings.Right =>
+            declare
+               High : constant Natural :=
+                 Super_Index_Non_Blank (Source, Backward);
+            begin
+               --  All blanks case
+
+               if High = 0 then
+                  return Result;
+               end if;
+
+               Result.Data (1 .. High) := Source.Data (1 .. High);
+               Result.Current_Length := High;
+            end;
+
+         when Strings.Both =>
+            declare
+               Low : constant Natural :=
+                 Super_Index_Non_Blank (Source, Forward);
+            begin
+               --  All blanks case
+
+               if Low = 0 then
+                  return Result;
+               end if;
+
+               declare
+                  High : constant Natural :=
+                    Super_Index_Non_Blank (Source, Backward);
+               begin
+                  Result.Data (1 .. High - Low + 1) :=
+                    Source.Data (Low .. High);
+                  Result.Current_Length := High - Low + 1;
+               end;
+            end;
+      end case;
 
-      Result.Current_Length := Last - First + 1;
-      Result.Data (1 .. Result.Current_Length) := Source.Data (First .. Last);
       return Result;
    end Super_Trim;
 
@@ -1724,28 +1916,54 @@ package body Ada.Strings.Superbounded is
      (Source : in out Super_String;
       Side   : Trim_End)
    is
-      Max_Length : constant Positive := Source.Max_Length;
-      Last       : Natural           := Source.Current_Length;
-      First      : Positive          := 1;
-      Temp       : String (1 .. Max_Length);
-
+      Last : constant Natural := Source.Current_Length;
    begin
-      Temp (1 .. Last) := Source.Data (1 .. Last);
-
-      if Side = Left or else Side = Both then
-         while First <= Last and then Temp (First) = ' ' loop
-            First := First + 1;
-         end loop;
-      end if;
+      case Side is
+         when Strings.Left =>
+            declare
+               Low : constant Natural :=
+                 Super_Index_Non_Blank (Source, Forward);
+            begin
+               --  All blanks case
 
-      if Side = Right or else Side = Both then
-         while Last >= First and then Temp (Last) = ' ' loop
-            Last := Last - 1;
-         end loop;
-      end if;
-
-      Source.Current_Length := Last - First + 1;
-      Source.Data (1 .. Source.Current_Length) := Temp (First .. Last);
+               if Low = 0 then
+                  Source.Current_Length := 0;
+               else
+                  Source.Data (1 .. Last - Low + 1) :=
+                    Source.Data (Low .. Last);
+                  Source.Current_Length := Last - Low + 1;
+               end if;
+            end;
+
+         when Strings.Right =>
+            declare
+               High : constant Natural :=
+                 Super_Index_Non_Blank (Source, Backward);
+            begin
+               Source.Current_Length := High;
+            end;
+
+         when Strings.Both =>
+            declare
+               Low : constant Natural :=
+                 Super_Index_Non_Blank (Source, Forward);
+            begin
+               --  All blanks case
+
+               if Low = 0 then
+                  Source.Current_Length := 0;
+               else
+                  declare
+                     High : constant Natural :=
+                       Super_Index_Non_Blank (Source, Backward);
+                  begin
+                     Source.Data (1 .. High - Low + 1) :=
+                       Source.Data (Low .. High);
+                     Source.Current_Length := High - Low + 1;
+                  end;
+               end if;
+            end;
+      end case;
    end Super_Trim;
 
    function Super_Trim
@@ -1754,22 +1972,31 @@ package body Ada.Strings.Superbounded is
       Right  : Maps.Character_Set) return Super_String
    is
       Result : Super_String (Source.Max_Length);
+      Low    : Natural;
+      High   : Natural;
 
    begin
-      for First in 1 .. Source.Current_Length loop
-         if not Is_In (Source.Data (First), Left) then
-            for Last in reverse First .. Source.Current_Length loop
-               if not Is_In (Source.Data (Last), Right) then
-                  Result.Current_Length := Last - First + 1;
-                  Result.Data (1 .. Result.Current_Length) :=
-                    Source.Data (First .. Last);
-                  return Result;
-               end if;
-            end loop;
-         end if;
-      end loop;
+      Low := Super_Index (Source, Left, Outside, Forward);
+
+      --  Case where source comprises only characters in Left
+
+      if Low = 0 then
+         return Result;
+      end if;
+
+      High := Super_Index (Source, Right, Outside, Backward);
+
+      --  Case where source comprises only characters in Right
+
+      if High = 0 then
+         return Result;
+      end if;
+
+      if High >= Low then
+         Result.Data (1 .. High - Low + 1) := Source.Data (Low .. High);
+         Result.Current_Length := High - Low + 1;
+      end if;
 
-      Result.Current_Length := 0;
       return Result;
    end Super_Trim;
 
@@ -1778,29 +2005,39 @@ package body Ada.Strings.Superbounded is
       Left   : Maps.Character_Set;
       Right  : Maps.Character_Set)
    is
+      Last : constant Natural := Source.Current_Length;
+      Temp : Super_String_Data (1 .. Last);
+      Low  : Natural;
+      High : Natural;
+
    begin
-      for First in 1 .. Source.Current_Length loop
-         if not Is_In (Source.Data (First), Left) then
-            for Last in reverse First .. Source.Current_Length loop
-               if not Is_In (Source.Data (Last), Right) then
-                  if First = 1 then
-                     Source.Current_Length := Last;
-                     return;
-                  else
-                     Source.Current_Length := Last - First + 1;
-                     Source.Data (1 .. Source.Current_Length) :=
-                       Source.Data (First .. Last);
-                     return;
-                  end if;
-               end if;
-            end loop;
+      Temp := Source.Data (1 .. Last);
+      Low := Super_Index (Source, Left, Outside, Forward);
+
+      --  Case where source comprises only characters in Left
+
+      if Low = 0 then
+         Source.Current_Length := 0;
+
+      else
+         High := Super_Index (Source, Right, Outside, Backward);
 
+         --  Case where source comprises only characters in Right
+
+         if High = 0 then
             Source.Current_Length := 0;
-            return;
-         end if;
-      end loop;
 
-      Source.Current_Length := 0;
+         elsif Low = 1 then
+            Source.Current_Length := High;
+
+         elsif High < Low then
+            Source.Current_Length := 0;
+
+         else
+            Source.Data (1 .. High - Low + 1) := Temp (Low .. High);
+            Source.Current_Length := High - Low + 1;
+         end if;
+      end if;
    end Super_Trim;
 
    -----------
@@ -1819,11 +2056,14 @@ package body Ada.Strings.Superbounded is
          raise Ada.Strings.Length_Error;
 
       else
-         Result.Current_Length := Left;
-
          for J in 1 .. Left loop
             Result.Data (J) := Right;
+            pragma Loop_Invariant (Result.Data (1 .. J)'Initialized);
+            pragma Loop_Invariant
+              (for all K in 1 .. J => Result.Data (K) = Right);
          end loop;
+
+         Result.Current_Length := Left;
       end if;
 
       return Result;
@@ -1835,23 +2075,88 @@ package body Ada.Strings.Superbounded is
       Max_Length : Positive) return Super_String
    is
       Result : Super_String (Max_Length);
-      Pos    : Positive         := 1;
+      Pos    : Natural          := 0;
       Rlen   : constant Natural := Right'Length;
       Nlen   : constant Natural := Left * Rlen;
 
+      --  Parts of the proof involving manipulations with the modulo operator
+      --  are complicated for the prover and can't be done automatically in
+      --  the global subprogram. That's why we isolate them in these two ghost
+      --  lemmas.
+
+      procedure Lemma_Mod (K : Integer) with
+        Ghost,
+        Pre =>
+          Rlen /= 0
+          and then Pos mod Rlen = 0
+          and then Pos in 0 .. Max_Length - Rlen
+          and then K in Pos .. Pos + Rlen - 1,
+        Post => K mod Rlen = K - Pos;
+      --  Lemma_Mod is applied to an index considered in Lemma_Split to prove
+      --  that it has the right value modulo Right'Length.
+
+      procedure Lemma_Split with
+        Ghost,
+        Pre  =>
+          Rlen /= 0
+            and then Pos mod Rlen = 0
+            and then Pos in 0 .. Max_Length - Rlen
+            and then Result.Data (1 .. Pos + Rlen)'Initialized
+            and then String (Result.Data (Pos + 1 .. Pos + Rlen)) = Right,
+        Post =>
+          (for all K in Pos + 1 .. Pos + Rlen =>
+            Result.Data (K) = Right (Right'First + (K - 1) mod Rlen));
+      --  Lemma_Split is used after Result.Data (Pos + 1 .. Pos + Rlen) is
+      --  updated to Right and concludes that the characters match for each
+      --  index when taken modulo Right'Length, as the considered slice starts
+      --  at index 1 modulo Right'Length.
+
+      ---------------
+      -- Lemma_Mod --
+      ---------------
+
+      procedure Lemma_Mod (K : Integer) is null;
+
+      -----------------
+      -- Lemma_Split --
+      -----------------
+
+      procedure Lemma_Split is
+      begin
+         for K in Pos + 1 .. Pos + Rlen loop
+            Lemma_Mod (K - 1);
+            pragma Loop_Invariant
+              (for all J in Pos + 1 .. K =>
+                 Result.Data (J) = Right (Right'First + (J - 1) mod Rlen));
+         end loop;
+      end Lemma_Split;
+
    begin
       if Nlen > Max_Length then
          raise Ada.Strings.Length_Error;
 
       else
-         Result.Current_Length := Nlen;
-
          if Nlen > 0 then
             for J in 1 .. Left loop
-               Result.Data (Pos .. Pos + Rlen - 1) := Right;
+               Result.Data (Pos + 1 .. Pos + Rlen) :=
+                 Super_String_Data (Right);
+               pragma Assert
+                 (for all K in 1 .. Rlen => Result.Data (Pos + K) =
+                    Right (Right'First - 1 + K));
+               pragma Assert
+                 (String (Result.Data (Pos + 1 .. Pos + Rlen)) = Right);
+               Lemma_Split;
                Pos := Pos + Rlen;
+               pragma Loop_Invariant (Pos = J * Rlen);
+               pragma Loop_Invariant (Result.Data (1 .. Pos)'Initialized);
+               pragma Loop_Invariant
+                 (for all K in 1 .. Pos =>
+                    Result.Data (K) =
+                      Right (Right'First + (K - 1) mod Rlen));
             end loop;
          end if;
+
+         Result.Current_Length := Nlen;
       end if;
 
       return Result;
@@ -1862,7 +2167,7 @@ package body Ada.Strings.Superbounded is
       Right : Super_String) return Super_String
    is
       Result : Super_String (Right.Max_Length);
-      Pos    : Positive := 1;
+      Pos    : Natural          := 0;
       Rlen   : constant Natural := Right.Current_Length;
       Nlen   : constant Natural := Left * Rlen;
 
@@ -1871,15 +2176,21 @@ package body Ada.Strings.Superbounded is
          raise Ada.Strings.Length_Error;
 
       else
-         Result.Current_Length := Nlen;
-
          if Nlen > 0 then
             for J in 1 .. Left loop
-               Result.Data (Pos .. Pos + Rlen - 1) :=
+               Result.Data (Pos + 1 .. Pos + Rlen) :=
                  Right.Data (1 .. Rlen);
                Pos := Pos + Rlen;
+               pragma Loop_Invariant (Pos = J * Rlen);
+               pragma Loop_Invariant (Result.Data (1 .. Pos)'Initialized);
+               pragma Loop_Invariant
+                 (for all K in 1 .. Pos =>
+                    Result.Data (K) =
+                      Right.Data (1 + (K - 1) mod Rlen));
             end loop;
          end if;
+
+         Result.Current_Length := Nlen;
       end if;
 
       return Result;
@@ -1891,7 +2202,7 @@ package body Ada.Strings.Superbounded is
 
    function To_Super_String
      (Source     : String;
-      Max_Length : Natural;
+      Max_Length : Positive;
       Drop       : Truncation := Error) return Super_String
    is
       Result : Super_String (Max_Length);
@@ -1899,20 +2210,20 @@ package body Ada.Strings.Superbounded is
 
    begin
       if Slen <= Max_Length then
+         Result.Data (1 .. Slen) := Super_String_Data (Source);
          Result.Current_Length := Slen;
-         Result.Data (1 .. Slen) := Source;
 
       else
          case Drop is
             when Strings.Right =>
+               Result.Data (1 .. Max_Length) := Super_String_Data
+                 (Source (Source'First .. Source'First - 1 + Max_Length));
                Result.Current_Length := Max_Length;
-               Result.Data (1 .. Max_Length) :=
-                 Source (Source'First .. Source'First - 1 + Max_Length);
 
             when Strings.Left =>
+               Result.Data (1 .. Max_Length) := Super_String_Data
+                 (Source (Source'Last - (Max_Length - 1) .. Source'Last));
                Result.Current_Length := Max_Length;
-               Result.Data (1 .. Max_Length) :=
-                 Source (Source'Last - (Max_Length - 1) .. Source'Last);
 
             when Strings.Error =>
                raise Ada.Strings.Length_Error;
diff --git a/gcc/ada/libgnat/a-strsup.ads b/gcc/ada/libgnat/a-strsup.ads
index 9e568a8..7428e9c 100644
--- a/gcc/ada/libgnat/a-strsup.ads
+++ b/gcc/ada/libgnat/a-strsup.ads
@@ -36,28 +36,47 @@
 --  length as the discriminant. Individual instantiations of Strings.Bounded
 --  use this type with an appropriate discriminant value set.
 
-with Ada.Strings.Maps;
+--  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. Postconditions and
+--  contract cases should not be executed at runtime as well, in order not to
+--  slow down the execution of these functions.
 
-package Ada.Strings.Superbounded is
+pragma Assertion_Policy (Pre            => Ignore,
+                         Post           => Ignore,
+                         Contract_Cases => Ignore,
+                         Ghost          => Ignore);
+
+with Ada.Strings.Maps; use type Ada.Strings.Maps.Character_Mapping_Function;
+with Ada.Strings.Search;
+
+package Ada.Strings.Superbounded with SPARK_Mode is
    pragma Preelaborate;
 
    --  Type Bounded_String in Ada.Strings.Bounded.Generic_Bounded_Length is
    --  derived from Super_String, with the constraint of the maximum length.
 
+   type Super_String_Data is new String with Relaxed_Initialization;
+
    type Super_String (Max_Length : Positive) is record
       Current_Length : Natural := 0;
-      Data           : String (1 .. Max_Length);
+      Data           : Super_String_Data (1 .. Max_Length);
       --  A previous version had a default initial value for Data, which is
       --  no longer necessary, because we now special-case this type in the
       --  compiler, so "=" composes properly for descendants of this type.
       --  Leaving it out is more efficient.
-   end record;
+   end record
+   with
+     Predicate =>
+       Current_Length <= Max_Length
+         and then Data (1 .. Current_Length)'Initialized;
 
    --  The subprograms defined for Super_String are similar to those
    --  defined for Bounded_String, except that they have different names, so
    --  that they can be renamed in Ada.Strings.Bounded.Generic_Bounded_Length.
 
-   function Super_Length (Source : Super_String) return Natural;
+   function Super_Length (Source : Super_String) return Natural
+   is (Source.Current_Length);
 
    --------------------------------------------------------
    -- Conversion, Concatenation, and Selection Functions --
@@ -65,109 +84,606 @@ package Ada.Strings.Superbounded is
 
    function To_Super_String
      (Source     : String;
-      Max_Length : Natural;
-      Drop       : Truncation := Error) return Super_String;
+      Max_Length : Positive;
+      Drop       : Truncation := Error) return Super_String
+   with
+     Pre            => (if Source'Length > Max_Length then Drop /= Error),
+     Post           => To_Super_String'Result.Max_Length = Max_Length,
+     Contract_Cases =>
+       (Source'Length <= Max_Length
+        =>
+          Super_To_String (To_Super_String'Result) = Source,
+
+        Source'Length > Max_Length and then Drop = Left
+        =>
+          Super_To_String (To_Super_String'Result) =
+            Source (Source'Last - Max_Length + 1 .. Source'Last),
+
+        others  --  Drop = Right
+        =>
+          Super_To_String (To_Super_String'Result) =
+            Source (Source'First .. Source'First - 1 + Max_Length)),
+     Global         => null;
    --  Note the additional parameter Max_Length, which specifies the maximum
    --  length setting of the resulting Super_String value.
 
    --  The following procedures have declarations (and semantics) that are
    --  exactly analogous to those declared in Ada.Strings.Bounded.
 
-   function Super_To_String (Source : Super_String) return String;
+   function Super_To_String (Source : Super_String) return String
+   is (String (Source.Data (1 .. Source.Current_Length)));
 
    procedure Set_Super_String
      (Target : out Super_String;
       Source : String;
-      Drop   : Truncation := Error);
+      Drop   : Truncation := Error)
+   with
+     Pre            =>
+       (if Source'Length > Target.Max_Length then Drop /= Error),
+     Contract_Cases =>
+       (Source'Length <= Target.Max_Length
+        =>
+          Super_To_String (Target) = Source,
+
+        Source'Length > Target.Max_Length and then Drop = Left
+        =>
+          Super_To_String (Target) =
+            Source (Source'Last - Target.Max_Length + 1 .. Source'Last),
+
+        others  --  Drop = Right
+        =>
+          Super_To_String (Target) =
+            Source (Source'First .. Source'First - 1 + Target.Max_Length)),
+     Global         => null;
 
    function Super_Append
      (Left  : Super_String;
       Right : Super_String;
-      Drop  : Truncation  := Error) return Super_String;
+      Drop  : Truncation  := Error) return Super_String
+   with
+     Pre            =>
+       Left.Max_Length = Right.Max_Length
+         and then
+           (if Super_Length (Left) > Left.Max_Length - Super_Length (Right)
+            then Drop /= Error),
+     Post           => Super_Append'Result.Max_Length = Left.Max_Length,
+     Contract_Cases =>
+       (Super_Length (Left) <= Left.Max_Length - Super_Length (Right)
+        =>
+          Super_Length (Super_Append'Result) =
+            Super_Length (Left) + Super_Length (Right)
+            and then
+              Super_Slice (Super_Append'Result, 1, Super_Length (Left)) =
+                Super_To_String (Left)
+            and then
+              (if Super_Length (Right) > 0 then
+                 Super_Slice (Super_Append'Result,
+                   Super_Length (Left) + 1,
+                   Super_Length (Super_Append'Result)) =
+                     Super_To_String (Right)),
+
+        Super_Length (Left) > Left.Max_Length - Super_Length (Right)
+          and then Drop = Strings.Left
+        =>
+          Super_Length (Super_Append'Result) = Left.Max_Length
+            and then
+              (if Super_Length (Right) < Left.Max_Length then
+                 String'(Super_Slice (Super_Append'Result,
+                   1, Left.Max_Length - Super_Length (Right))) =
+                     Super_Slice (Left,
+                       Super_Length (Left) - Left.Max_Length
+                         + Super_Length (Right) + 1,
+                       Super_Length (Left)))
+            and then
+              Super_Slice (Super_Append'Result,
+                Left.Max_Length - Super_Length (Right) + 1, Left.Max_Length) =
+                  Super_To_String (Right),
+
+        others  --  Drop = Right
+        =>
+          Super_Length (Super_Append'Result) = Left.Max_Length
+            and then
+              Super_Slice (Super_Append'Result, 1, Super_Length (Left)) =
+                Super_To_String (Left)
+            and then
+              (if Super_Length (Left) < Left.Max_Length then
+                 String'(Super_Slice (Super_Append'Result,
+                   Super_Length (Left) + 1, Left.Max_Length)) =
+                     Super_Slice (Right,
+                       1, Left.Max_Length - Super_Length (Left)))),
+     Global         => null;
 
    function Super_Append
      (Left  : Super_String;
       Right : String;
-      Drop  : Truncation := Error) return Super_String;
+      Drop  : Truncation := Error) return Super_String
+   with
+     Pre            =>
+       (if Right'Length > Left.Max_Length - Super_Length (Left)
+        then Drop /= Error),
+     Post           => Super_Append'Result.Max_Length = Left.Max_Length,
+     Contract_Cases =>
+       (Super_Length (Left) <= Left.Max_Length - Right'Length
+        =>
+          Super_Length (Super_Append'Result) =
+            Super_Length (Left) + Right'Length
+            and then
+              Super_Slice (Super_Append'Result, 1, Super_Length (Left)) =
+                Super_To_String (Left)
+            and then
+              (if Right'Length > 0 then
+                 Super_Slice (Super_Append'Result,
+                   Super_Length (Left) + 1,
+                   Super_Length (Super_Append'Result)) =
+                     Right),
+
+        Super_Length (Left) > Left.Max_Length - Right'Length
+          and then Drop = Strings.Left
+        =>
+          Super_Length (Super_Append'Result) = Left.Max_Length
+            and then
+              (if Right'Length < Left.Max_Length then
+
+                 --  The result is the end of Left followed by Right
+
+                 String'(Super_Slice (Super_Append'Result,
+                   1, Left.Max_Length - Right'Length)) =
+                     Super_Slice (Left,
+                       Super_Length (Left) - Left.Max_Length + Right'Length
+                         + 1,
+                       Super_Length (Left))
+                   and then
+                     Super_Slice (Super_Append'Result,
+                       Left.Max_Length - Right'Length + 1, Left.Max_Length) =
+                         Right
+               else
+                 --  The result is the last Max_Length characters of Right
+
+                 Super_To_String (Super_Append'Result) =
+                   Right (Right'Last - Left.Max_Length + 1 .. Right'Last)),
+
+        others  --  Drop = Right
+        =>
+          Super_Length (Super_Append'Result) = Left.Max_Length
+            and then
+              Super_Slice (Super_Append'Result, 1, Super_Length (Left)) =
+                Super_To_String (Left)
+            and then
+              (if Super_Length (Left) < Left.Max_Length then
+                 Super_Slice (Super_Append'Result,
+                   Super_Length (Left) + 1, Left.Max_Length) =
+                     Right (Right'First
+                       .. Left.Max_Length - Super_Length (Left)
+                            - 1 + Right'First))),
+     Global         => null;
 
    function Super_Append
      (Left  : String;
       Right : Super_String;
-      Drop  : Truncation := Error) return Super_String;
+      Drop  : Truncation := Error) return Super_String
+   with
+     Pre            =>
+       (if Left'Length > Right.Max_Length - Super_Length (Right)
+        then Drop /= Error),
+     Post           => Super_Append'Result.Max_Length = Right.Max_Length,
+     Contract_Cases =>
+       (Left'Length <= Right.Max_Length - Super_Length (Right)
+        =>
+          Super_Length (Super_Append'Result) =
+            Left'Length + Super_Length (Right)
+            and then Super_Slice (Super_Append'Result, 1, Left'Length) = Left
+            and then
+              (if Super_Length (Right) > 0 then
+                 Super_Slice (Super_Append'Result,
+                   Left'Length + 1, Super_Length (Super_Append'Result)) =
+                     Super_To_String (Right)),
+
+        Left'Length > Right.Max_Length - Super_Length (Right)
+          and then Drop = Strings.Left
+        =>
+          Super_Length (Super_Append'Result) = Right.Max_Length
+            and then
+              (if Super_Length (Right) < Right.Max_Length then
+                 Super_Slice (Super_Append'Result,
+                   1, Right.Max_Length - Super_Length (Right)) =
+                     Left
+                       (Left'Last - Right.Max_Length + Super_Length (Right) + 1
+                        .. Left'Last))
+            and then
+              Super_Slice (Super_Append'Result,
+                Right.Max_Length - Super_Length (Right) + 1,
+                Right.Max_Length) =
+                  Super_To_String (Right),
+
+        others  --  Drop = Right
+        =>
+          Super_Length (Super_Append'Result) = Right.Max_Length
+            and then
+              (if Left'Length < Right.Max_Length then
+
+                 --  The result is Left followed by the beginning of Right
+
+                 Super_Slice (Super_Append'Result, 1, Left'Length) = Left
+                   and then
+                     String'(Super_Slice (Super_Append'Result,
+                       Left'Length + 1, Right.Max_Length)) =
+                         Super_Slice (Right, 1, Right.Max_Length - Left'Length)
+               else
+                 --  The result is the first Max_Length characters of Left
+
+                 Super_To_String (Super_Append'Result) =
+                   Left (Left'First .. Right.Max_Length - 1 + Left'First))),
+     Global         => null;
 
    function Super_Append
      (Left  : Super_String;
       Right : Character;
-      Drop  : Truncation := Error) return Super_String;
+      Drop  : Truncation := Error) return Super_String
+   with
+     Pre            =>
+       (if Super_Length (Left) = Left.Max_Length then Drop /= Error),
+     Post           => Super_Append'Result.Max_Length = Left.Max_Length,
+     Contract_Cases =>
+       (Super_Length (Left) < Left.Max_Length
+        =>
+          Super_Length (Super_Append'Result) = Super_Length (Left) + 1
+            and then
+              Super_Slice (Super_Append'Result, 1, Super_Length (Left)) =
+                Super_To_String (Left)
+            and then
+              Super_Element (Super_Append'Result, Super_Length (Left) + 1) =
+                Right,
+
+        Super_Length (Left) = Left.Max_Length and then Drop = Strings.Right
+        =>
+          Super_Length (Super_Append'Result) = Left.Max_Length
+            and then
+              Super_To_String (Super_Append'Result) = Super_To_String (Left),
+
+        others  --  Drop = Left
+        =>
+          Super_Length (Super_Append'Result) = Left.Max_Length
+            and then
+              String'(Super_Slice (Super_Append'Result,
+                1, Left.Max_Length - 1)) =
+                  Super_Slice (Left, 2, Left.Max_Length)
+            and then
+              Super_Element (Super_Append'Result, Left.Max_Length) = Right),
+     Global         => null;
 
    function Super_Append
      (Left  : Character;
       Right : Super_String;
-      Drop  : Truncation := Error) return Super_String;
+      Drop  : Truncation := Error) return Super_String
+   with
+     Pre            =>
+       (if Super_Length (Right) = Right.Max_Length then Drop /= Error),
+     Post           => Super_Append'Result.Max_Length = Right.Max_Length,
+     Contract_Cases =>
+       (Super_Length (Right) < Right.Max_Length
+        =>
+          Super_Length (Super_Append'Result) = Super_Length (Right) + 1
+            and then
+              Super_Slice (Super_Append'Result, 2, Super_Length (Right) + 1) =
+                Super_To_String (Right)
+            and then Super_Element (Super_Append'Result, 1) = Left,
+
+        Super_Length (Right) = Right.Max_Length and then Drop = Strings.Left
+        =>
+          Super_Length (Super_Append'Result) = Right.Max_Length
+            and then
+              Super_To_String (Super_Append'Result) = Super_To_String (Right),
+
+        others  --  Drop = Right
+        =>
+          Super_Length (Super_Append'Result) = Right.Max_Length
+            and then
+              String'(Super_Slice (Super_Append'Result, 2, Right.Max_Length)) =
+                Super_Slice (Right, 1, Right.Max_Length - 1)
+            and then Super_Element (Super_Append'Result, 1) = Left),
+     Global         => null;
 
    procedure Super_Append
      (Source   : in out Super_String;
       New_Item : Super_String;
-      Drop     : Truncation  := Error);
+      Drop     : Truncation  := Error)
+   with
+     Pre            =>
+       Source.Max_Length = New_Item.Max_Length
+         and then
+           (if Super_Length (Source) >
+                 Source.Max_Length - Super_Length (New_Item)
+            then Drop /= Error),
+     Contract_Cases =>
+       (Super_Length (Source) <= Source.Max_Length - Super_Length (New_Item)
+        =>
+          Super_Length (Source) =
+            Super_Length (Source'Old) + Super_Length (New_Item)
+            and then
+              Super_Slice (Source, 1, Super_Length (Source'Old)) =
+                Super_To_String (Source'Old)
+            and then
+              (if Super_Length (New_Item) > 0 then
+                 Super_Slice (Source,
+                   Super_Length (Source'Old) + 1, Super_Length (Source)) =
+                     Super_To_String (New_Item)),
+
+        Super_Length (Source) > Source.Max_Length - Super_Length (New_Item)
+          and then Drop = Left
+        =>
+          Super_Length (Source) = Source.Max_Length
+            and then
+              (if Super_Length (New_Item) < Source.Max_Length then
+                 String'(Super_Slice (Source,
+                   1, Source.Max_Length - Super_Length (New_Item))) =
+                     Super_Slice (Source'Old,
+                       Super_Length (Source'Old) - Source.Max_Length
+                         + Super_Length (New_Item) + 1,
+                       Super_Length (Source'Old)))
+            and then
+              Super_Slice (Source,
+                Source.Max_Length - Super_Length (New_Item) + 1,
+                Source.Max_Length) =
+                  Super_To_String (New_Item),
+
+        others  --  Drop = Right
+        =>
+          Super_Length (Source) = Source.Max_Length
+            and then
+              Super_Slice (Source, 1, Super_Length (Source'Old)) =
+                Super_To_String (Source'Old)
+            and then
+              (if Super_Length (Source'Old) < Source.Max_Length then
+                 String'(Super_Slice (Source,
+                   Super_Length (Source'Old) + 1, Source.Max_Length)) =
+                     Super_Slice (New_Item,
+                       1, Source.Max_Length - Super_Length (Source'Old)))),
+     Global         => null;
 
    procedure Super_Append
      (Source   : in out Super_String;
       New_Item : String;
-      Drop     : Truncation  := Error);
+      Drop     : Truncation  := Error)
+   with
+     Pre            =>
+       (if New_Item'Length > Source.Max_Length - Super_Length (Source)
+        then Drop /= Error),
+     Contract_Cases =>
+       (Super_Length (Source) <= Source.Max_Length - New_Item'Length
+        =>
+          Super_Length (Source) = Super_Length (Source'Old) + New_Item'Length
+            and then
+              Super_Slice (Source, 1, Super_Length (Source'Old)) =
+                Super_To_String (Source'Old)
+            and then
+              (if New_Item'Length > 0 then
+                 Super_Slice (Source,
+                   Super_Length (Source'Old) + 1, Super_Length (Source)) =
+                     New_Item),
+
+        Super_Length (Source) > Source.Max_Length - New_Item'Length
+          and then Drop = Left
+        =>
+          Super_Length (Source) = Source.Max_Length
+            and then
+              (if New_Item'Length < Source.Max_Length then
+
+                 --  The result is the end of Source followed by New_Item
+
+                 String'(Super_Slice (Source,
+                   1, Source.Max_Length - New_Item'Length)) =
+                     Super_Slice (Source'Old,
+                       Super_Length (Source'Old) - Source.Max_Length
+                         + New_Item'Length + 1,
+                       Super_Length (Source'Old))
+                 and then
+                   Super_Slice (Source,
+                     Source.Max_Length - New_Item'Length + 1,
+                     Source.Max_Length) =
+                       New_Item
+               else
+                 --  The result is the last Max_Length characters of
+                 --  New_Item.
+
+                 Super_To_String (Source) = New_Item
+                   (New_Item'Last - Source.Max_Length + 1 .. New_Item'Last)),
+
+        others  --  Drop = Right
+        =>
+          Super_Length (Source) = Source.Max_Length
+            and then
+              Super_Slice (Source, 1, Super_Length (Source'Old)) =
+                Super_To_String (Source'Old)
+            and then
+              (if Super_Length (Source'Old) < Source.Max_Length then
+                 Super_Slice (Source,
+                   Super_Length (Source'Old) + 1, Source.Max_Length) =
+                     New_Item (New_Item'First
+                       .. Source.Max_Length - Super_Length (Source'Old) - 1
+                         + New_Item'First))),
+     Global         => null;
 
    procedure Super_Append
      (Source   : in out Super_String;
       New_Item : Character;
-      Drop     : Truncation  := Error);
+      Drop     : Truncation  := Error)
+   with
+     Pre            =>
+       (if Super_Length (Source) = Source.Max_Length then Drop /= Error),
+     Contract_Cases =>
+       (Super_Length (Source) < Source.Max_Length
+        =>
+          Super_Length (Source) = Super_Length (Source'Old) + 1
+            and then
+              Super_Slice (Source, 1, Super_Length (Source'Old)) =
+                Super_To_String (Source'Old)
+            and then
+              Super_Element (Source, Super_Length (Source'Old) + 1) = New_Item,
+
+        Super_Length (Source) = Source.Max_Length and then Drop = Right
+        =>
+          Super_Length (Source) = Source.Max_Length
+            and then Super_To_String (Source) = Super_To_String (Source'Old),
+
+        others  --  Drop = Left
+        =>
+          Super_Length (Source) = Source.Max_Length
+            and then
+              String'(Super_Slice (Source, 1, Source.Max_Length - 1)) =
+                Super_Slice (Source'Old, 2, Source.Max_Length)
+            and then Super_Element (Source, Source.Max_Length) = New_Item),
+     Global         => null;
 
    function Concat
      (Left  : Super_String;
-      Right : Super_String) return Super_String;
+      Right : Super_String) return Super_String
+   with
+     Pre    => Left.Max_Length = Right.Max_Length
+       and then Super_Length (Left) <= Left.Max_Length - Super_Length (Right),
+     Post   => Concat'Result.Max_Length = Left.Max_Length
+       and then
+         Super_Length (Concat'Result) =
+           Super_Length (Left) + Super_Length (Right)
+       and then
+         Super_Slice (Concat'Result, 1, Super_Length (Left)) =
+           Super_To_String (Left)
+       and then
+         (if Super_Length (Right) > 0 then
+            Super_Slice (Concat'Result,
+              Super_Length (Left) + 1, Super_Length (Concat'Result)) =
+              Super_To_String (Right)),
+     Global => null;
 
    function Concat
      (Left  : Super_String;
-      Right : String) return Super_String;
+      Right : String) return Super_String
+   with
+     Pre    => Right'Length <= Left.Max_Length - Super_Length (Left),
+     Post   => Concat'Result.Max_Length = Left.Max_Length
+       and then
+         Super_Length (Concat'Result) = Super_Length (Left) + Right'Length
+       and then
+         Super_Slice (Concat'Result, 1, Super_Length (Left)) =
+           Super_To_String (Left)
+       and then
+         (if Right'Length > 0 then
+            Super_Slice (Concat'Result,
+              Super_Length (Left) + 1, Super_Length (Concat'Result)) =
+                Right),
+     Global => null;
 
    function Concat
      (Left  : String;
-      Right : Super_String) return Super_String;
+      Right : Super_String) return Super_String
+   with
+     Pre    => Left'Length <= Right.Max_Length - Super_Length (Right),
+     Post   => Concat'Result.Max_Length = Right.Max_Length
+       and then
+         Super_Length (Concat'Result) = Left'Length + Super_Length (Right)
+       and then Super_Slice (Concat'Result, 1, Left'Length) = Left
+       and then
+         (if Super_Length (Right) > 0 then
+            Super_Slice (Concat'Result,
+              Left'Length + 1, Super_Length (Concat'Result)) =
+                Super_To_String (Right)),
+     Global => null;
 
    function Concat
      (Left  : Super_String;
-      Right : Character) return Super_String;
+      Right : Character) return Super_String
+   with
+     Pre    => Super_Length (Left) < Left.Max_Length,
+     Post   => Concat'Result.Max_Length = Left.Max_Length
+       and then Super_Length (Concat'Result) = Super_Length (Left) + 1
+       and then
+         Super_Slice (Concat'Result, 1, Super_Length (Left)) =
+           Super_To_String (Left)
+       and then Super_Element (Concat'Result, Super_Length (Left) + 1) = Right,
+     Global => null;
 
    function Concat
      (Left  : Character;
-      Right : Super_String) return Super_String;
+      Right : Super_String) return Super_String
+   with
+     Pre    => Super_Length (Right) < Right.Max_Length,
+     Post   => Concat'Result.Max_Length = Right.Max_Length
+       and then Super_Length (Concat'Result) = 1 + Super_Length (Right)
+       and then Super_Element (Concat'Result, 1) = Left
+       and then
+         Super_Slice (Concat'Result, 2, Super_Length (Concat'Result)) =
+           Super_To_String (Right),
+     Global => null;
 
    function Super_Element
      (Source : Super_String;
-      Index  : Positive) return Character;
+      Index  : Positive) return Character
+   is (if Index <= Source.Current_Length
+       then Source.Data (Index)
+       else raise Index_Error)
+   with Pre => Index <= Super_Length (Source);
 
    procedure Super_Replace_Element
      (Source : in out Super_String;
       Index  : Positive;
-      By     : Character);
+      By     : Character)
+   with
+     Pre    => Index <= Super_Length (Source),
+     Post   => Super_Length (Source) = Super_Length (Source'Old)
+       and then
+         (for all K in 1 .. Super_Length (Source) =>
+            Super_Element (Source, K) =
+              (if K = Index then By else Super_Element (Source'Old, K))),
+     Global => null;
 
    function Super_Slice
      (Source : Super_String;
       Low    : Positive;
-      High   : Natural) return String;
+      High   : Natural) return String
+   is (if Low - 1 > Source.Current_Length or else High > Source.Current_Length
+
+       --  Note: test of High > Length is in accordance with AI95-00128
+
+       then raise Index_Error
+       else
+          --  Note: in this case, superflat bounds are not a problem, we just
+          --  get the null string in accordance with normal Ada slice rules.
+
+          String (Source.Data (Low .. High)))
+   with Pre => Low - 1 <= Super_Length (Source)
+                 and then High <= Super_Length (Source);
 
    function Super_Slice
      (Source : Super_String;
       Low    : Positive;
-      High   : Natural) return Super_String;
+      High   : Natural) return Super_String
+    with
+     Pre    =>
+       Low - 1 <= Super_Length (Source) and then High <= Super_Length (Source),
+     Post   => Super_Slice'Result.Max_Length = Source.Max_Length
+       and then
+         Super_To_String (Super_Slice'Result) =
+           Super_Slice (Source, Low, High),
+     Global => null;
 
    procedure Super_Slice
      (Source : Super_String;
       Target : out Super_String;
       Low    : Positive;
-      High   : Natural);
+      High   : Natural)
+   with
+     Pre    => Source.Max_Length = Target.Max_Length
+       and then Low - 1 <= Super_Length (Source)
+       and then High <= Super_Length (Source),
+     Post   => Super_To_String (Target) = Super_Slice (Source, Low, High),
+     Global => null;
 
    function "="
      (Left  : Super_String;
-      Right : Super_String) return Boolean;
+      Right : Super_String) return Boolean
+   with
+     Pre    => Left.Max_Length = Right.Max_Length,
+     Post   => "="'Result = (Super_To_String (Left) = Super_To_String (Right)),
+     Global => null;
 
    function Equal
      (Left  : Super_String;
@@ -175,59 +691,111 @@ package Ada.Strings.Superbounded is
 
    function Equal
      (Left  : Super_String;
-      Right : String) return Boolean;
+      Right : String) return Boolean
+   with
+     Post   => Equal'Result = (Super_To_String (Left) = Right),
+     Global => null;
 
    function Equal
      (Left  : String;
-      Right : Super_String) return Boolean;
+      Right : Super_String) return Boolean
+   with
+     Post   => Equal'Result = (Left = Super_To_String (Right)),
+     Global => null;
 
    function Less
      (Left  : Super_String;
-      Right : Super_String) return Boolean;
+      Right : Super_String) return Boolean
+   with
+     Pre    => Left.Max_Length = Right.Max_Length,
+     Post   =>
+       Less'Result = (Super_To_String (Left) < Super_To_String (Right)),
+     Global => null;
 
    function Less
      (Left  : Super_String;
-      Right : String) return Boolean;
+      Right : String) return Boolean
+   with
+     Post   => Less'Result = (Super_To_String (Left) < Right),
+     Global => null;
 
    function Less
      (Left  : String;
-      Right : Super_String) return Boolean;
+      Right : Super_String) return Boolean
+   with
+     Post   => Less'Result = (Left < Super_To_String (Right)),
+     Global => null;
 
    function Less_Or_Equal
      (Left  : Super_String;
-      Right : Super_String) return Boolean;
+      Right : Super_String) return Boolean
+   with
+     Pre    => Left.Max_Length = Right.Max_Length,
+     Post   =>
+       Less_Or_Equal'Result =
+         (Super_To_String (Left) <= Super_To_String (Right)),
+     Global => null;
 
    function Less_Or_Equal
      (Left  : Super_String;
-      Right : String) return Boolean;
+      Right : String) return Boolean
+   with
+     Post   => Less_Or_Equal'Result = (Super_To_String (Left) <= Right),
+     Global => null;
 
    function Less_Or_Equal
      (Left  : String;
-      Right : Super_String) return Boolean;
+      Right : Super_String) return Boolean
+   with
+     Post   => Less_Or_Equal'Result = (Left <= Super_To_String (Right)),
+     Global => null;
 
    function Greater
      (Left  : Super_String;
-      Right : Super_String) return Boolean;
+      Right : Super_String) return Boolean
+   with
+     Pre    => Left.Max_Length = Right.Max_Length,
+     Post   =>
+       Greater'Result = (Super_To_String (Left) > Super_To_String (Right)),
+     Global => null;
 
    function Greater
      (Left  : Super_String;
-      Right : String) return Boolean;
+      Right : String) return Boolean
+   with
+     Post   => Greater'Result = (Super_To_String (Left) > Right),
+     Global => null;
 
    function Greater
      (Left  : String;
-      Right : Super_String) return Boolean;
+      Right : Super_String) return Boolean
+   with
+     Post   => Greater'Result = (Left > Super_To_String (Right)),
+     Global => null;
 
    function Greater_Or_Equal
      (Left  : Super_String;
-      Right : Super_String) return Boolean;
+      Right : Super_String) return Boolean
+   with
+     Pre    => Left.Max_Length = Right.Max_Length,
+     Post   =>
+       Greater_Or_Equal'Result =
+         (Super_To_String (Left) >= Super_To_String (Right)),
+     Global => null;
 
    function Greater_Or_Equal
      (Left  : Super_String;
-      Right : String) return Boolean;
+      Right : String) return Boolean
+   with
+     Post   => Greater_Or_Equal'Result = (Super_To_String (Left) >= Right),
+     Global => null;
 
    function Greater_Or_Equal
      (Left  : String;
-      Right : Super_String) return Boolean;
+      Right : Super_String) return Boolean
+   with
+     Post   => Greater_Or_Equal'Result = (Left >= Super_To_String (Right)),
+     Global => null;
 
    ----------------------
    -- Search Functions --
@@ -237,63 +805,449 @@ package Ada.Strings.Superbounded is
      (Source  : Super_String;
       Pattern : String;
       Going   : Direction := Forward;
-      Mapping : Maps.Character_Mapping := Maps.Identity) return Natural;
+      Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
+   with
+     Pre            => Pattern'Length > 0,
+     Post           => Super_Index'Result <= Super_Length (Source),
+     Contract_Cases =>
+
+       --  If Source is the empty string, then 0 is returned
+
+       (Super_Length (Source) = 0
+        =>
+          Super_Index'Result = 0,
+
+        --  If some slice of Source matches Pattern, then a valid index is
+        --  returned.
+
+        Super_Length (Source) > 0
+          and then
+            (for some J in 1 .. Super_Length (Source) - (Pattern'Length - 1) =>
+               Search.Match (Super_To_String (Source), Pattern, Mapping, J))
+        =>
+          --  The result is in the considered range of Source
+
+          Super_Index'Result in
+            1 .. Super_Length (Source) - (Pattern'Length - 1)
+
+            --  The slice beginning at the returned index matches Pattern
+
+            and then Search.Match
+              (Super_To_String (Source), Pattern, Mapping, Super_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 .. Super_Length (Source) =>
+                 (if (if Going = Forward
+                      then J <= Super_Index'Result - 1
+                      else J - 1 in Super_Index'Result
+                                    .. Super_Length (Source) - Pattern'Length)
+                  then not (Search.Match
+                    (Super_To_String (Source), Pattern, Mapping, J)))),
+
+        --  Otherwise, 0 is returned
+
+        others
+        =>
+          Super_Index'Result = 0),
+     Global         => null;
 
    function Super_Index
      (Source  : Super_String;
       Pattern : String;
       Going   : Direction := Forward;
-      Mapping : Maps.Character_Mapping_Function) return Natural;
+      Mapping : Maps.Character_Mapping_Function) return Natural
+   with
+     Pre            => Pattern'Length /= 0 and then Mapping /= null,
+     Post           => Super_Index'Result <= Super_Length (Source),
+     Contract_Cases =>
+
+       --  If Source is the empty string, then 0 is returned
+
+       (Super_Length (Source) = 0
+        =>
+          Super_Index'Result = 0,
+
+        --  If some slice of Source matches Pattern, then a valid index is
+        --  returned.
+
+        Super_Length (Source) > 0
+          and then
+            (for some J in 1 .. Super_Length (Source) - (Pattern'Length - 1) =>
+               Search.Match (Super_To_String (Source), Pattern, Mapping, J))
+        =>
+          --  The result is in the considered range of Source
+
+          Super_Index'Result in
+            1 .. Super_Length (Source) - (Pattern'Length - 1)
+
+            --  The slice beginning at the returned index matches Pattern
+
+            and then Search.Match
+              (Super_To_String (Source), Pattern, Mapping, Super_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 .. Super_Length (Source) =>
+                 (if (if Going = Forward
+                      then J <= Super_Index'Result - 1
+                      else J - 1 in Super_Index'Result
+                                    .. Super_Length (Source) - Pattern'Length)
+                  then not (Search.Match
+                    (Super_To_String (Source), Pattern, Mapping, J)))),
+
+        --  Otherwise, 0 is returned
+
+        others
+        =>
+          Super_Index'Result = 0),
+     Global         => null;
 
    function Super_Index
      (Source : Super_String;
       Set    : Maps.Character_Set;
       Test   : Membership := Inside;
-      Going  : Direction  := Forward) return Natural;
+      Going  : Direction  := Forward) return Natural
+   with
+     Post           => Super_Index'Result <= Super_Length (Source),
+     Contract_Cases =>
+
+        --  If no character of Source satisfies the property Test on Set,
+        --  then 0 is returned.
+
+       ((for all C of Super_To_String (Source) =>
+           (Test = Inside) /= Maps.Is_In (C, Set))
+        =>
+          Super_Index'Result = 0,
+
+        --  Otherwise, an index in the range of Source is returned
+
+        others
+        =>
+          --  The result is in the range of Source
+
+          Super_Index'Result in 1 .. Super_Length (Source)
+
+            --  The character at the returned index satisfies the property
+            --  Test on Set.
+
+            and then
+              (Test = Inside) =
+                Maps.Is_In (Super_Element (Source, Super_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 .. Super_Length (Source) =>
+                 (if J /= Super_Index'Result
+                       and then (J < Super_Index'Result) = (Going = Forward)
+                  then (Test = Inside)
+                       /= Maps.Is_In (Super_Element (Source, J), Set)))),
+     Global         => null;
 
    function Super_Index
      (Source  : Super_String;
       Pattern : String;
       From    : Positive;
       Going   : Direction := Forward;
-      Mapping : Maps.Character_Mapping := Maps.Identity) return Natural;
+      Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
+   with
+     Pre            =>
+       (if Super_Length (Source) /= 0 then From <= Super_Length (Source))
+         and then Pattern'Length /= 0,
+     Post           => Super_Index'Result <= Super_Length (Source),
+     Contract_Cases =>
+
+       --  If Source is the empty string, then 0 is returned
+
+       (Super_Length (Source) = 0
+        =>
+          Super_Index'Result = 0,
+
+        --  If some slice of Source matches Pattern, then a valid index is
+        --  returned.
+
+        Super_Length (Source) > 0
+          and then
+            (for some J in
+              (if Going = Forward then From else 1)
+               .. (if Going = Forward then Super_Length (Source) else From)
+                - (Pattern'Length - 1) =>
+              Search.Match (Super_To_String (Source), Pattern, Mapping, J))
+        =>
+          --  The result is in the considered range of Source
+
+          Super_Index'Result in
+            (if Going = Forward then From else 1)
+            .. (if Going = Forward then Super_Length (Source) else From)
+             - (Pattern'Length - 1)
+
+            --  The slice beginning at the returned index matches Pattern
+
+            and then Search.Match
+              (Super_To_String (Source), Pattern, Mapping, Super_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 .. Super_Length (Source) =>
+                 (if (if Going = Forward
+                      then J in From .. Super_Index'Result - 1
+                      else J - 1 in Super_Index'Result
+                                    .. From - Pattern'Length)
+                  then not (Search.Match
+                    (Super_To_String (Source), Pattern, Mapping, J)))),
+
+        --  Otherwise, 0 is returned
+
+        others
+        =>
+          Super_Index'Result = 0),
+     Global         => null;
 
    function Super_Index
      (Source  : Super_String;
       Pattern : String;
       From    : Positive;
       Going   : Direction := Forward;
-      Mapping : Maps.Character_Mapping_Function) return Natural;
+      Mapping : Maps.Character_Mapping_Function) return Natural
+   with
+     Pre            =>
+       (if Super_Length (Source) /= 0 then From <= Super_Length (Source))
+         and then Pattern'Length /= 0
+         and then Mapping /= null,
+     Post           => Super_Index'Result <= Super_Length (Source),
+     Contract_Cases =>
+
+       --  If Source is the empty string, then 0 is returned
+
+       (Super_Length (Source) = 0
+        =>
+          Super_Index'Result = 0,
+
+        --  If some slice of Source matches Pattern, then a valid index is
+        --  returned.
+
+        Super_Length (Source) > 0
+          and then
+            (for some J in
+              (if Going = Forward then From else 1)
+               .. (if Going = Forward then Super_Length (Source) else From)
+                - (Pattern'Length - 1) =>
+              Search.Match (Super_To_String (Source), Pattern, Mapping, J))
+        =>
+          --  The result is in the considered range of Source
+
+          Super_Index'Result in
+            (if Going = Forward then From else 1)
+            .. (if Going = Forward then Super_Length (Source) else From)
+             - (Pattern'Length - 1)
+
+            --  The slice beginning at the returned index matches Pattern
+
+            and then Search.Match
+              (Super_To_String (Source), Pattern, Mapping, Super_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 .. Super_Length (Source) =>
+                 (if (if Going = Forward
+                      then J in From .. Super_Index'Result - 1
+                      else J - 1 in Super_Index'Result
+                                    .. From - Pattern'Length)
+                  then not (Search.Match
+                    (Super_To_String (Source), Pattern, Mapping, J)))),
+
+        --  Otherwise, 0 is returned
+
+        others
+        =>
+          Super_Index'Result = 0),
+     Global         => null;
 
    function Super_Index
      (Source : Super_String;
       Set    : Maps.Character_Set;
       From   : Positive;
       Test   : Membership := Inside;
-      Going  : Direction := Forward) return Natural;
+      Going  : Direction := Forward) return Natural
+   with
+     Pre            =>
+       (if Super_Length (Source) /= 0 then From <= Super_Length (Source)),
+     Post           => Super_Index'Result <= Super_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.
+
+       (Super_Length (Source) = 0
+          or else
+            (for all J in 1 .. Super_Length (Source) =>
+               (if J = From or else (J > From) = (Going = Forward) then
+                  (Test = Inside) /=
+                    Maps.Is_In (Super_Element (Source, J), Set)))
+        =>
+          Super_Index'Result = 0,
+
+        --  Otherwise, an index in the considered range of Source is returned
+
+        others
+        =>
+          --  The result is in the considered range of Source
+
+          Super_Index'Result in 1 .. Super_Length (Source)
+            and then
+              (Super_Index'Result = From
+                 or else (Super_Index'Result > From) = (Going = Forward))
+
+            --  The character at the returned index satisfies the property
+            --  Test on Set.
+
+            and then
+              (Test = Inside) =
+                Maps.Is_In (Super_Element (Source, Super_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 .. Super_Length (Source) =>
+                 (if J /= Super_Index'Result
+                    and then (J < Super_Index'Result) = (Going = Forward)
+                    and then (J = From
+                                or else (J > From) = (Going = Forward))
+                  then (Test = Inside)
+                       /= Maps.Is_In (Super_Element (Source, J), Set)))),
+     Global         => null;
 
    function Super_Index_Non_Blank
      (Source : Super_String;
-      Going  : Direction := Forward) return Natural;
+      Going  : Direction := Forward) return Natural
+   with
+     Post           => Super_Index_Non_Blank'Result <= Super_Length (Source),
+     Contract_Cases =>
+
+        --  If all characters of Source are Space characters, then 0 is
+        --  returned.
+
+       ((for all C of Super_To_String (Source) => C = ' ')
+        =>
+          Super_Index_Non_Blank'Result = 0,
+
+        --  Otherwise, an index in the range of Source is returned
+
+        others
+        =>
+          --  The result is in the range of Source
+
+          Super_Index_Non_Blank'Result in 1 .. Super_Length (Source)
+
+            --  The character at the returned index is not a Space character
+
+            and then
+              Super_Element (Source, Super_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 .. Super_Length (Source) =>
+                 (if J /= Super_Index_Non_Blank'Result
+                       and then
+                         (J < Super_Index_Non_Blank'Result) = (Going = Forward)
+                  then Super_Element (Source, J) = ' '))),
+     Global         => null;
 
    function Super_Index_Non_Blank
      (Source : Super_String;
       From   : Positive;
-      Going  : Direction := Forward) return Natural;
+      Going  : Direction := Forward) return Natural
+   with
+     Pre            =>
+       (if Super_Length (Source) /= 0 then From <= Super_Length (Source)),
+     Post           => Super_Index_Non_Blank'Result <= Super_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.
+
+       (Super_Length (Source) = 0
+          or else
+            (for all J in 1 .. Super_Length (Source) =>
+               (if J = From or else (J > From) = (Going = Forward) then
+                  Super_Element (Source, J) = ' '))
+        =>
+          Super_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
+
+          Super_Index_Non_Blank'Result in 1 .. Super_Length (Source)
+            and then
+              (Super_Index_Non_Blank'Result = From
+                 or else
+                   (Super_Index_Non_Blank'Result > From) = (Going = Forward))
+
+            --  The character at the returned index is not a Space character
+
+            and then
+              Super_Element (Source, Super_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 .. Super_Length (Source) =>
+                 (if J /= Super_Index_Non_Blank'Result
+                    and then
+                      (J < Super_Index_Non_Blank'Result) = (Going = Forward)
+                    and then (J = From
+                                or else (J > From) = (Going = Forward))
+                  then Super_Element (Source, J) = ' '))),
+     Global         => null;
 
    function Super_Count
      (Source  : Super_String;
       Pattern : String;
-      Mapping : Maps.Character_Mapping := Maps.Identity) return Natural;
+      Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
+   with
+     Pre    => Pattern'Length /= 0,
+     Global => null;
 
    function Super_Count
      (Source  : Super_String;
       Pattern : String;
-      Mapping : Maps.Character_Mapping_Function) return Natural;
+      Mapping : Maps.Character_Mapping_Function) return Natural
+   with
+     Pre    => Pattern'Length /= 0 and then Mapping /= null,
+     Global => null;
 
    function Super_Count
      (Source : Super_String;
-      Set    : Maps.Character_Set) return Natural;
+      Set    : Maps.Character_Set) return Natural
+   with
+     Global => null;
 
    procedure Super_Find_Token
      (Source : Super_String;
@@ -301,14 +1255,112 @@ package Ada.Strings.Superbounded is
       From   : Positive;
       Test   : Membership;
       First  : out Positive;
-      Last   : out Natural);
+      Last   : out Natural)
+   with
+     Pre            =>
+       (if Super_Length (Source) /= 0 then From <= Super_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.
+
+       (Super_Length (Source) = 0
+          or else
+            (for all J in From .. Super_Length (Source) =>
+               (Test = Inside) /= Maps.Is_In (Super_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 .. Super_Length (Source)
+            and then Last in First .. Super_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 (Super_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 (Super_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 < Super_Length (Source)
+               then
+                 (Test = Inside) /=
+                   Maps.Is_In (Super_Element (Source, Last + 1), Set))),
+     Global         => null;
 
    procedure Super_Find_Token
      (Source : Super_String;
       Set    : Maps.Character_Set;
       Test   : Membership;
       First  : out Positive;
-      Last   : out Natural);
+      Last   : out Natural)
+   with
+     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.
+
+       (Super_Length (Source) = 0
+          or else
+            (for all J in 1 .. Super_Length (Source) =>
+               (Test = Inside) /= Maps.Is_In (Super_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 .. Super_Length (Source)
+            and then Last in First .. Super_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 (Super_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 (Super_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 < Super_Length (Source)
+               then
+                 (Test = Inside) /=
+                   Maps.Is_In (Super_Element (Source, Last + 1), Set))),
+     Global         => null;
 
    ------------------------------------
    -- String Translation Subprograms --
@@ -316,19 +1368,51 @@ package Ada.Strings.Superbounded is
 
    function Super_Translate
      (Source  : Super_String;
-      Mapping : Maps.Character_Mapping) return Super_String;
+      Mapping : Maps.Character_Mapping) return Super_String
+   with
+     Post   => Super_Translate'Result.Max_Length = Source.Max_Length
+       and then Super_Length (Super_Translate'Result) = Super_Length (Source)
+       and then
+         (for all K in 1 .. Super_Length (Source) =>
+            Super_Element (Super_Translate'Result, K) =
+              Ada.Strings.Maps.Value (Mapping, Super_Element (Source, K))),
+     Global => null;
 
    procedure Super_Translate
      (Source   : in out Super_String;
-      Mapping  : Maps.Character_Mapping);
+      Mapping  : Maps.Character_Mapping)
+   with
+     Post   => Super_Length (Source) = Super_Length (Source'Old)
+       and then
+         (for all K in 1 .. Super_Length (Source) =>
+            Super_Element (Source, K) =
+              Ada.Strings.Maps.Value (Mapping, Super_Element (Source'Old, K))),
+     Global => null;
 
    function Super_Translate
      (Source  : Super_String;
-      Mapping : Maps.Character_Mapping_Function) return Super_String;
+      Mapping : Maps.Character_Mapping_Function) return Super_String
+   with
+     Pre    => Mapping /= null,
+     Post   => Super_Translate'Result.Max_Length = Source.Max_Length
+       and then Super_Length (Super_Translate'Result) = Super_Length (Source)
+       and then
+         (for all K in 1 .. Super_Length (Source) =>
+            Super_Element (Super_Translate'Result, K) =
+              Mapping (Super_Element (Source, K))),
+     Global => null;
 
    procedure Super_Translate
      (Source  : in out Super_String;
-      Mapping : Maps.Character_Mapping_Function);
+      Mapping : Maps.Character_Mapping_Function)
+   with
+     Pre    => Mapping /= null,
+     Post   => Super_Length (Source) = Super_Length (Source'Old)
+       and then
+         (for all K in 1 .. Super_Length (Source) =>
+            Super_Element (Source, K) =
+              Mapping (Super_Element (Source'Old, K))),
+     Global => null;
 
    ---------------------------------------
    -- String Transformation Subprograms --
@@ -339,48 +1423,756 @@ package Ada.Strings.Superbounded is
       Low    : Positive;
       High   : Natural;
       By     : String;
-      Drop   : Truncation := Error) return Super_String;
+      Drop   : Truncation := Error) return Super_String
+   with
+     Pre            =>
+       Low - 1 <= Super_Length (Source)
+         and then
+           (if Drop = Error
+              then (if High >= Low
+                      then Low - 1
+                        <= Source.Max_Length - By'Length
+                         - Integer'Max (Super_Length (Source) - High, 0)
+                      else Super_Length (Source) <=
+                             Source.Max_Length - By'Length)),
+     Post           =>
+       Super_Replace_Slice'Result.Max_Length = Source.Max_Length,
+     Contract_Cases =>
+       (Low - 1 <= Source.Max_Length - By'Length - Integer'Max
+          (Super_Length (Source) - Integer'Max (High, Low - 1), 0)
+        =>
+          --  Total length is lower than Max_Length: nothing is dropped
+
+          --  Note that if High < Low, the insertion is done before Low, so in
+          --  all cases the starting position of the slice of Source remaining
+          --  after the replaced Slice is Integer'Max (High + 1, Low).
+
+          Super_Length (Super_Replace_Slice'Result) =
+            Low - 1 + By'Length + Integer'Max
+              (Super_Length (Source) - Integer'Max (High, Low - 1), 0)
+            and then
+              String'(Super_Slice (Super_Replace_Slice'Result, 1, Low - 1)) =
+                Super_Slice (Source, 1, Low - 1)
+            and then
+              Super_Slice (Super_Replace_Slice'Result,
+                Low, Low - 1 + By'Length) = By
+            and then
+              (if Integer'Max (High, Low - 1) < Super_Length (Source) then
+                 String'(Super_Slice (Super_Replace_Slice'Result,
+                   Low + By'Length,
+                   Super_Length (Super_Replace_Slice'Result))) =
+                     Super_Slice (Source,
+                       Integer'Max (High + 1, Low), Super_Length (Source))),
+
+        Low - 1 > Source.Max_Length - By'Length - Integer'Max
+          (Super_Length (Source) - Integer'Max (High, Low - 1), 0)
+          and then Drop = Left
+        =>
+          --  Final_Super_Slice is the length of the slice of Source remaining
+          --  after the replaced part.
+          (declare
+             Final_Super_Slice : constant Natural :=
+               Integer'Max
+                 (Super_Length (Source) - Integer'Max (High, Low - 1), 0);
+           begin
+             --  The result is of maximal length and ends by the last
+             --  Final_Super_Slice characters of Source.
+
+             Super_Length (Super_Replace_Slice'Result) = Source.Max_Length
+               and then
+                 (if Final_Super_Slice > 0 then
+                    String'(Super_Slice (Super_Replace_Slice'Result,
+                      Source.Max_Length - Final_Super_Slice + 1,
+                      Source.Max_Length)) =
+                        Super_Slice (Source,
+                          Integer'Max (High + 1, Low), Super_Length (Source)))
+
+               --  Depending on when we reach Max_Length, either the first
+               --  part of Source is fully dropped and By is partly dropped,
+               --  or By is fully added and the first part of Source is partly
+               --  dropped.
+
+               and then
+                (if Source.Max_Length - Final_Super_Slice - By'Length <= 0 then
+
+                   --  The first (possibly zero) characters of By are dropped
+
+                   (if Final_Super_Slice < Source.Max_Length then
+                      Super_Slice (Super_Replace_Slice'Result,
+                        1, Source.Max_Length - Final_Super_Slice) =
+                          By (By'Last - Source.Max_Length + Final_Super_Slice
+                                + 1
+                              .. By'Last))
+
+                 else  --  By is added to the result
+
+                   Super_Slice (Super_Replace_Slice'Result,
+                     Source.Max_Length - Final_Super_Slice - By'Length + 1,
+                     Source.Max_Length - Final_Super_Slice) =
+                       By
+
+                     --  The first characters of Source (1 .. Low - 1) are
+                     --  dropped.
+
+                     and then
+                       String'(Super_Slice (Super_Replace_Slice'Result, 1,
+                         Source.Max_Length - Final_Super_Slice - By'Length)) =
+                           Super_Slice (Source,
+                             Low - Source.Max_Length
+                               + Final_Super_Slice + By'Length,
+                             Low - 1))),
+
+        others  --  Drop = Right
+        =>
+          --  The result is of maximal length and starts by the first Low - 1
+          --  characters of Source.
+
+          Super_Length (Super_Replace_Slice'Result) = Source.Max_Length
+            and then
+              String'(Super_Slice (Super_Replace_Slice'Result, 1, Low - 1)) =
+                Super_Slice (Source, 1, Low - 1)
+
+            --  Depending on when we reach Max_Length, either the last part
+            --  of Source is fully dropped and By is partly dropped, or By
+            --  is fully added and the last part of Source is partly dropped.
+
+            and then
+              (if Low - 1 >= Source.Max_Length - By'Length then
+
+                 --  The last characters of By are dropped
+
+                 Super_Slice (Super_Replace_Slice'Result,
+                   Low, Source.Max_Length) =
+                     By (By'First .. Source.Max_Length - Low + By'First)
+
+               else  --  By is fully added
+
+                 Super_Slice (Super_Replace_Slice'Result,
+                   Low, Low + By'Length - 1) = By
+
+                   --  Then Source starting from Natural'Max (High + 1, Low)
+                   --  is added but the last characters are dropped.
+
+                   and then
+                     String'(Super_Slice (Super_Replace_Slice'Result,
+                       Low + By'Length, Source.Max_Length)) =
+                         Super_Slice (Source, Integer'Max (High + 1, Low),
+                           Integer'Max (High + 1, Low) +
+                             (Source.Max_Length - Low - By'Length)))),
+     Global         => null;
 
    procedure Super_Replace_Slice
      (Source  : in out Super_String;
       Low     : Positive;
       High    : Natural;
       By      : String;
-      Drop    : Truncation := Error);
+      Drop    : Truncation := Error)
+   with
+     Pre            =>
+       Low - 1 <= Super_Length (Source)
+         and then
+           (if Drop = Error
+              then (if High >= Low
+                      then Low - 1
+                        <= Source.Max_Length - By'Length
+                         - Natural'Max (Super_Length (Source) - High, 0)
+                      else Super_Length (Source) <=
+                             Source.Max_Length - By'Length)),
+     Contract_Cases =>
+       (Low - 1 <= Source.Max_Length - By'Length - Integer'Max
+          (Super_Length (Source) - Integer'Max (High, Low - 1), 0)
+        =>
+          --  Total length is lower than Max_Length: nothing is dropped
+
+          --  Note that if High < Low, the insertion is done before Low, so in
+          --  all cases the starting position of the slice of Source remaining
+          --  after the replaced Slice is Integer'Max (High + 1, Low).
+
+          Super_Length (Source) = Low - 1 + By'Length + Integer'Max
+            (Super_Length (Source'Old) - Integer'Max (High, Low - 1), 0)
+            and then
+              String'(Super_Slice (Source, 1, Low - 1)) =
+                Super_Slice (Source'Old, 1, Low - 1)
+            and then Super_Slice (Source, Low, Low - 1 + By'Length) = By
+            and then
+              (if Integer'Max (High, Low - 1) < Super_Length (Source'Old) then
+                 String'(Super_Slice (Source,
+                   Low + By'Length, Super_Length (Source))) =
+                     Super_Slice (Source'Old,
+                       Integer'Max (High + 1, Low),
+                       Super_Length (Source'Old))),
+
+        Low - 1 > Source.Max_Length - By'Length - Integer'Max
+          (Super_Length (Source) - Integer'Max (High, Low - 1), 0)
+          and then Drop = Left
+        =>
+          --  Final_Super_Slice is the length of the slice of Source remaining
+          --  after the replaced part.
+          (declare
+             Final_Super_Slice : constant Natural :=
+               Integer'Max (0,
+                 Super_Length (Source'Old) - Integer'Max (High, Low - 1));
+           begin
+             --  The result is of maximal length and ends by the last
+             --  Final_Super_Slice characters of Source.
+
+             Super_Length (Source) = Source.Max_Length
+               and then
+                 (if Final_Super_Slice > 0 then
+                    String'(Super_Slice (Source,
+                      Source.Max_Length - Final_Super_Slice + 1,
+                      Source.Max_Length)) =
+                        Super_Slice (Source'Old,
+                          Integer'Max (High + 1, Low),
+                          Super_Length (Source'Old)))
+
+               --  Depending on when we reach Max_Length, either the first
+               --  part of Source is fully dropped and By is partly dropped,
+               --  or By is fully added and the first part of Source is partly
+               --  dropped.
+
+               and then
+                 (if Source.Max_Length - Final_Super_Slice - By'Length <= 0
+                  then
+                    --  The first characters of By are dropped
+
+                    (if Final_Super_Slice < Source.Max_Length then
+                       Super_Slice (Source,
+                         1, Source.Max_Length - Final_Super_Slice) =
+                           By (By'Last - Source.Max_Length + Final_Super_Slice
+                                 + 1
+                               .. By'Last))
+
+                  else  --  By is added to the result
+
+                    Super_Slice (Source,
+                      Source.Max_Length - Final_Super_Slice - By'Length + 1,
+                      Source.Max_Length - Final_Super_Slice) = By
+
+                      --  The first characters of Source (1 .. Low - 1) are
+                      --  dropped.
+
+                      and then
+                        String'(Super_Slice (Source, 1,
+                          Source.Max_Length - Final_Super_Slice - By'Length)) =
+                            Super_Slice (Source'Old,
+                              Low - Source.Max_Length + Final_Super_Slice
+                                + By'Length,
+                              Low - 1))),
+
+        others  --  Drop = Right
+        =>
+          --  The result is of maximal length and starts by the first Low - 1
+          --  characters of Source.
+
+          Super_Length (Source) = Source.Max_Length
+            and then
+              String'(Super_Slice (Source, 1, Low - 1)) =
+                Super_Slice (Source'Old, 1, Low - 1)
+
+            --  Depending on when we reach Max_Length, either the last part
+            --  of Source is fully dropped and By is partly dropped, or By
+            --  is fully added and the last part of Source is partly dropped.
+
+            and then
+              (if Low - 1 >= Source.Max_Length - By'Length then
+
+                 --  The last characters of By are dropped
+
+                 Super_Slice (Source, Low, Source.Max_Length) =
+                   By (By'First .. Source.Max_Length - Low + By'First)
+
+               else  --  By is fully added
+
+                 Super_Slice (Source, Low, Low + By'Length - 1) = By
+
+                   --  Then Source starting from Natural'Max (High + 1, Low)
+                   --  is added but the last characters are dropped.
+
+                   and then
+                     String'(Super_Slice (Source,
+                       Low + By'Length, Source.Max_Length)) =
+                         Super_Slice (Source'Old, Integer'Max (High + 1, Low),
+                           Integer'Max (High + 1, Low) +
+                             (Source.Max_Length - Low - By'Length)))),
+     Global         => null;
 
    function Super_Insert
      (Source   : Super_String;
       Before   : Positive;
       New_Item : String;
-      Drop     : Truncation := Error) return Super_String;
+      Drop     : Truncation := Error) return Super_String
+   with
+     Pre            =>
+       Before - 1 <= Super_Length (Source)
+         and then
+           (if New_Item'Length > Source.Max_Length - Super_Length (Source)
+            then Drop /= Error),
+     Post           => Super_Insert'Result.Max_Length = Source.Max_Length,
+     Contract_Cases =>
+       (Super_Length (Source) <= Source.Max_Length - New_Item'Length
+        =>
+          --  Total length is lower than Max_Length: nothing is dropped
+
+          Super_Length (Super_Insert'Result) =
+            Super_Length (Source) + New_Item'Length
+            and then
+              String'(Super_Slice (Super_Insert'Result, 1, Before - 1)) =
+                Super_Slice (Source, 1, Before - 1)
+            and then
+              Super_Slice (Super_Insert'Result,
+                Before, Before - 1 + New_Item'Length) =
+                  New_Item
+            and then
+              (if Before <= Super_Length (Source) then
+                 String'(Super_Slice (Super_Insert'Result,
+                   Before + New_Item'Length,
+                   Super_Length (Super_Insert'Result))) =
+                     Super_Slice (Source, Before, Super_Length (Source))),
+
+        Super_Length (Source) > Source.Max_Length - New_Item'Length
+          and then Drop = Left
+        =>
+          --  The result is of maximal length and ends by the last characters
+          --  of Source.
+
+          Super_Length (Super_Insert'Result) = Source.Max_Length
+            and then
+              (if Before <= Super_Length (Source) then
+                 String'(Super_Slice (Super_Insert'Result,
+                   Source.Max_Length - Super_Length (Source) + Before,
+                   Source.Max_Length)) =
+                     Super_Slice (Source, Before, Super_Length (Source)))
+
+            --  Depending on when we reach Max_Length, either the first part
+            --  of Source is fully dropped and New_Item is partly dropped, or
+            --  New_Item is fully added and the first part of Source is partly
+            --  dropped.
+
+            and then
+              (if Source.Max_Length - Super_Length (Source) - 1 + Before
+                < New_Item'Length
+               then
+                 --  The first characters of New_Item are dropped
+
+                 (if Super_Length (Source) - Before + 1 < Source.Max_Length
+                  then
+                    Super_Slice (Super_Insert'Result, 1,
+                      Source.Max_Length - Super_Length (Source) - 1 + Before) =
+                        New_Item
+                          (New_Item'Last - Source.Max_Length
+                            + Super_Length (Source) - Before + 2
+                           .. New_Item'Last))
+
+               else  --  New_Item is added to the result
+
+                 Super_Slice (Super_Insert'Result,
+                   Source.Max_Length - Super_Length (Source) - New_Item'Length
+                     + Before,
+                   Source.Max_Length - Super_Length (Source) - 1 + Before) =
+                     New_Item
+
+                   --  The first characters of Source (1 .. Before - 1) are
+                   --  dropped.
+
+                   and then
+                     String'(Super_Slice (Super_Insert'Result,
+                       1, Source.Max_Length - Super_Length (Source)
+                         - New_Item'Length - 1 + Before)) =
+                           Super_Slice (Source,
+                             Super_Length (Source) - Source.Max_Length
+                               + New_Item'Length + 1,
+                             Before - 1)),
+
+        others  --  Drop = Right
+        =>
+          --  The result is of maximal length and starts by the first
+          --  characters of Source.
+
+          Super_Length (Super_Insert'Result) = Source.Max_Length
+            and then
+              String'(Super_Slice (Super_Insert'Result, 1, Before - 1)) =
+                Super_Slice (Source, 1, Before - 1)
+
+            --  Depending on when we reach Max_Length, either the last part
+            --  of Source is fully dropped and New_Item is partly dropped, or
+            --  New_Item is fully added and the last part of Source is partly
+            --  dropped.
+
+            and then
+              (if Before - 1 >= Source.Max_Length - New_Item'Length then
+
+                 --  The last characters of New_Item are dropped
+
+                 Super_Slice (Super_Insert'Result, Before, Source.Max_Length) =
+                   New_Item (New_Item'First
+                     .. Source.Max_Length - Before + New_Item'First)
+
+               else  --  New_Item is fully added
+
+                 Super_Slice (Super_Insert'Result,
+                   Before, Before + New_Item'Length - 1) =
+                     New_Item
+
+                   --  Then Source starting from Before is added but the
+                   --  last characters are dropped.
+
+                   and then
+                     String'(Super_Slice (Super_Insert'Result,
+                       Before + New_Item'Length, Source.Max_Length)) =
+                         Super_Slice (Source,
+                           Before, Source.Max_Length - New_Item'Length))),
+     Global         => null;
 
    procedure Super_Insert
      (Source   : in out Super_String;
       Before   : Positive;
       New_Item : String;
-      Drop     : Truncation := Error);
+      Drop     : Truncation := Error)
+   with
+     Pre            =>
+       Before - 1 <= Super_Length (Source)
+         and then
+           (if New_Item'Length > Source.Max_Length - Super_Length (Source)
+            then Drop /= Error),
+     Contract_Cases =>
+       (Super_Length (Source) <= Source.Max_Length - New_Item'Length
+        =>
+          --  Total length is lower than Max_Length: nothing is dropped
+
+          Super_Length (Source) = Super_Length (Source'Old) + New_Item'Length
+            and then
+              String'(Super_Slice (Source, 1, Before - 1)) =
+                Super_Slice (Source'Old, 1, Before - 1)
+            and then
+              Super_Slice (Source, Before, Before - 1 + New_Item'Length) =
+                New_Item
+            and then
+              (if Before <= Super_Length (Source'Old) then
+                 String'(Super_Slice (Source,
+                   Before + New_Item'Length, Super_Length (Source))) =
+                     Super_Slice (Source'Old,
+                       Before, Super_Length (Source'Old))),
+
+        Super_Length (Source) > Source.Max_Length - New_Item'Length
+          and then Drop = Left
+        =>
+          --  The result is of maximal length and ends by the last characters
+          --  of Source.
+
+          Super_Length (Source) = Source.Max_Length
+            and then
+              (if Before <= Super_Length (Source'Old) then
+                 String'(Super_Slice (Source,
+                   Source.Max_Length - Super_Length (Source'Old) + Before,
+                   Source.Max_Length)) =
+                     Super_Slice (Source'Old,
+                       Before, Super_Length (Source'Old)))
+
+            --  Depending on when we reach Max_Length, either the first part
+            --  of Source is fully dropped and New_Item is partly dropped, or
+            --  New_Item is fully added and the first part of Source is partly
+            --  dropped.
+
+            and then
+              (if Source.Max_Length - Super_Length (Source'Old) - 1 + Before
+                < New_Item'Length
+               then
+                 --  The first characters of New_Item are dropped
+
+                 (if Super_Length (Source'Old) - Before + 1 < Source.Max_Length
+                  then
+                    Super_Slice (Source,
+                      1, Source.Max_Length - Super_Length (Source'Old)
+                        - 1 + Before) =
+                          New_Item
+                            (New_Item'Last - Source.Max_Length
+                               + Super_Length (Source'Old) - Before + 2
+                             .. New_Item'Last))
+
+               else  --  New_Item is added to the result
+
+                 Super_Slice (Source,
+                   Source.Max_Length - Super_Length (Source'Old)
+                     - New_Item'Length + Before,
+                   Source.Max_Length - Super_Length (Source'Old) - 1 + Before)
+                     = New_Item
+
+                   --  The first characters of Source (1 .. Before - 1) are
+                   --  dropped.
+
+                   and then
+                     String'(Super_Slice (Source, 1,
+                       Source.Max_Length - Super_Length (Source'Old)
+                         - New_Item'Length - 1 + Before)) =
+                           Super_Slice (Source'Old,
+                             Super_Length (Source'Old)
+                               - Source.Max_Length + New_Item'Length + 1,
+                             Before - 1)),
+
+        others  --  Drop = Right
+        =>
+          --  The result is of maximal length and starts by the first
+          --  characters of Source.
+
+          Super_Length (Source) = Source.Max_Length
+            and then
+              String'(Super_Slice (Source, 1, Before - 1)) =
+                Super_Slice (Source'Old, 1, Before - 1)
+
+            --  Depending on when we reach Max_Length, either the last part
+            --  of Source is fully dropped and New_Item is partly dropped, or
+            --  New_Item is fully added and the last part of Source is partly
+            --  dropped.
+
+            and then
+              (if Before - 1 >= Source.Max_Length - New_Item'Length then
+
+                 --  The last characters of New_Item are dropped
+
+                 Super_Slice (Source, Before, Source.Max_Length) =
+                   New_Item (New_Item'First
+                     .. Source.Max_Length - Before + New_Item'First)
+
+               else  --  New_Item is fully added
+
+                 Super_Slice (Source, Before, Before + New_Item'Length - 1) =
+                   New_Item
+
+                   --  Then Source starting from Before is added but the
+                   --  last characters are dropped.
+
+                   and then
+                     String'(Super_Slice (Source,
+                       Before + New_Item'Length, Source.Max_Length)) =
+                         Super_Slice (Source'Old,
+                           Before, Source.Max_Length - New_Item'Length))),
+     Global         => null;
 
    function Super_Overwrite
      (Source   : Super_String;
       Position : Positive;
       New_Item : String;
-      Drop     : Truncation := Error) return Super_String;
+      Drop     : Truncation := Error) return Super_String
+   with
+     Pre            =>
+       Position - 1 <= Super_Length (Source)
+         and then (if New_Item'Length > Source.Max_Length - (Position - 1)
+                   then Drop /= Error),
+     Post           => Super_Overwrite'Result.Max_Length = Source.Max_Length,
+     Contract_Cases =>
+       (Position - 1 <= Source.Max_Length - New_Item'Length
+        =>
+          --  The length is unchanged, unless New_Item overwrites further than
+          --  the end of Source. In this contract case, we suppose New_Item
+          --  doesn't overwrite further than Max_Length.
+
+          Super_Length (Super_Overwrite'Result) =
+            Integer'Max (Super_Length (Source), Position - 1 + New_Item'Length)
+            and then
+              String'(Super_Slice (Super_Overwrite'Result, 1, Position - 1)) =
+                Super_Slice (Source, 1, Position - 1)
+            and then Super_Slice (Super_Overwrite'Result,
+              Position, Position - 1 + New_Item'Length) =
+                New_Item
+            and then
+              (if Position - 1 + New_Item'Length < Super_Length (Source) then
+
+                 --  There are some unchanged characters of Source remaining
+                 --  after New_Item.
+
+                 String'(Super_Slice (Super_Overwrite'Result,
+                   Position + New_Item'Length, Super_Length (Source))) =
+                     Super_Slice (Source,
+                       Position + New_Item'Length, Super_Length (Source))),
+
+        Position - 1 > Source.Max_Length - New_Item'Length and then Drop = Left
+        =>
+          Super_Length (Super_Overwrite'Result) = Source.Max_Length
+
+            --  If a part of the result has to be dropped, it means New_Item is
+            --  overwriting further than the end of Source. Thus the result is
+            --  necessarily ending by New_Item. However, we don't know whether
+            --  New_Item covers all Max_Length characters or some characters of
+            --  Source are remaining at the left.
+
+            and then
+              (if New_Item'Length > Source.Max_Length then
+
+                 --  New_Item covers all Max_Length characters
+
+                 Super_To_String (Super_Overwrite'Result) =
+                   New_Item
+                     (New_Item'Last - Source.Max_Length + 1 .. New_Item'Last)
+               else
+                 --  New_Item fully appears at the end
+
+                 Super_Slice (Super_Overwrite'Result,
+                   Source.Max_Length - New_Item'Length + 1,
+                   Source.Max_Length) =
+                     New_Item
+
+                   --  The left of Source is cut
+
+                   and then
+                     String'(Super_Slice (Super_Overwrite'Result,
+                       1, Source.Max_Length - New_Item'Length)) =
+                         Super_Slice (Source,
+                           Position - Source.Max_Length + New_Item'Length,
+                           Position - 1)),
+
+        others  --  Drop = Right
+        =>
+          --  The result is of maximal length and starts by the first
+          --  characters of Source.
+
+          Super_Length (Super_Overwrite'Result) = Source.Max_Length
+            and then
+              String'(Super_Slice (Super_Overwrite'Result, 1, Position - 1)) =
+                Super_Slice (Source, 1, Position - 1)
+
+            --  Then New_Item is written until Max_Length
+
+            and then Super_Slice (Super_Overwrite'Result,
+              Position, Source.Max_Length) =
+                New_Item (New_Item'First
+                          .. Source.Max_Length - Position + New_Item'First)),
+     Global         => null;
 
    procedure Super_Overwrite
      (Source    : in out Super_String;
       Position  : Positive;
       New_Item  : String;
-      Drop      : Truncation := Error);
+      Drop      : Truncation := Error)
+   with
+     Pre            =>
+       Position - 1 <= Super_Length (Source)
+         and then (if New_Item'Length > Source.Max_Length - (Position - 1)
+                   then Drop /= Error),
+     Contract_Cases =>
+       (Position - 1 <= Source.Max_Length - New_Item'Length
+        =>
+          --  The length is unchanged, unless New_Item overwrites further than
+          --  the end of Source. In this contract case, we suppose New_Item
+          --  doesn't overwrite further than Max_Length.
+
+          Super_Length (Source) = Integer'Max
+            (Super_Length (Source'Old), Position - 1 + New_Item'Length)
+            and then
+              String'(Super_Slice (Source, 1, Position - 1)) =
+                Super_Slice (Source'Old, 1, Position - 1)
+            and then Super_Slice (Source,
+              Position, Position - 1 + New_Item'Length) =
+                New_Item
+            and then
+              (if Position - 1 + New_Item'Length < Super_Length (Source'Old)
+               then
+                 --  There are some unchanged characters of Source remaining
+                 --  after New_Item.
+
+                 String'(Super_Slice (Source,
+                   Position + New_Item'Length, Super_Length (Source'Old))) =
+                     Super_Slice (Source'Old,
+                       Position + New_Item'Length, Super_Length (Source'Old))),
+
+        Position - 1 > Source.Max_Length - New_Item'Length and then Drop = Left
+        =>
+          Super_Length (Source) = Source.Max_Length
+
+            --  If a part of the result has to be dropped, it means New_Item is
+            --  overwriting further than the end of Source. Thus the result is
+            --  necessarily ending by New_Item. However, we don't know whether
+            --  New_Item covers all Max_Length characters or some characters of
+            --  Source are remaining at the left.
+
+            and then
+              (if New_Item'Length > Source.Max_Length then
+
+                 --  New_Item covers all Max_Length characters
+
+                 Super_To_String (Source) =
+                   New_Item
+                     (New_Item'Last - Source.Max_Length + 1 .. New_Item'Last)
+               else
+                 --  New_Item fully appears at the end
+
+                 Super_Slice (Source,
+                   Source.Max_Length - New_Item'Length + 1,
+                   Source.Max_Length) =
+                     New_Item
+
+                   --  The left of Source is cut
+
+                   and then
+                     String'(Super_Slice (Source,
+                       1, Source.Max_Length - New_Item'Length)) =
+                         Super_Slice (Source'Old,
+                           Position - Source.Max_Length + New_Item'Length,
+                           Position - 1)),
+
+        others  --  Drop = Right
+        =>
+          --  The result is of maximal length and starts by the first
+          --  characters of Source.
+
+          Super_Length (Source) = Source.Max_Length
+            and then
+              String'(Super_Slice (Source, 1, Position - 1)) =
+                Super_Slice (Source'Old, 1, Position - 1)
+
+            --  New_Item is written until Max_Length
+
+            and then Super_Slice (Source, Position, Source.Max_Length) =
+              New_Item (New_Item'First
+                        .. Source.Max_Length - Position + New_Item'First)),
+     Global         => null;
 
    function Super_Delete
      (Source  : Super_String;
       From    : Positive;
-      Through : Natural) return Super_String;
+      Through : Natural) return Super_String
+   with
+     Pre            =>
+       (if Through >= From then From - 1 <= Super_Length (Source)),
+     Post           => Super_Delete'Result.Max_Length = Source.Max_Length,
+     Contract_Cases =>
+       (Through >= From =>
+          Super_Length (Super_Delete'Result) =
+            From - 1 + Natural'Max (Super_Length (Source) - Through, 0)
+            and then
+              String'(Super_Slice (Super_Delete'Result, 1, From - 1)) =
+                Super_Slice (Source, 1, From - 1)
+            and then
+              (if Through < Super_Length (Source) then
+                 String'(Super_Slice (Super_Delete'Result,
+                   From, Super_Length (Super_Delete'Result))) =
+                     Super_Slice (Source, Through + 1, Super_Length (Source))),
+        others          =>
+          Super_Delete'Result = Source),
+     Global         => null;
 
    procedure Super_Delete
      (Source  : in out Super_String;
       From    : Positive;
-      Through : Natural);
+      Through : Natural)
+   with
+     Pre            =>
+       (if Through >= From then From - 1 <= Super_Length (Source)),
+     Contract_Cases =>
+       (Through >= From =>
+          Super_Length (Source) =
+            From - 1 + Natural'Max (Super_Length (Source'Old) - Through, 0)
+            and then
+              String'(Super_Slice (Source, 1, From - 1)) =
+                Super_Slice (Source'Old, 1, From - 1)
+            and then
+              (if Through < Super_Length (Source) then
+                 String'(Super_Slice (Source, From, Super_Length (Source))) =
+                   Super_Slice (Source'Old,
+                     Through + 1, Super_Length (Source'Old))),
+        others          =>
+          Source = Source'Old),
+     Global         => null;
 
    ---------------------------------
    -- String Selector Subprograms --
@@ -388,45 +2180,376 @@ package Ada.Strings.Superbounded is
 
    function Super_Trim
      (Source : Super_String;
-      Side   : Trim_End) return Super_String;
+      Side   : Trim_End) return Super_String
+   with
+     Post           => Super_Trim'Result.Max_Length = Source.Max_Length,
+     Contract_Cases =>
+
+       --  If all characters in Source are Space, the returned string is empty
+
+       ((for all C of Super_To_String (Source) => C = ' ')
+        =>
+          Super_Length (Super_Trim'Result) = 0,
+
+        --  Otherwise, the returned string is a slice of Source
+
+        others
+        =>
+          (declare
+             Low  : constant Positive :=
+               (if Side = Right then 1
+                else Super_Index_Non_Blank (Source, Forward));
+             High : constant Positive :=
+               (if Side = Left then Super_Length (Source)
+                else Super_Index_Non_Blank (Source, Backward));
+           begin
+             Super_To_String (Super_Trim'Result) =
+               Super_Slice (Source, Low, High))),
+     Global         => null;
 
    procedure Super_Trim
      (Source : in out Super_String;
-      Side   : Trim_End);
+      Side   : Trim_End)
+   with
+     Contract_Cases =>
+
+       --  If all characters in Source are Space, the returned string is empty
+
+       ((for all C of Super_To_String (Source) => C = ' ')
+        =>
+          Super_Length (Source) = 0,
+
+        --  Otherwise, the returned string is a slice of Source
+
+        others
+        =>
+          (declare
+             Low  : constant Positive :=
+               (if Side = Right then 1
+                else Super_Index_Non_Blank (Source'Old, Forward));
+             High : constant Positive :=
+               (if Side = Left then Super_Length (Source'Old)
+                else Super_Index_Non_Blank (Source'Old, Backward));
+           begin
+             Super_To_String (Source) = Super_Slice (Source'Old, Low, High))),
+     Global => null;
 
    function Super_Trim
      (Source : Super_String;
       Left   : Maps.Character_Set;
-      Right  : Maps.Character_Set) return Super_String;
+      Right  : Maps.Character_Set) return Super_String
+   with
+     Post           => Super_Trim'Result.Max_Length = Source.Max_Length,
+     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 Super_To_String (Source) => Maps.Is_In (C, Left))
+          or else
+            (for all C of Super_To_String (Source) => Maps.Is_In (C, Right))
+        =>
+          Super_Length (Super_Trim'Result) = 0,
+
+        --  Otherwise, the returned string is a slice of Source
+
+        others
+        =>
+          (declare
+             Low  : constant Positive :=
+               Super_Index (Source, Left, Outside, Forward);
+             High : constant Positive :=
+               Super_Index (Source, Right, Outside, Backward);
+           begin
+             Super_To_String (Super_Trim'Result) =
+               Super_Slice (Source, Low, High))),
+     Global         => null;
 
    procedure Super_Trim
      (Source : in out Super_String;
       Left   : Maps.Character_Set;
-      Right  : Maps.Character_Set);
+      Right  : Maps.Character_Set)
+   with
+     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 Super_To_String (Source) => Maps.Is_In (C, Left))
+          or else
+            (for all C of Super_To_String (Source) => Maps.Is_In (C, Right))
+        =>
+          Super_Length (Source) = 0,
+
+        --  Otherwise, the returned string is a slice of Source
+
+        others
+        =>
+          (declare
+             Low  : constant Positive :=
+               Super_Index (Source'Old, Left, Outside, Forward);
+             High : constant Positive :=
+               Super_Index (Source'Old, Right, Outside, Backward);
+           begin
+             Super_To_String (Source) = Super_Slice (Source'Old, Low, High))),
+     Global => null;
 
    function Super_Head
      (Source : Super_String;
       Count  : Natural;
       Pad    : Character := Space;
-      Drop   : Truncation := Error) return Super_String;
+      Drop   : Truncation := Error) return Super_String
+   with
+     Pre            => (if Count > Source.Max_Length then Drop /= Error),
+     Post           => Super_Head'Result.Max_Length = Source.Max_Length,
+     Contract_Cases =>
+       (Count <= Super_Length (Source)
+        =>
+          --  Source is cut
+
+          Super_To_String (Super_Head'Result) = Super_Slice (Source, 1, Count),
+        Count > Super_Length (Source) and then Count <= Source.Max_Length
+        =>
+          --  Source is followed by Pad characters
+
+          Super_Length (Super_Head'Result) = Count
+            and then
+              Super_Slice (Super_Head'Result, 1, Super_Length (Source)) =
+                Super_To_String (Source)
+            and then
+              String'(Super_Slice (Super_Head'Result,
+                Super_Length (Source) + 1, Count)) =
+                  (1 .. Count - Super_Length (Source) => Pad),
+        Count > Source.Max_Length and then Drop = Right
+        =>
+          --  Source is followed by Pad characters
+
+          Super_Length (Super_Head'Result) = Source.Max_Length
+            and then
+              Super_Slice (Super_Head'Result, 1, Super_Length (Source)) =
+                Super_To_String (Source)
+            and then
+              String'(Super_Slice (Super_Head'Result,
+                Super_Length (Source) + 1, Source.Max_Length)) =
+                  (1 .. Source.Max_Length - Super_Length (Source) => Pad),
+        Count - Super_Length (Source) > Source.Max_Length and then Drop = Left
+        =>
+          --  Source is fully dropped on the left
+
+          Super_To_String (Super_Head'Result) =
+            (1 .. Source.Max_Length => Pad),
+        others
+        =>
+          --  Source is partly dropped on the left
+
+          Super_Length (Super_Head'Result) = Source.Max_Length
+            and then
+              String'(Super_Slice (Super_Head'Result,
+                1, Source.Max_Length - Count + Super_Length (Source))) =
+                  Super_Slice (Source,
+                    Count - Source.Max_Length + 1, Super_Length (Source))
+            and then
+              String'(Super_Slice (Super_Head'Result,
+                Source.Max_Length - Count + Super_Length (Source) + 1,
+                Source.Max_Length)) =
+                  (1 .. Count - Super_Length (Source) => Pad)),
+     Global         => null;
 
    procedure Super_Head
      (Source : in out Super_String;
       Count  : Natural;
       Pad    : Character := Space;
-      Drop   : Truncation := Error);
+      Drop   : Truncation := Error)
+   with
+     Pre            => (if Count > Source.Max_Length then Drop /= Error),
+     Contract_Cases =>
+       (Count <= Super_Length (Source)
+        =>
+          --  Source is cut
+
+          Super_To_String (Source) = Super_Slice (Source'Old, 1, Count),
+        Count > Super_Length (Source) and then Count <= Source.Max_Length
+        =>
+          --  Source is followed by Pad characters
+
+          Super_Length (Source) = Count
+            and then
+              Super_Slice (Source, 1, Super_Length (Source'Old)) =
+                Super_To_String (Source'Old)
+            and then
+              String'(Super_Slice (Source,
+                Super_Length (Source'Old) + 1, Count)) =
+                  (1 .. Count - Super_Length (Source'Old) => Pad),
+        Count > Source.Max_Length and then Drop = Right
+        =>
+          --  Source is followed by Pad characters
+
+          Super_Length (Source) = Source.Max_Length
+            and then
+              Super_Slice (Source, 1, Super_Length (Source'Old)) =
+                Super_To_String (Source'Old)
+            and then
+              String'(Super_Slice (Source,
+                Super_Length (Source'Old) + 1, Source.Max_Length)) =
+                  (1 .. Source.Max_Length - Super_Length (Source'Old) => Pad),
+        Count - Super_Length (Source) > Source.Max_Length and then Drop = Left
+        =>
+          --  Source is fully dropped on the left
+
+          Super_To_String (Source) = (1 .. Source.Max_Length => Pad),
+        others
+        =>
+          --  Source is partly dropped on the left
+
+          Super_Length (Source) = Source.Max_Length
+            and then
+              String'(Super_Slice (Source,
+                1, Source.Max_Length - Count + Super_Length (Source'Old))) =
+                  Super_Slice (Source'Old,
+                    Count - Source.Max_Length + 1, Super_Length (Source'Old))
+            and then
+              String'(Super_Slice (Source,
+                Source.Max_Length - Count + Super_Length (Source'Old) + 1,
+                Source.Max_Length)) =
+                  (1 .. Count - Super_Length (Source'Old) => Pad)),
+     Global         => null;
 
    function Super_Tail
      (Source : Super_String;
       Count  : Natural;
       Pad    : Character := Space;
-      Drop   : Truncation := Error) return Super_String;
+      Drop   : Truncation := Error) return Super_String
+   with
+     Pre            => (if Count > Source.Max_Length then Drop /= Error),
+     Post           => Super_Tail'Result.Max_Length = Source.Max_Length,
+     Contract_Cases =>
+       (Count < Super_Length (Source)
+        =>
+          --  Source is cut
+
+          (if Count > 0 then
+             Super_To_String (Super_Tail'Result) =
+               Super_Slice (Source,
+                 Super_Length (Source) - Count + 1, Super_Length (Source))
+           else Super_Length (Super_Tail'Result) = 0),
+        Count >= Super_Length (Source) and then Count < Source.Max_Length
+        =>
+          --  Source is preceded by Pad characters
+
+          Super_Length (Super_Tail'Result) = Count
+            and then
+              String'(Super_Slice (Super_Tail'Result,
+                1, Count - Super_Length (Source))) =
+                  (1 .. Count - Super_Length (Source) => Pad)
+            and then
+              Super_Slice (Super_Tail'Result,
+                Count - Super_Length (Source) + 1, Count) =
+                  Super_To_String (Source),
+        Count >= Source.Max_Length and then Drop = Left
+        =>
+          --  Source is preceded by Pad characters
+
+          Super_Length (Super_Tail'Result) = Source.Max_Length
+            and then
+              String'(Super_Slice (Super_Tail'Result,
+                1, Source.Max_Length - Super_Length (Source))) =
+                  (1 .. Source.Max_Length - Super_Length (Source) => Pad)
+            and then
+              (if Super_Length (Source) > 0 then
+                 Super_Slice (Super_Tail'Result,
+                   Source.Max_Length - Super_Length (Source) + 1,
+                   Source.Max_Length) =
+                     Super_To_String (Source)),
+        Count - Super_Length (Source) >= Source.Max_Length
+          and then Drop /= Left
+        =>
+          --  Source is fully dropped on the right
+
+          Super_To_String (Super_Tail'Result) =
+            (1 .. Source.Max_Length => Pad),
+        others
+        =>
+          --  Source is partly dropped on the right
+
+          Super_Length (Super_Tail'Result) = Source.Max_Length
+            and then
+              String'(Super_Slice (Super_Tail'Result,
+                1, Count - Super_Length (Source))) =
+                  (1 .. Count - Super_Length (Source) => Pad)
+            and then
+              String'(Super_Slice (Super_Tail'Result,
+                Count - Super_Length (Source) + 1, Source.Max_Length)) =
+                  Super_Slice (Source,
+                    1, Source.Max_Length - Count + Super_Length (Source))),
+     Global         => null;
 
    procedure Super_Tail
      (Source : in out Super_String;
       Count  : Natural;
       Pad    : Character := Space;
-      Drop   : Truncation := Error);
+      Drop   : Truncation := Error)
+   with
+     Pre            => (if Count > Source.Max_Length then Drop /= Error),
+     Contract_Cases =>
+       (Count < Super_Length (Source)
+        =>
+          --  Source is cut
+
+          (if Count > 0 then
+             Super_To_String (Source) =
+               Super_Slice (Source'Old,
+                 Super_Length (Source'Old) - Count + 1,
+                 Super_Length (Source'Old))
+           else Super_Length (Source) = 0),
+        Count >= Super_Length (Source) and then Count < Source.Max_Length
+        =>
+          --  Source is preceded by Pad characters
+
+          Super_Length (Source) = Count
+            and then
+              String'(Super_Slice (Source,
+                1, Count - Super_Length (Source'Old))) =
+                  (1 .. Count - Super_Length (Source'Old) => Pad)
+            and then
+              Super_Slice (Source,
+                Count - Super_Length (Source'Old) + 1, Count) =
+                  Super_To_String (Source'Old),
+        Count >= Source.Max_Length and then Drop = Left
+        =>
+          --  Source is preceded by Pad characters
+
+          Super_Length (Source) = Source.Max_Length
+            and then
+              String'(Super_Slice (Source,
+                1, Source.Max_Length - Super_Length (Source'Old))) =
+                  (1 .. Source.Max_Length - Super_Length (Source'Old) => Pad)
+            and then
+              (if Super_Length (Source'Old) > 0 then
+                 Super_Slice (Source,
+                   Source.Max_Length - Super_Length (Source'Old) + 1,
+                   Source.Max_Length) =
+                     Super_To_String (Source'Old)),
+        Count - Super_Length (Source) >= Source.Max_Length
+          and then Drop /= Left
+        =>
+          --  Source is fully dropped on the right
+
+          Super_To_String (Source) = (1 .. Source.Max_Length => Pad),
+        others
+        =>
+          --  Source is partly dropped on the right
+
+          Super_Length (Source) = Source.Max_Length
+            and then
+              String'(Super_Slice (Source,
+                1, Count - Super_Length (Source'Old))) =
+                  (1 .. Count - Super_Length (Source'Old) => Pad)
+            and then
+              String'(Super_Slice (Source,
+                Count - Super_Length (Source'Old) + 1, Source.Max_Length)) =
+                  Super_Slice (Source'Old,
+                    1, Source.Max_Length - Count + Super_Length (Source'Old))),
+     Global         => null;
 
    ------------------------------------
    -- String Constructor Subprograms --
@@ -439,37 +2562,135 @@ package Ada.Strings.Superbounded is
    function Times
      (Left       : Natural;
       Right      : Character;
-      Max_Length : Positive) return Super_String;
+      Max_Length : Positive) return Super_String
+   with
+     Pre    => Left <= Max_Length,
+     Post   => Times'Result.Max_Length = Max_Length
+       and then Super_To_String (Times'Result) = (1 .. Left => Right),
+     Global => null;
    --  Note the additional parameter Max_Length
 
    function Times
      (Left       : Natural;
       Right      : String;
-      Max_Length : Positive) return Super_String;
+      Max_Length : Positive) return Super_String
+   with
+     Pre    => (if Left /= 0 then Right'Length <= Max_Length / Left),
+     Post   => Times'Result.Max_Length = Max_Length
+       and then Super_Length (Times'Result) = Left * Right'Length
+       and then
+         (if Right'Length > 0 then
+            (for all K in 1 .. Left * Right'Length =>
+               Super_Element (Times'Result, K) =
+                 Right (Right'First + (K - 1) mod Right'Length))),
+     Global => null;
    --  Note the additional parameter Max_Length
 
    function Times
      (Left  : Natural;
-      Right : Super_String) return Super_String;
+      Right : Super_String) return Super_String
+   with
+     Pre    =>
+       (if Left /= 0 then Super_Length (Right) <= Right.Max_Length / Left),
+     Post   => Times'Result.Max_Length = Right.Max_Length
+       and then Super_Length (Times'Result) = Left * Super_Length (Right)
+       and then
+         (if Super_Length (Right) > 0 then
+            (for all K in 1 .. Left * Super_Length (Right) =>
+               Super_Element (Times'Result, K) =
+                 Super_Element (Right, 1 + (K - 1) mod Super_Length (Right)))),
+     Global => null;
 
    function Super_Replicate
      (Count      : Natural;
       Item       : Character;
       Drop       : Truncation := Error;
-      Max_Length : Positive) return Super_String;
+      Max_Length : Positive) return Super_String
+   with
+     Pre    => (if Count > Max_Length then Drop /= Error),
+     Post   => Super_Replicate'Result.Max_Length = Max_Length
+       and then Super_To_String (Super_Replicate'Result) =
+         (1 .. Natural'Min (Max_Length, Count) => Item),
+     Global => null;
    --  Note the additional parameter Max_Length
 
    function Super_Replicate
      (Count      : Natural;
       Item       : String;
       Drop       : Truncation := Error;
-      Max_Length : Positive) return Super_String;
+      Max_Length : Positive) return Super_String
+   with
+     Pre            =>
+       (if Count /= 0 and then Item'Length > Max_Length / Count
+        then Drop /= Error),
+     Post           => Super_Replicate'Result.Max_Length = Max_Length,
+     Contract_Cases =>
+       (Count = 0 or else Item'Length <= Max_Length / Count
+        =>
+          Super_Length (Super_Replicate'Result) = Count * Item'Length
+            and then
+              (if Item'Length > 0 then
+                 (for all K in 1 .. Count * Item'Length =>
+                    Super_Element (Super_Replicate'Result, K) =
+                      Item (Item'First + (K - 1) mod Item'Length))),
+        Count /= 0
+          and then Item'Length > Max_Length / Count
+          and then Drop = Right
+        =>
+          Super_Length (Super_Replicate'Result) = Max_Length
+            and then
+              (for all K in 1 .. Max_Length =>
+                 Super_Element (Super_Replicate'Result, K) =
+                   Item (Item'First + (K - 1) mod Item'Length)),
+        others  --  Drop = Left
+        =>
+          Super_Length (Super_Replicate'Result) = Max_Length
+            and then
+              (for all K in 1 .. Max_Length =>
+                 Super_Element (Super_Replicate'Result, K) =
+                   Item (Item'Last - (Max_Length - K) mod Item'Length))),
+     Global         => null;
    --  Note the additional parameter Max_Length
 
    function Super_Replicate
      (Count : Natural;
       Item  : Super_String;
-      Drop  : Truncation := Error) return Super_String;
+      Drop  : Truncation := Error) return Super_String
+   with
+     Pre            =>
+       (if Count /= 0
+          and then Super_Length (Item) > Item.Max_Length / Count
+        then Drop /= Error),
+     Post           => Super_Replicate'Result.Max_Length = Item.Max_Length,
+     Contract_Cases =>
+       ((if Count /= 0 then Super_Length (Item) <= Item.Max_Length / Count)
+        =>
+          Super_Length (Super_Replicate'Result) = Count * Super_Length (Item)
+            and then
+              (if Super_Length (Item) > 0 then
+                 (for all K in 1 .. Count * Super_Length (Item) =>
+                    Super_Element (Super_Replicate'Result, K) =
+                      Super_Element (Item,
+                        1 + (K - 1) mod Super_Length (Item)))),
+        Count /= 0
+          and then Super_Length (Item) > Item.Max_Length / Count
+          and then Drop = Right
+        =>
+          Super_Length (Super_Replicate'Result) = Item.Max_Length
+            and then
+              (for all K in 1 .. Item.Max_Length =>
+                 Super_Element (Super_Replicate'Result, K) =
+                   Super_Element (Item, 1 + (K - 1) mod Super_Length (Item))),
+        others  --  Drop = Left
+        =>
+          Super_Length (Super_Replicate'Result) = Item.Max_Length
+            and then
+              (for all K in 1 .. Item.Max_Length =>
+                 Super_Element (Super_Replicate'Result, K) =
+                   Super_Element (Item,
+                     Super_Length (Item)
+                       - (Item.Max_Length - K) mod Super_Length (Item)))),
+     Global         => null;
 
 private
       --  Pragma Inline declarations