Ada2012 Invariants and obaque types

Ada2012 Invariants and obaque types

[Martin]

A fairly common Ada idiom is to define the full view of a private type
using an incomplete declaration. Thus leaving the actual
implementation to the package spec. Trying this out with the public
view defined with an invariant lead to a compiler error - is this:

a) expected?
b) an unexpected consequence? or
c) a compiler bug?

Example:
package P1 is
   type T1 is tagged private
      with Invariant => Is_Valid (T1);
   function Create               return T1;
   function Is_Valid (This : T1) return Boolean;
private
   type Imp;
   type T1 is
      record
         I : Imp;
      end record;
end P1;

gnatmake -ws -c -u -PH:\Ada\test_invariants\test_invariants.gpr p1.ads
gcc -c -g -g -gnatE -gnatVn -gnato -fstack-check -gnat12 -gnatf -I- -
gnatA H:\Ada\test_invariants\src\p1.ads
p1.ads:11:04: type "Imp" is frozen at line 3 before its full
declaration
p1.ads:13:09: full declaration of private type "T1" defined at line 3
must be a tagged type
p1.ads:15:14: invalid use of type before its full declaration
gnatmake: "H:\Ada\test_invariants\src\p1.ads" compilation error

[2011-06-21 09:46:55] process exited with status 4 (elapsed time:
00.26s)

Re: Ada2012 Invariants and obaque types

[Yannick Duchêne (Hibou57)]

Hi Martin,

Unless I've missed something, I do not see the point. Whether or not you  
use an invariant, if the public view assert the type is tagged, the full  
view must be tagged. This was the same, even prior to Ada 2012. Otherwise,  
how would you derive from a tagged public view and define class wide view,  
 from a type whose private view isn't tagged ?

Just out of curiosity: which GNAT flavor do you use for Ada 2012 ?

Le Tue, 21 Jun 2011 10:53:31 +0200, Martin <martin.dowie@btopenworld.com>  
a écrit:

> A fairly common Ada idiom is to define the full view of a private type
> using an incomplete declaration. Thus leaving the actual
> implementation to the package spec. Trying this out with the public
> view defined with an invariant lead to a compiler error - is this:
>
> a) expected?
> b) an unexpected consequence? or
> c) a compiler bug?
>
> Example:
> package P1 is
>    type T1 is tagged private
>       with Invariant => Is_Valid (T1);
>    function Create               return T1;
>    function Is_Valid (This : T1) return Boolean;
> private
>    type Imp;
>    type T1 is
>       record
>          I : Imp;
>       end record;
> end P1;
>
> gnatmake -ws -c -u -PH:\Ada\test_invariants\test_invariants.gpr p1.ads
> gcc -c -g -g -gnatE -gnatVn -gnato -fstack-check -gnat12 -gnatf -I- -
> gnatA H:\Ada\test_invariants\src\p1.ads
> p1.ads:11:04: type "Imp" is frozen at line 3 before its full
> declaration
> p1.ads:13:09: full declaration of private type "T1" defined at line 3
> must be a tagged type
> p1.ads:15:14: invalid use of type before its full declaration
> gnatmake: "H:\Ada\test_invariants\src\p1.ads" compilation error
>
> [2011-06-21 09:46:55] process exited with status 4 (elapsed time:
> 00.26s)


-- 
“Syntactic sugar causes cancer of the semi-colons.”  [Epigrams on  
Programming — Alan J. — P. Yale University]
“Structured Programming supports the law of the excluded muddle.” [Idem]
Java: Write once, Never revisit

Re: Ada2012 Invariants and obaque types

[Martin]

On Jun 21, 11:27 am, Yannick Duchêne (Hibou57)
<yannick_duch...@yahoo.fr> wrote:
> Hi Martin,
>
> Unless I've missed something, I do not see the point. Whether or not you  
> use an invariant, if the public view assert the type is tagged, the full  
> view must be tagged. This was the same, even prior to Ada 2012. Otherwise,  
> how would you derive from a tagged public view and define class wide view,  
>  from a type whose private view isn't tagged ?
>
> Just out of curiosity: which GNAT flavor do you use for Ada 2012 ?
>
> Le Tue, 21 Jun 2011 10:53:31 +0200, Martin <martin.do...@btopenworld.com>  
> a écrit:
>
>
>
>
>
>
>
>
>
> > A fairly common Ada idiom is to define the full view of a private type
> > using an incomplete declaration. Thus leaving the actual
> > implementation to the package spec. Trying this out with the public
> > view defined with an invariant lead to a compiler error - is this:
>
> > a) expected?
> > b) an unexpected consequence? or
> > c) a compiler bug?
>
> > Example:
> > package P1 is
> >    type T1 is tagged private
> >       with Invariant => Is_Valid (T1);
> >    function Create               return T1;
> >    function Is_Valid (This : T1) return Boolean;
> > private
> >    type Imp;
> >    type T1 is
> >       record
> >          I : Imp;
> >       end record;
> > end P1;
>
> > gnatmake -ws -c -u -PH:\Ada\test_invariants\test_invariants.gpr p1.ads
> > gcc -c -g -g -gnatE -gnatVn -gnato -fstack-check -gnat12 -gnatf -I- -
> > gnatA H:\Ada\test_invariants\src\p1.ads
> > p1.ads:11:04: type "Imp" is frozen at line 3 before its full
> > declaration
> > p1.ads:13:09: full declaration of private type "T1" defined at line 3
> > must be a tagged type
> > p1.ads:15:14: invalid use of type before its full declaration
> > gnatmake: "H:\Ada\test_invariants\src\p1.ads" compilation error
>
> > [2011-06-21 09:46:55] process exited with status 4 (elapsed time:
> > 00.26s)
>
> --
> “Syntactic sugar causes cancer of the semi-colons.”  [Epigrams on  
> Programming — Alan J. — P. Yale University]
> “Structured Programming supports the law of the excluded muddle.” [Idem]
> Java: Write once, Never revisit

