Re: On pragma Precondition and types

[Adam Beneschan <adam@irvine.com>]

On Oct 2, 7:35 am, Georg Bauhaus <rm.dash-bauh...@futureapps.de>
wrote:
> Suppose there is a type T with operations P and F,
>
>    type T is private;
>
>    procedure P (X: in out T);
>    function  F (X: T) return Boolean;
>
> I want to add a precondition of P. The precondition
> involves F,
>
>    procedure P (X: in out T);
>    pragma Precondition (F(X));
>
>    function  F (X: T) return Boolean;
>
> But when the compiler sees the pragma Precondition,
> it has not yet seen F.  Therefore, by the principle
> of linear reading, the precondition cannot be compiled,
> IIUC.
>
> Could there be a rule for pragmas, say, allowing forward
> references?

If you just heard a strange high-pitched noise, it was the sound of
several dozen compiler maintainers reacting to your proposal in
terror.  Sort of the same sound Janet Leigh made in "Psycho"........

                                 -- Adam