-extern cstring cstring_capitalize (cstring p_s) /*@*/ ;
-extern cstring cstring_capitalizeFree (/*@only@*/ cstring p_s) /*@modifies p_s@*/ ;
-extern cstring cstring_fill (cstring p_s, int p_n) /*@*/ ;
-extern cstring cstring_prefix (cstring p_s, int p_n) /*@*/ ;
-extern /*@observer@*/ cstring cstring_suffix (cstring p_s, int p_n) /*@*/ ;
-extern cstring cstring_concat (cstring p_s, cstring p_t) /*@*/ ;
+extern cstring cstring_capitalize (cstring p_s) /*@*/ /*@requires maxSet(p_s) >= 0 @*/ ;
+extern cstring cstring_capitalizeFree (/*@only@*/ cstring p_s) /*@modifies p_s@*/ /*@requires maxSet(p_s) >= 0 /\ maxRead(p_s) >= 0 @*/ ;
+
+extern cstring cstring_fill (cstring p_s, size_t p_n) /*@*/ /*@requires p_n >= 0 @*/;
+
+extern cstring cstring_prefix (cstring p_s, size_t p_n)
+ /*@*/
+ /*@requires maxRead(p_s) >= p_n /\ maxSet(p_s) >= p_n @*/
+ /*@ensures maxRead(result) == p_n /\ maxSet(result) == p_n @*/ ;
+
+extern /*@observer@*/ cstring cstring_suffix (cstring p_s, size_t p_n) /*@*/ ;
+extern cstring cstring_concat (cstring p_s, cstring p_t) /*@*/ /*@requires maxSet(p_s) >= 0 @*/;