Sorry - the pearls of doing a 'quick' demo...

Replace "type T1 is" with " type T1 is tagged"

and you still get:

> > p1.ads:11:04: type "Imp" is frozen at line 3 before its full
> > declaration
> > p1.ads:15:14: invalid use of type before its full declaration
> > gnatmake: "H:\Ada\test_invariants\src\p1.ads" compilation error

Which is the really what I'm asking about...

-- Martin

Re: Ada2012 Invariants and obaque types

[Ludovic Brenta]

Martin Dowie wrote on comp.lang.ada:
> A fairly common Ada idiom is to define the full view of a private type
> using an incomplete declaration. Thus leaving the actual
> implementation to the package spec. Trying this out with the public
> view defined with an invariant lead to a compiler error - is this:
>
> a) expected?
> b) an unexpected consequence? or
> c) a compiler bug?
>
> Example:
> package P1 is
>    type T1 is tagged private
>       with Invariant => Is_Valid (T1);
>    function Create               return T1;
>    function Is_Valid (This : T1) return Boolean;
> private
>    type Imp;
>    type T1 is
>       record
>          I : Imp;
>       end record;
> end P1;
>
> gnatmake -ws -c -u -PH:\Ada\test_invariants\test_invariants.gpr p1.ads
> gcc -c -g -g -gnatE -gnatVn -gnato -fstack-check -gnat12 -gnatf -I- -
> gnatA H:\Ada\test_invariants\src\p1.ads
> p1.ads:11:04: type "Imp" is frozen at line 3 before its full
> declaration
> p1.ads:13:09: full declaration of private type "T1" defined at line 3
> must be a tagged type
> p1.ads:15:14: invalid use of type before its full declaration
> gnatmake: "H:\Ada\test_invariants\src\p1.ads" compilation error
>
> [2011-06-21 09:46:55] process exited with status 4 (elapsed time:
> 00.26s)

This looks like a consequence of 13.14(8.2/1): "If an expression is
implicitly converted to a type or subtype T, then at the place where
the expression causes freezing, T is frozen." (where in this case the
expression is T1, which stands for the current instance of the type,
and the type T is also T1).

This subclause however seems to contradict 13.14(7.2/3): "At the
freezing point of the entity associated with an aspect_specification,
any expressions or names within the aspect_specification cause
freezing."; this subclause would defer the freezing point of T1 until
the end of the enclosing package spec or the declaration of a constant
of the type, whichever comes first (as is normal for tagged types).

Another possible interpretation is that Is_Valid must be called as
part of the elaboration of type T1, in which case the
aspect_specification is a function call, which freezes the types of
its parameters (per 13.14(10.1/3)).  But I doubt this is true.

So, this looks like an area of the language definition that needs
clarifying (but then again, freezing rules have always been difficult
to understand). The behavior of the compiler definitely looks
undesirable to me.  So I vote for b) an unexpected (and undesirable)
consequence (of existing rules).

--
Ludovic Brenta.

Re: Ada2012 Invariants and obaque types

[Martin]

On Jun 21, 11:27 am, Yannick Duchêne (Hibou57)
<yannick_duch...@yahoo.fr> wrote:
> Just out of curiosity: which GNAT flavor do you use for Ada 2012 ?

GNAT GPL 2011

-- Martin

Re: Ada2012 Invariants and obaque types

[Martin]

On Jun 21, 11:43 am, Ludovic Brenta <ludo...@ludovic-brenta.org>
wrote:
> Martin Dowie wrote on comp.lang.ada:
>
>
>
>
>
>
>
>
>
> > A fairly common Ada idiom is to define the full view of a private type
> > using an incomplete declaration. Thus leaving the actual
> > implementation to the package spec. Trying this out with the public
> > view defined with an invariant lead to a compiler error - is this:
>
> > a) expected?
> > b) an unexpected consequence? or
> > c) a compiler bug?
>
> > Example:
> > package P1 is
> >    type T1 is tagged private
> >       with Invariant => Is_Valid (T1);
> >    function Create               return T1;
> >    function Is_Valid (This : T1) return Boolean;
> > private
> >    type Imp;
> >    type T1 is
> >       record
> >          I : Imp;
> >       end record;
> > end P1;
>
> > gnatmake -ws -c -u -PH:\Ada\test_invariants\test_invariants.gpr p1.ads
> > gcc -c -g -g -gnatE -gnatVn -gnato -fstack-check -gnat12 -gnatf -I- -
> > gnatA H:\Ada\test_invariants\src\p1.ads
> > p1.ads:11:04: type "Imp" is frozen at line 3 before its full
> > declaration
> > p1.ads:13:09: full declaration of private type "T1" defined at line 3
> > must be a tagged type
> > p1.ads:15:14: invalid use of type before its full declaration
> > gnatmake: "H:\Ada\test_invariants\src\p1.ads" compilation error
>
> > [2011-06-21 09:46:55] process exited with status 4 (elapsed time:
> > 00.26s)
>
> This looks like a consequence of 13.14(8.2/1): "If an expression is
> implicitly converted to a type or subtype T, then at the place where
> the expression causes freezing, T is frozen." (where in this case the
> expression is T1, which stands for the current instance of the type,
> and the type T is also T1).
>
> This subclause however seems to contradict 13.14(7.2/3): "At the
> freezing point of the entity associated with an aspect_specification,
> any expressions or names within the aspect_specification cause
> freezing."; this subclause would defer the freezing point of T1 until
> the end of the enclosing package spec or the declaration of a constant
> of the type, whichever comes first (as is normal for tagged types).
>
> Another possible interpretation is that Is_Valid must be called as
> part of the elaboration of type T1, in which case the
> aspect_specification is a function call, which freezes the types of
> its parameters (per 13.14(10.1/3)).  But I doubt this is true.
>
> So, this looks like an area of the language definition that needs
> clarifying (but then again, freezing rules have always been difficult
> to understand). The behavior of the compiler definitely looks
> undesirable to me.  So I vote for b) an unexpected (and undesirable)
> consequence (of existing rules).
>
> --
> Ludovic Brenta.

