Files
Compile_And_Prove_Demo/proved/strings.ads
2017-04-05 19:27:27 +02:00

10 lines
265 B
Ada

package Strings is
subtype Str is String
with Predicate => Str'First = 1 and Str'Last < 10_000;
function Longest_Common_Prefix (X, Y : Str) return Natural with
Post => (for all J in 1 .. Longest_Common_Prefix'Result => X(J) = Y(J));
end Strings;