ada/libgnat/a-strunb.ads

57   Initial_Condition => Length (Null_Unbounded_String) = 0
62      Default_Initial_Condition => Length (Unbounded_String) = 0;
70    function Length (Source : Unbounded_String) return Natural with  subprogspec
88      Post   => Length (To_Unbounded_String'Result) = Source'Length,
93      (Length : Natural) return Unbounded_String
96        Ada.Strings.Unbounded.Length (To_Unbounded_String'Result) = Length,
102      Post   => To_String'Result'Length = Length (Source),
125      Pre    => Length (New_Item) <= Natural'Last - Length (Source),
126      Post   => Length (Source) = Length (Source)'Old + Length (New_Item),
133      Pre    => New_Item'Length <= Natural'Last - Length (Source),
134      Post   => Length (Source) = Length (Source)'Old + New_Item'Length,
141      Pre    => Length (Source) < Natural'Last,
142      Post   => Length (Source) = Length (Source)'Old + 1,
153      Pre    => Length (Right) <= Natural'Last - Length (Left),
154      Post   => Length ("&"'Result) = Length (Left) + Length (Right),
161      Pre    => Right'Length <= Natural'Last - Length (Left),
162      Post   => Length ("&"'Result) = Length (Left) + Right'Length,
169      Pre    => Left'Length <= Natural'Last - Length (Right),
170      Post   => Length ("&"'Result) = Left'Length + Length (Right),
177      Pre    => Length (Left) < Natural'Last,
178      Post   => Length ("&"'Result) = Length (Left) + 1,
185      Pre    => Length (Right) < Natural'Last,
186      Post   => Length ("&"'Result) = Length (Right) + 1,
199      Pre    => Index <= Length (Source),
209      Pre    => Index <= Length (Source),
210      Post   => Length (Source) = Length (Source)'Old,
221      Pre    => Low - 1 <= Length (Source) and then High <= Length (Source),
222      Post   => Slice'Result'Length = Natural'Max (0, High - Low + 1),
234      Pre    => Low - 1 <= Length (Source) and then High <= Length (Source),
236        Length (Unbounded_Slice'Result) = Natural'Max (0, High - Low + 1),
249      Pre    => Low - 1 <= Length (Source) and then High <= Length (Source),
250      Post   => Length (Target) = Natural'Max (0, High - Low + 1),
361      Pre    => Pattern'Length /= 0,
370      Pre    => Pattern'Length /= 0,
388      Pre    => (if Length (Source) /= 0 then From <= Length (Source))
389                and then Pattern'Length /= 0,
400      Pre    => (if Length (Source) /= 0 then From <= Length (Source))
401                and then Pattern'Length /= 0,
412      Pre    => (if Length (Source) /= 0 then From <= Length (Source)),
427      Pre    => (if Length (Source) /= 0 then From <= Length (Source)),
436      Pre    => Pattern'Length /= 0,
444      Pre    => Pattern'Length /= 0,
461      Pre    => (if Length (Source) /= 0 then From <= Length (Source)),
487      Post   => Length (Translate'Result) = Length (Source),
494      Post   => Length (Source) = Length (Source)'Old,
501      Post   => Length (Translate'Result) = Length (Source),
508      Post   => Length (Source) = Length (Source)'Old,
527        Low - 1 <= Length (Source)
530                      <= Natural'Last - By'Length
531                       - Natural'Max (Length (Source) - High, 0)
532                    else Length (Source) <= Natural'Last - By'Length),
535           Length (Replace_Slice'Result)
536         = Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0),
538           Length (Replace_Slice'Result) = Length (Source)'Old + By'Length),
548        Low - 1 <= Length (Source)
551                      <= Natural'Last - By'Length
552                       - Natural'Max (Length (Source) - High, 0)
553                    else Length (Source) <= Natural'Last - By'Length),
556           Length (Source)
557         = Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0),
559           Length (Source) = Length (Source)'Old + By'Length),
567      Pre    => Before - 1 <= Length (Source)
568                  and then New_Item'Length <= Natural'Last - Length (Source),
569      Post   => Length (Insert'Result) = Length (Source) + New_Item'Length,
577      Pre    => Before - 1 <= Length (Source)
578                  and then New_Item'Length <= Natural'Last - Length (Source),
579      Post   => Length (Source) = Length (Source)'Old + New_Item'Length,
587      Pre    => Position - 1 <= Length (Source)
588                  and then (if New_Item'Length /= 0
590                              New_Item'Length <= Natural'Last - (Position - 1)),
592        Length (Overwrite'Result)
593      = Natural'Max (Length (Source), Position - 1 + New_Item'Length),
601      Pre    => Position - 1 <= Length (Source)
602                  and then (if New_Item'Length /= 0
604                              New_Item'Length <= Natural'Last - (Position - 1)),
606        Length (Source)
607      = Natural'Max (Length (Source)'Old, Position - 1 + New_Item'Length),
616      Pre            => (if Through <= From then From - 1 <= Length (Source)),
619           Length (Delete'Result) = Length (Source) - (Through - From + 1),
621           Length (Delete'Result) = Length (Source)),
629      Pre            => (if Through <= From then From - 1 <= Length (Source)),
632           Length (Source) = Length (Source)'Old - (Through - From + 1),
634           Length (Source) = Length (Source)'Old),
641      Post   => Length (Trim'Result) <= Length (Source),
648      Post   => Length (Source) <= Length (Source)'Old,
656      Post   => Length (Trim'Result) <= Length (Source),
664      Post   => Length (Source) <= Length (Source)'Old,
672      Post   => Length (Head'Result) = Count,
680      Post   => Length (Source) = Count,
688      Post   => Length (Tail'Result) = Count,
696      Post   => Length (Source) = Count,
704      Post   => Length ("*"'Result) = Left,
711      Pre    => (if Left /= 0 then Right'Length <= Natural'Last / Left),
712      Post   => Length ("*"'Result) = Left * Right'Length,
719      Pre    => (if Left /= 0 then Length (Right) <= Natural'Last / Left),
720      Post   => Length ("*"'Result) = Left * Length (Right),
739    pragma Inline (Length);