Ok, thanks for that Ludovic...maybe need to post this one to ada-
auth...

-- Martin

Re: Ada2012 Invariants and obaque types

[Martin]

On Jun 21, 9:53 am, Martin <martin.do...@btopenworld.com> wrote:
> A fairly common Ada idiom is to define the full view of a private type
> using an incomplete declaration. Thus leaving the actual
> implementation to the package spec. Trying this out with the public
> view defined with an invariant lead to a compiler error - is this:
>
> a) expected?
> b) an unexpected consequence? or
> c) a compiler bug?
>
> Example:
> package P1 is
>    type T1 is tagged private
>       with Invariant => Is_Valid (T1);
>    function Create               return T1;
>    function Is_Valid (This : T1) return Boolean;
> private
>    type Imp;
>    type T1 is
>       record
>          I : Imp;
>       end record;
> end P1;
>
> gnatmake -ws -c -u -PH:\Ada\test_invariants\test_invariants.gpr p1.ads
> gcc -c -g -g -gnatE -gnatVn -gnato -fstack-check -gnat12 -gnatf -I- -
> gnatA H:\Ada\test_invariants\src\p1.ads
> p1.ads:11:04: type "Imp" is frozen at line 3 before its full
> declaration
> p1.ads:13:09: full declaration of private type "T1" defined at line 3
> must be a tagged type
> p1.ads:15:14: invalid use of type before its full declaration
> gnatmake: "H:\Ada\test_invariants\src\p1.ads" compilation error
>
> [2011-06-21 09:46:55] process exited with status 4 (elapsed time:
> 00.26s)

A more correct version is:

package P1 is
   type T1 is tagged private
     with Invariant => Is_Valid (T1);
   function Create               return T1;
   function Is_Valid (This : T1) return Boolean;
private
   type Imp;
   type Imp_Ref is not null access Imp;
   type T1 is tagged
      record
         I : Imp_Ref;
      end record;
end P1;

Resulting in:

gnatmake -d -PH:\Ada\test_invarients\test_invarients.gpr p1.ads
gcc -c -g -g -gnatE -fstack-check -gnato -gnatf -fcallgraph-info=su,da
-gnat12 -I- -gnatA H:\Ada\test_invarients\src\p1.ads
p1.ads:7:04: type "Imp" is frozen at line 2 before its full
declaration
gnatmake: "H:\Ada\test_invarients\src\p1.ads" compilation error

[2011-06-21 11:50:40] process exited with status 4 (elapsed time:
00.42s)

Re: Ada2012 Invariants and obaque types

[Robert A Duff]

Martin <martin.dowie@btopenworld.com> writes:

> A fairly common Ada idiom is to define the full view of a private type
> using an incomplete declaration. Thus leaving the actual
> implementation to the package spec.

Body?

>...Trying this out with the public
> view defined with an invariant lead to a compiler error - is this:
>
> a) expected?
> b) an unexpected consequence? or
> c) a compiler bug?
>
> Example:
> package P1 is
>    type T1 is tagged private
>       with Invariant => Is_Valid (T1);
>    function Create               return T1;
>    function Is_Valid (This : T1) return Boolean;
> private
>    type Imp;
>    type T1 is
>       record
>          I : Imp;
>       end record;
> end P1;

This has nothing to do with invariants.  Incomplete types can only
be used in very restricted ways.  Not as components.  You need to
use an access type.

This dates back to Ada 83 -- it's always been illegal, and still is.

When compiling clients of P1 that declare objects of type T1,
how would the compiler know the size?  It could treat it as
dynamic, or it could take a peek at the body, but if either of
those was the intended compilation model, then there would be no
need for private parts in the first place -- we'd put the completion
of a private type in the body, where it belongs.

I suggest you erase the invariant, fix the errors, and then put the
invariant back in.  There's nothing wrong with your invariant.

- Bob

Re: Ada2012 Invariants and obaque types

[Martin]

On Jun 21, 12:31 pm, Robert A Duff <bobd...@shell01.TheWorld.com>
wrote:
> Martin <martin.do...@btopenworld.com> writes:
> > A fairly common Ada idiom is to define the full view of a private type
> > using an incomplete declaration. Thus leaving the actual
> > implementation to the package spec.
>
> Body?

Yes!


> I suggest you erase the invariant, fix the errors, and then put the
> invariant back in.  There's nothing wrong with your invariant.

Did that...but still getting an error - see my post from 12:14.

TIA
-- Martin

Re: Ada2012 Invariants and obaque types

[Martin]

On Jun 21, 12:31 pm, Robert A Duff <bobd...@shell01.TheWorld.com>
wrote:
> I suggest you erase the invariant, fix the errors, and then put the
> invariant back in.  There's nothing wrong with your invariant.

