Thread overview
Missing function body bug
Aug 23, 2004
Arcane Jill
Aug 25, 2004
Arcane Jill
Aug 25, 2004
Walter
Aug 26, 2004
Arcane Jill
Aug 26, 2004
Walter
August 23, 2004
The following compiles, links and runs without complaint. The output is -nan. This is wrong.

What I would have /expected/ is that the program would compile, but not link, since the function body of squareRoot() has not been supplied.

This is exactly the sort of thing you want to put in a "header file".


#    double squareRoot(double d)
#    in
#    {
#        assert(d >= 0);
#    };
#    // function body supplied in linked library
#
#    void main()
#    {
#        double d = squareRoot(2.0);
#        printf("d = %f\n", d);
#    }


This also reinforces my point that preconditions need to be checked by the callee (unlike postconditions).

Jill


August 25, 2004
Erk. I seem to have written "callee" when I meant "caller".
caller = the code which calls a function
callee = the code inside the function body.
Sorry.

So of course, I should have said:
>This also reinforces my point that preconditions need to be checked by the caller (unlike postconditions).
>    ^^



In article <cgcjqc$2ag5$1@digitaldaemon.com>, Arcane Jill says...
>
>The following compiles, links and runs without complaint. The output is -nan. This is wrong.
>
>What I would have /expected/ is that the program would compile, but not link, since the function body of squareRoot() has not been supplied.
>
>This is exactly the sort of thing you want to put in a "header file".
>
>
>#    double squareRoot(double d)
>#    in
>#    {
>#        assert(d >= 0);
>#    };
>#    // function body supplied in linked library
>#
>#    void main()
>#    {
>#        double d = squareRoot(2.0);
>#        printf("d = %f\n", d);
>#    }
>
>
>This also reinforces my point that preconditions need to be checked by the callee^Hr (unlike postconditions).
>
>Jill
>
>


August 25, 2004
I've fixed it so the compiler generates an error if you have an in without a body.

"Arcane Jill" <Arcane_member@pathlink.com> wrote in message news:cgcjqc$2ag5$1@digitaldaemon.com...
> The following compiles, links and runs without complaint. The output
is -nan.
> This is wrong.
>
> What I would have /expected/ is that the program would compile, but not
link,
> since the function body of squareRoot() has not been supplied.
>
> This is exactly the sort of thing you want to put in a "header file".
>
>
> #    double squareRoot(double d)
> #    in
> #    {
> #        assert(d >= 0);
> #    };
> #    // function body supplied in linked library
> #
> #    void main()
> #    {
> #        double d = squareRoot(2.0);
> #        printf("d = %f\n", d);
> #    }
>
>
> This also reinforces my point that preconditions need to be checked by the callee (unlike postconditions).
>
> Jill
>
>


August 26, 2004
In article <cgiphe$2ev0$3@digitaldaemon.com>, Walter says...
>
>I've fixed it so the compiler generates an error if you have an in without a body.

But a closed-source library would /want/ to specify an in without a body. You need to be able to expose the precondition to the caller without the implementation.

Arcane Jill


August 26, 2004
"Arcane Jill" <Arcane_member@pathlink.com> wrote in message news:cgk49c$213$1@digitaldaemon.com...
> In article <cgiphe$2ev0$3@digitaldaemon.com>, Walter says...
> >
> >I've fixed it so the compiler generates an error if you have an in
without a
> >body.
>
> But a closed-source library would /want/ to specify an in without a body.
You
> need to be able to expose the precondition to the caller without the implementation.

This would imply that the caller must execute the precondition rather than the callee. This is problematical in the case of polymorphic preconditions.

It may be possible to solve that problem, but if so, it would be a post 1.0 feature. For 1.0, preconditions are part of the callee implementation, and so must have a body to go with them.