Programming by Contract, Rosetta Code and Learn by AdaCore, post conditions with a function

General
1

Hi;

I’m puzzled by the second solution of the Rosetta Code Task (Test a function - Rosetta Code).

The function used by the first solution is being replaced by a function with a post condition. The code as written (perhaps due to formatting bug(s) on Rosetta Code?) fails to compile as there is no begin fr the function. My attempt to fix this fails as I do not understand how to properly use the post condition in conjunction with the required return statement for functions. I then looked up, again, on the Learn AdaCore web site regarding Programming by Contract. The examples there only use procedures, not functions.

This is the original function for the second solution:
function Palindrome (Text : String) return Boolean
with Post => Palindrome’Result =
(Text’Length < 2 or else
((Text(Text’First) = Text(Text’Last)) and then
Palindrome(Text(Text’First+1 … Text’Last-1))));

This is my attempt at a fix to the problem about the missing begin statement for the function, but don’t know how to correctly place the return statement:

function Palindrome (Text : String) return Boolean with
Post =>
Palindrome’Result =
(Text’Length < 2
or else
((Text (Text’First) = Text (Text’Last))
and then Palindrome (Text (Text’First + 1 … Text’Last - 1))))
is
begin
null;
end Palindrome;

Thanks in advance for the help.
Retired_Build_Engineer

2

Have you tried just replacing the Palindrome function in the first solution with the second Palindrome function (the one with post condition?)? Using the first solution main program?

3

Yes. I used the same calling environment and replaced the original function with the second version of the function.

Thanks,
Retired_Build_Engineer

4

It’s not another version of the function, it’s a specification of the function, which replaces the implicit specification of the first version.

Insert it before the unchanged original function.

5

Thank you, Simon! Why didn’t I see the obvious…

6

Probably beczuse you were looking somewhere else!