Ok, with no Invariant:

package P1 is
   type T1 is tagged private;
   function Is_Valid (This : T1) return Boolean;
private
   type Imp;
   type Imp_Ref is not null access Imp;
   type T1 is tagged
      record
         I : Imp_Ref;
      end record;
end P1;

I get:
gnatmake -d -PH:\Ada\test_invarients\test_invarients.gpr p1.ads
gcc -c -g -g -gnatE -fstack-check -gnato -gnatf -fcallgraph-info=su,da
-gnat12 -I- -gnatA H:\Ada\test_invarients\src\p1.ads
cannot generate code for file p1.ads (package spec)
gnatmake: "H:\Ada\test_invarients\src\p1.ads" compilation error

[2011-06-21 12:58:10] process exited with status 4 (elapsed time:
00.37s)

i.e. no error.

The most reduced version I can come up with is now:
package P1 is
   type T1 is tagged private
     with Invariant => True;  -- NB: not even a 'real' function
private
   type Imp;
   type Imp_Ref is not null access Imp;
   type T1 is tagged
      record
         I : Imp_Ref;
      end record;
end P1;

which produces the same original error:

gnatmake -d -PH:\Ada\test_invarients\test_invarients.gpr p1.ads
gcc -c -g -g -gnatE -fstack-check -gnato -gnatf -fcallgraph-info=su,da
-gnat12 -I- -gnatA H:\Ada\test_invarients\src\p1.ads
p1.ads:5:04: type "Imp" is frozen at line 2 before its full
declaration
gnatmake: "H:\Ada\test_invarients\src\p1.ads" compilation error

[2011-06-21 13:01:10] process exited with status 4 (elapsed time:
00.53s)

-- Martin

Re: Ada2012 Invariants and obaque types

[Dmitry A. Kazakov]

On Tue, 21 Jun 2011 01:53:31 -0700 (PDT), Martin wrote:

> package P1 is
>    type T1 is tagged private
>       with Invariant => Is_Valid (T1);

Unrelated to Ada, but in theory, an invariant is a private implementation
dependent thing. An invariant is trivially true in all public views of the
object, i.e. between any two calls to the object's operations. From that
follows, when mentioned in a public part then:

   type T1 is tagged private with Invariant => True;

(Again, I don't know which ideas Ada designers had about invariants, I am
not a language lawyer.)

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Ada2012 Invariants and obaque types

[Robert A Duff]

Martin <martin.dowie@btopenworld.com> writes:

> package P1 is
>    type T1 is tagged private
>      with Invariant => True;  -- NB: not even a 'real' function
> private
>    type Imp;
>    type Imp_Ref is not null access Imp;
>    type T1 is tagged
>       record
>          I : Imp_Ref;
>       end record;
> end P1;
>
> which produces the same original error:

Looks like a compiler bug.

- Bob

Re: Ada2012 Invariants and obaque types

[Georg Bauhaus]

On 21.06.11 14:08, Dmitry A. Kazakov wrote:
> On Tue, 21 Jun 2011 01:53:31 -0700 (PDT), Martin wrote:
> 
>> package P1 is
>>    type T1 is tagged private
>>       with Invariant => Is_Valid (T1);
> 
> Unrelated to Ada, but in theory, an invariant is a private implementation
> dependent thing. An invariant is trivially true in all public views of the
> object, i.e. between any two calls to the object's operations. From that
> follows, when mentioned in a public part then:
> 
>    type T1 is tagged private with Invariant => True;
> 
> (Again, I don't know which ideas Ada designers had about invariants, I am
> not a language lawyer.)

In another theory, the invariant may express things
such as
 Num_Green_Lights (T1) >= 3;
or
'Length < State_of_Things (T1) * 2;
where Num_Green_Lights is a publicly visible function whose
result is somehow computed.  These predicates would be informative,
and formal.

Would they be private implementation dependent things?  Or could
I expect, seeing the public view and its invariant, the possibility
of different implementations (of both the view and the invariant)?

Re: Ada2012 Invariants and obaque types

[Martin]

On Jun 21, 1:13 pm, Robert A Duff <bobd...@shell01.TheWorld.com>
wrote:
> Martin <martin.do...@btopenworld.com> writes:
> > package P1 is
> >    type T1 is tagged private
> >      with Invariant => True;  -- NB: not even a 'real' function
> > private
> >    type Imp;
> >    type Imp_Ref is not null access Imp;
> >    type T1 is tagged
> >       record
> >          I : Imp_Ref;
> >       end record;
> > end P1;
>
> > which produces the same original error:
>
> Looks like a compiler bug.
>
> - Bob

Thanks! I'll just have to stick with "with Post =>" on all the
operations instead for now...until GNAT GPL 2012!! :-)

Shame the GPL version only updates once per year...don't suppose
there's any chance of even a twice-yearly release schedule?...

-- Martin

Re: Ada2012 Invariants and obaque types

[Dmitry A. Kazakov]

On Tue, 21 Jun 2011 14:17:11 +0200, Georg Bauhaus wrote:

