You've already forked Compile_And_Prove_Demo
mirror of
https://github.com/AdaCore/Compile_And_Prove_Demo.git
synced 2026-02-12 12:45:02 -08:00
17 lines
481 B
Ada
17 lines
481 B
Ada
package body Strings is
|
|
|
|
function Longest_Common_Prefix (X, Y : Str) return Natural is
|
|
Length : Natural := 0;
|
|
Max_Length : constant Natural := Natural'Min(X'Length, Y'Length);
|
|
begin
|
|
while Length < Max_Length loop
|
|
pragma Loop_Invariant (for all J in 1 .. Length => X(J) = Y(J));
|
|
exit when X (Length + 1) /= Y (Length + 1);
|
|
Length := Length + 1;
|
|
end loop;
|
|
|
|
return Length;
|
|
end Longest_Common_Prefix;
|
|
|
|
end Strings;
|