ada/libgnat/a-strunb.ads

56   Initial_Condition => Length (Null_Unbounded_String) = 0
68    function Length (Source : Unbounded_String) return Natural with  subprogspec
86      Post   => Length (To_Unbounded_String'Result) = Source'Length,
91      (Length : Natural) return Unbounded_String
94        Ada.Strings.Unbounded.Length (To_Unbounded_String'Result)
95      = Length,
101      Post   => To_String'Result'Length = Length (Source),
124      Pre    => Length (New_Item) <= Natural'Last - Length (Source),
125      Post   => Length (Source) = Length (Source)'Old + Length (New_Item),
132      Pre    => New_Item'Length <= Natural'Last - Length (Source),
133      Post   => Length (Source) = Length (Source)'Old + New_Item'Length,
140      Pre    => Length (Source) < Natural'Last,
141      Post   => Length (Source) = Length (Source)'Old + 1,
152      Pre    => Length (Right) <= Natural'Last - Length (Left),
153      Post   => Length ("&"'Result) = Length (Left) + Length (Right),
160      Pre    => Right'Length <= Natural'Last - Length (Left),
161      Post   => Length ("&"'Result) = Length (Left) + Right'Length,
168      Pre    => Left'Length <= Natural'Last - Length (Right),
169      Post   => Length ("&"'Result) = Left'Length + Length (Right),
176      Pre    => Length (Left) < Natural'Last,
177      Post   => Length ("&"'Result) = Length (Left) + 1,
184      Pre    => Length (Right) < Natural'Last,
185      Post   => Length ("&"'Result) = Length (Right) + 1,
198      Pre    => Index <= Length (Source),
208      Pre    => Index <= Length (Source),
209      Post   => Length (Source) = Length (Source)'Old,
220      Pre    => Low - 1 <= Length (Source) and then High <= Length (Source),
221      Post   => Slice'Result'Length = Natural'Max (0, High - Low + 1),
233      Pre    => Low - 1 <= Length (Source) and then High <= Length (Source),
235        Length (Unbounded_Slice'Result) = Natural'Max (0, High - Low + 1),
248      Pre    => Low - 1 <= Length (Source) and then High <= Length (Source),
249      Post   => Length (Target) = Natural'Max (0, High - Low + 1),
360      Pre    => Pattern'Length /= 0,
369      Pre    => Pattern'Length /= 0,
387      Pre    => (if Length (Source) /= 0 then From <= Length (Source))
388                and then Pattern'Length /= 0,
399      Pre    => (if Length (Source) /= 0 then From <= Length (Source))
400                and then Pattern'Length /= 0,
411      Pre    => (if Length (Source) /= 0 then From <= Length (Source)),
426      Pre    => (if Length (Source) /= 0 then From <= Length (Source)),
435      Pre    => Pattern'Length /= 0,
443      Pre    => Pattern'Length /= 0,
460      Pre    => (if Length (Source) /= 0 then From <= Length (Source)),
486      Post   => Length (Translate'Result) = Length (Source),
493      Post   => Length (Source) = Length (Source)'Old,
500      Post   => Length (Translate'Result) = Length (Source),
507      Post   => Length (Source) = Length (Source)'Old,
526        Low - 1 <= Length (Source)
529                    <= Natural'Last - By'Length
530                     - Natural'Max (Length (Source) - High, 0)
531                  else Length (Source) <= Natural'Last - By'Length),
534           Length (Replace_Slice'Result)
535         = Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0),
537           Length (Replace_Slice'Result) = Length (Source)'Old + By'Length),
547        Low - 1 <= Length (Source)
550                    <= Natural'Last - By'Length
551                     - Natural'Max (Length (Source) - High, 0)
552                  else Length (Source) <= Natural'Last - By'Length),
555           Length (Source)
556         = Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0),
558           Length (Source) = Length (Source)'Old + By'Length),
566      Pre    => Before - 1 <= Length (Source)
567                  and then New_Item'Length <= Natural'Last - Length (Source),
568      Post   => Length (Insert'Result) = Length (Source) + New_Item'Length,
576      Pre    => Before - 1 <= Length (Source)
577                  and then New_Item'Length <= Natural'Last - Length (Source),
578      Post   => Length (Source) = Length (Source)'Old + New_Item'Length,
586      Pre    => Position - 1 <= Length (Source)
587                  and then (if New_Item'Length /= 0
589                            New_Item'Length <= Natural'Last - (Position - 1)),
591        Length (Overwrite'Result)
592      = Natural'Max (Length (Source), Position - 1 + New_Item'Length),
600      Pre    => Position - 1 <= Length (Source)
601                  and then (if New_Item'Length /= 0
603                            New_Item'Length <= Natural'Last - (Position - 1)),
605        Length (Source)
606      = Natural'Max (Length (Source)'Old, Position - 1 + New_Item'Length),
615      Pre            => (if Through <= From then From - 1 <= Length (Source)),
618           Length (Delete'Result) = Length (Source) - (Through - From + 1),
620           Length (Delete'Result) = Length (Source)),
628      Pre            => (if Through <= From then From - 1 <= Length (Source)),
631           Length (Source) = Length (Source)'Old - (Through - From + 1),
633           Length (Source) = Length (Source)'Old),
640      Post   => Length (Trim'Result) <= Length (Source),
647      Post   => Length (Source) <= Length (Source)'Old,
655      Post   => Length (Trim'Result) <= Length (Source),
663      Post   => Length (Source) <= Length (Source)'Old,
671      Post   => Length (Head'Result) = Count,
679      Post   => Length (Source) = Count,
687      Post   => Length (Tail'Result) = Count,
695      Post   => Length (Source) = Count,
703      Post   => Length ("*"'Result) = Left,
710      Pre    => (if Left /= 0 then Right'Length <= Natural'Last / Left),
711      Post   => Length ("*"'Result) = Left * Right'Length,
718      Pre    => (if Left /= 0 then Length (Right) <= Natural'Last / Left),
719      Post   => Length ("*"'Result) = Left * Length (Right),
736    pragma Inline (Length);