> On 21.06.11 14:08, Dmitry A. Kazakov wrote:
>> On Tue, 21 Jun 2011 01:53:31 -0700 (PDT), Martin wrote:
>> 
>>> package P1 is
>>>    type T1 is tagged private
>>>       with Invariant => Is_Valid (T1);
>> 
>> Unrelated to Ada, but in theory, an invariant is a private implementation
>> dependent thing. An invariant is trivially true in all public views of the
>> object, i.e. between any two calls to the object's operations. From that
>> follows, when mentioned in a public part then:
>> 
>>    type T1 is tagged private with Invariant => True;
>> 
>> (Again, I don't know which ideas Ada designers had about invariants, I am
>> not a language lawyer.)
> 
> In another theory, the invariant may express things
> such as
>  Num_Green_Lights (T1) >= 3;
> or
> 'Length < State_of_Things (T1) * 2;
> where Num_Green_Lights is a publicly visible function whose
> result is somehow computed.  These predicates would be informative,
> and formal.

That is not an invariant, but a constraint. Constraint creates a subtype,
it is a type-algebraic operation. Invariant does nothing, it is just a
predicate known to be true for all instances of the type in public
contexts. As such it can be removed any time without changing the program
semantics. A constraint cannot be removed, because its violation is 1)
possible and legal, 2) has defined effect (exception). Violation of an
invariant in public context is impossible in a correct program.

   subtype Line is String (1..80); -- 1..80 is a constraint
   Line'Length = 80 -- This is an invariant

P.S. Again, no idea how Ada 2012 treats this issue, differently I guess.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Ada2012 Invariants and obaque types

[Robert A Duff]

Martin <martin.dowie@btopenworld.com> writes:

> Thanks!

You're welcome.

>... I'll just have to stick with "with Post =>" on all the
> operations instead for now...until GNAT GPL 2012!! :-)

Or don't use incomplete types completed in the body.

- Bob

Re: Ada2012 Invariants and obaque types

[Martin]

On Jun 21, 1:54 pm, Robert A Duff <bobd...@shell01.TheWorld.com>
wrote:
> Martin <martin.do...@btopenworld.com> writes:
> > Thanks!
>
> You're welcome.
>
> >... I'll just have to stick with "with Post =>" on all the
> > operations instead for now...until GNAT GPL 2012!! :-)
>
> Or don't use incomplete types completed in the body.
>
> - Bob

Yes, I was thinking of replacing this with discriminant to an
interface instead...(think 'strategy pattern' but with only 1
strategy)...wonder hold Invar/Pre/Post will cope with that!! :-)

-- Martin

Re: Ada2012 Invariants and obaque types

[Georg Bauhaus]

On 21.06.11 14:31, Dmitry A. Kazakov wrote:

>> In another theory, the invariant may express things
>> such as
>>  Num_Green_Lights (T1) >= 3;
>> or
>> 'Length < State_of_Things (T1) * 2;
>> where Num_Green_Lights is a publicly visible function whose
>> result is somehow computed.  These predicates would be informative,
>> and formal.
> 
> That is not an invariant, but a constraint.

I don't see bounds in the above.

I can state, though, that there will be---invariably---at least
three green lights because that is a property of how each
implementation of the type will be constructed.  How is that
variant?  That is, if the (theoretical) assertion is "at least,
no matter what, under all circumstances, in each implementation",
isn't this an invariant?

Re: Ada2012 Invariants and obaque types

[Dmitry A. Kazakov]

On Tue, 21 Jun 2011 15:29:22 +0200, Georg Bauhaus wrote:

> On 21.06.11 14:31, Dmitry A. Kazakov wrote:
> 
>>> In another theory, the invariant may express things
>>> such as
>>>  Num_Green_Lights (T1) >= 3;
>>> or
>>> 'Length < State_of_Things (T1) * 2;
>>> where Num_Green_Lights is a publicly visible function whose
>>> result is somehow computed.  These predicates would be informative,
>>> and formal.
>> 
>> That is not an invariant, but a constraint.
> 
> I don't see bounds in the above.

Constraint could be any, not only bounds. It is not the formula, but the
meaning of:

   S = { x | x in T and P (x) }

here P is a constraint, which produces S.

   x in S => Q (x)

here Q is an invariant of S. It might happen that Q (x) <=> P (x). Then you
could define S using Q, that would make Q constraint and P invariant.

> That is, if the (theoretical) assertion is "at least,
> no matter what, under all circumstances, in each implementation",
> isn't this an invariant?

1. Different implementations of the same specification may have different
invariants. That are the predicates which cannot be derived from the
specification.

2. When a predicate can be derived from the specification that does not yet
imply its equivalence to the specification. Invariant does not necessarily
defines the type.

3. The difference is the intent. The specification defines the [sub]type.
Invariant merely is a predicate provable true for the given implementation
of the specification. (Properly constructed invariants can be used in
construction of implementations, e.g. Dijkstra's approach to programming,
loop invariants etc)

4. You cannot distinguish predicates used in definitions from ones used in
proofs by just looking at them. It is the language's task to do this by
syntax means.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Ada2012 Invariants and obaque types

[Yannick Duchêne (Hibou57)]

Le Tue, 21 Jun 2011 14:08:15 +0200, Dmitry A. Kazakov  
<mailbox@dmitry-kazakov.de> a écrit:

> On Tue, 21 Jun 2011 01:53:31 -0700 (PDT), Martin wrote:
>
>> package P1 is
>>    type T1 is tagged private
>>       with Invariant => Is_Valid (T1);
>
> Unrelated to Ada, but in theory, an invariant is a private implementation
> dependent thing. An invariant is trivially true in all public views of  
> the object,
I understand the point and had the same first feeling too. While that's OK  
in theory, in practice the user may wish methods to check for validity  
rules defined for a type. Then, Is_Valid is abstract enough. And  
after-all, you already have 'Valid attribute in Ada. This is useful for  
designs relying on defensive programming and which disallow use of  
exceptions.

