ada/libgnat/a-strunb__shared.ads

83   Initial_Condition => Length (Null_Unbounded_String) = 0
92    function Length (Source : Unbounded_String) return Natural with  subprogspec
106      Post   => Length (To_Unbounded_String'Result) = Source'Length,
110      (Length : Natural) return Unbounded_String
113        Ada.Strings.Unbounded.Length (To_Unbounded_String'Result) = Length,
117      Post   => To_String'Result'Length = Length (Source),
131      Pre    => Length (New_Item) <= Natural'Last - Length (Source),
132      Post   => Length (Source) = Length (Source)'Old + Length (New_Item),
139      Pre    => New_Item'Length <= Natural'Last - Length (Source),
140      Post   => Length (Source) = Length (Source)'Old + New_Item'Length,
147      Pre    => Length (Source) < Natural'Last,
148      Post   => Length (Source) = Length (Source)'Old + 1,
155      Pre    => Length (Right) <= Natural'Last - Length (Left),
156      Post   => Length ("&"'Result) = Length (Left) + Length (Right),
163      Pre    => Right'Length <= Natural'Last - Length (Left),
164      Post   => Length ("&"'Result) = Length (Left) + Right'Length,
171      Pre    => Left'Length <= Natural'Last - Length (Right),
172      Post   => Length ("&"'Result) = Left'Length + Length (Right),
179      Pre    => Length (Left) < Natural'Last,
180      Post   => Length ("&"'Result) = Length (Left) + 1,
187      Pre    => Length (Right) < Natural'Last,
188      Post   => Length ("&"'Result) = Length (Right) + 1,
195      Pre    => Index <= Length (Source),
203      Pre    => Index <= Length (Source),
204      Post   => Length (Source) = Length (Source)'Old,
212      Pre    => Low - 1 <= Length (Source) and then High <= Length (Source),
213      Post   => Slice'Result'Length = Natural'Max (0, High - Low + 1),
221      Pre    => Low - 1 <= Length (Source) and then High <= Length (Source),
223        Length (Unbounded_Slice'Result) = Natural'Max (0, High - Low + 1),
233      Pre    => Low - 1 <= Length (Source) and then High <= Length (Source),
234      Post   => Length (Target) = Natural'Max (0, High - Low + 1),
338      Pre    => Pattern'Length /= 0,
347      Pre    => Pattern'Length /= 0,
365      Pre    => (if Length (Source) /= 0
366                 then From <= Length (Source))
367                        and then Pattern'Length /= 0,
378      Pre    => (if Length (Source) /= 0
379                 then From <= Length (Source))
380                        and then Pattern'Length /= 0,
392      Pre    => (if Length (Source) /= 0 then From <= Length (Source)),
407      Pre    => (if Length (Source) /= 0 then From <= Length (Source)),
416      Pre    => Pattern'Length /= 0,
424      Pre    => Pattern'Length /= 0,
441      Pre    => (if Length (Source) /= 0 then From <= Length (Source)),
462      Post   => Length (Translate'Result) = Length (Source),
469      Post   => Length (Source) = Length (Source)'Old,
476      Post   => Length (Translate'Result) = Length (Source),
483      Post   => Length (Source) = Length (Source)'Old,
497        Low - 1 <= Length (Source)
500                      <= Natural'Last - By'Length
501                       - Natural'Max (Length (Source) - High, 0)
502                    else Length (Source) <= Natural'Last - By'Length),
505           Length (Replace_Slice'Result)
506         = Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0),
508           Length (Replace_Slice'Result) = Length (Source)'Old + By'Length),
518        Low - 1 <= Length (Source)
521                      <= Natural'Last - By'Length
522                       - Natural'Max (Length (Source) - High, 0)
523                    else Length (Source) <= Natural'Last - By'Length),
526           Length (Source)
527         = Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0),
529           Length (Source) = Length (Source)'Old + By'Length),
537      Pre    => Before - 1 <= Length (Source)
538                  and then New_Item'Length <= Natural'Last - Length (Source),
539      Post   => Length (Insert'Result) = Length (Source) + New_Item'Length,
547      Pre    => Before - 1 <= Length (Source)
548                  and then New_Item'Length <= Natural'Last - Length (Source),
549      Post   => Length (Source) = Length (Source)'Old + New_Item'Length,
557      Pre    => Position - 1 <= Length (Source)
558                  and then (if New_Item'Length /= 0
560                              New_Item'Length <= Natural'Last - (Position - 1)),
562        Length (Overwrite'Result)
563      = Natural'Max (Length (Source), Position - 1 + New_Item'Length),
571      Pre    => Position - 1 <= Length (Source)
572                  and then (if New_Item'Length /= 0
574                              New_Item'Length <= Natural'Last - (Position - 1)),
576        Length (Source)
577      = Natural'Max (Length (Source)'Old, Position - 1 + New_Item'Length),
586      Pre            => (if Through <= From then From - 1 <= Length (Source)),
589           Length (Delete'Result) = Length (Source) - (Through - From + 1),
591           Length (Delete'Result) = Length (Source)),
599      Pre            => (if Through <= From then From - 1 <= Length (Source)),
602           Length (Source) = Length (Source)'Old - (Through - From + 1),
604           Length (Source) = Length (Source)'Old),
611      Post   => Length (Trim'Result) <= Length (Source),
618      Post   => Length (Source) <= Length (Source)'Old,
626      Post   => Length (Trim'Result) <= Length (Source),
634      Post   => Length (Source) <= Length (Source)'Old,
642      Post   => Length (Head'Result) = Count,
650      Post   => Length (Source) = Count,
658      Post   => Length (Tail'Result) = Count,
666      Post   => Length (Source) = Count,
674      Post   => Length ("*"'Result) = Left,
681      Pre    => (if Left /= 0 then Right'Length <= Natural'Last / Left),
682      Post   => Length ("*"'Result) = Left * Right'Length,
689      Pre    => (if Left /= 0 then Length (Right) <= Natural'Last / Left),
690      Post   => Length ("*"'Result) = Left * Length (Right),
694    pragma Inline (Length);
718       Length : Natural) return Boolean;