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

[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.