-- 
“Syntactic sugar causes cancer of the semi-colons.”  [Epigrams on  
Programming — Alan J. — P. Yale University]
“Structured Programming supports the law of the excluded muddle.” [Idem]
Java: Write once, Never revisit

Re: Ada2012 Invariants and obaque types

[Yannick Duchêne (Hibou57)]

Le Tue, 21 Jun 2011 12:46:35 +0200, Martin <martin.dowie@btopenworld.com>  
a écrit:

> On Jun 21, 11:27 am, Yannick Duchêne (Hibou57)
> <yannick_duch...@yahoo.fr> wrote:
>> Just out of curiosity: which GNAT flavor do you use for Ada 2012 ?
>
> GNAT GPL 2011

OK, so that's unfortunately not an MGPL version.


-- 
“Syntactic sugar causes cancer of the semi-colons.”  [Epigrams on  
Programming — Alan J. — P. Yale University]
“Structured Programming supports the law of the excluded muddle.” [Idem]
Java: Write once, Never revisit

Re: Ada2012 Invariants and obaque types

[Dmitry A. Kazakov]

On Tue, 21 Jun 2011 20:37:44 +0200, Yannick Duch�ne (Hibou57) wrote:

> Le Tue, 21 Jun 2011 14:08:15 +0200, Dmitry A. Kazakov  
> <mailbox@dmitry-kazakov.de> a �crit:
> 
>> On Tue, 21 Jun 2011 01:53:31 -0700 (PDT), Martin wrote:
>>
>>> package P1 is
>>>    type T1 is tagged private
>>>       with Invariant => Is_Valid (T1);
>>
>> Unrelated to Ada, but in theory, an invariant is a private implementation
>> dependent thing. An invariant is trivially true in all public views of  
>> the object,
> I understand the point and had the same first feeling too.

The first feeling is always the right one. (:-))

> While that's OK  
> in theory, in practice the user may wish methods to check for validity  
> rules defined for a type.

Validity is a misconception. In a properly typed language any value is
valid, that is the property of being typed. A value is invalid when the
type system was circumvented, which should never happen publicly.

> Then, Is_Valid is abstract enough. And  
> after-all, you already have 'Valid attribute in Ada. This is useful for  
> designs relying on defensive programming and which disallow use of  
> exceptions.

'Valid is a hack around missing value initialization enforcement or some
kludges to support Unchecked_Conversion. It cannot justify anything because
'Valid itself lacks credibility.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Ada2012 Invariants and obaque types

[Vinzent Hoefler]

Dmitry A. Kazakov wrote:

> 'Valid is a hack around missing value initialization enforcement or some
> kludges to support Unchecked_Conversion. It cannot justify anything because
> 'Valid itself lacks credibility.

How do you properly initialise and/or validate values coming from an untrusted
external source (i.e. "bus")? Always using the full bit pattern and write the
conversion routine yourself?


Vinzent.

-- 
f u cn rd ths, u cn gt a gd jb n cmptr prgrmmng.

Re: Ada2012 Invariants and obaque types

[Dmitry A. Kazakov]

On Tue, 21 Jun 2011 21:34:31 +0200, Vinzent Hoefler wrote:

> Dmitry A. Kazakov wrote:
> 
>> 'Valid is a hack around missing value initialization enforcement or some
>> kludges to support Unchecked_Conversion. It cannot justify anything because
>> 'Valid itself lacks credibility.
> 
> How do you properly initialise and/or validate values coming from an untrusted
> external source (i.e. "bus")? Always using the full bit pattern and write the
> conversion routine yourself?

Yes, I always do exactly this, at least in order to make my program
portable. E.g. instead of querying the endianness of the machine and trying
to guess what kind of bit shuffling might be appropriate in order to map an
external representation onto the machine one through Unchecked_Conversion
(provided such mapping exists, which in real life could not be the case
when working with bus encodings), I just interpret bits as they are
described. It is safer, cleaner, easier to understand, requires no
preprocessing. If this could be slightly less efficient, I don't care.

BTW, what I do miss for this stuff is cross type checks. E.g.

   X : Integer := ...;

   if X in Unsigned_32'Range then

The problem is that both

   if X in Integer (Unsigned_32'First)..Integer (Unsigned_32'Last) then

or

   if Unsigned_32 (X) in Unsigned_32'Range then

might fail on different machines. I need a test if the value of the type T
can be converted to the type S. (For real types it can be a quite
non-trivial to test)

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Ada2012 Invariants and obaque types

[Manuel Collado]

El 21/06/2011 20:53, Dmitry A. Kazakov escribi�:
> On Tue, 21 Jun 2011 20:37:44 +0200, Yannick Duch�ne (Hibou57) wrote:
>
>> Le Tue, 21 Jun 2011 14:08:15 +0200, Dmitry A. Kazakov
>> <mailbox@dmitry-kazakov.de>  a �crit:
>>
>>> On Tue, 21 Jun 2011 01:53:31 -0700 (PDT), Martin wrote:
>>>
>>>> package P1 is
>>>>     type T1 is tagged private
>>>>        with Invariant =>  Is_Valid (T1);
>>>
>>> Unrelated to Ada, but in theory, an invariant is a private implementation
>>> dependent thing. An invariant is trivially true in all public views of
>>> the object,
>> I understand the point and had the same first feeling too.
>
> The first feeling is always the right one. (:-))
>
>> While that's OK
>> in theory, in practice the user may wish methods to check for validity
>> rules defined for a type.
>
> Validity is a misconception. In a properly typed language any value is
> valid, that is the property of being typed. A value is invalid when the
> type system was circumvented, which should never happen publicly.

Humm... What about an integral type whose set of valid values are the 
prime numbers (upto some representation limit)?

Common practice is to define such type as Integer, Natural or Positive, 
and write some validation function to check values at runtime.

Or do you mean that Ada is not a properly typed language?

-- 
Manuel Collado - http://lml.ls.fi.upm.es/~mcollado

Re: Ada2012 Invariants and obaque types

[Vinzent Hoefler]

Dmitry A. Kazakov wrote:

> On Tue, 21 Jun 2011 21:34:31 +0200, Vinzent Hoefler wrote:
>
>> Dmitry A. Kazakov wrote:
>>
>>> 'Valid is a hack around missing value initialization enforcement or some
>>> kludges to support Unchecked_Conversion. It cannot justify anything because
>>> 'Valid itself lacks credibility.
>>
>> How do you properly initialise and/or validate values coming from an untrusted
>> external source (i.e. "bus")? Always using the full bit pattern and write the
>> conversion routine yourself?
>
> Yes, I always do exactly this, at least in order to make my program
> portable.

Hmm. Reading bus values in a particular endianes and being portable... ;)

Example:

     --  type used for clock source and retrigger mode selections
     --  bits [4:2]
     --  RTG  PSC_SEL EXT_CLK   clock mode
     --    0        0       0   Internal, cpu clock, gated
     --    0        0       1   External
     --    0        1       0   Internal, prescaled, gated
     --    0        1       1   N/A (same as 001)
     --    1        0       0   Internal, cpu clock, retriggered
     --    1        0       1   N/A (same as 001)
     --    1        1       0   internal, prescaled, retriggered
     --    1        1       1   N/A (same as 001)
     type Clock_Source is (Internal_Gated,
                           External,
                           Prescaled_Gated,
                           Internal_Retriggered,
                           Prescaled_Retriggered);

     for Clock_Source use (Internal_Gated        => 2#000#,
                           External              => 2#001#,
                           Prescaled_Gated       => 2#010#,
                           Internal_Retriggered  => 2#100#,
                           Prescaled_Retriggered => 2#110#);

     for Clock_Source'Size use 3;

Would you actually do without the type representation here and start masking off the
bits by hand again instead of using 'Valid, just in case of of those "N/A" values
sneak in?


Vinzent.

-- 
f u cn rd ths, u cn gt a gd jb n cmptr prgrmmng.

Re: Ada2012 Invariants and obaque types

[Dmitry A. Kazakov]

On Tue, 21 Jun 2011 23:50:04 +0200, Vinzent Hoefler wrote:

> Dmitry A. Kazakov wrote:
> 
>> On Tue, 21 Jun 2011 21:34:31 +0200, Vinzent Hoefler wrote:
>>
>>> Dmitry A. Kazakov wrote:
>>>
>>>> 'Valid is a hack around missing value initialization enforcement or some
>>>> kludges to support Unchecked_Conversion. It cannot justify anything because
>>>> 'Valid itself lacks credibility.
>>>
>>> How do you properly initialise and/or validate values coming from an untrusted
>>> external source (i.e. "bus")? Always using the full bit pattern and write the
>>> conversion routine yourself?
>>
>> Yes, I always do exactly this, at least in order to make my program
>> portable.
> 
> Hmm. Reading bus values in a particular endianes and being portable... ;)
> 
> Example:
> 
>      --  type used for clock source and retrigger mode selections
>      --  bits [4:2]
>      --  RTG  PSC_SEL EXT_CLK   clock mode
>      --    0        0       0   Internal, cpu clock, gated
>      --    0        0       1   External
>      --    0        1       0   Internal, prescaled, gated
>      --    0        1       1   N/A (same as 001)
>      --    1        0       0   Internal, cpu clock, retriggered
>      --    1        0       1   N/A (same as 001)
>      --    1        1       0   internal, prescaled, retriggered
>      --    1        1       1   N/A (same as 001)
>      type Clock_Source is (Internal_Gated,
>                            External,
>                            Prescaled_Gated,
>                            Internal_Retriggered,
>                            Prescaled_Retriggered);
> 
>      for Clock_Source use (Internal_Gated        => 2#000#,
>                            External              => 2#001#,
>                            Prescaled_Gated       => 2#010#,
>                            Internal_Retriggered  => 2#100#,
>                            Prescaled_Retriggered => 2#110#);
> 
>      for Clock_Source'Size use 3;
> 
> Would you actually do without the type representation here and start masking off the
> bits by hand again instead of using 'Valid, just in case of of those "N/A" values
> sneak in?

Yes. I always provide a low-level I/O package which defines operations for
getting objects from, say, an octet array and putting it back:

   procedure Get
             (  Data    : Octet_Array;
                Pointer : in out Integer; -- Advanced to the next octet
                Value   : out Clock_Source  -- May raise Data_Error
             );

I never use memory mapping of read data. Incoming data are parsed by a
sequence of calls to the corresponding Get operations.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Ada2012 Invariants and obaque types

[Dmitry A. Kazakov]

On Tue, 21 Jun 2011 23:18:49 +0200, Manuel Collado wrote:

> El 21/06/2011 20:53, Dmitry A. Kazakov escribi�:
>> On Tue, 21 Jun 2011 20:37:44 +0200, Yannick Duch�ne (Hibou57) wrote:
>>
>>> Le Tue, 21 Jun 2011 14:08:15 +0200, Dmitry A. Kazakov
>>> <mailbox@dmitry-kazakov.de>  a �crit:
>>>
>>>> On Tue, 21 Jun 2011 01:53:31 -0700 (PDT), Martin wrote:
>>>>
>>>>> package P1 is
>>>>>     type T1 is tagged private
>>>>>        with Invariant =>  Is_Valid (T1);
>>>>
>>>> Unrelated to Ada, but in theory, an invariant is a private implementation
>>>> dependent thing. An invariant is trivially true in all public views of
>>>> the object,
>>> I understand the point and had the same first feeling too.
>>
>> The first feeling is always the right one. (:-))
>>
>>> While that's OK
>>> in theory, in practice the user may wish methods to check for validity
>>> rules defined for a type.
>>
>> Validity is a misconception. In a properly typed language any value is
>> valid, that is the property of being typed. A value is invalid when the
>> type system was circumvented, which should never happen publicly.
> 
> Humm... What about an integral type whose set of valid values are the 
> prime numbers (upto some representation limit)?

Prime numbers (as a set) are not numbers (e.g. do not form an additive
group: if p1, p2 are primes, p1 + p2 is not necessarily prime.)

> Common practice is to define such type as Integer, Natural or Positive, 
> and write some validation function to check values at runtime.

To have a publicly integer type of only prime numbers would be a bad idea.

> Or do you mean that Ada is not a properly typed language?

Ada's typing is better than of any other language I know. Yes, it has
issues, especially with construction-destruction of tagged types, nobody is
perfect.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Ada2012 Invariants and obaque types

[Egil Høvik]

> Example:
> package P1 is
>    type T1 is tagged private
>       with Invariant => Is_Valid (T1);

I believe it's called Type_Invariant, not just Invariant.

 http://www.ada-auth.org/standards/12rm/html/RM-7-3-2.html#I3544

Re: Ada2012 Invariants and obaque types

[Martin]

On Jun 22, 11:39 am, Egil Høvik <egilho...@hotmail.com> wrote:
> > Example:
> > package P1 is
> >    type T1 is tagged private
> >       with Invariant => Is_Valid (T1);
>
> I believe it's called Type_Invariant, not just Invariant.
>
>  http://www.ada-auth.org/standards/12rm/html/RM-7-3-2.html#I3544

Sadly, that still didn't help:

package P1 is
   type T1 is tagged private
     with Type_Invariant => True;
private
   type Imp;
   type Imp_Ref is not null access Imp;
   type T1 is tagged
      record
         I : Imp_Ref;
      end record;
end P1;

Results in:
gnatmake -d -PH:\Ada\test_invarients\test_invarients.gpr p1.ads
gcc -c -g -g -gnatE -fstack-check -gnato -gnatf -fcallgraph-info=su,da
-gnat12 -I- -gnatA H:\Ada\test_invarients\src\p1.ads
p1.ads:5:04: type "Imp" is frozen at line 2 before its full
declaration
gnatmake: "H:\Ada\test_invarients\src\p1.ads" compilation error

[2011-06-22 14:53:53] process exited with status 4 (elapsed time:
16.29s)

Thanks anyway.

-- Martin
p.s. I got 'Invariant' from the AI...must now remember that AI's are
not always the 'latest-and-greatest'!

Re: Ada2012 Invariants and obaque types

[anon]

package P1 is

   type T1 is tagged private
      with Invariant => Is_Valid ( T1 ) ;

   function Create               return T1 ;
   function Is_Valid ( This : T1 ) return Boolean ;

private
   type Imp ; --  ???? Where is the completed type definition of "Imp"

              --  Another thing the syntax for Aspect Types may require
              --  that "Imp" be defined before T1, so "Imp" may be 
              --  required in this example to be public.

   type T1 is tagged record -- ???? You forgot the keyword "tagged" 
                       I : Imp ;
                     end record ;
end P1 ;


An Example of one that might work is from sem_ch13.ads

      package AspectVis is
        R_Size : constant Integer := 32;
   
        package Inner is

          type R is new Integer with
              Size => R_Size;

             F : R; -- freezes
             R_Size : constant Integer := 64;
             S : constant Integer := R'Size; -- 32 not 64
          end Inner;

       end AspectVis;

Check file Aspects.ads for a list of Aspects like "Invariant"


In <239a78ad-0937-4a7a-8163-231430fd5ffe@k27g2000yqn.googlegroups.com>, Martin <martin.dowie@btopenworld.com> writes:
>A fairly common Ada idiom is to define the full view of a private type
>using an incomplete declaration. Thus leaving the actual
>implementation to the package spec. Trying this out with the public
>view defined with an invariant lead to a compiler error - is this:
>
>a) expected?
>b) an unexpected consequence? or
>c) a compiler bug?
>
>Example:
>package P1 is
>   type T1 is tagged private
>      with Invariant => Is_Valid (T1);
>   function Create               return T1;
>   function Is_Valid (This : T1) return Boolean;
>private
>   type Imp;
>   type T1 is
>      record
>         I : Imp;
>      end record;
>end P1;
>
>gnatmake -ws -c -u -PH:\Ada\test_invariants\test_invariants.gpr p1.ads
>gcc -c -g -g -gnatE -gnatVn -gnato -fstack-check -gnat12 -gnatf -I- -
>gnatA H:\Ada\test_invariants\src\p1.ads
>p1.ads:11:04: type "Imp" is frozen at line 3 before its full
>declaration
>p1.ads:13:09: full declaration of private type "T1" defined at line 3
>must be a tagged type
>p1.ads:15:14: invalid use of type before its full declaration
>gnatmake: "H:\Ada\test_invariants\src\p1.ads" compilation error
>
>[2011-06-21 09:46:55] process exited with status 4 (elapsed time:
>00.26s)