Ada 2012 Constraints (WRT an Ada IR)

Ada 2012 Constraints (WRT an Ada IR)

[Shark8]

So, with Ada 2012 we gained some really nice possibilities with the way to express constraints, the downside is that there's now a fairly wide range of ways to express constraints on types. Obviously these differences must be accounted for, but the are functionally equivalent, for example:

Subtype P0 is Natural range Natural'Succ(Natural'First)..Natural'Last;
Subtype P1 is Integer range 1..Integer'Last;
Subtype P2 is Integer with Static_Predicate => P2 in 1..Integer'Last or else raise Constraint_Error;
Subtype P3 is Integer with
  Static_Predicate  => P3 in 1..Integer'Last,
  Predicate_Failure => raise Constraint_Error;

Now, these should be generally the same way of writing the same thing (ie "Positive") -- though I'm not completely certain that this is the case in terms of subtle semantics (am I missing something?) -- it certainly would be convenient if they were as then we could have an IR wherein the general form of a type-constraint is uniformly handled.

Comments? Insights?

Re: Ada 2012 Constraints (WRT an Ada IR)

[G.B.]

On 29.11.16 00:49, Shark8 wrote:
> it certainly would be convenient if they were as then we could have an IR wherein the general form of a type-constraint is uniformly handled.

The notes section of LRM 3.2.4 may be of interest here.

Also, by way of extending the range of perspectives, maybe the
added flexibility of predicates entails not only overlap but also
separate handling. For example, being a positive (counting)
number means being an integer greater than 0. So, conceptually,
there is just one condition, not two as in a subtype constraint.


    generic
       type I is range <>;
    package G is

       subtype P is I with
         Static_Predicate => P > 0;

    end G;


-- 
"HOTDOGS ARE NOT BOOKMARKS"
Springfield Elementary teaching staff

Re: Ada 2012 Constraints (WRT an Ada IR)

[Shark8]

On Tuesday, November 29, 2016 at 1:17:38 AM UTC-7, G.B. wrote:
> On 29.11.16 00:49, Shark8 wrote:
> > it certainly would be convenient if they were as then we could have an IR wherein the general form of a type-constraint is uniformly handled.
> 
> The notes section of LRM 3.2.4 may be of interest here.
> 
> Also, by way of extending the range of perspectives, maybe the
> added flexibility of predicates entails not only overlap but also
> separate handling. For example, being a positive (counting)
> number means being an integer greater than 0. So, conceptually,
> there is just one condition, not two as in a subtype constraint.
> 
> 
>     generic
>        type I is range <>;
>     package G is
> 
>        subtype P is I with
>          Static_Predicate => P > 0;
> 
>     end G;
> 
> 
> -- 
> "HOTDOGS ARE NOT BOOKMARKS"
> Springfield Elementary teaching staff

Perhaps, but thinking about an IR, it seems like it would be nice to use Ada's already implicit usage of sets more explicitly -- by which I mean things like CASE requiring every value in its type (i.e. the set of values in its range) -- things like the "A predicate specification does not cause a subtype to be considered constrained." has no impact on delineating the set of acceptable values. Example:

Type Serial_Number is new String
  with Dynamic_Predicate => (for all Ch of Serial_Number => Ch in '0'..'9';

The above has a constraint -- that of only holding digits -- but still is unconstrained. If we were doing a formal CS class we'd say something like "The type Serial_Number contains all strings that have only the decimal digits therein." (Or somesuch, I'm borrowing from my memories of the class on DFAs, NFAs, etc.)

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 2016-11-29 21:32, Shark8 wrote:

> The above has a constraint -- that of only holding digits -- but
> still  is unconstrained. If we were doing a formal CS class we'd say something
> like "The type Serial_Number contains all strings that have only the
> decimal digits therein."

You want convariance, that is a completely different beast. It is a new 
type with some operations overridden, e.g. the operation that yields a 
value of a discrete type for case statement. It is an implicit operation 
in Ada, yet it is an operation. It must be covariant, i.e. returning the 
new type rather than the old one for the case be satisfied with the new 
set of values. Same with already mentioned 'First, 'Last, 'Range. Or, 
for that matter, 'Succ and 'Pred if the new type has a non-contiguous 
values set, e.g. Odd_Number. You cannot get there by merely putting some 
predicate on the assignment operation (which Ada's predicates do). That 
model is too weak to express such things.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Shark8]

On Tuesday, November 29, 2016 at 1:44:43 PM UTC-7, Dmitry A. Kazakov wrote:
> On 2016-11-29 21:32, Shark8 wrote:
> 
> > The above has a constraint -- that of only holding digits -- but
> > still  is unconstrained. If we were doing a formal CS class we'd say something
> > like "The type Serial_Number contains all strings that have only the
> > decimal digits therein."
> 
> You want convariance, that is a completely different beast.

No, I really don't.
I'm not talking about Ada-syntax, I'm talking about how to map underlying ideas uniformly -- IOW, this topic is *NOT* about "how do I do _X_ in Ada?" but rather "How is Ada doing X best [uniformly] represented?".

> It is a new 
> type with some operations overridden, e.g. the operation that yields a 
> value of a discrete type for case statement. It is an implicit operation 
> in Ada, yet it is an operation. It must be covariant, i.e. returning the 
> new type rather than the old one for the case be satisfied with the new 
> set of values. Same with already mentioned 'First, 'Last, 'Range. Or, 
> for that matter, 'Succ and 'Pred if the new type has a non-contiguous 
> values set, e.g. Odd_Number. You cannot get there by merely putting some 
> predicate on the assignment operation (which Ada's predicates do). That 
> model is too weak to express such things.

This is not about defining a type in Ada, it's about abstracting the making of a type [in Ada] and how best to represent _that_.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 2016-11-29 21:51, Shark8 wrote:
> On Tuesday, November 29, 2016 at 1:44:43 PM UTC-7, Dmitry A. Kazakov wrote:
>> On 2016-11-29 21:32, Shark8 wrote:
>>
>>> The above has a constraint -- that of only holding digits -- but
>>> still  is unconstrained. If we were doing a formal CS class we'd say something
>>> like "The type Serial_Number contains all strings that have only the
>>> decimal digits therein."
>>
>> You want convariance, that is a completely different beast.
>
> No, I really don't.
> I'm not talking about Ada-syntax,

Yes you do, covariance vs. contravariance is semantics, not syntax.

>> It is a new
>> type with some operations overridden, e.g. the operation that yields a
>> value of a discrete type for case statement. It is an implicit operation
>> in Ada, yet it is an operation. It must be covariant, i.e. returning the
>> new type rather than the old one for the case be satisfied with the new
>> set of values. Same with already mentioned 'First, 'Last, 'Range. Or,
>> for that matter, 'Succ and 'Pred if the new type has a non-contiguous
>> values set, e.g. Odd_Number. You cannot get there by merely putting some
>> predicate on the assignment operation (which Ada's predicates do). That
>> model is too weak to express such things.
>
> This is not about defining a type in Ada, it's about abstracting the
> making of a type [in Ada] and how best to represent _that_.

What is abstracting making the type? In order to have a type you must 
define it = define the set of values, the set of operations, the 
semantics of the operations and provide an implementation of these 
(values representation, bodies of the operations)

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Shark8]

On Tuesday, November 29, 2016 at 2:06:21 PM UTC-7, Dmitry A. Kazakov wrote:
> On 2016-11-29 21:51, Shark8 wrote:
> > On Tuesday, November 29, 2016 at 1:44:43 PM UTC-7, Dmitry A. Kazakov wrote:
> >> On 2016-11-29 21:32, Shark8 wrote:
> >>
> >>> The above has a constraint -- that of only holding digits -- but
> >>> still  is unconstrained. If we were doing a formal CS class we'd say something
> >>> like "The type Serial_Number contains all strings that have only the
> >>> decimal digits therein."
> >>
> >> You want convariance, that is a completely different beast.
> >
> > No, I really don't.
> > I'm not talking about Ada-syntax,
> 
> Yes you do, covariance vs. contravariance is semantics, not syntax.

Maybe I'm misunderstanding.
I simply don't see how covariance vs. contravariance is at all germane to representing the definition of a type.

> >> It is a new
> >> type with some operations overridden, e.g. the operation that yields a
> >> value of a discrete type for case statement. It is an implicit operation
> >> in Ada, yet it is an operation. It must be covariant, i.e. returning the
> >> new type rather than the old one for the case be satisfied with the new
> >> set of values. Same with already mentioned 'First, 'Last, 'Range. Or,
> >> for that matter, 'Succ and 'Pred if the new type has a non-contiguous
> >> values set, e.g. Odd_Number. You cannot get there by merely putting some
> >> predicate on the assignment operation (which Ada's predicates do). That
> >> model is too weak to express such things.
> >
> > This is not about defining a type in Ada, it's about abstracting the
> > making of a type [in Ada] and how best to represent _that_.
> 
> What is abstracting making the type?

Perhaps I should have used the word "defining" or "representing" instead of "making".

> In order to have a type you must 
> define it = define the set of values, the set of operations, the 
> semantics of the operations and provide an implementation of these 
> (values representation, bodies of the operations)

Agreed, but restating the motivation of the question isn't often helpful for answering the question. -- Rather like if I were to wake at three in the morning, ask myself "what should I do until sunrise?" and answer with "In a few more hours, the sun will come up."... I mean, it's completely a true statement... but useless for answering the question of what to do until then.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 29/11/2016 23:59, Shark8 wrote:
> On Tuesday, November 29, 2016 at 2:06:21 PM UTC-7, Dmitry A. Kazakov wrote:
>> On 2016-11-29 21:51, Shark8 wrote:
>>> On Tuesday, November 29, 2016 at 1:44:43 PM UTC-7, Dmitry A. Kazakov wrote:
>>>> On 2016-11-29 21:32, Shark8 wrote:
>>>>
>>>>> The above has a constraint -- that of only holding digits -- but
>>>>> still  is unconstrained. If we were doing a formal CS class we'd say something
>>>>> like "The type Serial_Number contains all strings that have only the
>>>>> decimal digits therein."
>>>>
>>>> You want convariance, that is a completely different beast.
>>>
>>> No, I really don't.
>>> I'm not talking about Ada-syntax,
>>
>> Yes you do, covariance vs. contravariance is semantics, not syntax.
>
> Maybe I'm misunderstanding.
> I simply don't see how covariance vs. contravariance is at all
> germane  to representing the definition of a type.

It is relevant to the difference between Ada 83 style constrained types 
and constrained types introduced by predicates. Ada 83 constraints are 
more consistent because they took into account operations that must be 
covariant. E.g. adding to the list of examples:

    subtype Text is String (1..80);

That overrides 'First, 'Last, 'Range, 'Length and propagates the 
constraint to other types by promoting Text definite. None of this 
happens if you add a predicate because all operations are inherited 
as-is = contravariant.

>>>> It is a new
>>>> type with some operations overridden, e.g. the operation that yields a
>>>> value of a discrete type for case statement. It is an implicit operation
>>>> in Ada, yet it is an operation. It must be covariant, i.e. returning the
>>>> new type rather than the old one for the case be satisfied with the new
>>>> set of values. Same with already mentioned 'First, 'Last, 'Range. Or,
>>>> for that matter, 'Succ and 'Pred if the new type has a non-contiguous
>>>> values set, e.g. Odd_Number. You cannot get there by merely putting some
>>>> predicate on the assignment operation (which Ada's predicates do). That
>>>> model is too weak to express such things.
>>>
>>> This is not about defining a type in Ada, it's about abstracting the
>>> making of a type [in Ada] and how best to represent _that_.
>>
>> What is abstracting making the type?
>
> Perhaps I should have used the word "defining" or "representing" instead of "making".

So it *is* about "defining" now?

[I still do not understand what you meant.]

BTW, "representing" is certainly irrelevant because Ada is a statically 
typed language, hence, no types are ever represented in an Ada program 
[they are in the compiler and then the representations are thrown away].

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Shark8]

On Wednesday, November 30, 2016 at 1:31:17 AM UTC-7, Dmitry A. Kazakov wrote:
> 
> BTW, "representing" is certainly irrelevant because Ada is a statically 
> typed language, hence, no types are ever represented in an Ada program 
> [they are in the compiler and then the representations are thrown away].

Insofar as you can think of the Ada translator as a function of the form "Function Translate( Input : Source ) Return Executable_or_Library_Object;" that's absolutely true... it is untrue if you are considering an IR (intermediate representation).

Now we could decompose Translate along the phases of compilation as something perhaps like:

    Function Translate( Input : Source ) Return Executable_or_Library_Object is
    ( Code_Generator(Optimizer(Semantic_Analyzer((Parser((Lexer(Source))))))) );

and, further, if we were to instead do something like this:

    Function Translate( Input : Source ) Return Executable_or_Library_Object is
    Begin
      declare
        Semantic_Tree : constant Semantic_Analysis_Result := 
            Semantic_Analyzer(Parser(Lexer(Source)));
      begin
        Semantic_Analysis_Result'Write( IR_Stream, Semantic_Tree );
        Return Code_Generator(Optimizer(Semantic_Tree));
      end;
    End Translate;

The result would be that the compiler phases 'Lexer' through 'Semantic_Analyzer' have been "captured" into the stream IR_Stream, and it's guaranteed to be valid Ada (insofar as the correctness of the implementation of those phases are concerned) and, moreover, consistent w/ itself. We could then at a later date read that stream into a Semantic_Analysis_Result object and continue the compilation process (optimizing and code-gen). -- So, with that in mind it makes sense to consider the usefulness of making Semantic_Analysis_Result its own formal language: the Intermediate Representation.

Because of the properties listed above, every instance of Semantic_Analysis_Result is valid, consistent Ada -- by uniformly representing the underlying construct/concepts of the Ada-source we can severely cut down the complexity needed by the later stages of the compiler^1  (like, say, the DER encodings vs the BER encodings of ASN.1).

These properties are ideal for many applications -- one of the most practical to addressing some of the complaints/difficulties leveled at Ada (like a poor ecosystem) would be implementation of a CPAN-style repository... but far better -- for if we can, say, make this IR amiable to storage in a DB (with attendant consistency-checks) we can eliminate the storage of invalid Ada in said repository; furthermore, because we have all the semantic-information already we could build-in tools to allow correct dependency-storage, like Gnoga using Simple Components, but with proper versioning so that a breaking change in a new version's API could be detected and the older one with the required properties could be retrieved.

> On 29/11/2016 23:59, Shark8 wrote:
> > On Tuesday, November 29, 2016 at 2:06:21 PM UTC-7, Dmitry A. Kazakov wrote:
> >> On 2016-11-29 21:51, Shark8 wrote:
> >>> On Tuesday, November 29, 2016 at 1:44:43 PM UTC-7, Dmitry A. Kazakov wrote:
> >>>> On 2016-11-29 21:32, Shark8 wrote:
> >>>>
> >>>>> The above has a constraint -- that of only holding digits -- but
> >>>>> still  is unconstrained. If we were doing a formal CS class we'd say something
> >>>>> like "The type Serial_Number contains all strings that have only the
> >>>>> decimal digits therein."
> >>>>
> >>>> You want convariance, that is a completely different beast.
> >>>
> >>> No, I really don't.
> >>> I'm not talking about Ada-syntax,
> >>
> >> Yes you do, covariance vs. contravariance is semantics, not syntax.
> >
> > Maybe I'm misunderstanding.
> > I simply don't see how covariance vs. contravariance is at all
> > germane  to representing the definition of a type.
> 
> It is relevant to the difference between Ada 83 style constrained types 
> and constrained types introduced by predicates. Ada 83 constraints are 
> more consistent because they took into account operations that must be 
> covariant. E.g. adding to the list of examples:
> 
>     subtype Text is String (1..80);
> 
> That overrides 'First, 'Last, 'Range, 'Length and propagates the 
> constraint to other types by promoting Text definite. None of this 
> happens if you add a predicate because all operations are inherited 
> as-is = contravariant.

And shouldn't that (eg Predicated_Subtype'Pred or 'Last, etc) be caught by the semantic-analysis phase? If so, then it's entirely a moot point, isn't it?

But it certainly doesn't invalidate the concept of considering a type [and subtype] as the collection of a set of values and a set of operations on those values; for example:

    Type Nybble is range 0..15 with Size => 4;
    Subtype Prime_Nybble is Nybble with
      Static_Predicate => Prime_Nybble in 2|3|5|7|11|13;

could be represented as something which visualized-as-text would be:

   Nybble is
    Size            : Bits(4)
    Internal_Values : Set(0..15)
    Offset          : 0          -- So we could represent 1..16 w/ 4-bits
    Operations      : Arithmetic_ops & Scalar_Attributes

   
   Prime_Nybble modifying Nybble is
    Operations      : Operations without Scalar_Attributes

or somesuch.

> >>>> It is a new
> >>>> type with some operations overridden, e.g. the operation that yields a
> >>>> value of a discrete type for case statement. It is an implicit operation
> >>>> in Ada, yet it is an operation. It must be covariant, i.e. returning the
> >>>> new type rather than the old one for the case be satisfied with the new
> >>>> set of values. Same with already mentioned 'First, 'Last, 'Range. Or,
> >>>> for that matter, 'Succ and 'Pred if the new type has a non-contiguous
> >>>> values set, e.g. Odd_Number. You cannot get there by merely putting some
> >>>> predicate on the assignment operation (which Ada's predicates do). That
> >>>> model is too weak to express such things.
> >>>
> >>> This is not about defining a type in Ada, it's about abstracting the
> >>> making of a type [in Ada] and how best to represent _that_.
> >>
> >> What is abstracting making the type?
> >
> > Perhaps I should have used the word "defining" or "representing" instead of "making".
> 
> So it *is* about "defining" now?
> 
> [I still do not understand what you meant.]

In some sense, yes. -- By making the IR a mapping of Ada's concepts (such as defining a new type, or adding constraints thereon, [ie] the particular subject of this thread) in a general manner we can simplify some complexity of the Ada language insofar as [implementations of] tools and the back-end of compilers are concerned.

But as a whole, no -- the IR is about (a) abstracting the concepts that underlay Ada, and (b) storing/transforming an Ada text-source in terms of those concepts.

Does that clear things up?

--------------------------------------

^1 -- As an example the Standard says that a renaming of a function-call and a constant-object initialized to that function-call are equivalent; it is therefore quite sensible to have a single IR-construct to represent both... if exact source-text recovery is important then simply adding a discriminant/field of "Is_Renaming : Boolean" would be enough to track source recovery for that construct.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Niklas Holsti]

On 16-11-30 20:28 , Shark8 wrote:

> In some sense, yes. -- By making the IR a mapping of Ada's concepts
> (such as defining a new type, or adding constraints thereon, [ie] the
> particular subject of this thread) in a general manner we can
> simplify some complexity of the Ada language insofar as
> [implementations of] tools and the back-end of compilers are
> concerned.
>
> But as a whole, no -- the IR is about (a) abstracting the concepts
> that underlay Ada, and (b) storing/transforming an Ada text-source in
> terms of those concepts.

Are you trying to revive DIANA 
(https://en.wikipedia.org/wiki/DIANA_(intermediate_language)) or replace 
the IR's used by ASIS implementations 
(https://en.wikipedia.org/wiki/Ada_Semantic_Interface_Specification)?

Or are those too close to the source-code level for you, and your IR 
would go deeper to some simpler, more uniform "theory of all Ada"?

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .

Re: Ada 2012 Constraints (WRT an Ada IR)

[Shark8]

On Wednesday, November 30, 2016 at 1:26:52 PM UTC-7, Niklas Holsti wrote:
> On 16-11-30 20:28 , Shark8 wrote:
> 
> > In some sense, yes. -- By making the IR a mapping of Ada's concepts
> > (such as defining a new type, or adding constraints thereon, [ie] the
> > particular subject of this thread) in a general manner we can
> > simplify some complexity of the Ada language insofar as
> > [implementations of] tools and the back-end of compilers are
> > concerned.
> >
> > But as a whole, no -- the IR is about (a) abstracting the concepts
> > that underlay Ada, and (b) storing/transforming an Ada text-source in
> > terms of those concepts.
> 
> Are you trying to revive DIANA 
> (https://en.wikipedia.org/wiki/DIANA_(intermediate_language)) or replace 
> the IR's used by ASIS implementations 
> (https://en.wikipedia.org/wiki/Ada_Semantic_Interface_Specification)?
> 
> Or are those too close to the source-code level for you, and your IR 
> would go deeper to some simpler, more uniform "theory of all Ada"?

In some sense Yes to both DIANA and the "uniform theory of Ada".

It seems to me that ASIS ought to instead be a language about a language about meta-programming upon Ada -- something that would abstract things so that, say, Ada.[wide_[wide_]]strings could all share the same code/description/definition for their common operations, perhaps with the ability to also use "interfaces upon package-specs" and such.

That's different than the thrust I'm going for; IMO, DIANA was a solid idea, but hampered by the facts that (a) they chose to rate source-code retrieval/regeneration so highly; (b) it was defined as an ADT, but not particularly presented as one^1; (c) low adoption-rate of compilers and tools.^2

The first is entirely a design-decision, and understandable. My preference is more toward a "unified theory" though. -- The third I think could be addressed by having a "CPAN-like tool" that uses the IR, essentially relegating to generation of consumable source-text to a pretty-printer function/program.

I simply see a lot of advantage in a good "universal Ada theory" and DB-amiable intermediate representation.

-----------------

^1 -- DIANA Reference Manual (Rev 3) ch 1 intro paragraph 3 AND  1.1 [paragraph 2] vs the given DIANA package as an example in 4.6 of this PDF: http://www.dtic.mil/get-tr-doc/pdf?AD=ADA128232 rather than using a more generic approach. (Such as "type NODE(<>) is private;" w/ "function ARITY( N : NODE ) return NATURAL;")

^2 -- An interesting system that did use DIANA was the R-1000; and it seems to me that the DIANA adoption was hurt by the [Computer Science/Programming] industry's adoption of inferior systems. (e.g. C with preprocessor #include instead of an actual module-system.)

NOTE: There's a draft of revision 4 here: http://www.dtic.mil/cgi-bin/GetTRDoc?Location=U2&doc=GetTRDoc.pdf&AD=ADA272792

Re: Ada 2012 Constraints (WRT an Ada IR)

[Randy Brukardt]

"Shark8" <onewingedshark@gmail.com> wrote in message 
news:f3fbdf99-6ba6-4108-95dd-203a84a885ae@googlegroups.com...
On Wednesday, November 30, 2016 at 1:26:52 PM UTC-7, Niklas Holsti wrote:
...
>That's different than the thrust I'm going for; IMO, DIANA was a solid 
>idea,
>but hampered by the facts that (a) they chose to rate source-code
>retrieval/regeneration so highly; (b) it was defined as an ADT, but not
>particularly presented as one^1; (c) low adoption-rate of compilers and 
>tools.^2

DIANA was far too memory intensive for the benefits (not obvious) that it 
had. On many host machines of the time, there simply wasn't the memory to 
hold an entire decorated program in memory at once, and working around that 
would slow a compiler down a lot (one would have to make the structure 
disk-based, and disks were a lot slower back then, too). That's especially 
true for dealing with non-local units ("with").

Other, less memory intensive organizations provided faster compilation; and 
as I noted before, most of the interesting stuff happens on the low-level IR 
and its translation to machine code. So I'm not at all surprised that it 
didn't get used much. ASIS is really the second generation of DIANA, and its 
better - especially more abstract - but still a long way from what I'd 
consider ideal.

                                       Randy.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 2016-11-30 19:28, Shark8 wrote:

> So, with that in mind it makes sense to
> consider the usefulness of making Semantic_Analysis_Result its own
> formal language: the Intermediate Representation.

It would be difficult without making intermediate effectively target 
language, e.g. byte code. What you have in mind is some sort of data 
definition language [DDL] (operations' semantics stripped).

> These properties are ideal for many applications -- one of the most
> practical to addressing some of the complaints/difficulties leveled at
> Ada (like a poor ecosystem) would be implementation of a CPAN-style
> repository... but far better -- for if we can, say, make this IR amiable
> to storage in a DB (with attendant consistency-checks) we can eliminate
> the storage of invalid Ada in said repository; furthermore, because we
> have all the semantic-information already we could build-in tools to
> allow correct dependency-storage, like Gnoga using Simple Components,
> but with proper versioning so that a breaking change in a new version's
> API could be detected and the older one with the required properties
> could be retrieved.

Surely some level of introspection would be extremely helpful for 
distributed and persistency systems.

Versioning is a huge issue unresolved. I am afraid that type 
representation if not enough by far, because you need a lot of 
additional information to decide substitutablity, which is key to 
handling type versions.

>>>>> No, I really don't.
>>>>> I'm not talking about Ada-syntax,
>>>>
>>>> Yes you do, covariance vs. contravariance is semantics, not syntax.
>>>
>>> Maybe I'm misunderstanding.
>>> I simply don't see how covariance vs. contravariance is at all
>>> germane  to representing the definition of a type.
>>
>> It is relevant to the difference between Ada 83 style constrained types
>> and constrained types introduced by predicates. Ada 83 constraints are
>> more consistent because they took into account operations that must be
>> covariant. E.g. adding to the list of examples:
>>
>>     subtype Text is String (1..80);
>>
>> That overrides 'First, 'Last, 'Range, 'Length and propagates the
>> constraint to other types by promoting Text definite. None of this
>> happens if you add a predicate because all operations are inherited
>> as-is = contravariant.
>
> And shouldn't that (eg Predicated_Subtype'Pred or 'Last, etc) be
> caught by the semantic-analysis phase? If so, then it's entirely a moot
> point, isn't it?

The compiler cannot read minds. The information that the semantics of 
'Pred must be changed (and thus the operation becomes covariant) is 
nowhere to get. In the model of tagged types covariance is the default. 
In the model of added predicates it is contravariance the default. 
Ada-83 subtypes mix contravariance and covariance by hardwired rules.

> But it certainly doesn't invalidate the concept of considering a
> type  [and subtype] as the collection of a set of values and a set of
> operations on those values; for example:
>
>     Type Nybble is range 0..15 with Size => 4;
>     Subtype Prime_Nybble is Nybble with
>       Static_Predicate => Prime_Nybble in 2|3|5|7|11|13;
>
> could be represented as something which visualized-as-text would be:
>
>    Nybble is
>     Size            : Bits(4)
>     Internal_Values : Set(0..15)
>     Offset          : 0          -- So we could represent 1..16 w/ 4-bits
>     Operations      : Arithmetic_ops & Scalar_Attributes
>
>
>    Prime_Nybble modifying Nybble is
>     Operations      : Operations without Scalar_Attributes
>
> or somesuch.

You describe here DDL and leave all semantics of the operations aside.

Prime numbers do not have arithmetic because arithmetic operations on 
primes do not yield a prime. A semantically correct choice for "+" is 
either leave it contravariant:

    function "+" (Left, Right : Prime) return Universal_Integer;

or drop it

    function "+" (Left, Right : Prime) return Prime is abstract;

For attributes the choices are different. It depends on the properties 
of the mathematical structure the [sub]type is to model. There is no way 
the language could decide that. It can for built-in types, because they 
are built-in.

[...]

 > Does that clear things up?

Yes, you are under the delusion that DDL is a type system. It is not, 
DDL is weakly/untyped and as such is fundamentally incapable to describe 
Ada type system, not even in first approximation.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Shark8]

On Wednesday, November 30, 2016 at 1:45:04 PM UTC-7, Dmitry A. Kazakov wrote:
> On 2016-11-30 19:28, Shark8 wrote:
> 
> > So, with that in mind it makes sense to
> > consider the usefulness of making Semantic_Analysis_Result its own
> > formal language: the Intermediate Representation.
> 
> It would be difficult without making intermediate effectively target 
> language, e.g. byte code. What you have in mind is some sort of data 
> definition language [DDL] (operations' semantics stripped).

In the sense that a program *IS* data, it certainly is a DDL.

> > These properties are ideal for many applications -- one of the most
> > practical to addressing some of the complaints/difficulties leveled at
> > Ada (like a poor ecosystem) would be implementation of a CPAN-style
> > repository... but far better -- for if we can, say, make this IR amiable
> > to storage in a DB (with attendant consistency-checks) we can eliminate
> > the storage of invalid Ada in said repository; furthermore, because we
> > have all the semantic-information already we could build-in tools to
> > allow correct dependency-storage, like Gnoga using Simple Components,
> > but with proper versioning so that a breaking change in a new version's
> > API could be detected and the older one with the required properties
> > could be retrieved.
> 
> Surely some level of introspection would be extremely helpful for 
> distributed and persistency systems.

This is true, but I don't think that ought to be the concern of the IR. -- Insofar as a CPAN-like tool is concerned w/ the IR the major operations are merely STORE and RETRIEVE; other functionality such as, say, tracking licenses or searching/indexing stored data don't involve the IR... in fact, the only operations that would are listing the dependencies and the aforementioned version-control.

Maybe a tool [or language for] operating on the IR would be appropriate, perhaps using generic/template functionality to enable the expression of a "compressed" form so that (e.g.) [[Wide_[Wide_]]String could all share common portions and so that you could have something operating across the interfaces of packages, generic or not, meta-programming stuff... but that seems pretty far outside the scope of creating an IR.

> Versioning is a huge issue unresolved. I am afraid that type 
> representation if not enough by far, because you need a lot of 
> additional information to decide substitutablity, which is key to 
> handling type versions.

This is true, a full "bullet-proof system" would require extensive unit-tests tightly coupled with the particular program/library... perhaps more than are comfortable/practical for the hobbyist and small-business types.

Requiring that level of support would be nice, from an end-user point-of-view, and certainly has appeal to me given my admiration of provability and desires for "the industry" to embrace better practices... but that would require *MUCH* more work, and hamper ease-of-use [to the point of hampering usability itself, I suspect] on the program/library uploader.

As much as I like "completely correct", versioning at the CPAN-like-repository level should probably be restricted to the public interface. (Essentially the analog of "can it compile?" asked of a prolog program with the sets of modules involved, starting with the most-recent versions and backtracking until the solution is found.)

> >>>>> No, I really don't.
> >>>>> I'm not talking about Ada-syntax,
> >>>>
> >>>> Yes you do, covariance vs. contravariance is semantics, not syntax.
> >>>
> >>> Maybe I'm misunderstanding.
> >>> I simply don't see how covariance vs. contravariance is at all
> >>> germane  to representing the definition of a type.
> >>
> >> It is relevant to the difference between Ada 83 style constrained types
> >> and constrained types introduced by predicates. Ada 83 constraints are
> >> more consistent because they took into account operations that must be
> >> covariant. E.g. adding to the list of examples:
> >>
> >>     subtype Text is String (1..80);
> >>
> >> That overrides 'First, 'Last, 'Range, 'Length and propagates the
> >> constraint to other types by promoting Text definite. None of this
> >> happens if you add a predicate because all operations are inherited
> >> as-is = contravariant.
> >
> > And shouldn't that (eg Predicated_Subtype'Pred or 'Last, etc) be
> > caught by the semantic-analysis phase? If so, then it's entirely a moot
> > point, isn't it?
> 
> The compiler cannot read minds. The information that the semantics of 
> 'Pred must be changed (and thus the operation becomes covariant) is 
> nowhere to get.

Of course it is, it's in the set of operations available to the subtype... imagine extending the ability to add constraints to values, but with operations. It is, in a very general sense, the same thing -- the values a type has are a set, the operations a type has are a set: if we can exclude items from the value-set, why can't we exclude operations from the operation-set?

> In the model of tagged types covariance is the default. 
> In the model of added predicates it is contravariance the default. 
> Ada-83 subtypes mix contravariance and covariance by hardwired rules.

Then wouldn't a way to represent both be applicable to representing an Ada-83 type?

> > But it certainly doesn't invalidate the concept of considering a
> > type  [and subtype] as the collection of a set of values and a set of
> > operations on those values; for example:
> >
> >     Type Nybble is range 0..15 with Size => 4;
> >     Subtype Prime_Nybble is Nybble with
> >       Static_Predicate => Prime_Nybble in 2|3|5|7|11|13;
> >
> > could be represented as something which visualized-as-text would be:
> >
> >    Nybble is
> >     Size            : Bits(4)
> >     Internal_Values : Set(0..15)
> >     Offset          : 0          -- So we could represent 1..16 w/ 4-bits
> >     Operations      : Arithmetic_ops & Scalar_Attributes
> >
> >
> >    Prime_Nybble modifying Nybble is
> >     Operations      : Operations without Scalar_Attributes
> >
> > or somesuch.
> 
> You describe here DDL and leave all semantics of the operations aside.

Are the semantics needed when semantic validity has been ensured by the semantic-analysis phase? 

> Prime numbers do not have arithmetic because arithmetic operations on 
> primes do not yield a prime. A semantically correct choice for "+" is 
> either leave it contravariant:
> 
>     function "+" (Left, Right : Prime) return Universal_Integer;
> 
> or drop it
> 
>     function "+" (Left, Right : Prime) return Prime is abstract;

Or we could simply assume Ada's model w/ subtypes. (i.e. that "+"(Left, Right : Integer) Return Integer can be used for subtypes like Natural.)

The IR is to model Ada programs, not behaviors.

> For attributes the choices are different. It depends on the properties 
> of the mathematical structure the [sub]type is to model. There is no way 
> the language could decide that. It can for built-in types, because they 
> are built-in.
> 
> [...]
> 
>  > Does that clear things up?
> 
> Yes, you are under the delusion that DDL is a type system. It is not, 
> DDL is weakly/untyped and as such is fundamentally incapable to describe 
> Ada type system, not even in first approximation.

No, you misunderstand -- my thought is that the Ada type-system (insofar as defining types) can be modeled in a DDL. DIANA was just such a system, an instance of IDL, and could represent Ada's type-declarations. QED.

What I'm looking for is a more unified, universal way to do so that encompass constraints generally.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 01/12/2016 01:58, Shark8 wrote:
> On Wednesday, November 30, 2016 at 1:45:04 PM UTC-7, Dmitry A. Kazakov wrote:
>> On 2016-11-30 19:28, Shark8 wrote:
>>
>>> So, with that in mind it makes sense to
>>> consider the usefulness of making Semantic_Analysis_Result its own
>>> formal language: the Intermediate Representation.
>>
>> It would be difficult without making intermediate effectively target
>> language, e.g. byte code. What you have in mind is some sort of data
>> definition language [DDL] (operations' semantics stripped).
>
> In the sense that a program *IS* data, it certainly is a DDL.

No, that thing is called "code", not program. A program would include 
semantics of what the program is supposed to do in the problem space.

>> Versioning is a huge issue unresolved. I am afraid that type
>> representation if not enough by far, because you need a lot of
>> additional information to decide substitutablity, which is key to
>> handling type versions.
>
> This is true, a full "bullet-proof system" would require extensive
> unit-tests tightly coupled with the particular program/library...

You need no other language to run tests, as if they were of any use in 
this case.

> As much as I like "completely correct", versioning at the
> CPAN-like-repository level should probably be restricted to the public
> interface.

Surely so. The problem is that it is undecidable right now unless 
interfaces were limited to an assorted set of subprograms. Anything 
beyond complexity of C API stops working.

>>> And shouldn't that (eg Predicated_Subtype'Pred or 'Last, etc) be
>>> caught by the semantic-analysis phase? If so, then it's entirely a moot
>>> point, isn't it?
>>
>> The compiler cannot read minds. The information that the semantics of
>> 'Pred must be changed (and thus the operation becomes covariant) is
>> nowhere to get.
>
> Of course it is, it's in the set of operations available to the
> subtype... imagine extending the ability to add constraints to values,
> but with operations. It is, in a very general sense, the same thing --
> the values a type has are a set, the operations a type has are a set: if
> we can exclude items from the value-set, why can't we exclude operations
> from the operation-set?

Because that breaks other programs and operations. You cannot exclude 
"+" if there is "average" somewhere. The approach of putting arbitrary 
constraints does not work. It simply cannot work. In mathematics tasks 
involving constrained sets are way more difficult than unconstrained 
ones. E.g. looking for a maximum. Whole divisions are devoted to certain 
types of constraints. So it is beyond any how microscopic chance, you 
don't need even start.

>> In the model of tagged types covariance is the default.
>> In the model of added predicates it is contravariance the default.
>> Ada-83 subtypes mix contravariance and covariance by hardwired rules.
>
> Then wouldn't a way to represent both be applicable to representing an Ada-83 type?

Sure, but it is not a representation. The Ada type system certainly can 
be generalized and simplified. It was somehow discussed before, but 
there is no interest.

>> You describe here DDL and leave all semantics of the operations aside.
>
> Are the semantics needed when semantic validity has been ensured by
> the semantic-analysis phase?

All sematic analysis merely resolving names. The language is designed to 
have nominal typing, for very good reason...

>> Prime numbers do not have arithmetic because arithmetic operations on
>> primes do not yield a prime. A semantically correct choice for "+" is
>> either leave it contravariant:
>>
>>     function "+" (Left, Right : Prime) return Universal_Integer;
>>
>> or drop it
>>
>>     function "+" (Left, Right : Prime) return Prime is abstract;
>
> Or we could simply assume Ada's model w/ subtypes. (i.e. that
> "+"(Left, Right : Integer) Return Integer can be used for subtypes like
> Natural.)
>
> The IR is to model Ada programs, not behaviors.

In your model of creating types (types algebra) you must answer the 
question what happens with the operations of the original types. The 
point was there is no answer to this without knowing of the problem 
space semantics.

>> For attributes the choices are different. It depends on the properties
>> of the mathematical structure the [sub]type is to model. There is no way
>> the language could decide that. It can for built-in types, because they
>> are built-in.
>>
>> [...]
>>
>>  > Does that clear things up?
>>
>> Yes, you are under the delusion that DDL is a type system. It is not,
>> DDL is weakly/untyped and as such is fundamentally incapable to describe
>> Ada type system, not even in first approximation.
>
> No, you misunderstand -- my thought is that the Ada type-system
> (insofar as defining types) can be modeled in a DDL. DIANA was just such
> a system, an instance of IDL, and could represent Ada's
> type-declarations. QED.

Argument to Turing-completeness, huh? That applies to x86 assembly too.

> What I'm looking for is a more unified, universal way to do so that
> encompass constraints generally.

I don't think there is any need in that from the programming POV. We 
cannot handle existing types of constraints in meaningful way already. 
The problem is not expressing some arbitrary constraint, but in 
propagating the constraint to dependent types and other language 
constructs. That usage determines the type of constraint. Ada 83 
understood that very well. On the contrary, predicates is useless and 
dangerous mess.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:o1oohd$13nu$1@gioia.aioe.org...
...
>On the contrary, predicates is useless and dangerous mess.

I can understand "useless" (that's an opinion I don't share, but it's fair 
to have it), and I understand "mess" (the difference between static and 
dynamic predicates shouldn't have happened; I wanted set constraints instead 
of static predicates, which would have been more consistent), but I don't 
understand dangerous. Predicates (and all contracts, for that matter) are 
designed not the affect the semantics of a program at all if they are 
removed (or "Ignored"). With the solitary exception of static predicates and 
case and loops (see "mess" above). Ergo, there can be no danger from 
including a contract; indeed, if there *is* a danger, there is a bug in 
either the implementation or the language.

Moreover, predicates are inherited in much the same way that constraints 
(and null exclusions as well, those also aren't formally constraints); 
there's little difference in the way any of these work. So it's hard to see 
why constraints would be OK and predicates would be dangerous. (It's 
actually more the other way around, since suppressing a contraint can 
actually make a program dangerous; that's not possible for a predicate.)

                                           Randy.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 01/12/2016 23:26, Randy Brukardt wrote:
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
> news:o1oohd$13nu$1@gioia.aioe.org...
> ...
>> On the contrary, predicates is useless and dangerous mess.
>
> I can understand "useless" (that's an opinion I don't share, but it's fair
> to have it), and I understand "mess" (the difference between static and
> dynamic predicates shouldn't have happened; I wanted set constraints instead
> of static predicates, which would have been more consistent), but I don't
> understand dangerous. Predicates (and all contracts, for that matter) are
> designed not the affect the semantics of a program at all if they are
> removed (or "Ignored").

When the contract specifies some behavior, e.g. raising or not raising 
exceptions?

> Moreover, predicates are inherited in much the same way that constraints
> (and null exclusions as well, those also aren't formally constraints);

Inheritance by no means imply safety.

Unconditional substitutability requires strengthening constraints of the 
out-parameters and weakening constraints of the in-parameters. For 
in-out it is both weakening the pre- and strengthening post-conditions, 
i.e. always wrong unless proven otherwise...

If under "inheritance" you mean conjunction with the parent's predicate 
it is strengthening.

> there's little difference in the way any of these work. So it's hard to see
> why constraints would be OK and predicates would be dangerous. (It's
> actually more the other way around, since suppressing a contraint can
> actually make a program dangerous; that's not possible for a predicate.)

Selected constraints are OK, because they are known to do known things. 
Predicates are just arbitrary expressions the programmer sets without 
understanding all effects of his actions. There is no language support 
to eliminate undesired effects or to define in any form the behavior 
expected to be checked against one in effect.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:o1s71b$oi7$1@gioia.aioe.org...
> On 01/12/2016 23:26, Randy Brukardt wrote:
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>> news:o1oohd$13nu$1@gioia.aioe.org...
>> ...
>>> On the contrary, predicates is useless and dangerous mess.
>>
>> I can understand "useless" (that's an opinion I don't share, but it's 
>> fair
>> to have it), and I understand "mess" (the difference between static and
>> dynamic predicates shouldn't have happened; I wanted set constraints 
>> instead
>> of static predicates, which would have been more consistent), but I don't
>> understand dangerous. Predicates (and all contracts, for that matter) are
>> designed not the affect the semantics of a program at all if they are
>> removed (or "Ignored").
>
> When the contract specifies some behavior, e.g. raising or not raising 
> exceptions?

That's a bad contract. (Especially for predicates.)

Some of us (including me) wanted to have Ada require no side-effects in 
contracts, but we got bogged down in deciding precisely what is a 
side-effect and it ended up as an unimplementable implementation permission. 
Hopefully, Ada 202x will handle this better.

>> Moreover, predicates are inherited in much the same way that constraints
>> (and null exclusions as well, those also aren't formally constraints);
>
> Inheritance by no means imply safety.
>
> Unconditional substitutability requires strengthening constraints of the 
> out-parameters and weakening constraints of the in-parameters. For in-out 
> it is both weakening the pre- and strengthening post-conditions, i.e. 
> always wrong unless proven otherwise...
>
> If under "inheritance" you mean conjunction with the parent's predicate it 
> is strengthening.

Constraints work the same way. So why the difference??

>> there's little difference in the way any of these work. So it's hard to 
>> see
>> why constraints would be OK and predicates would be dangerous. (It's
>> actually more the other way around, since suppressing a contraint can
>> actually make a program dangerous; that's not possible for a predicate.)
>
> Selected constraints are OK, because they are known to do known things. 
> Predicates are just arbitrary expressions the programmer sets without 
> understanding all effects of his actions. There is no language support to 
> eliminate undesired effects or to define in any form the behavior expected 
> to be checked against one in effect.

I agree with the last statement (outside of static predicates, which are 
quite restricted expressions and thus can only do limited things), but that 
should change in the next version of Ada. At least I hope it does.

                          Randy.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 2016-12-02 20:15, Randy Brukardt wrote:

> Some of us (including me) wanted to have Ada require no side-effects in
> contracts, but we got bogged down in deciding precisely what is a
> side-effect and it ended up as an unimplementable implementation permission.
> Hopefully, Ada 202x will handle this better.

Well, but a contract that does not describe behavior is useless. The 
problem is not if contracts define but how they do. Raising 
Constraint_Error is too low-level to be useful.

>> If under "inheritance" you mean conjunction with the parent's predicate it
>> is strengthening.
>
> Constraints work the same way. So why the difference??

Constraints on discriminants work because there are few operations 
involved, especially because discriminants cannot be changed. 
Constraints on numeric types do different things to different operations 
they know about, that is why they work better.

IMO, predicates could work, but only as an implementation method (moved 
to private) in combination with exception contracts. I.e. instead of 
considering them contract, I would make them a tool to compose 
operation: take old body add [virtually] a prologue and epilogue raising 
exceptions. The contract stays. If it gets broken due to exception 
[statically checked] you must replace the body.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[G.B.]

On 02.12.16 17:21, Dmitry A. Kazakov wrote:
> Predicates are just arbitrary expressions the programmer sets without understanding all effects of his actions.

So are programs.

While I think I understand the desire for a fully proven
type centered, consistent, awesome Ada program and supporting
language, meanwhile a simple

   pragma Assert (Is_Sorted (S));  -- S a library level constant

has in effect created a desirable change in behavior of an
older program here. Even though the behavior so far had not
caused any concern, a bug was sure lurking.

The predicate Is_Sorted is reflecting formally what had been
a comment only in that program. Making it an executable
predicate has made me spot an error in this:

    To_Mapping ("abcdefghijklmnopqrstuvxyz",
                "ABCDEFGHIJKLMNOPQRSTUVXYZ");

After fixing, one change will be that the program will behave
more correctly, irrespective of the Assert's ignorable
operational effects.

  "I did not realize that the success of tests is that
    they test the programmer, not the program." -- Tony Hoare

It's programmers who write programs, improving their understanding
of a lot of thing that affects their programs, using assertions.

Now, do assertion distract from learning how to write correct
programs using types that manage to express them? And in such
a way that an Ada compiler can determine truth at compile time?

-- 
"HOTDOGS ARE NOT BOOKMARKS"
Springfield Elementary teaching staff

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 2016-12-02 20:50, G.B. wrote:
> On 02.12.16 17:21, Dmitry A. Kazakov wrote:
>> Predicates are just arbitrary expressions the programmer sets without
>> understanding all effects of his actions.
>
> So are programs.

When written in C?

> While I think I understand the desire for a fully proven
> type centered, consistent, awesome Ada program and supporting
> language, meanwhile a simple
>
>   pragma Assert (Is_Sorted (S));  -- S a library level constant
>
> has in effect created a desirable change in behavior of an
> older program here. Even though the behavior so far had not
> caused any concern, a bug was sure lurking.

That is exactly the point. You falsely assume that the effect of 
run-time assertion fault would be better than the effect of potential 
bug in any given context.

When swapping one bug for another you still have it, and as with all 
bugs, the effect is not to predict.

> It's programmers who write programs, improving their understanding
> of a lot of thing that affects their programs, using assertions.

and tracing and tests...

> Now, do assertion distract from learning how to write correct
> programs using types that manage to express them?

Yes they do. It has nothing to do with correct programs, as you change 
one bug for another.

> And in such
> a way that an Ada compiler can determine truth at compile time?

This is not how predicates work and has nothing to do with truth. The 
only truth about a program is whether it exposes predefined behavior.

The main objection to arbitrary predicates is that they expose an 
undefined, undecidable, unexpected, undesired behavior. It is all a 
decent software design technique is against.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[G.B.]

On 03.12.16 11:23, Dmitry A. Kazakov wrote:
> On 2016-12-02 20:50, G.B. wrote:
>> On 02.12.16 17:21, Dmitry A. Kazakov wrote:
>>> Predicates are just arbitrary expressions the programmer sets without
>>> understanding all effects of his actions.
>>
>> So are programs.
>
> When written in C?

No, Ada. The question that you didn't answer was about how all normal
Ada source texts can be known to express a fully proven program,
by omitting assertions and replacing them with something else.

Mind you, I don't think this would make sense either way: contracts
based design IMHO is
  (a) for testing,
  (b) for description (e.g., guides for programmers),
but not for expressing the solution. (This does not say anything
yet about part-of or turned-off etc.)


>>   pragma Assert (Is_Sorted (S));  -- S a library level constant

> You falsely assume that the effect of run-time assertion fault would be better than the effect of potential bug in any given context.

Please don't put assumptions into my context. There will be
no run-time assertions caused by this Assert. Guess why?

The joint assertion and build process have fixed a bug for sure.
It is proven to be gone. The bug was discovered by formalizing
an already existing informal predicate. The now formal predicate,
will be ignored at run-time. As before.


>> Now, do assertion distract from learning how to write correct
>> programs using types that manage to express them?
>
> Yes they do.

Maybe, but without knowing predicates, one will never know
what "correct" stands for.

Correct programs need the preparatory work of asserting, I think.

>> And in such
>> a way that an Ada compiler can determine truth at compile time?
>
> This is not how predicates work

So?

> and has nothing to do with truth.

Predicates, a.k.a. all Boolean expressions, are our only way
of making statements that can be true or not. Or so I have learned.

-- 
"HOTDOGS ARE NOT BOOKMARKS"
Springfield Elementary teaching staff

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 2016-12-03 15:02, G.B. wrote:
> On 03.12.16 11:23, Dmitry A. Kazakov wrote:
>> On 2016-12-02 20:50, G.B. wrote:
>>> On 02.12.16 17:21, Dmitry A. Kazakov wrote:
>>>> Predicates are just arbitrary expressions the programmer sets without
>>>> understanding all effects of his actions.
>>>
>>> So are programs.
>>
>> When written in C?
>
> No, Ada.

Ada programs are not written without understanding what they do, not 
usually.

> The question that you didn't answer was about how all normal
> Ada source texts can be known to express a fully proven program,
> by omitting assertions and replacing them with something else.

I was answering to your claim about how [Ada] programs are written.

>  There will be
> no run-time assertions caused by this Assert. Guess why?

No idea, it is irrelevant. The discussion was about predicates.

> Predicates, a.k.a. all Boolean expressions, are our only way
> of making statements that can be true or not. Or so I have learned.

But in this discussion predicates have the meaning defined in Ada RM. My 
point was about their usefulness for Ada programming.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Robert Eachus]

On Saturday, December 3, 2016 at 11:27:02 AM UTC-5, Dmitry A. Kazakov wrote:
>
> But in this discussion predicates have the meaning defined in Ada RM. My 
> point was about their usefulness for Ada programming.

I've been following this discussion with puzzlement.  Assertions can be wonderful tools when debugging (usually during unit test).  But the most  important feature of pragma Assert is that it can be turned off globally in production code.

If there are Booleans which do need to be checked at run time, for example when validating inputs, those checks often should have a tightly wrapped exception handler, and certainly should not use pragma Assert.

I would consider it a major bug to have a pragma Assert that could fail at run-time absent a hardware failure or some such. (Even though it would be turned off in production code.)

Re: Ada 2012 Constraints (WRT an Ada IR)

[Stefan.Lucks]

[-- Attachment #1: Type: text/plain, Size: 1735 bytes --]

On Sun, 4 Dec 2016, Robert Eachus wrote:

> If there are Booleans which do need to be checked at run time, for 
> example when validating inputs, those checks often should have a tightly 
> wrapped exception handler, and certainly should not use pragma Assert.

Agreed!

> I would consider it a major bug to have a pragma Assert that could fail 
> at run-time absent a hardware failure or some such. (Even though it 
> would be turned off in production code.)

I don't quite think so. A failed Assert (or a failed pre- or 
postcondition, which are essentially a nice way to put Asserts in 
specifications) *may* be checked even in the productin system. What is 
important is to always shut down when upon Assert-failure -- preferably 
after writing diagnostic information to wherever digagnostics goe.

On one hand, there are systems that must not shut down (maybe an autopilot 
at flight time). If that is the case, Assert-checking in production 
executables is plain wrong.

On the other hand, there are systems, where a malfunction is worse than no 
function (e.g., a secure router -- better no communication than allowing 
attackers to pass through the security perimeter). In such cases, it may
be wise do perform Assert-checking even in production executables.

In either case, it is always wrong to handle Assertion_Error and then 
tring to continue. Which may easily happen with sloppily written software 
using "when others" exception handlers, unfortunately.


--------  I  love  the  taste  of  Cryptanalysis  in  the morning!  --------
www.uni-weimar.de/de/medien/professuren/mediensicherheit/people/stefan-lucks
----Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universität Weimar, Germany----

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 05/12/2016 09:41, Stefan.Lucks@uni-weimar.de wrote:
> On Sun, 4 Dec 2016, Robert Eachus wrote:

>> I would consider it a major bug to have a pragma Assert that could
>> fail at run-time absent a hardware failure or some such. (Even though
>> it would be turned off in production code.)
>
> I don't quite think so. A failed Assert (or a failed pre- or
> postcondition, which are essentially a nice way to put Asserts in
> specifications) *may* be checked even in the productin system. What is
> important is to always shut down when upon Assert-failure -- preferably
> after writing diagnostic information to wherever digagnostics goe.

A run-time "failed" Assert is an if-statement evaluating false. There is 
nothing of failure there.

Things called in Ada pre- and post-conditions if evaluated during 
run-time are merely subprogram bodies booby-trapped with unanticipated 
exceptions. Bad thing.

> On one hand, there are systems that must not shut down (maybe an
> autopilot at flight time). If that is the case, Assert-checking in
> production executables is plain wrong.

It is plain wrong regardless. If assertion is a correctness statement it 
shall never be checked at run time. If assertion is an if-statement with 
exception raised upon one of the outcomes it must *always* be evaluated 
unless the condition proven static. It is either or, never both.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Simon Wright]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:

> On 05/12/2016 09:41, Stefan.Lucks@uni-weimar.de wrote:
>> On Sun, 4 Dec 2016, Robert Eachus wrote:
>
>>> I would consider it a major bug to have a pragma Assert that could
>>> fail at run-time absent a hardware failure or some such. (Even though
>>> it would be turned off in production code.)

Yes. Though it's really up to the system engineers to decide on system
behaviour in the presence of software failure.

>> I don't quite think so. A failed Assert (or a failed pre- or
>> postcondition, which are essentially a nice way to put Asserts in
>> specifications) *may* be checked even in the productin system. What is
>> important is to always shut down when upon Assert-failure -- preferably
>> after writing diagnostic information to wherever digagnostics goe.
[...]
> Things called in Ada pre- and post-conditions if evaluated during
> run-time are merely subprogram bodies booby-trapped with unanticipated
> exceptions. Bad thing.

Just as bad a thing as Constraint_Error.

To me, there's no practical difference, at any rate from a black box
point of view, between a language-defined exception and an assertion (or
condifion) failure; just a matter of who defines what is out of the
envelope for the program.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Shark8]

On Monday, December 5, 2016 at 4:09:42 AM UTC-7, Simon Wright wrote:
>
> [...]
> > Things called in Ada pre- and post-conditions if evaluated during
> > run-time are merely subprogram bodies booby-trapped with unanticipated
> > exceptions. Bad thing.
> 
> Just as bad a thing as Constraint_Error.
> 
> To me, there's no practical difference, at any rate from a black box
> point of view, between a language-defined exception and an assertion (or
> condifion) failure; just a matter of who defines what is out of the
> envelope for the program.


And now we come back full-circle to the topic of the thread:

    Subtype P0 is Integer range 1..Integer'Last;
    Subtype P3 is Integer with
      Static_Predicate  => P3 in 1..Integer'Last,
      Predicate_Failure => raise Constraint_Error; 

are conceptually the same thing (although in Ada they are implemented differently such that turning off assertions makes P3 not raise Constraint_Error).

Since these are conceptually the same, they should have similar representations in an IR, preferably the same representation with a flag/discriminant on the constraint indicating whether or not turning assertions off impacts the condition-check.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 2016-12-05 19:42, Shark8 wrote:

> And now we come back full-circle to the topic of the thread:
>
>     Subtype P0 is Integer range 1..Integer'Last;
>     Subtype P3 is Integer with
>       Static_Predicate  => P3 in 1..Integer'Last,
>       Predicate_Failure => raise Constraint_Error;
>
> are conceptually the same thing

What makes you think so?

> Since these are conceptually the same,

They are not, so long the programmer intentions are unclear. [They also 
behave differently for some operations].

P0 is numeric range constraint. It is a well defined mathematical 
concept the subtype models.

P1 is an arbitrary predicate supposedly expresses programmer's intention 
unstated.

P0 is a contract (contiguous numeric subset) and implementation (built-in)

P1 is an implementation and no contract.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Shark8]

On Monday, December 5, 2016 at 3:13:42 PM UTC-7, Dmitry A. Kazakov wrote:
> On 2016-12-05 19:42, Shark8 wrote:
> 
> > And now we come back full-circle to the topic of the thread:
> >
> >     Subtype P0 is Integer range 1..Integer'Last;
> >     Subtype P3 is Integer with
> >       Static_Predicate  => P3 in 1..Integer'Last,
> >       Predicate_Failure => raise Constraint_Error;
> >
> > are conceptually the same thing
> 
> What makes you think so?
> 
> > Since these are conceptually the same,
> 
> They are not, so long the programmer intentions are unclear. [They also 
> behave differently for some operations].
> 
> P0 is numeric range constraint. It is a well defined mathematical 
> concept the subtype models.
> 
> P1 is an arbitrary predicate supposedly expresses programmer's intention 
> unstated.
> 
> P0 is a contract (contiguous numeric subset) and implementation (built-in)
> 
> P1 is an implementation and no contract.
> 
> -- 
> Regards,
> Dmitry A. Kazakov
> http://www.dmitry-kazakov.de

That's funny --- there's no P1 in the post you replied to.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 2016-12-06 21:51, Shark8 wrote:

> That's funny --- there's no P1 in the post you replied to.

P1 = P3, sorry

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Shark8]

On Tuesday, December 6, 2016 at 2:07:07 PM UTC-7, Dmitry A. Kazakov wrote:
> 
> P1 = P3, sorry

It's ok, I was just giving you a hard time.

But something did occur to me in the interim:

One reason that an IR could be handy is as an execution model -- like how Intel's iAPX 432 was designed for Ada's feature-set -- having a generalized form for constraints/violations would mean that the the chip would only have to handle one kind of constraint-type instead of having to have specialized forms for P3 and P0.

Perhaps a construction like:

   -- Failure indicates which exception is used, Message indicates the
   -- "with String" message, and Asserted indicates if the assertion-
   -- form is being used (and might therefore be suppressed).
   Type Constraint_Node(
        Failure : Exception_Node := Constraint_Error;
        Message : AString        := Empty_String;
        Asserted : Boolean       := False
      ) is record
     Constraint : However_We_Represent_Constraints_Node;
   end record;

Heck, if we went with an OOP class-hierarchy of tagged items we could have a root Node type with inherited types for the classes of nodes (eg DIANA's classification for structural-, semantic-, lexical-, and code- attributes).

Re: Ada 2012 Constraints (WRT an Ada IR)

[Randy Brukardt]

"Shark8" <onewingedshark@gmail.com> wrote in message 
news:10e8cb52-1cbd-40ed-ba11-f474c2263ced@googlegroups.com...
>On Tuesday, December 6, 2016 at 2:07:07 PM UTC-7, Dmitry A. Kazakov wrote:
>>
>> P1 = P3, sorry
>
>It's ok, I was just giving you a hard time.
>
>But something did occur to me in the interim:
>
>One reason that an IR could be handy is as an execution model -- like how
>Intel's iAPX 432 was designed for Ada's feature-set -- having a generalized
>form for constraints/violations would mean that the the chip would only 
>have
>to handle one kind of constraint-type instead of having to have specialized
>forms for P3 and P0.

You seem to be assuming that it is practical to represent all kinds of 
predicates as some sort of set. That's definitely not true; one of the major 
reasons that you can't use divide or mod in a static predicate is the 
difficulty of representing the set. For instance, consider:

     subtype Even is new Natural with Dynamic_Predicate => Even mod 2 = 0;

If Natural is a 64 bit type, Even is a set of 2**63 items, no two are 
contiguous. The representation of that is going to be a problem. One could 
imagine some special case to deal with this particular case, but then there 
are many other possible predicates with this property.

Thus, your hypothetical IR would have to represent ranges as predicates, 
rather than as some sort of set. But that would make it hard to do 
operations on the IR (such as merging and check elimination).

                                     Randy.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Shark8]

On Tuesday, December 6, 2016 at 4:23:55 PM UTC-7, Randy Brukardt wrote:
> "Shark8" wrote in message 
> >
> >But something did occur to me in the interim:
> >
> >One reason that an IR could be handy is as an execution model -- like how
> >Intel's iAPX 432 was designed for Ada's feature-set -- having a generalized
> >form for constraints/violations would mean that the the chip would only 
> >have
> >to handle one kind of constraint-type instead of having to have specialized
> >forms for P3 and P0.
> 
> You seem to be assuming that it is practical to represent all kinds of 
> predicates as some sort of set. That's definitely not true; one of the major 
> reasons that you can't use divide or mod in a static predicate is the 
> difficulty of representing the set. For instance, consider:
> 
>      subtype Even is new Natural with Dynamic_Predicate => Even mod 2 = 0;
> 
> If Natural is a 64 bit type, Even is a set of 2**63 items, no two are 
> contiguous. The representation of that is going to be a problem. One could 
> imagine some special case to deal with this particular case, but then there 
> are many other possible predicates with this property.

Just because it's represented as a set doesn't mean that the set has to be represented as a bit-mask. (The obvious breaking example for that implementation here would be a string subtype constrained to contain only numeric characters.)

Haskell, IIRC, has no problem dealing with infinite sequences.

> Thus, your hypothetical IR would have to represent ranges as predicates, 
> rather than as some sort of set. But that would make it hard to do 
> operations on the IR (such as merging and check elimination).

Would it though? Don't we have tools (and entire programming languages) built around predicate-logic?

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dennis Lee Bieber]

On Tue, 6 Dec 2016 13:44:27 -0800 (PST), Shark8 <onewingedshark@gmail.com>
declaimed the following:

>
>One reason that an IR could be handy is as an execution model -- like how Intel's iAPX 432 was designed for Ada's feature-set -- having a generalized form for constraints/violations would mean that the the chip would only have to handle one kind of constraint-type instead of having to have specialized forms for P3 and P0.
>
	With modern processor silicon, the iAPX432 might almost run fast enough
to be usable.

	(Was a nice idea -- but the overhead of all the protection handling
bogged it down too much to get a foot-hold, or even a hand-hold <G>)
-- 
	Wulfraed                 Dennis Lee Bieber         AF6VN
    wlfraed@ix.netcom.com    HTTP://wlfraed.home.netcom.com/

Re: Ada 2012 Constraints (WRT an Ada IR)

[Niklas Holsti]

On 16-12-07 03:08 , Dennis Lee Bieber wrote:
> On Tue, 6 Dec 2016 13:44:27 -0800 (PST), Shark8 <onewingedshark@gmail.com>
> declaimed the following:
>
>>
>> One reason that an IR could be handy is as an execution model -- like how Intel's iAPX 432 was designed for Ada's feature-set -- having a generalized form for constraints/violations would mean that the the chip would only have to handle one kind of constraint-type instead of having to have specialized forms for P3 and P0.
>>
> 	With modern processor silicon, the iAPX432 might almost run fast enough
> to be usable.
>
> 	(Was a nice idea -- but the overhead of all the protection handling
> bogged it down too much to get a foot-hold, or even a hand-hold <G>)

There's a new processor architecture in development called "the Mill", 
which has a lot of protection built-in, but promises to be fast, at 
least in the computation-per-watt measure. See http://millcomputing.com/.

I don't know enough about the iAPX432 to compare the protection levels, 
but it seems that the Mill will catch a lot of the common protection 
violations and other undefined behaviour in C programs.

The Mill looks like a very good processor for Ada, for example all 
operations on integers have variants that wrap around, saturate, or 
trap, on over/underflow.

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dennis Lee Bieber]

On Wed, 7 Dec 2016 08:36:18 +0200, Niklas Holsti
<niklas.holsti@tidorum.invalid> declaimed the following:

>I don't know enough about the iAPX432 to compare the protection levels, 
>but it seems that the Mill will catch a lot of the common protection 
>violations and other undefined behaviour in C programs.
>
	I'd have to dig up the hard-cover book I'd bought in the 80s covering
the iAPX432. For the time period, the processor had to be split into two
separate chips -- something like one to do the security checks before
passing the fetched data/code to the execution unit; couldn't fit it all
into one piece of silicon.

	According to Wikipedia, it also relied upon the segment/offset type of
access -- with a segment table holding the access rights for the object...
Even code fetches were checked for access rights. Oh -- and the offset into
a segment? That was a /bit/ offset, not byte oriented -- meaning a segment
could be at most 8kBytes.

-- 
	Wulfraed                 Dennis Lee Bieber         AF6VN
    wlfraed@ix.netcom.com    HTTP://wlfraed.home.netcom.com/

Re: Ada 2012 Constraints (WRT an Ada IR)

[Brian Drummond]

On Wed, 07 Dec 2016 08:10:59 -0500, Dennis Lee Bieber wrote:

> On Wed, 7 Dec 2016 08:36:18 +0200, Niklas Holsti
> <niklas.holsti@tidorum.invalid> declaimed the following:
> 
>>I don't know enough about the iAPX432 to compare the protection levels,
>>but it seems that the Mill will catch a lot of the common protection
>>violations and other undefined behaviour in C programs.
>>
> 	I'd have to dig up the hard-cover book I'd bought in the 80s 
covering
> the iAPX432. For the time period, the processor had to be split into two
> separate chips -- something like one to do the security checks before
> passing the fetched data/code to the execution unit; couldn't fit it all
> into one piece of silicon.

Worse than that ... it had to push everything across a 16-bit bus between 
the two chips! Slightly bigger silicon and slightly more pins per 
package, and it would have been exponentially faster.

The Linn Rekursiv, only a decade later, was able to use 299 pin packages 
and a 128-bit wide microcode word coordinating up to 40 small functional 
units in parallel - had that been available to the 432's designers it 
would have been a lot faster.

-- Brian
 

Re: Ada 2012 Constraints (WRT an Ada IR)

[Shark8]

On Tuesday, December 6, 2016 at 11:36:22 PM UTC-7, Niklas Holsti wrote:
> On 16-12-07 03:08 , Dennis Lee Bieber wrote:
> > On Tue, 6 Dec 2016 13:44:27 -0800 (PST), Shark8
> > declaimed the following:
> >
> >>
> >> One reason that an IR could be handy is as an execution model -- like how Intel's iAPX 432 was designed for Ada's feature-set -- having a generalized form for constraints/violations would mean that the the chip would only have to handle one kind of constraint-type instead of having to have specialized forms for P3 and P0.
> >>
> > 	With modern processor silicon, the iAPX432 might almost run fast enough
> > to be usable.
> >
> > 	(Was a nice idea -- but the overhead of all the protection handling
> > bogged it down too much to get a foot-hold, or even a hand-hold <G>)
> 
> There's a new processor architecture in development called "the Mill", 
> which has a lot of protection built-in, but promises to be fast, at 
> least in the computation-per-watt measure. See http://millcomputing.com/.
> 
> I don't know enough about the iAPX432 to compare the protection levels, 
> but it seems that the Mill will catch a lot of the common protection 
> violations and other undefined behaviour in C programs.
> 
> The Mill looks like a very good processor for Ada, for example all 
> operations on integers have variants that wrap around, saturate, or 
> trap, on over/underflow.

The Mill does look interesting; I hope that Ada can find a home on it -- and that /would/ be a bit of an incentive to get another implementation up.

Re: Ada 2012 Constraints (WRT an Ada IR)

[G.B.]

On 07.12.16 02:08, Dennis Lee Bieber wrote:
> 	(Was a nice idea -- but the overhead of all the protection handling
> bogged it down too much to get a foot-hold, or even a hand-hold <G>)

The article https://en.wikipedia.org/wiki/Intel_iAPX_432 and
its siblings mention a few specifics, hinting at how not the
entire design might have failed. In no particular order:

-  bit-alignment, not word-alignment,
-  two-chip CGP speed limited by wiring on the board,
-  no (small?) caches, few registers
-  the compiler has routinely used slow general instructions,
    even when much faster alternatives would have worked
    (e.g., a call vs a jump, enter_environment for each
    use of a variable)
-  always call-by-value

But given this kind of support in hardware, is it unthinkable
to have special pieces of hardware that carry out assertion checking
specially? I.e., have the compiler translate the check into some
separate implementation running alongside the "real" program.
One that only reads memory, and that either stops that program or,
if so requested in the program using a dedicated exception handler,
activates the handler in the real program.

-- 
"HOTDOGS ARE NOT BOOKMARKS"
Springfield Elementary teaching staff

Re: Ada 2012 Constraints (WRT an Ada IR)

[G.B.]

On 07.12.16 11:04, G.B. wrote:

> -  two-chip CGP speed limited by wiring on the board,
	_ ? "CGP" = "GDP"

Re: Ada 2012 Constraints (WRT an Ada IR)

[J-P. Rosen]

Le 07/12/2016 à 11:04, G.B. a écrit :
> I.e., have the compiler translate the check into some
> separate implementation running alongside the "real" program.
> One that only reads memory, and that either stops that program or,
> if so requested in the program using a dedicated exception handler,
> activates the handler in the real program.
The Rational R1000 worked this way

-- 
J-P. Rosen
Adalog
2 rue du Docteur Lombard, 92441 Issy-les-Moulineaux CEDEX
Tel: +33 1 45 29 21 52, Fax: +33 1 45 29 25 00
http://www.adalog.fr

Re: Ada 2012 Constraints (WRT an Ada IR)

[G.B.]

On 07.12.16 11:51, J-P. Rosen wrote:

> The Rational R1000 worked this way

This machine is a well kept secret!
Or maybe I can't fill a search box properly.

-- 
"HOTDOGS ARE NOT BOOKMARKS"
Springfield Elementary teaching staff

Re: Ada 2012 Constraints (WRT an Ada IR)

[J-P. Rosen]

Le 08/12/2016 à 19:33, G.B. a écrit :
> On 07.12.16 11:51, J-P. Rosen wrote:
> 
>> The Rational R1000 worked this way
> 
> This machine is a well kept secret!
> Or maybe I can't fill a search box properly.
> 
???
https://en.wikipedia.org/wiki/Rational_R1000

(found by typing "rational r1000" to Google ;-) )

-- 
J-P. Rosen
Adalog
2 rue du Docteur Lombard, 92441 Issy-les-Moulineaux CEDEX
Tel: +33 1 45 29 21 52, Fax: +33 1 45 29 25 00
http://www.adalog.fr

Re: Ada 2012 Constraints (WRT an Ada IR)

[G.B.]

On 09.12.16 09:26, J-P. Rosen wrote:
> Le 08/12/2016 à 19:33, G.B. a écrit :
>> On 07.12.16 11:51, J-P. Rosen wrote:
>>
>>> The Rational R1000 worked this way
>>
>> This machine is a well kept secret!
>> Or maybe I can't fill a search box properly.
>>
> ???
> https://en.wikipedia.org/wiki/Rational_R1000
>

Yes, and it has dead links, but I had missed the whole
bookshelf and showroom in .dk... so thanks for putting
the article under my nose again. (It also states "because of
the classified nature of much Ada programming, these units
had been wiped"... triggers a knee-jerk reaction)

-- 
"HOTDOGS ARE NOT BOOKMARKS"
Springfield Elementary teaching staff

Re: Ada 2012 Constraints (WRT an Ada IR)

[Jacob Sparre Andersen]

G.B. <bauhaus@notmyhomepage.invalid> writes:

> (It also states "because of the classified nature of much Ada
> programming, these units had been wiped"... triggers a knee-jerk
> reaction)

The R1000 at the Danish computing museum was used by a defense
contractor, so it makes sense that they wiped the machine.  It would of
course have been nice, if they had kept an installation media for later
users of the machine, but how many of us think that far?

Greetings,

Jacob
-- 
Who guards the guardians?

Re: Ada 2012 Constraints (WRT an Ada IR)

[Shark8]

On Saturday, December 10, 2016 at 8:13:42 AM UTC-7, Jacob Sparre Andersen wrote:
> G.B.writes:
> 
> > (It also states "because of the classified nature of much Ada
> > programming, these units had been wiped"... triggers a knee-jerk
> > reaction)
> 
> The R1000 at the Danish computing museum was used by a defense
> contractor, so it makes sense that they wiped the machine.  It would of
> course have been nice, if they had kept an installation media for later
> users of the machine, but how many of us think that far?
> 
> Greetings,
> 
> Jacob
> -- 
> Who guards the guardians?

There's also some interesting and informative posts regarding the R-1000 on the following blog:
http://www.somethinkodd.com/oddthinking/category/geek/software-development/rat1000/

There's also this evaluation, which I've read (sometimes a bit dry, but interesting), here:
http://repository.cmu.edu/cgi/viewcontent.cgi?article=1141&context=sei

Here are the experimental transcripts, which I've not yet read:
http://www.dtic.mil/get-tr-doc/pdf?AD=ADA204634

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 2016-12-05 12:09, Simon Wright wrote:
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
>
>> On 05/12/2016 09:41, Stefan.Lucks@uni-weimar.de wrote:
>>> On Sun, 4 Dec 2016, Robert Eachus wrote:
>>
>>>> I would consider it a major bug to have a pragma Assert that could
>>>> fail at run-time absent a hardware failure or some such. (Even though
>>>> it would be turned off in production code.)
>
> Yes. Though it's really up to the system engineers to decide on system
> behaviour in the presence of software failure.

There is no such thing. Software failure per definition means the 
decided behavior didn't happen.

>>> I don't quite think so. A failed Assert (or a failed pre- or
>>> postcondition, which are essentially a nice way to put Asserts in
>>> specifications) *may* be checked even in the productin system. What is
>>> important is to always shut down when upon Assert-failure -- preferably
>>> after writing diagnostic information to wherever digagnostics goe.
> [...]
>> Things called in Ada pre- and post-conditions if evaluated during
>> run-time are merely subprogram bodies booby-trapped with unanticipated
>> exceptions. Bad thing.
>
> Just as bad a thing as Constraint_Error.

Not at all. Constraint_Error is defined and *desired* behavior. 
Exceptions from pre-/post-conditions is undefined behavior.

> To me, there's no practical difference, at any rate from a black box
> point of view, between a language-defined exception and an assertion (or
> condifion) failure; just a matter of who defines what is out of the
> envelope for the program.

The same behavior can be wrong or good depending on the specification. 
That is the practical difference.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:o24of4$1n05$1@gioia.aioe.org...
> On 2016-12-05 12:09, Simon Wright wrote:
...
>> Just as bad a thing as Constraint_Error.
>
> Not at all. Constraint_Error is defined and *desired* behavior. Exceptions 
> from pre-/post-conditions is undefined behavior.

Why?

Consider (part of) the procedure Delete in the Map container:

procedure Delete (Container : in out Map;
                  Position  : in out Cursor);
    -- If Position equals No_Element, then Constraint_Error is propagated.

As you say, this is defined and desired behavior.

Now, consider a better (IMHO) definition of this definition:

procedure Delete (Container : in out Map;
                  Position  : in out Cursor)
    with Pre => (if not Has_Element (Position) then raise Constraint_Error);

Here, instead of using an English comment to define this behavior, we've 
used an Ada precondition. So what's undefined about this? It's exactly the 
same semantics, and indeed my hope is that we update the RM to do this for 
all of the container routines in Ada 202x. (That makes the description of 
the primary function of the routine much easier to find, because it gets rid 
of all of the special conditions that start most of those descriptions. And 
it should make static analysis easier as well.)

IMHO, this is the only sensible use of a precondition (that is, it is some 
function of the parameters of the routine); it surely looks as defined as 
any if statement (which is what it would have to be written as in pre-Ada 
2012).

                                            Randy.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 07/12/2016 00:09, Randy Brukardt wrote:
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
> news:o24of4$1n05$1@gioia.aioe.org...
>> On 2016-12-05 12:09, Simon Wright wrote:
> ...
>>> Just as bad a thing as Constraint_Error.
>>
>> Not at all. Constraint_Error is defined and *desired* behavior. Exceptions
>> from pre-/post-conditions is undefined behavior.
>
> Why?
>
> Consider (part of) the procedure Delete in the Map container:
>
> procedure Delete (Container : in out Map;
>                   Position  : in out Cursor);
>     -- If Position equals No_Element, then Constraint_Error is propagated.
>
> As you say, this is defined and desired behavior.
>
> Now, consider a better (IMHO) definition of this definition:
>
> procedure Delete (Container : in out Map;
>                   Position  : in out Cursor)
>     with Pre => (if not Has_Element (Position) then raise Constraint_Error);

Sure, except that:

1. This is not a precondition. Delete still *can* be called when Pre is 
false. A true precondition here is that Container is Map. You cannot 
call Delete if Container is Long_Float.

2. This is a mixture of two independent things:

2.a an exception contract. Delete can raise Constraint_Error

2.b implementation. Delete must raise Constraint_Error at least when 
Has_Element (Position) is false and in who knows which other cases and 
it may raise Constraint_Error but not required to in some other 
undefined cases...

2.b is BAD because it brings implementation in. Unless you cannot prove 
that Constraint_Error is raised when Has_Element (Position) is false you 
may not contract it.

1 and 2 put together. If you can prove exceptions raised and not raised, 
then it can be a contract, but then it must be a *post-condition*, not a 
precondition (imaginary syntax):

procedure Delete (Container : in out Map;
                   Position  : in out Cursor)
    with Post => Constraint_Error when not Has_Element (Position);

This is a contract that burdens the callee's implementation. 
Precondition would be a contract that does all potential callers, not a 
very good thing to do, really.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:o28mpn$1doo$1@gioia.aioe.org...
> On 07/12/2016 00:09, Randy Brukardt wrote:
...
> 2. This is a mixture of two independent things:
>
> 2.a an exception contract. Delete can raise Constraint_Error

Which is being made explicit.

> 2.b implementation. Delete must raise Constraint_Error at least when 
> Has_Element (Position) is false and in who knows which other cases and it 
> may raise Constraint_Error but not required to in some other undefined 
> cases...

This happens because Ada doesn't (yet) have exception contracts (which apply 
to the body, not the precondition). If it did, it wouldn't include 
Constraint_Error (there being no other correct reason for raising 
Constraint_Error from delete).

I want Ada to have exception contracts, precisely for reusable code like the 
containers. But there is a lot of opposition, mainly because experience with 
them in other languages (notably Java) isn't good. I believe that is because 
exception contracts mainly help code that is used by many projects (and thus 
the contract cannot change in any way without notice), and not so much 
within a single project (when changing details of contracts might be more 
work than benefit). In any case, Ada exception contracts would have to be 
optional, and the usage problems seem to happen when they are manditory.

..
> Precondition would be a contract that does all potential callers, not a 
> very good thing to do, really.

Of course it is a good thing to do, the alternative is to let callers call 
with anything they like (within the type system), which is obvious nonsense. 
Not everything can be described as a type (object state, for instance).

                                 Randy.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 07/12/2016 23:37, Randy Brukardt wrote:

> Of course it is a good thing to do, the alternative is to let callers call
> with anything they like (within the type system), which is obvious nonsense.
> Not everything can be described as a type (object state, for instance).

Sure, but if you can you must. And in this case you can.

IMO you are still confusing contracts with behavior. They are different 
for exactly the reasons you mentioned, it is impossible to describe 
everything through contracts. The object state is the part of what 
*cannot* be fully contracted. It is the program behavior when you decide 
if you call "+" or "-" with given numeric objects. The contract is that 
you can call either.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Jacob Sparre Andersen]

Randy Brukardt wrote:

> procedure Delete (Container : in out Map;
>                   Position  : in out Cursor)
>     with Pre => (if not Has_Element (Position) then raise Constraint_Error);
>
> Here, instead of using an English comment to define this behavior, we've 
> used an Ada precondition. So what's undefined about this? It's exactly the 
> same semantics, and indeed my hope is that we update the RM to do this for 
> all of the container routines in Ada 202x.

Good plan!

Jacob
-- 
"Problems worthy of attack
 prove their worth by hitting back" -- Piet Hein

Re: Ada 2012 Constraints (WRT an Ada IR)

[Robert Eachus]

On Monday, December 5, 2016 at 6:09:42 AM UTC-5, Simon Wright wrote:

> >>> I would consider it a major bug to have a pragma Assert that could
> >>> fail at run-time absent a hardware failure or some such. (Even though
> >>> it would be turned off in production code.)
> 
> Yes. Though it's really up to the system engineers to decide on system
> behavior in the presence of software failure.

I picked this since it quotes me, rather than to pick on Simon.  The important thing that is getting missed in this discussion is that there are lots of uses for software.  I spent most of my career working on software for radars, planes, and missiles, where production software means the stuff that flies--or gets installed on a mountain with no software or system engineer in easy reach.

Sometimes that means that crashing the software (well a controlled crash that turns off the radar then restarts from the beginning) is the right safety feature.  But in an aircraft you leave it to the pilot to shut the engines down.  Yes, the engine might be about to tear itself into little pieces in five minutes--but this may be the only working engine that will get you to the airport.  I remember one incident where the mechanic didn't put the o-rings on the (new) oil plugs.  The pilot shut down the center engine for low oil pressure, and headed back to Palm Beach.  Then the other two engines had oil pressure warnings.  He ran them as long as possible, glided until just above the waves--and restarted the center engine.  Safe landing, barely.

But notice that the cockpit crew should never end up fighting the software warning system.  If it doesn't help, cut the warning.  Read about what happened to the Quantas A380, when an engine failed and cut some of the wires in the wing.  Telling the cockpit crew IN THE AIR that thus and so is not reporting every few seconds is NOT helpful. On the ground?  Fine, if it is a deadline issue. (Hmm.  Not clock deadlines, deadlines as in the plane won't fly.)

Why do I remember such incidents?  And why did I consider it important for me to know about them.  It all comes back to this issue.  Who are your diagnostics and exceptions expected to help?

To bring it back here, as far as I am concerned, the Assert feature makes it easier to insure that debug only code does not end up causing real accidents.  Exceptions often need to be handled in production code, but such exceptions should usually be wrapped closely in specific handlers.

Oh, and that handler around one line might as well say "when others."  There may be some code you don't see that could result in an unexpected exception, say "Device_Error" not "Use_Error" when reading from a file, but the behavior to deal with it is the same.

Re: Ada 2012 Constraints (WRT an Ada IR)

[G.B.]

On 05.12.16 09:58, Dmitry A. Kazakov wrote:
> It is either or, never both.

Allow me to consider this statement about assertions as part
of programming as done in general by programmers, assisted by
compilers and such:

  (for all It)[HALT("It is either or, never both.")]

We don't know in general, i.e. not before the fact. Where fact
is proof, or a run-time assertion failing to become true, or
an assumption like some kind of axiom such as "Like the LRM says".

But we can try to express what we think we know, regardless of
whether It is statically true or whether It should be tested
at run-time. At least we can do so until liability is extended
to include perfect functioning of each and every instruction
originating in statements of programs.

-- 
"HOTDOGS ARE NOT BOOKMARKS"
Springfield Elementary teaching staff

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 2016-12-05 20:22, G.B. wrote:
> On 05.12.16 09:58, Dmitry A. Kazakov wrote:
>> It is either or, never both.
>
> Allow me to consider this statement about assertions as part
> of programming as done in general by programmers

Mutual exclusion follows from definitions. Program and statements about 
the program are not same per definition.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:o23a8a$11e9$1@gioia.aioe.org...
...
> Things called in Ada pre- and post-conditions if evaluated during run-time 
> are merely subprogram bodies booby-trapped with unanticipated exceptions. 
> Bad thing.

Until you compare to the alternative, which is a subprogram body that gives 
the wrong answer without detection. As I said in another message, a visible 
bug is much better than an invisible bug.

You're certainly right that a dynamic contract doesn't eliminate any bugs, 
it just moves them from being invisible and/or mysterious to 
hit-one-over-the-head visible. It's the same reason that constraint checks 
are better than ignoring out-of-range array indexes; the same reason that 
exceptions are preferable to error codes when making library calls like 
opening files. I don't think I could live without those things, and dynamic 
contracts are just building on that strength.

                                         Randy.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 2016-12-05 23:12, Randy Brukardt wrote:
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
> news:o23a8a$11e9$1@gioia.aioe.org...
> ...
>> Things called in Ada pre- and post-conditions if evaluated during run-time
>> are merely subprogram bodies booby-trapped with unanticipated exceptions.
>> Bad thing.
>
> Until you compare to the alternative, which is a subprogram body that gives
> the wrong answer without detection. As I said in another message, a visible
> bug is much better than an invisible bug.

The alternative is a contract to raise exception. So there is no bug 
anymore, just well-defined behavior.

> You're certainly right that a dynamic contract doesn't eliminate any bugs,
> it just moves them from being invisible and/or mysterious to
> hit-one-over-the-head visible. It's the same reason that constraint checks
> are better than ignoring out-of-range array indexes; the same reason that
> exceptions are preferable to error codes when making library calls like
> opening files. I don't think I could live without those things, and dynamic
> contracts are just building on that strength.

I don't propose to live without them. I only insist on naming things 
what they are. When evaluated at run-time they are just implementations 
and must be named and handled accordingly. This has nothing to do with 
bugs or contracts.

Out of range index is not a bug. Similarly an index in the range is not 
automatically correct. Both are just program states for which the 
behavior is contracted to raise exception or access an element. Neither 
is right or wrong, so long programmer's intentions are not stated.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Simon Wright]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:

> On 2016-12-05 23:12, Randy Brukardt wrote:
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>> news:o23a8a$11e9$1@gioia.aioe.org...
>> ...
>>> Things called in Ada pre- and post-conditions if evaluated during
>>> run-time are merely subprogram bodies booby-trapped with
>>> unanticipated exceptions.  Bad thing.
>>
>> Until you compare to the alternative, which is a subprogram body that
>> gives the wrong answer without detection. As I said in another
>> message, a visible bug is much better than an invisible bug.
>
> The alternative is a contract to raise exception. So there is no bug
> anymore, just well-defined behavior.

I'm sorry, but this argument is ridiculous. If I write the code to
implement the required behaviour to the best of my ability, but get it
wrong, then the code will not have the required behaviour and will not
meet any contract that might be placed on it.

The equivalent of your contract would be

   with Post => Correct_Behaviour_Implemented
      or else Something_Terrible_Occurs;

which isn't worth saying.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 06/12/2016 10:29, Simon Wright wrote:
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
>
>> On 2016-12-05 23:12, Randy Brukardt wrote:
>>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>>> news:o23a8a$11e9$1@gioia.aioe.org...
>>> ...
>>>> Things called in Ada pre- and post-conditions if evaluated during
>>>> run-time are merely subprogram bodies booby-trapped with
>>>> unanticipated exceptions.  Bad thing.
>>>
>>> Until you compare to the alternative, which is a subprogram body that
>>> gives the wrong answer without detection. As I said in another
>>> message, a visible bug is much better than an invisible bug.
>>
>> The alternative is a contract to raise exception. So there is no bug
>> anymore, just well-defined behavior.
>
> I'm sorry, but this argument is ridiculous. If I write the code to
> implement the required behaviour to the best of my ability, but get it
> wrong, then the code will not have the required behaviour and will not
> meet any contract that might be placed on it.

It is called a bug. E.g. you implement addition and 2+2 yields 5.

> The equivalent of your contract would be
>
>    with Post => Correct_Behaviour_Implemented
>       or else Something_Terrible_Occurs;
>
> which isn't worth saying.

1. It is not my contract. My contract would be "in the range" or else 
exception. Which means the caller must be prepared to handle the 
exception. Your alternative is that the contract is "no exception" but 
the caller gets it anyway. That is clearly a violation. Either of the 
parties must be fixed before compiling. Now, if you cannot fix the 
callee to ensure the thing in the range, be honest to the caller => make 
exception into the contract.

2. You cannot specify all behavior through the contracts. Contracts are 
necessarily weaker than that. You can roughly outline some of the 
behavior in the contract, like: in the range vs. out of the range.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:o24phv$1ou6$1@gioia.aioe.org...
> On 2016-12-05 23:12, Randy Brukardt wrote:
...
>> Until you compare to the alternative, which is a subprogram body that 
>> gives
>> the wrong answer without detection. As I said in another message, a 
>> visible
>> bug is much better than an invisible bug.
>
> The alternative is a contract to raise exception. So there is no bug 
> anymore, just well-defined behavior.

All contracts raise an exception (I'm pretty sure Assertion_Error is an 
exception :-).

Moreover, most contracts (at least the ones I'd write) raise specific 
exceptions (not Assertion_Error). Indeed, this is a far better way to define 
something that raises an exception than an English comment. (Which is the 
only other alternative for the specification - and its the specification 
that matters, not the body.)

                       Randy.


                      Randy.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 07/12/2016 00:15, Randy Brukardt wrote:
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
> news:o24phv$1ou6$1@gioia.aioe.org...
>> On 2016-12-05 23:12, Randy Brukardt wrote:
> ...
>>> Until you compare to the alternative, which is a subprogram body that
>>> gives the wrong answer without detection. As I said in another message, a
>>> visible bug is much better than an invisible bug.
>>
>> The alternative is a contract to raise exception. So there is no bug
>> anymore, just well-defined behavior.
>
> All contracts raise an exception (I'm pretty sure Assertion_Error is an
> exception :-).

They don't raise, it was sloppy language. A correct statement would be 
that the contract requires the behavior to propagate exception.

In that sense, namely when you willing to include it into the contract, 
Assertion_Error is not a violation of, but a fulfillment of.

> Moreover, most contracts (at least the ones I'd write) raise specific
> exceptions (not Assertion_Error). Indeed, this is a far better way to define
> something that raises an exception than an English comment. (Which is the
> only other alternative for the specification - and its the specification
> that matters, not the body.)

As I said in another post it is a bad idea. The list exceptions, their 
names, must tell the reader when they are to propagate. You could 
specify the exact condition in a few very limited cases. In a real life 
scenario you cannot specify the Boolean expression guarding Disk_Error. 
Moreover, in most cases that would be an over-specification.

My point is that either you don't need the expression or else it 
must/can be statically provable and thus become a proper 
pre-/post-condition with no exceptions involved.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:o28non$1fn8$1@gioia.aioe.org...
> On 07/12/2016 00:15, Randy Brukardt wrote:
...
>> Moreover, most contracts (at least the ones I'd write) raise specific
>> exceptions (not Assertion_Error). Indeed, this is a far better way to 
>> define
>> something that raises an exception than an English comment. (Which is the
>> only other alternative for the specification - and its the specification
>> that matters, not the body.)
>
> As I said in another post it is a bad idea. The list exceptions, their 
> names, must tell the reader when they are to propagate. You could specify 
> the exact condition in a few very limited cases. In a real life scenario 
> you cannot specify the Boolean expression guarding Disk_Error. Moreover, 
> in most cases that would be an over-specification.

I never meant the above to be exclusive. Sometimes, as you say, an exception 
is raised by something external to the Ada program, and that is probably 
besst described in English. I was just talking about exceptions that depend 
only on the parameter values.

> My point is that either you don't need the expression or else it must/can 
> be statically provable and thus become a proper pre-/post-condition with 
> no exceptions involved.

Not everything can be statically proven (think Unchecked_Conversion), and a 
lot of stuff can only be proven in a full-program scenario, so I'm dubious 
of the above in any case. But even if that turns out to be possible years 
from now, I'm more interested in what I can do today -- especially if it is 
likely to be helpful to present (i.e. Codepeer) and future provers. A 
dynamic check that can be proven (or better proven and eliminated by the 
compiler) helps more than specifications with no machine-processable 
description.

                              Randy.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 07/12/2016 23:26, Randy Brukardt wrote:
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
> news:o28non$1fn8$1@gioia.aioe.org...
>> On 07/12/2016 00:15, Randy Brukardt wrote:
> ...
>>> Moreover, most contracts (at least the ones I'd write) raise specific
>>> exceptions (not Assertion_Error). Indeed, this is a far better way to
>>> define
>>> something that raises an exception than an English comment. (Which is the
>>> only other alternative for the specification - and its the specification
>>> that matters, not the body.)
>>
>> As I said in another post it is a bad idea. The list exceptions, their
>> names, must tell the reader when they are to propagate. You could specify
>> the exact condition in a few very limited cases. In a real life scenario
>> you cannot specify the Boolean expression guarding Disk_Error. Moreover,
>> in most cases that would be an over-specification.
>
> I never meant the above to be exclusive. Sometimes, as you say, an exception
> is raised by something external to the Ada program, and that is probably
> besst described in English. I was just talking about exceptions that depend
> only on the parameter values.

That does not change much. In most cases you still cannot do that 
without having the expression as complex as the body itself. Instead of 
one implementation you have two and thus you double the opportunity for 
making an error.

>> My point is that either you don't need the expression or else it must/can
>> be statically provable and thus become a proper pre-/post-condition with
>> no exceptions involved.
>
> Not everything can be statically proven (think Unchecked_Conversion), and a
> lot of stuff can only be proven in a full-program scenario, so I'm dubious
> of the above in any case. But even if that turns out to be possible years
> from now, I'm more interested in what I can do today -- especially if it is
> likely to be helpful to present (i.e. Codepeer) and future provers.

Right

> A
> dynamic check that can be proven (or better proven and eliminated by the
> compiler) helps more than specifications with no machine-processable
> description.

Wrong. The proper way to do this is elevate the check into the behavior 
and contract an exception. Later, when proofs are mature, client could 
prove absence of the exception. Nothing lost, everybody is happy.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[G.B.]

On 08.12.16 09:57, Dmitry A. Kazakov wrote:
> The proper way to do this is elevate the check into the behavior and contract an exception.

What will these two parts look like in the example,
bothrelating to "+", and to Plus?

procedure Plus is
    Y : Standard.Integer := Standard.Integer'Last;
begin
    Y := Y + 1;
end Plus;


-- 
"HOTDOGS ARE NOT BOOKMARKS"
Springfield Elementary teaching staff

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 08/12/2016 10:42, G.B. wrote:
> On 08.12.16 09:57, Dmitry A. Kazakov wrote:
>> The proper way to do this is elevate the check into the behavior and
>> contract an exception.
>
> What will these two parts look like in the example,
> bothrelating to "+", and to Plus?
>
> procedure Plus is
>    Y : Standard.Integer := Standard.Integer'Last;
> begin
>    Y := Y + 1;
> end Plus;

The contract of Plus is can [or must] raise Constraint_Error.

If the client will prove absence of Constraint_Error it must handle that 
anytime Plus is called.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[G.B.]

On 08.12.16 11:03, Dmitry A. Kazakov wrote:
>> What will these two parts look like in the example,
>> bothrelating to "+", and to Plus?
>>
>> procedure Plus is
>>    Y : Standard.Integer := Standard.Integer'Last;
>> begin
>>    Y := Y + 1;
>> end Plus;
>
> The contract of Plus is can [or must] raise Constraint_Error.
>
> If the client will prove absence of Constraint_Error it must handle that anytime Plus is called.
>

So, the following function will also just announce that
it can raise Constraint_Error?

function Plus_Too (A, B: Standard.Integer)
                   return Standard.Integer is
begin
    return A + B;
end Plus_Too;


-- 
"HOTDOGS ARE NOT BOOKMARKS"
Springfield Elementary teaching staff

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 08/12/2016 19:35, G.B. wrote:
> On 08.12.16 11:03, Dmitry A. Kazakov wrote:
>>> What will these two parts look like in the example,
>>> bothrelating to "+", and to Plus?
>>>
>>> procedure Plus is
>>>    Y : Standard.Integer := Standard.Integer'Last;
>>> begin
>>>    Y := Y + 1;
>>> end Plus;
>>
>> The contract of Plus is can [or must] raise Constraint_Error.
>>
>> If the client will prove absence of Constraint_Error it must handle
>> that anytime Plus is called.
>
> So, the following function will also just announce that
> it can raise Constraint_Error?
>
> function Plus_Too (A, B: Standard.Integer)
>                   return Standard.Integer is
> begin
>    return A + B;
> end Plus_Too;

At least. Contracts have different precision of the post-condition:

1.    Constraint_Error
    or none

2.    Constraint_Error when combination of argument values
    or none

3.    Constraint_Error when combination of argument values
    or 0 when combination of argument values
    or 1 when combination of argument values
    ...

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[G.B.]

On 09/12/2016 10:38, Dmitry A. Kazakov wrote:
> On 08/12/2016 19:35, G.B. wrote:
>> So, the following function will also just announce that
>> it can raise Constraint_Error?
>>
>> function Plus_Too (A, B: Standard.Integer)
>>                   return Standard.Integer is
>> begin
>>    return A + B;
>> end Plus_Too;
>
> At least. Contracts have different precision of the post-condition:
>
> 1.    Constraint_Error
>    or none
>
> 2.    Constraint_Error when combination of argument values
>    or none
>
> 3.    Constraint_Error when combination of argument values
>    or 0 when combination of argument values
>    or 1 when combination of argument values
>    ...

So, what is it, and (not?) elevated to implementation in this case
of Plus_Too?

McJones and Stepanov show an example which, I think, is related[1,2].
Note the precondition.

T remainder(T a, T b)
{
    // precondition a ≥ b > 0
    if (a - b >= b) {
       a = remainder(a, b + b);
       if (a < b) return a;
    }
    return a - b;
}

"... requires thinking."

They move towards Correctness, introducing, IIUC, a (finite) semi-group
of integers with both a 1 and Archimedes' axiom, < total, ... T a QuotientType
(I won't guess what the latter is, but will guess that some here might know that).

And, a precondition is stated as a comment, but the caller doesn't know it
unless he or she studies the body! Not the specification.
Granted, the programming language they use is a small language made for a book,
and the precondition is given on the first line. But if the language
were based on Ada, shouldn't it become a Pre aspect, so that the caller
knows what to do about a and b and the implementation of `remainder` can
assume it's been done?

    function Remainder (A, B : T) return T
       with Pre => A >= B and B > 0, ...;


Taken from near 28:20 in any of
  [1]: https://itunes.apple.com/de/podcast/3.-elements-programming-november/id414065199
  [2]: https://www.youtube.com/watch?v=Ih9gpJga4Vc

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 2016-12-11 12:21, G.B. wrote:
> On 09/12/2016 10:38, Dmitry A. Kazakov wrote:
>> On 08/12/2016 19:35, G.B. wrote:
>>> So, the following function will also just announce that
>>> it can raise Constraint_Error?
>>>
>>> function Plus_Too (A, B: Standard.Integer)
>>>                   return Standard.Integer is
>>> begin
>>>    return A + B;
>>> end Plus_Too;
>>
>> At least. Contracts have different precision of the post-condition:
>>
>> 1.    Constraint_Error
>>    or none
>>
>> 2.    Constraint_Error when combination of argument values
>>    or none
>>
>> 3.    Constraint_Error when combination of argument values
>>    or 0 when combination of argument values
>>    or 1 when combination of argument values
>>    ...
>
> So, what is it, and (not?) elevated to implementation in this case
> of Plus_Too?

?

> McJones and Stepanov show an example which, I think, is related[1,2].
> Note the precondition.

It is not.

> T remainder(T a, T b)
> {
>    // precondition a ≥ b > 0
>    if (a - b >= b) {
>       a = remainder(a, b + b);
>       if (a < b) return a;
>    }
>    return a - b;
> }
>
> "... requires thinking."
>
> They move towards Correctness, introducing, IIUC, a (finite) semi-group
> of integers with both a 1 and Archimedes' axiom, < total, ... T a
> QuotientType
> (I won't guess what the latter is, but will guess that some here might
> know that).
>
> And, a precondition is stated as a comment, but the caller doesn't know it
> unless he or she studies the body! Not the specification.
> Granted, the programming language they use is a small language made for
> a book, and the precondition is given on the first line. But if the language
> were based on Ada, shouldn't it become a Pre aspect,
>
>    function Remainder (A, B : T) return T
>       with Pre => A >= B and B > 0, ...;

To be a proper precondition it must be SPARK, not Ada.

An expression evaluated in the program is never a precondition. Pre-, 
post-, invariants are expressions evaluated by the *prover*. They are in 
the language of *prover*, they are *not* statements of the object language.

 > so that the caller
 > knows what to do about a and b and the implementation of `remainder`
 > can assume it's been done?

That does not translate to me into anything.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[G.B.]

On 11/12/2016 13:28, Dmitry A. Kazakov wrote:
>> so that the caller
>> knows what to do about a and b and the implementation of `remainder`
>> can assume it's been done?
>
> That does not translate to me into anything.

Seeing

     function X (A, B: T) return T;

I can write

      Y (X (A => any of T, B => any of T));

Seeing

     function X (A, B: T) return T
       with Pre => A > B;

I must first establish A > B before calling X,
because "Pre" tells me so.

Me.

Me, the programmer who plans a call of X.

Me, who is meant to respect the law, i.e., the contract.

CLU uses "requires", Eiffel uses "require" for Pre,
perhaps preventing a misunderstanding:
Pre only happens to be descriptive in proven programs.
Pre is really meant for programmers unconditionally.
Pre produces a maximally informed start for programming.


How much should a function declaration tell a programmer about
the relation between parameters A and B in the following? Just:
True (nothing), but be prepared for Constraint_Error to be
raised for reasons that we don't tell you?

function Plus_Too (A, B: Standard.Integer)
                   return Standard.Integer is
begin
    return A + B;
end Plus_Too;

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 2016-12-11 14:31, G.B. wrote:
> On 11/12/2016 13:28, Dmitry A. Kazakov wrote:
>>> so that the caller
>>> knows what to do about a and b and the implementation of `remainder`
>>> can assume it's been done?
>>
>> That does not translate to me into anything.
>
> Seeing
>
>     function X (A, B: T) return T;
>
> I can write
>
>      Y (X (A => any of T, B => any of T));
>
> Seeing
>
>     function X (A, B: T) return T
>       with Pre => A > B;
>
> I must first establish A > B before calling X,
> because "Pre" tells me so.

I still do not understand you question about caller "doing things" with 
parameters. Caller passes parameters that's all.

> How much should a function declaration tell a programmer about
> the relation between parameters A and B in the following?

Remainder is not a relation. Relation is a Boolean-valued function.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[G.B.]

On 11/12/2016 16:40, Dmitry A. Kazakov wrote:
> On 2016-12-11 14:31, G.B. wrote:

>> Seeing
>>
>>     function X (A, B: T) return T
>>       with Pre => A > B;
>>
>> I must first establish A > B before calling X,
>> because "Pre" tells me so.
>
> I still do not understand you question about caller "doing things" with parameters. Caller passes parameters that's all.


   If Algorithm_Establishing_A_Gt_B then
      Y (X (A, B));
   else
      --  proverbial "This shouldn't happen!"
      raise Program_Error;
   end if;


I.e., the programmer writing Y (X (A, B)) has ensured that
the assumption expressed as X'Pre is actually true before
calling X.

>> How much should a function declaration tell a programmer about
>> the relation between parameters A and B in the following?
>
> Remainder is not a relation. Relation is a Boolean-valued function.

Given parameters A, B : T and

    Pre => A > B

the ">" is the relation, ((A, B) ∈ ">")  ≣  (A > B).

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 11/12/2016 21:51, G.B. wrote:
> On 11/12/2016 16:40, Dmitry A. Kazakov wrote:
>> On 2016-12-11 14:31, G.B. wrote:
>
>>> Seeing
>>>
>>>     function X (A, B: T) return T
>>>       with Pre => A > B;
>>>
>>> I must first establish A > B before calling X,
>>> because "Pre" tells me so.
>>
>> I still do not understand you question about caller "doing things"
>> with parameters. Caller passes parameters that's all.
>
>   If Algorithm_Establishing_A_Gt_B then
>      Y (X (A, B));
>   else
>      --  proverbial "This shouldn't happen!"
>      raise Program_Error;
>   end if;
>
>
> I.e., the programmer writing Y (X (A, B)) has ensured that
> the assumption expressed as X'Pre is actually true before
> calling X.

So what? Programmers program programs, and how is that related to 
contracts etc?

>>> How much should a function declaration tell a programmer about
>>> the relation between parameters A and B in the following?
>>
>> Remainder is not a relation. Relation is a Boolean-valued function.
>
> Given parameters A, B : T and
>
>    Pre => A > B
>
> the ">" is the relation, ((A, B) ∈ ">")  ≣  (A > B).

Right, ">" is a relation, Remainder is not. And the point was?

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[G.B.]

On 12/12/2016 09:27, Dmitry A. Kazakov wrote:

>> I.e., the programmer writing Y (X (A, B)) has ensured that
>> the assumption expressed as X'Pre is actually true before
>> calling X.
>
> So what? Programmers program programs, and how is that related to contracts etc?

Informing is contracts' primary purpose, informing about contractual
obligations in particular. For X, True means void IMHO. As in
"Warranty void if called with unsuitable parameters".

>>>> How much should a function declaration tell a programmer about
>>>> the relation between parameters A and B in the following?
>>>
>>> Remainder is not a relation. Relation is a Boolean-valued function.
>>
>> Given parameters A, B : T and
>>
>>    Pre => A > B
>>
>> the ">" is the relation, ((A, B) ∈ ">")  ≣  (A > B).
>
> Right, ">" is a relation, Remainder is not. And the point was?

The point was:
How much should the declaration of function Remainder tell a programmer
about the relation between parameters A and B?
My answer:
The declaration should include that they must be related by A > B.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 2016-12-12 16:31, G.B. wrote:
> On 12/12/2016 09:27, Dmitry A. Kazakov wrote:
>
>>> I.e., the programmer writing Y (X (A, B)) has ensured that
>>> the assumption expressed as X'Pre is actually true before
>>> calling X.
>>
>> So what? Programmers program programs, and how is that related to
>> contracts etc?
>
> Informing is contracts' primary purpose,

Nope. The contract's purpose is to constrain contracted parties. 
Informing is the purpose of E-mail, newspaper etc...

>> Right, ">" is a relation, Remainder is not. And the point was?
>
> The point was:
> How much should the declaration of function Remainder tell a programmer
> about the relation between parameters A and B?

It should not unless statically enforceable. And there are lots of other 
mathematical facts about remainders and relations defined on the 
argument and the result you are conveniently ignoring. Including 
relations between stack pointer and stack size. Reason?

Now, from the software design POW, preconditions (the true ones, not the 
things you call so) must be as weak as possible. Thus even if A>B would 
be statically provable it is against good design practice to impose it 
because it burdens clients and means distributed overhead.

As I said before it must be moved to the post-condition, Storage_Error, 
or whatever raised upon stack overflow included.

> My answer:
> The declaration should include that they must be related by A > B.

They are not. Remainder is defined for A <= B as Constraint_Error, 
unless you get Storage_Error before that...

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[G.B.]

On 12/12/2016 18:39, Dmitry A. Kazakov wrote:
> As I said before it must be moved to the post-condition, Storage_Error, or whatever raised upon stack overflow included.

Could you please show a good Post aspect for

function Plus_Too (A, B: Standard.Integer)
                   return Standard.Integer is
begin
    return A + B;
end Plus_Too;


>
>> My answer:
>> The declaration should include that they must be related by A > B.
>
> They are not.

Only when the client has violated the contract about
which the programmer has never been told...

A shrug does not work, for any agreed-upon premise
in a contract.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 2016-12-12 19:55, G.B. wrote:
> On 12/12/2016 18:39, Dmitry A. Kazakov wrote:
>> As I said before it must be moved to the post-condition,
>> Storage_Error, or whatever raised upon stack overflow included.
>
> Could you please show a good Post aspect for
>
> function Plus_Too (A, B: Standard.Integer)
>                   return Standard.Integer is
> begin
>    return A + B;
> end Plus_Too;

None. Don't use aspects they are not good. I have already listed 
post-conditions, see my post from 2016-12-09.

>>> My answer:
>>> The declaration should include that they must be related by A > B.
>>
>> They are not.
>
> Only when the client has violated the contract about
> which the programmer has never been told...

Implied contracts are outside the scope. They question was about the 
explicit ones. There is an infinite number of implied contracts which 
can be violated, e.g. the one that the Earth does not turn black hole...

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[G.B.]

On 12/12/2016 21:53, Dmitry A. Kazakov wrote:
> On 2016-12-12 19:55, G.B. wrote:
>> On 12/12/2016 18:39, Dmitry A. Kazakov wrote:
>>> As I said before it must be moved to the post-condition,
>>> Storage_Error, or whatever raised upon stack overflow included.
>>
>> Could you please show a good Post aspect for
>>
>> function Plus_Too (A, B: Standard.Integer)
>>                   return Standard.Integer is
>> begin
>>    return A + B;
>> end Plus_Too;
>
> None. Don't use aspects they are not good. I have already listed post-conditions, see my post from 2016-12-09.

No Ada in there. I was thinking of this posting.

So, is there nothing we can say about the arguments
when we declare Plus_Too, such as how they need to be
related for Plus_Too at all having a chance of not raising?

> Implied contracts are outside the scope.

My point. Why should contracts not be explicit, in particular
when they had already been formal, albeit in a comment?

> There is an infinite number of implied contracts which can be violated,
>  e.g. the one that the Earth does not turn black hole...

That's curious. Can you show us the contract written and explicitly
stating that the Earth does not turn black hole, and then explain
how a programmer writing a call can violate this contract?

(Actually, there is no variable in the predicate other than those
implied in sub-expressions of Earth turning a black hole.
IIRC, the Large Hadron Collider was thought capable of violating
this contract according to explicit statements of some scientist.)

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 13/12/2016 08:15, G.B. wrote:
> On 12/12/2016 21:53, Dmitry A. Kazakov wrote:
>> On 2016-12-12 19:55, G.B. wrote:
>>> On 12/12/2016 18:39, Dmitry A. Kazakov wrote:
>>>> As I said before it must be moved to the post-condition,
>>>> Storage_Error, or whatever raised upon stack overflow included.
>>>
>>> Could you please show a good Post aspect for
>>>
>>> function Plus_Too (A, B: Standard.Integer)
>>>                   return Standard.Integer is
>>> begin
>>>    return A + B;
>>> end Plus_Too;
>>
>> None. Don't use aspects they are not good. I have already listed
>> post-conditions, see my post from 2016-12-09.
>
> No Ada in there. I was thinking of this posting.

Ada is an object language here. Thus it can never be Ada. It could be a 
meta language of annotations for Ada, like SPARK.

> So, is there nothing we can say about the arguments
> when we declare Plus_Too, such as how they need to be
> related for Plus_Too at all having a chance of not raising?
>
>> Implied contracts are outside the scope.
>
> My point. Why should contracts not be explicit, in particular
> when they had already been formal, albeit in a comment?

Explicit contracts are only ones the framework can enforce, at all or 
pragmatically. Anything it cannot goes into the "implicit" bin.

>> There is an infinite number of implied contracts which can be violated,
>>  e.g. the one that the Earth does not turn black hole...
>
> That's curious. Can you show us the contract written and explicitly
> stating that the Earth does not turn black hole, and then explain
> how a programmer writing a call can violate this contract?

It is an explicit contract. The contract gets violated when the Plus_Too 
does not return expected value due to consumption of the CPU by the 
black hole.

> (Actually, there is no variable in the predicate other than those
> implied in sub-expressions of Earth turning a black hole.

Your fault. Formally no such predicate could even exist, merely due to 
Goedel incompleteness.

There is an old programmer's saying: never check bugs you are not going 
fix...

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[G.B.]

On 13/12/2016 09:27, Dmitry A. Kazakov wrote:

>> No Ada in there. I was thinking of this posting.
>
> Ada is an object language here. Thus it can never be Ada. It could be a meta language of annotations for Ada, like SPARK.

Pre doesn't have to be object language as has now been
said and confirmed a number of times.


>>> Implied contracts are outside the scope.
>>
>> My point. Why should contracts not be explicit, in particular
>> when they had already been formal, albeit in a comment?
>
> Explicit contracts are only ones the framework can enforce, at all or pragmatically.

Which role do programmers play in this? Are frameworks so much
better at proving and enforcing than humans? They are man made
frameworks after all, so whether they should necessarily limit
the scope of man seems dubious.


> It is an explicit contract.

Can you make it a Boolean expression?

> The contract gets violated when the Plus_Too does not return expected value due to consumption of the CPU by the black hole.

So, what are expected values for various inputs of A and B
passed to Plus_Too? Can this be stated? Partially? I do think so.

>> (Actually, there is no variable in the predicate other than those
>> implied in sub-expressions of Earth turning a black hole.
>
> Your fault. Formally no such predicate could even exist, merely due to Goedel incompleteness.

Gödel's results do not apply to "+" in Standard.Integer,
so nothing is due to them here.

> There is an old programmer's saying: never check bugs you are not going fix...

Which is reflected in the saying that a failed Pre check
puts some bug directly under my nose, and that's by intent.

No proof can show bugs' absence whenever there is no predicate
describing expected values.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 13/12/2016 11:39, G.B. wrote:
> On 13/12/2016 09:27, Dmitry A. Kazakov wrote:
>
>>> No Ada in there. I was thinking of this posting.
>>
>> Ada is an object language here. Thus it can never be Ada. It could be
>> a meta language of annotations for Ada, like SPARK.
>
> Pre doesn't have to be object language as has now been
> said and confirmed a number of times.

Being a part of the body it does not belong to declarations.

>>>> Implied contracts are outside the scope.
>>>
>>> My point. Why should contracts not be explicit, in particular
>>> when they had already been formal, albeit in a comment?
>>
>> Explicit contracts are only ones the framework can enforce, at all or
>> pragmatically.
>
> Which role do programmers play in this?  Are frameworks so much
> better at proving and enforcing than humans? They are man made
> frameworks after all, so whether they should necessarily limit
> the scope of man seems dubious.

You can translate Ada programs into machine instructions manually, if 
you feel yourself so superior. I prefer to to rely on frameworks.

>> It is an explicit contract.
>
> Can you make it a Boolean expression?

That depends on the language in question. It is not an expression in Ada 
and cannot be made one.

> So, what are expected values for various inputs of A and B
> passed to Plus_Too? Can this be stated?

Yes it can and it is already done by the provided implementation of 
Plus_Too. This is exactly what implementations are for.

You keep on confusing program behavior with statements about it. These 
are necessarily expressed in different frameworks and thus in different 
languages. It is impossible to mix them, that is a hard mathematical fact.

>>> (Actually, there is no variable in the predicate other than those
>>> implied in sub-expressions of Earth turning a black hole.
>>
>> Your fault. Formally no such predicate could even exist, merely due to
>> Goedel incompleteness.
>
> Gödel's results do not apply to "+" in Standard.Integer,
> so nothing is due to them here.

They apply to a framework capable to spell all preconditions of "+". No 
such thing can exist. Therefore some [most] contracts will remain 
implied forever.

> No proof can show bugs' absence whenever there is no predicate
> describing expected values.

Proofs show absence of bugs under the premise that all implied contracts 
hold.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[G.B.]

On 13/12/2016 12:19, Dmitry A. Kazakov wrote:
> On 13/12/2016 11:39, G.B. wrote:
>> On 13/12/2016 09:27, Dmitry A. Kazakov wrote:
>>
>>>> No Ada in there. I was thinking of this posting.
>>>
>>> Ada is an object language here. Thus it can never be Ada. It could be
>>> a meta language of annotations for Ada, like SPARK.
>>
>> Pre doesn't have to be object language as has now been
>> said and confirmed a number of times.
>
> Being a part of the body it does not belong to declarations.

Right, Pre aspects are *not* body!  They have a right to
be part of some sort of monitoring program that observes
the first if they are to have an operational effect at all.
They are assertions separate from the program itself.

And they need *not* be exhaustive, even saying of what
would be hard, if possible at all. I think that is
agreement.

Whatever GNAT happens to do now does not change all this.

>>> It is an explicit contract.
>>
>> Can you make it a Boolean expression?
>
> That depends on the language in question. It is not an expression in Ada and cannot be made one.

Please, it's simple, actually, for what I had suggested,
a relation involving the two parameters A and B to be
passed to Plus_Too, since Standard.Integer is finite.

One lists inputs to Plus_Too as pairs that one specifies as not
mathematically overflowing the sum in Integer, for a start.
That's far from not expressible in Ada, it's not perfect
either, and it is highly inconvenient.

   (A => Integer'Last, B => Integer'Last)

will be a pair not listed,

   (A => -1, B => 42)

meets the requirements, and is listed.


>> So, what are expected values for various inputs of A and B
>> passed to Plus_Too? Can this be stated?
>
> Yes it can and it is already done by the provided implementation of Plus_Too.

It needs to be stated before the fact to be useful.

Without an implementation yet, one cannot infer its precondition.
But it is possible to write a predicate that is the specification
of a set of values from which some implementation is to compute
results.

> You keep on confusing program behavior with statements about it.

See above.


>> Gödel's results do not apply to "+" in Standard.Integer,
>> so nothing is due to them here.
>
> They apply to a framework capable to spell all preconditions of "+". No such thing can exist. Therefore some [most] contracts will remain implied forever.

I only asked for a relation between A and B as inputs to Plus_Too.
I cannot reasonably ask for an exhaustive Boolean expression that
makes the silly attempt to describe the universe of possibilities
in which Ada's "+" may have a number of effects.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 2016-12-13 17:59, G.B. wrote:
> On 13/12/2016 12:19, Dmitry A. Kazakov wrote:
>> On 13/12/2016 11:39, G.B. wrote:
>>> On 13/12/2016 09:27, Dmitry A. Kazakov wrote:
>>>
>>>>> No Ada in there. I was thinking of this posting.
>>>>
>>>> Ada is an object language here. Thus it can never be Ada. It could be
>>>> a meta language of annotations for Ada, like SPARK.
>>>
>>> Pre doesn't have to be object language as has now been
>>> said and confirmed a number of times.
>>
>> Being a part of the body it does not belong to declarations.
>
> Right, Pre aspects are *not* body!

They are being executed at run time.

>>>> It is an explicit contract.
>>>
>>> Can you make it a Boolean expression?
>>
>> That depends on the language in question. It is not an expression in
>> Ada and cannot be made one.
>
> Please, it's simple, actually,

It is a predicate which has nothing to do with Ada's Boolean expression 
you wrote. See another post in this thread.

>>> So, what are expected values for various inputs of A and B
>>> passed to Plus_Too? Can this be stated?
>>
>> Yes it can and it is already done by the provided implementation of
>> Plus_Too.
>
> It needs to be stated before the fact to be useful.
>
> Without an implementation yet, one cannot infer its precondition.
> But it is possible to write a predicate that is the specification
> of a set of values from which some implementation is to compute
> results.

Sure, it is possible to do calculus on predicates. But Ada expression 
A>B is not a predicate and if not A>B then raise Constraint_Error; end 
if; is not calculus of predicates.

> I only asked for a relation between A and B as inputs to Plus_Too.

No, you asked for an Ada program that evaluates a relation in connection 
with the semantics of Plus_To. There is no such thing. A relation is, 
the program is not. Another program, e.g. SPARK may do calculus, but not 
the object program. There is no way you could cross that line.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Shark8]

On Tuesday, December 13, 2016 at 2:11:42 PM UTC-7, Dmitry A. Kazakov wrote:
> On 2016-12-13 17:59, G.B. wrote:
> > On 13/12/2016 12:19, Dmitry A. Kazakov wrote:
> >> On 13/12/2016 11:39, G.B. wrote:
> >> Being a part of the body it does not belong to declarations.
> >
> > Right, Pre aspects are *not* body!
> 
> They are being executed at run time.

So?
The construct "Procedure X( Y: Positive );" has to have Y checked at runtime in the general case. (Yes, it can be optimized out IFF the compiler can prove that all call-sites are already of subtype Positive.)


> >>>> It is an explicit contract.
> >>>
> >>> Can you make it a Boolean expression?
> >>
> >> That depends on the language in question. It is not an expression in
> >> Ada and cannot be made one.
> >
> > Please, it's simple, actually,
> 
> It is a predicate which has nothing to do with Ada's Boolean expression 
> you wrote. See another post in this thread.

Ok, I'm looking at the original post... it's another post, and on this thread, but doesn't really seem germane to the point you're trying to make.  ;)

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 13/12/2016 23:13, Shark8 wrote:
> On Tuesday, December 13, 2016 at 2:11:42 PM UTC-7, Dmitry A. Kazakov wrote:
>> On 2016-12-13 17:59, G.B. wrote:
>>> On 13/12/2016 12:19, Dmitry A. Kazakov wrote:
>>>> On 13/12/2016 11:39, G.B. wrote:
>>>> Being a part of the body it does not belong to declarations.
>>>
>>> Right, Pre aspects are *not* body!
>>
>> They are being executed at run time.
>
> So?
> The construct "Procedure X( Y: Positive );" has to have Y checked at
> runtime in the general case.

X is an integer operation, defined on Integer Y.

The precondition here is *not* (Y in Positive), it is (Y in Integer). It 
is legal to call X on any Integer. Checking Y>=0 is semantically a part 
of the X's body, even if the compiler could inline this part at the 
caller's side or optimize it or the rest of the body away.

>>>>>> It is an explicit contract.
>>>>>
>>>>> Can you make it a Boolean expression?
>>>>
>>>> That depends on the language in question. It is not an expression in
>>>> Ada and cannot be made one.
>>>
>>> Please, it's simple, actually,
>>
>> It is a predicate which has nothing to do with Ada's Boolean expression
>> you wrote. See another post in this thread.
>
> Ok, I'm looking at the original post... it's another post, and on
> this  thread, but doesn't really seem germane to the point you're trying to
> make. ;)

No need to look further the difference between evaluation of some P(x) 
and proving Q |= P. These are just different things. Georg attempts to 
sell former for the latter. Won't happen.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[G.B.]

On 14/12/2016 09:42, Dmitry A. Kazakov wrote:
>
> The precondition here is *not* (Y in Positive), it is (Y in Integer). It is legal to call X on any Integer. Checking Y>=0 is semantically a part of the X's body, even if the compiler could inline this part at the caller's side or optimize it or the rest of the body away.

And this is where Design by Contract, by intent, would differ
from current choice of Ada's defensive style:

   The programmer is NOT allowed to just call an operation
   when there is a Pre aspect that says: Don't!

So, by intent, if you declare

   procedure X (Y : Positive)
      with
         Pre => Y > 0;

then a client programmer is required, by contract, to not
call X with a non-positive Integer.  If he or she does,
then the programmer is violating the contract, and held
responsible for any damage caused by the body of X.

This is what contract based programming is all about.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 14/12/2016 12:04, G.B. wrote:
> On 14/12/2016 09:42, Dmitry A. Kazakov wrote:
>>
>> The precondition here is *not* (Y in Positive), it is (Y in Integer).
>> It is legal to call X on any Integer. Checking Y>=0 is semantically a
>> part of the X's body, even if the compiler could inline this part at
>> the caller's side or optimize it or the rest of the body away.
>
> And this is where Design by Contract, by intent, would differ
> from current choice of Ada's defensive style:
>
>   The programmer is NOT allowed to just call an operation
>   when there is a Pre aspect that says: Don't!

So long the program remains legal that is not a contract from the 
language point of view.

> So, by intent, if you declare
>
>   procedure X (Y : Positive)
>      with
>         Pre => Y > 0;
>
> then a client programmer is required, by contract, to not
> call X with a non-positive Integer.  If he or she does,
> then the programmer is violating the contract, and held
> responsible for any damage caused by the body of X.

It is about formal language-supported contracts and all sorts of other 
contracts.

 > This is what contract based programming is all about.

That is the problem with implied contracts. Is this legal:

begin
    loop
       X (Read (Stream));
    end loop;
exception
    when Constraint_Error =>
       null;
end;

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[G.B.]

On 14/12/2016 12:25, Dmitry A. Kazakov wrote:

> That is the problem with implied contracts. Is this legal:
>
> begin
>    loop
>       X (Read (Stream));
>    end loop;
> exception
>    when Constraint_Error =>
>       null;
> end;

    "Assertions are not an input checking mechanism"
    "To avoid a common misunderstanding, make sure to note
that each of the contracts discussed holds between a routine
(the supplier) and another routine (its caller): we are concerned
about software-to-software communication, not software-to-human
or software-to-outside-world. (...) Here there is no substitute
for the usual condition-checking constructs, include the venerable
IF ... THEN ...; the exception handling mechanism ... may also be
helpful ". [1]


[1] Meyer, Bertrand: OOSC2, 2nd ed, §11.6

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 14/12/2016 13:44, G.B. wrote:
> On 14/12/2016 12:25, Dmitry A. Kazakov wrote:
>
>> That is the problem with implied contracts. Is this legal:
>>
>> begin
>>    loop
>>       X (Read (Stream));
>>    end loop;
>> exception
>>    when Constraint_Error =>
>>       null;
>> end;
>
>    "Assertions are not an input checking mechanism"
>    "To avoid a common misunderstanding, make sure to note
> that each of the contracts discussed holds between a routine
> (the supplier) and another routine (its caller): we are concerned
> about software-to-software communication, not software-to-human
> or software-to-outside-world. (...) Here there is no substitute
> for the usual condition-checking constructs, include the venerable
> IF ... THEN ...; the exception handling mechanism ... may also be
> helpful ". [1]
>
> [1] Meyer, Bertrand: OOSC2, 2nd ed, §11.6

Is it legal or not?

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[G.B.]

On 14/12/2016 13:52, Dmitry A. Kazakov wrote:
> On 14/12/2016 13:44, G.B. wrote:
>> On 14/12/2016 12:25, Dmitry A. Kazakov wrote:
>>
>>> That is the problem with implied contracts. Is this legal:
>>>
>>> begin
>>>    loop
>>>       X (Read (Stream));
>>>    end loop;
>>> exception
>>>    when Constraint_Error =>
>>>       null;
>>> end;
>>
>>    "Assertions are not an input checking mechanism"
>>    "To avoid a common misunderstanding, make sure to note
>> that each of the contracts discussed holds between a routine
>> (the supplier) and another routine (its caller): we are concerned
>> about software-to-software communication, not software-to-human
>> or software-to-outside-world. (...) Here there is no substitute
>> for the usual condition-checking constructs, include the venerable
>> IF ... THEN ...; the exception handling mechanism ... may also be
>> helpful ". [1]
>>
>> [1] Meyer, Bertrand: OOSC2, 2nd ed, §11.6
>
> Is it legal or not?

Like you have said, "It is about formal language-supported contracts
and all sorts of other contracts". So, I think there is enough material
there to conclude that this kind or that kind of contract should
be legally dominating a particular program design decision.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 2016-12-14 17:31, G.B. wrote:
> On 14/12/2016 13:52, Dmitry A. Kazakov wrote:
>> On 14/12/2016 13:44, G.B. wrote:
>>> On 14/12/2016 12:25, Dmitry A. Kazakov wrote:
>>>
>>>> That is the problem with implied contracts. Is this legal:
>>>>
>>>> begin
>>>>    loop
>>>>       X (Read (Stream));
>>>>    end loop;
>>>> exception
>>>>    when Constraint_Error =>
>>>>       null;
>>>> end;
>>>
>>>    "Assertions are not an input checking mechanism"
>>>    "To avoid a common misunderstanding, make sure to note
>>> that each of the contracts discussed holds between a routine
>>> (the supplier) and another routine (its caller): we are concerned
>>> about software-to-software communication, not software-to-human
>>> or software-to-outside-world. (...) Here there is no substitute
>>> for the usual condition-checking constructs, include the venerable
>>> IF ... THEN ...; the exception handling mechanism ... may also be
>>> helpful ". [1]
>>>
>>> [1] Meyer, Bertrand: OOSC2, 2nd ed, §11.6
>>
>> Is it legal or not?
>
> Like you have said, "It is about formal language-supported contracts
> and all sorts of other contracts". So, I think there is enough material
> there to conclude that this kind or that kind of contract should
> be legally dominating a particular program design decision.

That is no answer. A program is either legal or not. The program is 
legal. The contract you implied is violated. Thus what you called 
contract is not a formal contract. q.e.d.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[G.B.]

On 14/12/2016 17:52, Dmitry A. Kazakov wrote:
> On 2016-12-14 17:31, G.B. wrote:
>> On 14/12/2016 13:52, Dmitry A. Kazakov wrote:
>>> On 14/12/2016 13:44, G.B. wrote:
>>>> On 14/12/2016 12:25, Dmitry A. Kazakov wrote:
>>>>
>>>>> That is the problem with implied contracts. Is this legal:
>>>>>
>>>>> begin
>>>>>    loop
>>>>>       X (Read (Stream));
>>>>>    end loop;
>>>>> exception
>>>>>    when Constraint_Error =>
>>>>>       null;
>>>>> end;
>>>>
>>>>    "Assertions are not an input checking mechanism"
>>>>    "To avoid a common misunderstanding, make sure to note
>>>> that each of the contracts discussed holds between a routine
>>>> (the supplier) and another routine (its caller): we are concerned
>>>> about software-to-software communication, not software-to-human
>>>> or software-to-outside-world. (...) Here there is no substitute
>>>> for the usual condition-checking constructs, include the venerable
>>>> IF ... THEN ...; the exception handling mechanism ... may also be
>>>> helpful ". [1]
>>>>
>>>> [1] Meyer, Bertrand: OOSC2, 2nd ed, §11.6
>>>
>>> Is it legal or not?
>>
>> Like you have said, "It is about formal language-supported contracts
>> and all sorts of other contracts". So, I think there is enough material
>> there to conclude that this kind or that kind of contract should
>> be legally dominating a particular program design decision.
>
> That is no answer.

It is an answer, even with some "legality" coming out of nowhere,
as if RM legality, I guess, were a sufficient condition for
  (a) correctness, and
  (b) justifying misuse of contracts (see below, and above),
and the answer invalidates the premises of your proof:
"There is no substitute ..." is universally quantified, and it
suggests to not *ever* use aspects when checking input. See the
first sentence of Meyer, which is a heading.
"The exception handling mechanism ... may ... helpful", while politely
suggesting existential qualification, is accompanied by a requirement
of Eiffel style exception handling.



> A program is either legal or not. The program is legal. The contract you implied is violated. Thus what you called contract is not a formal contract. q.e.d.

It is interesting to learn that I must have implied all kinds
of contracts (which ones? which kind?) when I speak in favor of
expressly written aspects.

Re: Ada 2012 Constraints (WRT an Ada IR)

[G.B.]

On 14/12/2016 09:42, Dmitry A. Kazakov wrote:
> No need to look further the difference between evaluation of some P(x) and proving Q |= P. These are just different things. Georg attempts to sell former for the latter.

I don't, since they are different things.
But they are related. Formal verification
and program design are related, too, and
they are different things.
Program text is just a vehicle for seeing the
relationships.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Shark8]

On Wednesday, December 14, 2016 at 1:42:34 AM UTC-7, Dmitry A. Kazakov wrote:
> On 13/12/2016 23:13, Shark8 wrote:
> >
> > So?
> > The construct "Procedure X( Y: Positive );" has to have Y checked at
> > runtime in the general case.
> 
> X is an integer operation, defined on Integer Y.

And the contract here states that the value of said integer is positive.
The [implicit] contract also states (via LTM) what should happen if this is violated: CONSTRAINT_ERROR.

> 
> The precondition here is *not* (Y in Positive), it is (Y in Integer).

You are observably wrong.
If you supply a negative number, the body of X never executes.


> It is legal to call X on any Integer. Checking Y>=0 is semantically a
> part of the X's body, even if the compiler could inline this part at the 
> caller's side or optimize it or the rest of the body away.

Of course you're utterly ignoring a very important fact:
Ada was designed to (a) be implementable, (b) have static checkers [indeed, a *lot* of static checking is mandated by requirements of the translator], and (c) be optimizable. -- In fact, DIANA was designed to facilitate (b) and (c) by providing a "common language" that static-analyzers, optimizers, and code-generators could all "speak".

Many of the static checks that Ada demands of the translators were, at the time (Ada 83), bleeding-edge technology. SPARK is a step in that direction though with static-analysis and proof-checking rather than optimization -- but proof-checking allows many more opportunities for optimization, and may be said to be the basis of optimization (if you can prove construct X is better than construct A by some metric, and both are equivalent, you can optimize for that metric by replacing all occurrences of A with X).

In this light, integrating SPARK proving with the Ada compiler could allow for better optimizations... and if it can be done in such a way that it can be leveraged in other portions of the compiler (say semantic checks), then why not use it?

> > Ok, I'm looking at the original post... it's another post, and on
> > this  thread, but doesn't really seem germane to the point you're trying to
> > make. ;)
> 
> No need to look further the difference between evaluation of some P(x) 
> and proving Q |= P. These are just different things. Georg attempts to 
> sell former for the latter. Won't happen.

Read this -- https://www.cs.unm.edu/~forrest/publications/negsharingilcp.pdf -- it's intuitively obvious how this is a possible answer to my original posting; it's also obvious how it can be used in solvers, since that's the particular domain the paper's about.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 2016-12-14 20:23, Shark8 wrote:
> On Wednesday, December 14, 2016 at 1:42:34 AM UTC-7, Dmitry A. Kazakov wrote:
>> On 13/12/2016 23:13, Shark8 wrote:
>>>
>>> So?
>>> The construct "Procedure X( Y: Positive );" has to have Y checked at
>>> runtime in the general case.
>>
>> X is an integer operation, defined on Integer Y.
>
> And the contract here states that the value of said integer is positive.

No it does not.

> The [implicit] contract also states (via LTM) what should happen if
> this is violated: CONSTRAINT_ERROR.

It is explicit, written in the declaration of procedure X, Y : Positive.

>> The precondition here is *not* (Y in Positive), it is (Y in Integer).
>
> You are observably wrong.
> If you supply a negative number, the body of X never executes.

Of course it does. Semantically any effect of a call to X is due to X's 
body. There is nothing else there.

>> It is legal to call X on any Integer. Checking Y>=0 is semantically a
>> part of the X's body, even if the compiler could inline this part at the
>> caller's side or optimize it or the rest of the body away.
>
> Of course you're utterly ignoring a very important fact:
> Ada was designed to (a) be implementable, (b) have static checkers
> [indeed, a *lot* of static checking is mandated by requirements of the
> translator], and (c) be optimizable. -- In fact, DIANA was designed to
> facilitate (b) and (c) by providing a "common language" that
> static-analyzers, optimizers, and code-generators could all "speak".

Naturally I ignore all this as irrelevant to the issue at hand. It is 
legal to call X with any integer. Period.

> In this light, integrating SPARK proving with the Ada compiler could
> allow for better optimizations... and if it can be done in such a way
> that it can be leveraged in other portions of the compiler (say semantic
> checks), then why not use it?

When that comes into life, programmers surely will, though not in the 
form of preconditions, because as I said, it is bad design. The rule is 
weakening preconditions, strengthening post-conditions.

>>> Ok, I'm looking at the original post... it's another post, and on
>>> this  thread, but doesn't really seem germane to the point you're trying to
>>> make. ;)
>>
>> No need to look further the difference between evaluation of some P(x)
>> and proving Q |= P. These are just different things. Georg attempts to
>> sell former for the latter. Won't happen.
>
> Read this --
> https://www.cs.unm.edu/~forrest/publications/negsharingilcp.pdf -- it's
> intuitively obvious how this is a possible answer to my original
> posting; it's also obvious how it can be used in solvers, since that's
> the particular domain the paper's about.

I don't see how is it relevant.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Shark8]

On Wednesday, December 14, 2016 at 1:04:53 PM UTC-7, Dmitry A. Kazakov wrote:
> On 2016-12-14 20:23, Shark8 wrote:
> > Read this --
> > https://www.cs.unm.edu/~forrest/publications/negsharingilcp.pdf -- it's
> > intuitively obvious how this is a possible answer to my original
> > posting; it's also obvious how it can be used in solvers, since that's
> > the particular domain the paper's about.
> 
> I don't see how is it relevant.

Perhaps re-reading the first post would help:
On Monday, November 28, 2016 at 4:49:39 PM UTC-7, Shark8 wrote:
> So, with Ada 2012 we gained some really nice possibilities with the way to express constraints, the downside is that there's now a fairly wide range of ways to express constraints on types. Obviously these differences must be accounted for, but the are functionally equivalent, for example:
> 
> Subtype P0 is Natural range Natural'Succ(Natural'First)..Natural'Last;
> Subtype P1 is Integer range 1..Integer'Last;
> Subtype P2 is Integer with Static_Predicate => P2 in 1..Integer'Last or else raise Constraint_Error;
> Subtype P3 is Integer with
>   Static_Predicate  => P3 in 1..Integer'Last,
>   Predicate_Failure => raise Constraint_Error;
> 
> Now, these should be generally the same way of writing the same thing (ie "Positive") -- though I'm not completely certain that this is the case in terms of subtle semantics (am I missing something?) -- it certainly would be convenient if they were as then we could have an IR wherein the general form of a type-constraint is uniformly handled.
> 
> Comments? Insights?

It's relevant because it is exactly showing how to represent restrictions [exclusions] on values (within a set); and, as we know, a type is a set of values and a set of operations acting on those values. -- This maps directly to Ada, given the LRM's definition of subtypes.

> > In this light, integrating SPARK proving with the Ada compiler could
> > allow for better optimizations... and if it can be done in such a way
> > that it can be leveraged in other portions of the compiler (say semantic
> > checks), then why not use it?
> 
> When that comes into life, programmers surely will, though not in the 
> form of preconditions, because as I said, it is bad design. The rule is 
> weakening preconditions, strengthening post-conditions.

I think you may be overestimating the group "programmers".
Seriously, the thread "C# new features (v.7)" -- https://groups.google.com/forum/#!topic/comp.lang.ada/mLZIo_Sjm5c -- lists things that "modern" languages are just getting that Ada has had for years.

Integrating these useful technologies into the compiler in a manner that is invisible to users [non-implementer Ada programmers] is a good way to ensure that the tools are used. (e.g. the Ada compiler does automatically what C's Lint did, and is much better for it. [Most of the C programmers I knew in college *never* used lint.])

Now, if we can also leverage these technologies to make implementations [of Ada] better [quality-wise] and more maintainable, then that's win-win all the way around at the cost of (a) designing your IR to be amiable to the prover-module, and (b) implementing the prover-module.

And if you're doing a SPARK implementation then you'd need to do all the work for (b) anyway -- so in that case it's really at the cost of designing the IR... which, if you'll remember, is the real topic of this thread.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 14/12/2016 22:46, Shark8 wrote:
> On Wednesday, December 14, 2016 at 1:04:53 PM UTC-7, Dmitry A. Kazakov wrote:

> It's relevant because it is exactly showing how to represent
> restrictions [exclusions] on values (within a set); and, as we know, a
> type is a set of values and a set of operations acting on those values.
> -- This maps directly to Ada, given the LRM's definition of subtypes.

Well, but first it is an implementation issue, as such, of a very 
secondary order to the question of constrained types and other means to 
create new types. Secondly arbitrary constraints is low level and thus a 
bad idea to introduce into the type system, as dynamic predicates 
promptly illustrate. Resemblance to Ada 83 subtypes is only superficial.

>>> In this light, integrating SPARK proving with the Ada compiler could
>>> allow for better optimizations... and if it can be done in such a way
>>> that it can be leveraged in other portions of the compiler (say semantic
>>> checks), then why not use it?
>>
>> When that comes into life, programmers surely will, though not in the
>> form of preconditions, because as I said, it is bad design. The rule is
>> weakening preconditions, strengthening post-conditions.
>
> I think you may be overestimating the group "programmers".
> Seriously, the thread "C# new features (v.7)" --
> https://groups.google.com/forum/#!topic/comp.lang.ada/mLZIo_Sjm5c --
> lists things that "modern" languages are just getting that Ada has had
> for years.

Ada programmers? Ada people are very interested in formal verification. 
The problem is integration of SPARK into Ada and arbitrary constraints 
would be only obstacle here. The lower is the level of a construct more 
difficult is verification.

> Integrating these useful technologies into the compiler in a manner
> that is invisible to users [non-implementer Ada programmers] is a good
> way to ensure that the tools are used. (e.g. the Ada compiler does
> automatically what C's Lint did, and is much better for it. [Most of the
> C programmers I knew in college *never* used lint.])

Right, because it is a tool you could use or not. In Ada type 
declarations must be there, so it is not a tool, but an integral part of 
the language. This is why "pre"-aspects is a non-starter even ignoring 
their semantic consistency issues. You can do things with or without 
them. Psychologically it won't work.

> Now, if we can also leverage these technologies to make
> implementations [of Ada] better [quality-wise] and more maintainable,
> then that's win-win all the way around at the cost of (a) designing your
> IR to be amiable to the prover-module, and (b) implementing the
> prover-module.

I am against that, see above, it must be an integral part of the Ada's 
declarative framework, never a module or a tool.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[G.B.]

On 15/12/2016 09:41, Dmitry A. Kazakov wrote:
> In Ada type declarations must be there, so it is not a tool, but an integral part of the language. This is why "pre"-aspects is a non-starter even ignoring their semantic consistency issues. You can do things with or without them. Psychologically it won't work.

Problem statement:
Devise a type that represents an ordered pair of linearly
ordered numbers, such that programmers can create objects that
have the two elements in proper order.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 15/12/2016 11:31, G.B. wrote:
> On 15/12/2016 09:41, Dmitry A. Kazakov wrote:
>> In Ada type declarations must be there, so it is not a tool, but an
>> integral part of the language. This is why "pre"-aspects is a
>> non-starter even ignoring their semantic consistency issues. You can
>> do things with or without them. Psychologically it won't work.
>
> Problem statement:
> Devise a type that represents an ordered pair of linearly
> ordered numbers, such that programmers can create objects that
> have the two elements in proper order.

It is a good illustration of what is wrong with ideas you promote. You 
are thinking in terms of implementations.

Ada, at least Ada 83 was focused on ADT and designed to be language that 
supporting software design in terms of ADTs as opposed to loose data 
structures.

An Ada programmer would rather design an integer interval type than data 
structure you described. Whether he would choose a pair of interval 
bounds to represent it, or the lower bound and length, or whatever else 
he would not expose it in the declarations.

Neither there is any reason to derive an interval type from a pair and 
put a constraint on the pair as you seem suggest. That is an 
implementation. Semantically pairs and intervals are not related types.

Then lower<=higher is not a constraint, it is an invariant, if any. 
Furthermore from the correctness proofs standpoint the post-conditions 
of interval arithmetic trivially ensure the invariant. E.g.

    [a,b] + [c,d] = [min(a,b), max(c,b)]

So there is no need to spell the invariant. And finally, invariant is an 
implementation detail not to expose anyway.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 15/12/2016 14:17, Dmitry A. Kazakov wrote:
>
>    [a,b] + [c,d] = [min(a,b), max(c,b)]

  [a,b] + [c,d] = [min(a,c), max(b,d)]

of course.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[G.B.]

On 15/12/2016 14:17, Dmitry A. Kazakov wrote:
> On 15/12/2016 11:31, G.B. wrote:
>> On 15/12/2016 09:41, Dmitry A. Kazakov wrote:
>>> In Ada type declarations must be there, so it is not a tool, but an
>>> integral part of the language. This is why "pre"-aspects is a
>>> non-starter even ignoring their semantic consistency issues. You can
>>> do things with or without them. Psychologically it won't work.
>>
>> Problem statement:
>> Devise a type that represents an ordered pair of linearly
>> ordered numbers, such that programmers can create objects that
>> have the two elements in proper order.
>
> It is a good illustration of what is wrong with ideas you promote. You are thinking in terms of implementations.

Am I?  ;-)

In any case, I wasn't thinking of arithmetic at all. Maybe graphs'
edges. But certainly I had the simple concept of an order pair in mind.

Trying to follow your advice, though, with Post for emphasis,
lets see how well the type works without Pre.

    type Immutable_Ordered_Pair (<>) is private;

    function Make (First, Second: POT) return Immutable_Ordered_Pair
    with
      --Pre => First <= Second,   -- (*)
      Post => Make'Result in Immutable_Ordered_Pair; -- or raise

    function First (Pair : Immutable_Ordered_Pair) return POT;
    function Second (Pair : Immutable_Ordered_Pair) return POT;

Type POT has "<=", its name suggesting a partially ordered set.
The full view of Immutable_Ordered_Pair carries a hidden

    Type_Invariant => First <= Second;

naming obvious components, and it is hidden in the private part
as requested.

Now what will (*) yield if uncommented, thus ignoring your advice?
First, this is what Make could do without a Pre aspect:

   - raise some X_E if "<=" can raise X_E;

   - handle X_E and reorder the parameters ("At your service!")
     and retry, noting the attempt and raise X_E if "<=" does it
     again, otherwise return a pair made form the parameters reversed;

   - an unnecessary check in case the programmer passes First and
     Second properly ordered, i.e. (First <= Second) = True.

Now give the programmer Pre as it follows from {Post, Type_Invariant},
and you are designing by contract:

   - Make assumes Pre is true, so it simply returns a new object,
     since its assumption, Pre, entails {Post, Type_Invariant}.

It is contract violation if the programmer has passed values
not in "<=", violating Pre, so Make will not create and object.

Simple, no secrets, consistent, and efficient.

As opposed to:
Not Simple, arcane, consistent, and inefficient.

The reversal of parameters in the body of the rather complex Make
(when Pre is undisclosed) could instead be made a service procedure
or constructing function. For variables:

    procedure Swapped_As_Necessary (X, Y : in out POT)
    with
      Pre => True,
      Post => (if X'Old <= Y'Old
               then X = X'Old and Y = Y'Old
               else X = Y'Old and Y = X'Old);

But whenever an algorithm already has Post => x < y, then there
is no need to use that service procedure. Just call Make (x, y),
it is safe WRT contracts. Rest assured that Make won't raise A_F
and instead will produce objects as desired, and quickly.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 2016-12-15 20:50, G.B. wrote:
> On 15/12/2016 14:17, Dmitry A. Kazakov wrote:
>> On 15/12/2016 11:31, G.B. wrote:
>>> On 15/12/2016 09:41, Dmitry A. Kazakov wrote:
>>>> In Ada type declarations must be there, so it is not a tool, but an
>>>> integral part of the language. This is why "pre"-aspects is a
>>>> non-starter even ignoring their semantic consistency issues. You can
>>>> do things with or without them. Psychologically it won't work.
>>>
>>> Problem statement:
>>> Devise a type that represents an ordered pair of linearly
>>> ordered numbers, such that programmers can create objects that
>>> have the two elements in proper order.
>>
>> It is a good illustration of what is wrong with ideas you promote. You
>> are thinking in terms of implementations.
>
> Am I?  ;-)
>
> In any case, I wasn't thinking of arithmetic at all. Maybe graphs'
> edges. But certainly I had the simple concept of an order pair in mind.
>
> Trying to follow your advice, though, with Post for emphasis,
> lets see how well the type works without Pre.
>
>    type Immutable_Ordered_Pair (<>) is private;
>
>    function Make (First, Second: POT) return Immutable_Ordered_Pair
>    with
>      --Pre => First <= Second,   -- (*)
>      Post => Make'Result in Immutable_Ordered_Pair; -- or raise

Right, no precondition

>    function First (Pair : Immutable_Ordered_Pair) return POT;
>    function Second (Pair : Immutable_Ordered_Pair) return POT;
>
> Type POT has "<=", its name suggesting a partially ordered set.
> The full view of Immutable_Ordered_Pair carries a hidden
 >
>    Type_Invariant => First <= Second;
>
> naming obvious components, and it is hidden in the private part
> as requested.
>
> Now what will (*) yield if uncommented, thus ignoring your advice?
> First, this is what Make could do without a Pre aspect:
>
>   - raise some X_E if "<=" can raise X_E;
 >
>   - handle X_E and reorder the parameters ("At your service!")
>     and retry, noting the attempt and raise X_E if "<=" does it
>     again, otherwise return a pair made form the parameters reversed;
>
>   - an unnecessary check in case the programmer passes First and
>     Second properly ordered, i.e. (First <= Second) = True.
>
> Now give the programmer Pre as it follows from {Post, Type_Invariant},
> and you are designing by contract:

No. Pre does not follow from Post. The one that does is different:

    First >= Second or else Constraint_Error is propagating

The key difference is that Constraint_Error must be *already* underway 
when First < Second. Precondition is an obligation for the caller:

    if First >= Second then
       X := Make (First, Second);
    else
       raise Constraint_Error;
       X := Make (First, Second); -- Not going into
    end if;

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[G.B.]

On 16/12/2016 11:04, Dmitry A. Kazakov wrote:

>>    function Make (First, Second: POT) return Immutable_Ordered_Pair
>>    with
>>      --Pre => First <= Second,   -- (*)
>>      Post => Make'Result in Immutable_Ordered_Pair; -- or raise
>
> Right, no precondition

As you have chosen to not address, except for here saying
"no precondition" while stating a Pre later, the lack of Pre
will cause major differences. They comprise both Make
and the whole design and efficiency, all as outlined.
How could anyone always ignore these differences?

>> Now give the programmer Pre as it follows from {Post, Type_Invariant},
>> and you are designing by contract:
>
> No. Pre does not follow from Post. The one that does is different:
>
>    First >= Second or else Constraint_Error is propagating

I assume you meant

     First <= Second or else Constraint_Error is propagating?

Which is basically the observable behavior of current Ada,
except that

- with Pre,
     a call may have been started, but is stopped from entering
     the Ada-body,

- without Pre,
     the Ada-body has started checking and runs into all sorts
     of decisions, and possibly into the Type_Invariant not
     being True for the parameters it has already "accepted".

> The key difference is

... a design choice: establishing the precondition is work
to be done be the programmer who writes the call. There may be
Make'Pre as a guide. If there isn't, the implementers of
Make and writers of Make'Post have not done their homework.

But this is puzzling:
Suppose the compiler can't prove that calling Make is safe in the
Pre/Post sense. Then, how did the programmer of Make determine
which parameters will lead to safe return? And be silent about it?

Again, I think that an important purpose of the Pre aspect is to
inform the programmer about when *not* to call.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Stefan.Lucks]

[-- Attachment #1: Type: text/plain, Size: 3327 bytes --]

On Fri, 16 Dec 2016, G.B. wrote:

> ... a design choice: establishing the precondition is work
> to be done be the programmer who writes the call. There may be
> Make'Pre as a guide. If there isn't, the implementers of
> Make and writers of Make'Post have not done their homework.

Make'Pre isn't just a guide, it is a contract. ;-)

> But this is puzzling:
> Suppose the compiler can't prove that calling Make is safe in the
> Pre/Post sense. Then, how did the programmer of Make determine
> which parameters will lead to safe return? And be silent about it?

Technically, the programmer is responsible for *never* violating the 
precondition, ever. That is the whole point of a *precondition*.

So First <= Second is a proper precondition, telling the customer to 
never, ever call Make with First > Second:

    function Make (First, Second: POT) return Immutable_Ordered_Pair
    with
      Pre => First <= Second,
      Post => ...

In contrast, the notation with "or else Exception" is technically not a 
precondition, any more. It tells the reader/client: "You don't need to 
bother with the order of First and Second. If you call Make with First > 
Second, I will raise a specific exception that you may handle, then.":

    function Make (First, Second: POT) return Immutable_Ordered_Pair
    with
      Pre => First <= Second or else Raise_Constaint_Error,
      Post => ...

While Ada writes this conveniently as a precondition, it actually is a 
postcondition. Dmitry is right at that point.

Now, I am not as dogmatic as Dmitry sometimes is. Sure, the "or else 
Exception" notation is a minor abuse of the "Pre" aspect, and the "Post" 
aspect would have fitted better. But this is just a marginal syntactic 
issue, and having the option to specify the specific exception is great!

> Again, I think that an important purpose of the Pre aspect is to
> inform the programmer about when *not* to call.

Well, that is the purpose of a precondition, but we have to live with the 
fact that the "Pre" aspect is also used for certain postconditions. Else 
something like

      Pre => First <= Second or else Raise_Constaint_Error,

would not make any sense at all!

If you never call the subprogram with First > Second, it will not raise 
the exception. And if the exception is not raised, anyway, then why, on 
earth, whould you care which exception is not raised?


A related but different point: Some people go even further and claim that

      Pre => First <= Second,

is not a proper precondition, because this is, de facto, the shorthand for

      Pre => First <= Second or else Assertion_Error.

I am afraid, that argument leads eventually into madness. If the compiler 
cannot prove that a certain call does not violate the contract, and if the 
programmer actually violates the contract, it makes sense to write some 
diagnostic information to somewhere and then shut down. Of course, 
handling Assertion_Error and then continuing, instead of shutting down, 
may be express route into madness. ;-)



--------  I  love  the  taste  of  Cryptanalysis  in  the morning!  --------
www.uni-weimar.de/de/medien/professuren/mediensicherheit/people/stefan-lucks
----Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universität Weimar, Germany----

Re: Ada 2012 Constraints (WRT an Ada IR)

[Randy Brukardt]

<Stefan.Lucks@uni-weimar.de> wrote in message 
news:alpine.DEB.2.20.1612161308590.29766@debian...
...
>If you never call the subprogram with First > Second, it will not raise
>the exception. And if the exception is not raised, anyway, then why, on
>earth, whould you care which exception is not raised?

Only one reason: for compatibility with a previous version of the same 
routine that didn't have the precondition.

The embedded raise expression exists to ease the transition from not having 
preconditions to having them. Without it, one could not take existing code 
like Text_IO or Ada.Containers.Vectors and write it with preconditions. 
Allowing preconditions to be usable only on new code would slow the 
adoption.

Ideally, no one would ever call Ada.Text_IO.Put with a closed file. By 
making that a precondition, we allow tools to detect the mistake so that 
hopefully no one ever is handling Status_Error. But if some existing code is 
handling Status_Error, we can't raise Assertion_Error instead and expect 
that to be OK.

There shouldn't be much need to specify the exception with preconditions for 
new code. Maybe if one needs to be similar to related existing code, but 
that's about it.

                                      Randy.

Re: Ada 2012 Constraints (WRT an Ada IR)

[G.B.]

On 16/12/2016 13:56, Stefan.Lucks@uni-weimar.de wrote:
> In contrast, the notation with "or else Exception" is technically not a precondition, any more. It tells the reader/client: "You don't need to bother with the order of First and Second. If you call Make with First > Second, I will raise a specific exception that you may handle, then.":
>
>    function Make (First, Second: POT) return Immutable_Ordered_Pair
>    with
>      Pre => First <= Second or else Raise_Constaint_Error,
>      Post => ...

Following the Eiffel lead, and also Randy Brukardt's reminder
to consider RM 6.4(10/2), I think it is correct to say that
no statement of the Ada block

   begin   -- of Make
     ....
   end Make;

will execute "raise Constraint_Error" announced in Pre. In fact,
RM 6.1.1(36/3) shows that Make cannot possibly raise the exception
from inside, because then, technically, it could handle it there,
contradicting the RM.

So if "Post" means "After", then a contract violation may come
first and an Assertion_Error is raised after that, but the
execution of statements of Make will not have begun. So, in
contract based design, Make does what it is supposed to do and
does *not* check its Pre, just like proofs do not check their
premises. (Eiffel just attaches names to "require"'s Boolean
expressions, for reference.)


That's a difference, I think, between contract based programming
and plain old defensive programming with exceptions, or "programming
by announced jumping", if I may call it that.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Stefan.Lucks]

[-- Attachment #1: Type: text/plain, Size: 1993 bytes --]

On Fri, 16 Dec 2016, G.B. wrote:

> no statement of the Ada block
>
>  begin   -- of Make
>    ....
>  end Make;
>
> will execute "raise Constraint_Error" announced in Pre. In fact,
> RM 6.1.1(36/3) shows that Make cannot possibly raise the exception
> from inside, because then, technically, it could handle it there,
> contradicting the RM.
>
> So if "Post" means "After", then a contract violation may come
> first and an Assertion_Error is raised after that, but the
> execution of statements of Make will not have begun. So, in
> contract based design, Make does what it is supposed to do and
> does *not* check its Pre, just like proofs do not check their
> premises. (Eiffel just attaches names to "require"'s Boolean
> expressions, for reference.)

Well, follosing the Eiffel lead and Bertrand Mayer's writings, the client 
will not care where, exactly, the exception is raised. The client is 
calling the subprogram with certain values as parameters, and the client 
will get some expected result, even if it is a specific exception.

The else-clause still turns the Pre aspect into a postcondition.

On the other hand, Randy's point is quite convincing: If we want to 
introduce contracts -- and, specifically, preconditions -- into existing 
libraries without breaking compatibility, then the else clause is exactly 
what is needed.

So then the Pre-part of the contract essentially says:

    Don't call Make with First > Last!   -- This is a proper precondition.

    but your legacy code, which has been written before we fixed this
    contract, does not need to be rewritten.
    -- This is about software which still expects no precondition, but
    -- the old postcondition.

That makes sense!


--------  I  love  the  taste  of  Cryptanalysis  in  the morning!  --------
www.uni-weimar.de/de/medien/professuren/mediensicherheit/people/stefan-lucks
----Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universität Weimar, Germany----

Re: Ada 2012 Constraints (WRT an Ada IR)

[Randy Brukardt]

<Stefan.Lucks@uni-weimar.de> wrote in message 
news:alpine.DEB.2.20.1612171023380.1039@debian...
...
>The else-clause still turns the Pre aspect into a postcondition.
>
>On the other hand, Randy's point is quite convincing: If we want to
>introduce contracts -- and, specifically, preconditions -- into existing
>libraries without breaking compatibility, then the else clause is exactly
>what is needed.

I know the point is convincing; we spent significant parts of ARG meetings 
in 2012 inventing the raise expression (and lots of other rejected solutions 
to this problem) specifically because I had convinced the rest of the ARG 
that this needed  to be addressed. :-) I'd be surprised if it has lost its 
power in the intervening years.

                                     Randy.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 16/12/2016 12:48, G.B. wrote:

>> The key difference is
>
> ... a design choice: establishing the precondition is work
> to be done be the programmer who writes the call.

Yep, a burden one could easily avoid had the designer cared to do his 
job properly.

> But this is puzzling:
> Suppose the compiler can't prove that calling Make is safe in the
> Pre/Post sense.

Then the program must be illegal,

> Then, how did the programmer of Make determine
> which parameters will lead to safe return? And be silent about it?

This presumes the programmer has absolutely no idea why he is calling 
the subprogram. This is certainly not the way of work Ada should promote.

Furthermore, the compiler does not prove if Make call is safe. The 
compiler proves if the code calling Make is correct. E.g.:

1. the code was contracted not to raise Constraint_Error
2. a call to Make possibly propagates Constraint_Error
3. Constraint_Error is not handled
---------
Incorrect

This is a sufficiently different approach to software design from what 
you seemingly have in mind. If Make has a precondition it would become:

1. precondition is true
--------
Cannot prove First <= Second, incorrect

The former is a lot easier to deal with, which is why the design rule 
orders to weaken preconditions.

> Again, I think that an important purpose of the Pre aspect is to
> inform the programmer about when *not* to call.

Not at all. The sole purpose of a precondition is to state the contract. 
Information as to why Make is called and what Make is supposed to do is 
a problem space concept, not a correctness concept.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Shark8]

On Thursday, December 15, 2016 at 1:41:50 AM UTC-7, Dmitry A. Kazakov wrote:
> 
> I am against that, see above, it must be an integral part of the Ada's 
> declarative framework, never a module or a tool.

Tooling is *the* most cited thing on my survey of why Ada isn't more popular -- it includes things like IDEs, too -- but you're conveniently ignoring almost everything I said because I mentioned C's Lint and how it wasn't used.

> > Integrating these useful technologies into the compiler in a manner
> > that is invisible to users [non-implementer Ada programmers] is a good
> > way to ensure that the tools are used. (e.g. the Ada compiler does
> > automatically what C's Lint did, and is much better for it. [Most of the
> > C programmers I knew in college *never* used lint.])
> 
> Right, because it is a tool you could use or not. In Ada type 
> declarations must be there, so it is not a tool, but an integral part of 
> the language. This is why "pre"-aspects is a non-starter even ignoring 
> their semantic consistency issues. You can do things with or without 
> them. Psychologically it won't work.

See? Right there, read my first sentence in that paragraph again.
Here, I'll even quote it for you:

> Integrating these useful technologies into the compiler in a manner that
> is invisible to users [non-implementer Ada programmers] is a good way to
> ensure that the tools are used.


> > It's relevant because it is exactly showing how to represent
> > restrictions [exclusions] on values (within a set); and, as we know, a
> > type is a set of values and a set of operations acting on those values.
> > -- This maps directly to Ada, given the LRM's definition of subtypes.
> 
> Well, but first it is an implementation issue, as such, of a very 
> secondary order to the question of constrained types and other means to 
> create new types.

It seems like something's being lost in translation. Let me try restating it:
* The thread asks about implementation of a particular concept.
* The topic of the thread is of the implementation of a concept similar to the paper's.
* The question posed at the start of this thread is about how to deal with representing the quality of Ada's subtypes as "a possibly empty set of constraints on a value".
* Ada now has two syntactic methods of adding constraints to subtypes, the topic of the thread is how to represent these in a uniform manner.
* The post is about how there ought to be a representation of the removal of values from a type which is suitable for all methods of expressing that concept in Ada.

> Secondly arbitrary constraints is low level and thus a bad idea to
> introduce into the type system, as dynamic predicates promptly
> illustrate. Resemblance to Ada 83 subtypes is only superficial.

No, it's not superficial.
Here's why: I'm using the actual definitions of the LRM; it is quite clear that predicates on subtypes do the same basic function that range-constraints do: eliminating possible values from the parent-type's set of possible values.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 15/12/2016 15:34, Shark8 wrote:
> On Thursday, December 15, 2016 at 1:41:50 AM UTC-7, Dmitry A. Kazakov wrote:

> See? Right there, read my first sentence in that paragraph again.
> Here, I'll even quote it for you:
>
>> Integrating these useful technologies into the compiler in a manner that
>> is invisible to users [non-implementer Ada programmers] is a good way to
>> ensure that the tools are used.

This can mean or apply to just anything.

>>> It's relevant because it is exactly showing how to represent
>>> restrictions [exclusions] on values (within a set); and, as we know, a
>>> type is a set of values and a set of operations acting on those values.
>>> -- This maps directly to Ada, given the LRM's definition of subtypes.
>>
>> Well, but first it is an implementation issue, as such, of a very
>> secondary order to the question of constrained types and other means to
>> create new types.
>
> It seems like something's being lost in translation. Let me try restating it:
> * The thread asks about implementation of a particular concept.
> * The topic of the thread is of the implementation of a concept similar to the paper's.
> * The question posed at the start of this thread is about how to deal with representing the quality of Ada's subtypes as "a possibly empty set of constraints on a value".
> * Ada now has two syntactic methods of adding constraints to subtypes, the topic of the thread is how to represent these in a uniform manner.
> * The post is about how there ought to be a representation of the removal of values from a type which is suitable for all methods of expressing that concept in Ada.

Nothing was lost.

- The concept is wrong.
- Implementation is of little or no interest.
- Representation is no issue.
- Ada's dynamic predicates was a mistake.
- Type specialization must be supported by more high-level and 
consistent means (especially with ADT and separation of interfaces).

>> Secondly arbitrary constraints is low level and thus a bad idea to
>> introduce into the type system, as dynamic predicates promptly
>> illustrate. Resemblance to Ada 83 subtypes is only superficial.
>
> No, it's not superficial.
> Here's why: I'm using the actual definitions of the LRM; it is quite
> clear that predicates on subtypes do the same basic function that
> range-constraints do: eliminating possible values from the parent-type's
> set of possible values.

I tried to explain why they are different on many levels.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Shark8]

On Thursday, December 15, 2016 at 7:53:59 AM UTC-7, Dmitry A. Kazakov wrote:
> On 15/12/2016 15:34, Shark8 wrote:
> >
> > It seems like something's being lost in translation. Let me try restating it:
> > * The thread asks about implementation of a particular concept.
> > * The topic of the thread is of the implementation of a concept similar to the paper's.
> > * The question posed at the start of this thread is about how to deal with representing the quality of Ada's subtypes as "a possibly empty set of constraints on a value".
> > * Ada now has two syntactic methods of adding constraints to subtypes, the topic of the thread is how to represent these in a uniform manner.
> > * The post is about how there ought to be a representation of the removal of values from a type which is suitable for all methods of expressing that concept in Ada.
> 
> Nothing was lost.

I beg to differ, as shown by your following list:

> 
> - The concept is wrong.

The concept of (a) a type consisting of two parts (1) a set of values, and (b) a set of operations upon those values; or (b) that there ought to be a way to represent constraints on the values that a type can use?

> - Implementation is of little or no interest.

Given that the topic of the thread is inimitably concerned with implementation you are manifestly wrong, at least insofar as this thread is concerned.

> - Representation is no issue.

It is in the case of an intermediate representation.

> - Ada's dynamic predicates was a mistake.

Irrelevant to the question the thread poses.

> - Type specialization must be supported by more high-level and 
> consistent means (especially with ADT and separation of interfaces).

That's a different issue altogether.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 15/12/2016 23:34, Shark8 wrote:
>> - The concept is wrong.
>
> The concept of (a) a type consisting of two parts (1) a set of
> values,  and (b) a set of operations upon those values;

The notion of type violated arbitrary constraining violates.

> or (b) that there ought
> to be a way to represent constraints on the values that a type can use?

Right, as it is in plain contradiction with both the definition of a 
type you quoted as well as with the concept of static types.

There is no need to represent constraints on the type values unless for 
a debugger, maybe.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Shark8]

On Friday, December 16, 2016 at 1:28:55 AM UTC-7, Dmitry A. Kazakov wrote:
> On 15/12/2016 23:34, Shark8 wrote:
> >> - The concept is wrong.
> >
> > The concept of (a) a type consisting of two parts (1) a set of
> > values,  and (b) a set of operations upon those values;
> 
> The notion of type violated arbitrary constraining violates.

What?

> 
> > or (b) that there ought
> > to be a way to represent constraints on the values that a type can use?
> 
> Right, as it is in plain contradiction with both the definition of a 
> type you quoted as well as with the concept of static types.

Ada specifiably has the ability to add a constraint -- like RANGE 1..INTEGER'LAST -- and has had that from its inception. *THAT* is Ada's notion of subtype.

The question of the thread is about representing such constraints.

Re: Ada 2012 Constraints (WRT an Ada IR)

[G.B.]

On 13/12/2016 22:11, Dmitry A. Kazakov wrote:

>> Right, Pre aspects are *not* body!
>
> They are being executed at run time.

Actually, Pre aspects do not need to be executed at run-time.
Nor do they need to be part of "the program" if checking, so
not part of a body there. But they can be physically separate,
so they could even be prevented from having side effects.
Like the source of an interrupt that can be blocked.


> But Ada expression A>B is not a predicate

To any programmer concerned with the intent of ">", i.e. not
with the LRM exegesis of operation ">", nor with some "unruly"
user defined ">", etc. I bet that "A>B" is a sentence that has
two variables, universally quantified, the universe being T.
T is the type of both A and B and has the set of values for both
A and B.

So, as far as contract based programming by programmers goes,

    Pre => A > B

is to mean that

   (forall A)(forall B)[A in T -> (B in T -> A > B)]

SHALL be true so that the client gets what it deserves.
Including the effects of unruly ">" if that Pre is checked
somehow, somewhere, but that's for human lawyers and contract
law because a failure (a) needs to be attributed, and (b) can
actually be attributed: There is a contract stating Pre.

>> I only asked for a relation between A and B as inputs to Plus_Too.
>
> No, you asked for an Ada program that evaluates a relation in connection with the semantics of Plus_To.

And ... see above.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 14/12/2016 13:21, G.B. wrote:
> On 13/12/2016 22:11, Dmitry A. Kazakov wrote:

> So, as far as contract based programming by programmers goes,
>
>    Pre => A > B
>
> is to mean that
>
>   (forall A)(forall B)[A in T -> (B in T -> A > B)]
>
> SHALL be true so that the client gets what it deserves.

Then it is

    SHALL ((forall A)(forall B)[A in T -> (B in T -> A > B)] |= True)

By no means this is an Ada expression.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[G.B.]

On 14/12/2016 13:55, Dmitry A. Kazakov wrote:
> On 14/12/2016 13:21, G.B. wrote:
>> On 13/12/2016 22:11, Dmitry A. Kazakov wrote:
>
>> So, as far as contract based programming by programmers goes,
>>
>>    Pre => A > B
>>
>> is to mean that
       ^^^^^^^
>>
>>   (forall A)(forall B)[A in T -> (B in T -> A > B)]
>>
>> SHALL be true so that the client gets what it deserves.
>
> Then it is
>
>    SHALL ((forall A)(forall B)[A in T -> (B in T -> A > B)] |= True)
>
> By no means this is an Ada expression.

But reasonably close to a quantified expression that must
be true, in case one is needed in place of just "A > B".

If Pre => A > B means something to Ada programmers while
following their contractual obligations, I don't think it is that
all A>B entails True. Nor need the Post aspect be ignored
as a source both for developing an implementation, and refining
Pre.  If we do know what must be true for an implementation
to produce a desired result, though, it will be negligent to not
say so and instead start operations anyway.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 2016-12-14 17:21, G.B. wrote:
> On 14/12/2016 13:55, Dmitry A. Kazakov wrote:
>> On 14/12/2016 13:21, G.B. wrote:
>>> On 13/12/2016 22:11, Dmitry A. Kazakov wrote:
>>
>>> So, as far as contract based programming by programmers goes,
>>>
>>>    Pre => A > B
>>>
>>> is to mean that
>       ^^^^^^^
>>>
>>>   (forall A)(forall B)[A in T -> (B in T -> A > B)]
>>>
>>> SHALL be true so that the client gets what it deserves.
>>
>> Then it is
>>
>>    SHALL ((forall A)(forall B)[A in T -> (B in T -> A > B)] |= True)
>>
>> By no means this is an Ada expression.
>
> But reasonably close to a quantified expression that must
> be true, in case one is needed in place of just "A > B".
>
> If Pre => A > B means something to Ada programmers while
> following their contractual obligations, I don't think it is that
> all A>B entails True. Nor need the Post aspect be ignored
> as a source both for developing an implementation, and refining
> Pre.  If we do know what must be true for an implementation
> to produce a desired result, though, it will be negligent to not
> say so and instead start operations anyway.

You cannot say it in Ada, as the example shows. You must do that in 
English or in SPARK or in any other language where you can *spell* it. 
In Ada you cannot.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[G.B.]

On 14/12/2016 17:55, Dmitry A. Kazakov wrote:
> You cannot say it in Ada, as the example shows. You must do that in English or in SPARK or in any other language where you can *spell* it. In Ada you cannot.

It?  Boolean expressions or expressions about Boolean
expressions? Rules of inference? Proofs? Why? A contract
does not argue.

Automatic quantifiers are obviously present when A and B
are parameters, and they are of a MUST kind if the programmer
doesn't reduce them in rank to SHALL or MAY by controlling
checking, say.

  function ... (A, B: T) return ...
   with
    Pre => A > B;

Pre is meant to hold for *any* pair of values A and B, to be
passed to the function. So the programmer can infer a universal
requirement.

It is of no concern how any tool or any programmer arrives
at Pre. If he arrives at Pre => True, then this can be
well-reasoned. Does the client programmer care?

Re: Ada 2012 Constraints (WRT an Ada IR)

[Shark8]

On Tuesday, December 13, 2016 at 4:19:17 AM UTC-7, Dmitry A. Kazakov wrote:
> On 13/12/2016 11:39, G.B. wrote:
> >
> > Pre doesn't have to be object language as has now been
> > said and confirmed a number of times.
> 
> Being a part of the body it does not belong to declarations.

By that logic we shouldn't have something like:
    type Item is null record;            -- Stub
    type Pointer is access Item;         -- Access type
    subtype Handle is not null Pointer;  -- Subtype excluding null
    
    Procedure Something(Object : Handle); -- Object can't be null.
because we could instead say:
    Procedure Something(Object : Pointer) is
    begin
      if Object = Null then --...
    end;

Or, really, any subtype.

> >> It is an explicit contract.
> >
> > Can you make it a Boolean expression?
> 
> That depends on the language in question. It is not an expression in Ada 
> and cannot be made one.

But this works against your whole anti-pre, anti-post, anti-aspect argument... those *ARE* [generally] Ada Boolean expressions.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 2016-12-13 19:25, Shark8 wrote:
> On Tuesday, December 13, 2016 at 4:19:17 AM UTC-7, Dmitry A. Kazakov wrote:
>> On 13/12/2016 11:39, G.B. wrote:
>>>
>>> Pre doesn't have to be object language as has now been
>>> said and confirmed a number of times.
>>
>> Being a part of the body it does not belong to declarations.
>
> By that logic we shouldn't have something like:
>     type Item is null record;            -- Stub
>     type Pointer is access Item;         -- Access type
>     subtype Handle is not null Pointer;  -- Subtype excluding null
>
>     Procedure Something(Object : Handle); -- Object can't be null.
> because we could instead say:
>     Procedure Something(Object : Pointer) is
>     begin
>       if Object = Null then --...
>     end;
>
> Or, really, any subtype.

No. Type/subtype declarations are expressions involving type-algebraic 
operations [some operands are types, results are types].

You cannot use them in the bodies. They implicitly define operations of 
the resulting type and the corresponding bodies. This has nothing to do 
with the bodies defined explicitly in the declarative region by the 
programmer.

You could point at:

    overriding procedure Foo (X : Bar) is null;

That would be right, and I would wholeheartedly agree that this is 
against the principle of implementation separation.

>>>> It is an explicit contract.
>>>
>>> Can you make it a Boolean expression?
>>
>> That depends on the language in question. It is not an expression in Ada
>> and cannot be made one.
>
> But this works against your whole anti-pre, anti-post, anti-aspect
> argument... those *ARE* [generally] Ada Boolean expressions.

They are not, what was meant would be a predicate, spelled fully:

    forall a > b, a in T, b in T  exist n in N
    a = b * n + a rem b

It is not a Boolean expression and it cannot be written or evaluated in 
Ada. Though it is possible to write a program in Ada that would perform 
calculus on such expressions, e.g. SPARK.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Shark8]

On Tuesday, December 13, 2016 at 2:11:56 PM UTC-7, Dmitry A. Kazakov wrote:
> On 2016-12-13 19:25, Shark8 wrote:
> > On Tuesday, December 13, 2016 at 4:19:17 AM UTC-7, Dmitry A. Kazakov wrote:
> >> On 13/12/2016 11:39, G.B. wrote:
> >>>
> >>> Pre doesn't have to be object language as has now been
> >>> said and confirmed a number of times.
> >>
> >> Being a part of the body it does not belong to declarations.
> >
> > By that logic we shouldn't have something like:
> >     type Item is null record;            -- Stub
> >     type Pointer is access Item;         -- Access type
> >     subtype Handle is not null Pointer;  -- Subtype excluding null
> >
> >     Procedure Something(Object : Handle); -- Object can't be null.
> > because we could instead say:
> >     Procedure Something(Object : Pointer) is
> >     begin
> >       if Object = Null then --...
> >     end;
> >
> > Or, really, any subtype.
> 
> No. Type/subtype declarations are expressions involving type-algebraic 
> operations [some operands are types, results are types].
 
And now we're back to the question I presented illustrating the thrust of this thread* with the P0, P1, P2, & P3 examples.


> You cannot use them in the bodies. They implicitly define operations of 
> the resulting type and the corresponding bodies.

Nope.
Ada 83 LRM (3.3.2) says, in part:
"A type mark denotes a type or a subtype. If a type mark is the name of a type, the type mark denotes this type and also the corresponding unconstrained subtype. The base type of a type mark is, by definition, the base type of the type or subtype denoted by the type mark."

And (3.3) says, as its very first sentence:
"A type is characterized by a set of values and a set of operations."

It is therefore *MOT* the subtype which defines the operations.

> This has nothing to do 
> with the bodies defined explicitly in the declarative region by the 
> programmer.

I never claimed it did -- just that your reasoning would carry over to spec/body as shown.

> > But this works against your whole anti-pre, anti-post, anti-aspect
> > argument... those *ARE* [generally] Ada Boolean expressions.
> 
> They are not, what was meant would be a predicate, spelled fully:
> 
>     forall a > b, a in T, b in T  exist n in N
>     a = b * n + a rem b
> 
> It is not a Boolean expression and it cannot be written or evaluated in 
> Ada. Though it is possible to write a program in Ada that would perform 
> calculus on such expressions, e.g. SPARK.

I agree that SPARK is all about doing those proofs... but what are (for all x in Y => ...) about then if not to facilitate this sort of thing?


* Namely: what is a good way to define constraints that can generally be applied to all forms of Ada 2012.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 13/12/2016 23:32, Shark8 wrote:
> On Tuesday, December 13, 2016 at 2:11:56 PM UTC-7, Dmitry A. Kazakov wrote:
>> On 2016-12-13 19:25, Shark8 wrote:
>>> On Tuesday, December 13, 2016 at 4:19:17 AM UTC-7, Dmitry A. Kazakov wrote:
>>>> On 13/12/2016 11:39, G.B. wrote:
>>>>>
>>>>> Pre doesn't have to be object language as has now been
>>>>> said and confirmed a number of times.
>>>>
>>>> Being a part of the body it does not belong to declarations.
>>>
>>> By that logic we shouldn't have something like:
>>>     type Item is null record;            -- Stub
>>>     type Pointer is access Item;         -- Access type
>>>     subtype Handle is not null Pointer;  -- Subtype excluding null
>>>
>>>     Procedure Something(Object : Handle); -- Object can't be null.
>>> because we could instead say:
>>>     Procedure Something(Object : Pointer) is
>>>     begin
>>>       if Object = Null then --...
>>>     end;
>>>
>>> Or, really, any subtype.
>>
>> No. Type/subtype declarations are expressions involving type-algebraic
>> operations [some operands are types, results are types].
>
> And now we're back to the question I presented illustrating the
> thrust  of this thread* with the P0, P1, P2, & P3 examples.

Why? Of course you can define a type by providing operation's body in a 
declaration. The objection was: it is bad language design. That point 
stands. Others tried to argue that such bodies are not bodies but 
magically "preconditions". No, they are still bodies, just misplaced ones.

>> You cannot use them in the bodies. They implicitly define operations of
>> the resulting type and the corresponding bodies.
>
> Nope.
> Ada 83 LRM (3.3.2) says, in part:
> "A type mark denotes a type or a subtype. If a type mark is the name
> of a type, the type mark denotes this type and also the corresponding
> unconstrained subtype. The base type of a type mark is, by definition,
> the base type of the type or subtype denoted by the type mark."
>
> And (3.3) says, as its very first sentence:
> "A type is characterized by a set of values and a set of operations."
>
> It is therefore *MOT* the subtype which defines the operations.

There was a discussion on this topic in c.l.a. before. A subtype *is* a 
type, regardless how you read ARM. The proof is simple, a subtype has 
some operations that behave differently than ones of the unconstrained 
parent type, e.g. they raise Constraint_Error. Different operations, 
ergo different type.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:o2r1ca$184u$1@gioia.aioe.org...
...
> Others tried to argue that such bodies are not bodies but magically 
> "preconditions". No, they are still bodies, just misplaced ones.

Body /= implementation!! (Using "implementation" here in your sense as the 
entire execution of a subprogram.) A body is just the hidden part of the 
implementation; the part that is exposed to callers includes constraint, 
null exclusion, and predicate checks, and the precondition. The caller has a 
need to know about part of the implementation, and hopefully not about the 
rest. Exactly where the split between the specification and the body goes 
clearly depends on a need to know basis, and it has nothing to do with 
whether it is static or dynamic or provable.

                           Randy.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 14/12/2016 23:53, Randy Brukardt wrote:
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
> news:o2r1ca$184u$1@gioia.aioe.org...
> ...
>> Others tried to argue that such bodies are not bodies but magically
>> "preconditions". No, they are still bodies, just misplaced ones.
>
> Body /= implementation!! (Using "implementation" here in your sense as the
> entire execution of a subprogram.) A body is just the hidden part of the
> implementation; the part that is exposed to callers includes constraint,
> null exclusion, and predicate checks, and the precondition. The caller has a
> need to know about part of the implementation, and hopefully not about the
> rest. Exactly where the split between the specification and the body goes
> clearly depends on a need to know basis, and it has nothing to do with
> whether it is static or dynamic or provable.

This pretty good summarizes why I consider it such a bad idea.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:o2tl62$1aro$1@gioia.aioe.org...
> On 14/12/2016 23:53, Randy Brukardt wrote:
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>> news:o2r1ca$184u$1@gioia.aioe.org...
>> ...
>>> Others tried to argue that such bodies are not bodies but magically
>>> "preconditions". No, they are still bodies, just misplaced ones.
>>
>> Body /= implementation!! (Using "implementation" here in your sense as 
>> the
>> entire execution of a subprogram.) A body is just the hidden part of the
>> implementation; the part that is exposed to callers includes constraint,
>> null exclusion, and predicate checks, and the precondition. The caller 
>> has a
>> need to know about part of the implementation, and hopefully not about 
>> the
>> rest. Exactly where the split between the specification and the body goes
>> clearly depends on a need to know basis, and it has nothing to do with
>> whether it is static or dynamic or provable.
>
> This pretty good summarizes why I consider it such a bad idea.

The only alternative is to get rid of the separation of specifications and 
bodies (many languages do exactly that). Then you don't need any kind of 
contract.

Contracts that are too weak don't help; if a prover (or programmer!) has to 
look into the implementation  (and that would necessarily be the case in 
your model), then there is no real separation.

                             Randy.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 15/12/2016 23:19, Randy Brukardt wrote:
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
> news:o2tl62$1aro$1@gioia.aioe.org...
>> On 14/12/2016 23:53, Randy Brukardt wrote:
>>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>>> news:o2r1ca$184u$1@gioia.aioe.org...
>>> ...
>>>> Others tried to argue that such bodies are not bodies but magically
>>>> "preconditions". No, they are still bodies, just misplaced ones.
>>>
>>> Body /= implementation!! (Using "implementation" here in your sense as the
>>> entire execution of a subprogram.) A body is just the hidden part of the
>>> implementation; the part that is exposed to callers includes constraint,
>>> null exclusion, and predicate checks, and the precondition. The caller
>>> has a need to know about part of the implementation, and hopefully not about
>>> the rest. Exactly where the split between the specification and the body goes
>>> clearly depends on a need to know basis, and it has nothing to do with
>>> whether it is static or dynamic or provable.
>>
>> This pretty good summarizes why I consider it such a bad idea.
>
> The only alternative is to get rid of the separation of specifications and
> bodies (many languages do exactly that). Then you don't need any kind of
> contract.

Exactly the opposite. Body /= implementation stance is getting rid of 
the separation. And Ada is well along that path since Ada 05.

> Contracts that are too weak don't help; if a prover (or programmer!) has to
> look into the implementation  (and that would necessarily be the case in
> your model), then there is no real separation.

Surely they help. Moreover it is very important not to have to strong 
contracts. The contract strength is how much the contract determines the 
implementation. Too strong contracts prevent substitutability and thus 
code reuse. Since any modification of a type breaks something somewhere. 
Which is why contracts are relaxed in order to allow a range of 
implementations, e.g. raising and handling exceptions etc. 
Overspecification is a bad as underspecification.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:o3095a$1f4q$1@gioia.aioe.org...
> On 15/12/2016 23:19, Randy Brukardt wrote:
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>> news:o2tl62$1aro$1@gioia.aioe.org...
>>> On 14/12/2016 23:53, Randy Brukardt wrote:
>>>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>>>> news:o2r1ca$184u$1@gioia.aioe.org...
>>>> ...
>>>>> Others tried to argue that such bodies are not bodies but magically
>>>>> "preconditions". No, they are still bodies, just misplaced ones.
>>>>
>>>> Body /= implementation!! (Using "implementation" here in your sense as 
>>>> the
>>>> entire execution of a subprogram.) A body is just the hidden part of 
>>>> the
>>>> implementation; the part that is exposed to callers includes 
>>>> constraint,
>>>> null exclusion, and predicate checks, and the precondition. The caller
>>>> has a need to know about part of the implementation, and hopefully not 
>>>> about
>>>> the rest. Exactly where the split between the specification and the 
>>>> body goes
>>>> clearly depends on a need to know basis, and it has nothing to do with
>>>> whether it is static or dynamic or provable.
>>>
>>> This pretty good summarizes why I consider it such a bad idea.
>>
>> The only alternative is to get rid of the separation of specifications 
>> and
>> bodies (many languages do exactly that). Then you don't need any kind of
>> contract.
>
> Exactly the opposite. Body /= implementation stance is getting rid of the 
> separation. And Ada is well along that path since Ada 05.

The path was that set by Ada 83 with the idea of constraints. By your model, 
constraint checks belong to the implementation, and those have always been 
exposed in the specification. Later versions of Ada have just built on this 
already existing (and very successful) idea, extending it to further cases.

>> Contracts that are too weak don't help; if a prover (or programmer!) has 
>> to
>> look into the implementation  (and that would necessarily be the case in
>> your model), then there is no real separation.
>
> Surely they help. Moreover it is very important not to have to strong 
> contracts. The contract strength is how much the contract determines the 
> implementation. Too strong contracts prevent substitutability and thus 
> code reuse. Since any modification of a type breaks something somewhere. 
> Which is why contracts are relaxed in order to allow a range of 
> implementations, e.g. raising and handling exceptions etc. 
> Overspecification is a bad as underspecification.

True enough. But irrelevant unless you're arguing for weak typing (and I 
know you're not doing that).

                              Randy.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 2016-12-16 20:51, Randy Brukardt wrote:
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
> news:o3095a$1f4q$1@gioia.aioe.org...
>> On 15/12/2016 23:19, Randy Brukardt wrote:
>>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>>> news:o2tl62$1aro$1@gioia.aioe.org...
>>>> On 14/12/2016 23:53, Randy Brukardt wrote:
>>>>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>>>>> news:o2r1ca$184u$1@gioia.aioe.org...
>>>>> ...
>>>>>> Others tried to argue that such bodies are not bodies but magically
>>>>>> "preconditions". No, they are still bodies, just misplaced ones.
>>>>>
>>>>> Body /= implementation!! (Using "implementation" here in your sense as
>>>>> the
>>>>> entire execution of a subprogram.) A body is just the hidden part of
>>>>> the
>>>>> implementation; the part that is exposed to callers includes
>>>>> constraint,
>>>>> null exclusion, and predicate checks, and the precondition. The caller
>>>>> has a need to know about part of the implementation, and hopefully not
>>>>> about
>>>>> the rest. Exactly where the split between the specification and the
>>>>> body goes
>>>>> clearly depends on a need to know basis, and it has nothing to do with
>>>>> whether it is static or dynamic or provable.
>>>>
>>>> This pretty good summarizes why I consider it such a bad idea.
>>>
>>> The only alternative is to get rid of the separation of specifications and
>>> bodies (many languages do exactly that). Then you don't need any kind of
>>> contract.
>>
>> Exactly the opposite. Body /= implementation stance is getting rid of the
>> separation. And Ada is well along that path since Ada 05.
>
> The path was that set by Ada 83 with the idea of constraints. By your model,
> constraint checks belong to the implementation, and those have always been
> exposed in the specification.

Not explicitly. It is like the implementation of "+" when an integer 
type declared. The implementation is assumed but not specified.

> Later versions of Ada have just built on this
> already existing (and very successful) idea, extending it to further cases.

I meant explicit code snippets in declarations, which includes "is 
null", checks, etc.

It is very different from having type operations producing new 
[sub]types like

    subtype Y is X range 1..100;

or

    type T is array (I) of E;

They declare and implement operations implicitly.

>>> Contracts that are too weak don't help; if a prover (or programmer!) has
>>> to look into the implementation  (and that would necessarily be the case in
>>> your model), then there is no real separation.
>>
>> Surely they help. Moreover it is very important not to have to strong
>> contracts. The contract strength is how much the contract determines the
>> implementation. Too strong contracts prevent substitutability and thus
>> code reuse. Since any modification of a type breaks something somewhere.
>> Which is why contracts are relaxed in order to allow a range of
>> implementations, e.g. raising and handling exceptions etc.
>> Overspecification is a bad as underspecification.
>
> True enough. But irrelevant unless you're arguing for weak typing (and I
> know you're not doing that).

Typing is an example of usefulness of weak contracts. You just match 
types and ignore the rest.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:o32vjg$1jv4$1@gioia.aioe.org...
> On 2016-12-16 20:51, Randy Brukardt wrote:
...
>> The path was that set by Ada 83 with the idea of constraints. By your 
>> model,
>> constraint checks belong to the implementation, and those have always 
>> been
>> exposed in the specification.
>
> Not explicitly. It is like the implementation of "+" when an integer type 
> declared. The implementation is assumed but not specified.

Explicitly, by the semantic model I quoted earlier.

>> Later versions of Ada have just built on this
>> already existing (and very successful) idea, extending it to further 
>> cases.
>
> I meant explicit code snippets in declarations, which includes "is null", 
> checks, etc.
>
> It is very different from having type operations producing new [sub]types 
> like
>
>    subtype Y is X range 1..100;
>
> or
>
>    type T is array (I) of E;
>
> They declare and implement operations implicitly.

Only in your world-view, not the official Ada semantics, for a subtype. 
Operations are only declared for a type, not a subtype (and the location of 
declaration matters).

And I'm not sure why
    subtype Y is X range 1 .. 100;
is OK and
    subtype Z is X with Static_Predicate => Z > 0;
is not. They both have explicit declarations of the subtype, and the 
semantics is effectively the same.

                              Randy.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 2016-12-19 23:33, Randy Brukardt wrote:
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
> news:o32vjg$1jv4$1@gioia.aioe.org...
>> On 2016-12-16 20:51, Randy Brukardt wrote:
> ...
>>> The path was that set by Ada 83 with the idea of constraints. By your
>>> model,
>>> constraint checks belong to the implementation, and those have always
>>> been
>>> exposed in the specification.
>>
>> Not explicitly. It is like the implementation of "+" when an integer type
>> declared. The implementation is assumed but not specified.
>
> Explicitly, by the semantic model I quoted earlier.
>
>>> Later versions of Ada have just built on this
>>> already existing (and very successful) idea, extending it to further
>>> cases.
>>
>> I meant explicit code snippets in declarations, which includes "is null",
>> checks, etc.
>>
>> It is very different from having type operations producing new [sub]types
>> like
>>
>>    subtype Y is X range 1..100;
>>
>> or
>>
>>    type T is array (I) of E;
>>
>> They declare and implement operations implicitly.
>
> Only in your world-view,

Sure.

> not the official Ada semantics, for a subtype.

Which must be fixed.

> Operations are only declared for a type, not a subtype (and the location of
> declaration matters).
>
> And I'm not sure why
>     subtype Y is X range 1 .. 100;
> is OK and
>     subtype Z is X with Static_Predicate => Z > 0;
> is not. They both have explicit declarations of the subtype, and the
> semantics is effectively the same.

The former declares a continuous range from which the semantics of 
numeric operations and attributes can be deduced. For the later, nobody 
has any idea without looking at the expression = implementation.

"Effectively same" is meaningless on its own. The generated object code 
is "effectively same" too.

As I said, it is low-level and useless from SW design POV. You must be 
able to answer questions like if you used Z in an algorithm of X, would 
it work? If not, how, when, where etc. A range allows answering such 
questions, an arbitrary constraint does not. The only things deducible 
from an arbitrary constraint are assignment and equality comparison. 
Already enumeration types have more operations than these.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Shark8]

On Tuesday, December 20, 2016 at 4:00:57 AM UTC-7, Dmitry A. Kazakov wrote:
> On 2016-12-19 23:33, Randy Brukardt wrote:
> > "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
> > news:o32vjg$1jv4$1@gioia.aioe.org...
> >> On 2016-12-16 20:51, Randy Brukardt wrote:
> > ...
> >>> The path was that set by Ada 83 with the idea of constraints. By your
> >>> model,
> >>> constraint checks belong to the implementation, and those have always
> >>> been
> >>> exposed in the specification.
> >>
> >> Not explicitly. It is like the implementation of "+" when an integer type
> >> declared. The implementation is assumed but not specified.
> >
> > Explicitly, by the semantic model I quoted earlier.
> >
> >>> Later versions of Ada have just built on this
> >>> already existing (and very successful) idea, extending it to further
> >>> cases.
> >>
> >> I meant explicit code snippets in declarations, which includes "is null",
> >> checks, etc.
> >>
> >> It is very different from having type operations producing new [sub]types
> >> like
> >>
> >>    subtype Y is X range 1..100;
> >>
> >> or
> >>
> >>    type T is array (I) of E;
> >>
> >> They declare and implement operations implicitly.
> >
> > Only in your world-view,
> 
> Sure.
> 
> > not the official Ada semantics, for a subtype.
> 
> Which must be fixed.

No, it doesn't.
Ada's notion/definition of "subtype" is rational, reasonable, and useful.

This doesn't change the fact that CS/OOP "subtype" is also a useful definition, but they are separate, distinct, and different.

A *LOT* of you communication problems on the matter stem from your refusal to "talk in Ada" (use its definitions) -- as illustrates by Randy pointing out that section in the RM which specifies a call with arguments violating the subtype never execute the body.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:o3b316$153k$2@gioia.aioe.org...
> On 2016-12-19 23:33, Randy Brukardt wrote:
...
>> And I'm not sure why
>>     subtype Y is X range 1 .. 100;
>> is OK and
>>     subtype Z is X with Static_Predicate => Z > 0;
>> is not. They both have explicit declarations of the subtype, and the
>> semantics is effectively the same.
>
> The former declares a continuous range from which the semantics of numeric 
> operations and attributes can be deduced. For the later, nobody has any 
> idea without looking at the expression = implementation.

The expression is just a poor way of describing a set. I wanted to call 
these set constraints with appropriate set syntax, but I lost that argument. 
The semantics is the same either way. It's unlikely that a compiler would 
execute this expression as-is when making a check; it's most likely going to 
be making a set check.

> "Effectively same" is meaningless on its own. The generated object code is 
> "effectively same" too.

I said "effectively the same" because there are subtle wording differences 
which only matter in a few cases. Had we had first-class set constraints, 
we'd have had the same rules (as we didn't want to support discontigous 
arrays).

So far as the set of operations and reasoning goes, there's no difference 
between reasoning for a set and for a single range (which is just a subset 
of a set anyway).

> As I said, it is low-level and useless from SW design POV. You must be 
> able to answer questions like if you used Z in an algorithm of X, would it 
> work? If not, how, when, where etc. A range allows answering such 
> questions, an arbitrary constraint does not.

A static_predicate is not an *arbitrary* constraint. It's restricted to 
expressions that can easily be represented as a set with a small number of 
ranges. One certainly can reason about it.

(A dynamic_predicate is just an assertion that gets automatically placed at 
type conversions, quite a different thing. [There's a reason the names are 
different!] But my understanding is that provers are quite happy to use 
assertions in their proofs. Even so, I specifically was not talking about 
them.)

                                            Randy.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 2016-12-21 01:59, Randy Brukardt wrote:
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
> news:o3b316$153k$2@gioia.aioe.org...
>> On 2016-12-19 23:33, Randy Brukardt wrote:
> ...
>>> And I'm not sure why
>>>     subtype Y is X range 1 .. 100;
>>> is OK and
>>>     subtype Z is X with Static_Predicate => Z > 0;
>>> is not. They both have explicit declarations of the subtype, and the
>>> semantics is effectively the same.
>>
>> The former declares a continuous range from which the semantics of numeric
>> operations and attributes can be deduced. For the later, nobody has any
>> idea without looking at the expression = implementation.
>
> The expression is just a poor way of describing a set.

It is not about the way you specifying a set it is about what properties 
the parent's mathematical structure retains on that set. If the set is 
any, the answer is just none.

>> "Effectively same" is meaningless on its own. The generated object code is
>> "effectively same" too.
>
> I said "effectively the same" because there are subtle wording differences
> which only matter in a few cases. Had we had first-class set constraints,
> we'd have had the same rules (as we didn't want to support discontigous
> arrays).
>
> So far as the set of operations and reasoning goes, there's no difference
> between reasoning for a set and for a single range (which is just a subset
> of a set anyway).

It is a continuous subset. This preserves a lot of properties like being 
a convex set a,b in S => (a+b)/2 in S etc.

>> As I said, it is low-level and useless from SW design POV. You must be
>> able to answer questions like if you used Z in an algorithm of X, would it
>> work? If not, how, when, where etc. A range allows answering such
>> questions, an arbitrary constraint does not.
>
> A static_predicate is not an *arbitrary* constraint. It's restricted to
> expressions that can easily be represented as a set with a small number of
> ranges.

Implementation is irrelevant.

> One certainly can reason about it.

You can tell nothing about such subsets, they are general case subsets. 
They are worse than that, if the constraint is allowed to use non-local 
dynamic Boolean functions. That would produce non-sets.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[G.B.]

On 21/12/2016 16:56, Dmitry A. Kazakov wrote:

> It is a continuous subset. This preserves a lot of properties like being a convex set a,b in S => (a+b)/2 in S etc.

The subtype in question seems to be this:

    subtype Z_Too is
      X range X'Range  -- 1 .. 100
    with Static_Predicate => Z_Too > 0;

I see no breaks there. But the subset of floors (of buildings) in the USA,
arguably reflects normal expectations:

    subtype ZZ is
      X range X'Range
    with Static_Predicate => ZZ /= 13;

    V1 : constant ZZ := 13;  -- compiler complains

But!  The Static_Predicate is *not* meant to be defining or implementing
a type that excludes 13!  Instead, it *should* be documenting a property
of the ZZ objects that a correct algorithm is using.


A useful curiosity for users of Float, maybe,

    type F is new Float with Static_Predicate => F /= 0.0;

as in
    function A (...) return F;

Then any checking before division, like in

    V := A (...);
    if V /= 0 then
       ... W / V ...;

is truly useless.
Will it be possible, in any normal project, to write a 0.0-excluding
private type in Ada, say, thus making Static_Predicate strictly
the equivalent of redundant, with all expectations on FPT still met?


> That would produce non-sets.

At compile time? Otherwise, how can a specification of membership by
any Boolean function "produce" anything but that decision, if it does
compute a result? Also, how can one predict, from a SW design POV or
otherwise, that those "run-time sets" of subtypes do not reflect what
the engineers had been carefully designing, and documenting that way?



  

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 2016-12-21 19:26, G.B. wrote:
> On 21/12/2016 16:56, Dmitry A. Kazakov wrote:
>
>> It is a continuous subset. This preserves a lot of properties like
>> being a convex set a,b in S => (a+b)/2 in S etc.
>
> The subtype in question seems to be this:
>
>    subtype Z_Too is
>      X range X'Range  -- 1 .. 100
>    with Static_Predicate => Z_Too > 0;
>
> I see no breaks there.

It is for the compiler to see breaks, which it cannot. There is a far 
better and safer model to produce user-defined subtypes that this mess.

>> That would produce non-sets.
>
> At compile time? Otherwise, how can a specification of membership by
> any Boolean function "produce" anything but that decision, if it does
> compute a result?

When predicate is not a complete function of the argument, e.g.

    P (x) = (Integer (Clock - Epoch) mod 2) = 1

> Also, how can one predict, from a SW design POV or
> otherwise,  that those "run-time sets" of subtypes do not reflect what
> the engineers had been carefully designing, and documenting that way?

Easy. Anything contradicting results of more general frameworks, like 
logic, mathematics etc is not even considered. Engineers insisting that 
2+2=5 or doing things because the spirit of Napoleon told them so are to 
be fired and probably sent to medical examination.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[G.B.]

On 21/12/2016 22:15, Dmitry A. Kazakov wrote:

> There is a far better and safer model to produce user-defined subtypes that this mess.

Can you, please, show one?


>>> That would produce non-sets.
>>
>> At compile time? Otherwise, how can a specification of membership by
>> any Boolean function "produce" anything but that decision, if it does
>> compute a result?
>
> When predicate is not a complete function of the argument, e.g.
>
>    P (x) = (Integer (Clock - Epoch) mod 2) = 1

   Dynamic_Predicate => ... as you specified ...

produces a set, however random; this is predictable. Just like
before in older Ada, i.e., to the extent that the set of a range
constraint on S is predictable in

    procedure ... (N : Integer) is
       subtype S is Natural range 2 .. N;

Your Clock base membership stest will be more involved, whatever its
purpose might  be. It will compute a Boolean result, as long as the
inputs allow. See below.

>  Engineers insisting that 2+2=5 or doing things because the spirit of Napoleon told them so are to be fired and probably sent to medical examination.

Why does 2+2=5 apply when from a static predicate, but not when
from an Ada expression in general?

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 2016-12-22 10:54, G.B. wrote:
> On 21/12/2016 22:15, Dmitry A. Kazakov wrote:
>
>> There is a far better and safer model to produce user-defined subtypes
>> that this mess.
>
> Can you, please, show one?

You define a derived type by providing conversions from and back the 
parent type. Operations are inherited per composition with the 
conversion. The representation of the derived type's values can be any. 
That is.

When

1. the representation is same;
2. the forward conversion is
    if not P(x) then
       raise Constraint_Error;
    else
       return x;
    end if;

you get your predicate-constrained subtypes.

It is far more expressive and safer because it is a private opaque type.

> Your Clock base membership stest will be more involved, whatever its
> purpose might  be. It will compute a Boolean result, as long as the
> inputs allow. See below.

The point was about properties of the result not about whether you could 
have them.

> Why does 2+2=5 apply when from a static predicate, but not when
> from an Ada expression in general?

Ada 83 range subtype construct retained properties of the base and so 
made sense. Arbitrary predicate does make any sense, thus does not 
belong to the declarative region. You can have it in the implementation 
somewhere, no problem, but not at the language level.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[G.B.]

On 13/12/2016 22:11, Dmitry A. Kazakov wrote:
>
> They are not, what was meant would be a predicate, spelled fully:
>
>    forall a > b, a in T, b in T  exist n in N
>    a = b * n + a rem b
>
> It is not a Boolean expression and it cannot be written or evaluated in Ada. Though it is possible to write a program in Ada that would perform calculus on such expressions, e.g. SPARK.

I'm not exactly sure which set you are referring to, and why.
A theory of remainder values is not identical with contracts,
being much more ambitious and being "meta" indeed.

It looks like rewriting something to do with McJones and Stepanov
and `remainder` in predicates only, possibly defining a result set,
where

   b in what you have written may be 0 in "a rem b",
      also negative.
   N, if the natural numbers, is from some other domain.

Whereas I mentioned the example only because they have stated

  // Precondition: a ≥ b > 0

to then show how their `requires(ArchimedianMonoid(T))`
together with this precondition will produce a terminating
algorithm that does what it is supposed to do. Provided that
b > 0, for example.

And that statement of a precondition is something a programmer
can work with in Ada, by deriving from it a Pre aspect for
a contract.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Shark8]

On Monday, December 12, 2016 at 10:39:28 AM UTC-7, Dmitry A. Kazakov wrote:
> On 2016-12-12 16:31, G.B. wrote:
> > On 12/12/2016 09:27, Dmitry A. Kazakov wrote:
> >
> >>> I.e., the programmer writing Y (X (A, B)) has ensured that
> >>> the assumption expressed as X'Pre is actually true before
> >>> calling X.
> >>
> >> So what? Programmers program programs, and how is that related to
> >> contracts etc?
> >
> > Informing is contracts' primary purpose,
> 
> Nope. The contract's purpose is to constrain contracted parties. 
> Informing is the purpose of E-mail, newspaper etc...

They aren't exactly mutually exclusive -- consider electronic components, they have a data-sheet that both informs you of their limitations and operate within prescribed bounds when those conditions are met. (Absent manufacturing defects and wear-out, obviously.)

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 2016-12-12 20:48, Shark8 wrote:
> On Monday, December 12, 2016 at 10:39:28 AM UTC-7, Dmitry A. Kazakov wrote:
>> On 2016-12-12 16:31, G.B. wrote:
>>> On 12/12/2016 09:27, Dmitry A. Kazakov wrote:
>>>
>>>>> I.e., the programmer writing Y (X (A, B)) has ensured that
>>>>> the assumption expressed as X'Pre is actually true before
>>>>> calling X.
>>>>
>>>> So what? Programmers program programs, and how is that related to
>>>> contracts etc?
>>>
>>> Informing is contracts' primary purpose,
>>
>> Nope. The contract's purpose is to constrain contracted parties.
>> Informing is the purpose of E-mail, newspaper etc...
>
> They aren't exactly mutually exclusive -- consider electronic
> components, they have a data-sheet that both informs you of their
> limitations and operate within prescribed bounds when those conditions
> are met. (Absent manufacturing defects and wear-out, obviously.)

Add data-sheets to the list...

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Shark8]

On Monday, December 12, 2016 at 1:46:15 PM UTC-7, Dmitry A. Kazakov wrote:
> 
> Add data-sheets to the list...

Er, what list?

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 12/12/2016 22:33, Shark8 wrote:
> On Monday, December 12, 2016 at 1:46:15 PM UTC-7, Dmitry A. Kazakov wrote:
>>
>> Add data-sheets to the list...
>
> Er, what list?

The list of thing informing about something...

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Shark8]

On Tuesday, December 13, 2016 at 1:28:57 AM UTC-7, Dmitry A. Kazakov wrote:
> On 12/12/2016 22:33, Shark8 wrote:
> > On Monday, December 12, 2016 at 1:46:15 PM UTC-7, Dmitry A. Kazakov wrote:
> >>
> >> Add data-sheets to the list...
> >
> > Er, what list?
> 
> The list of thing informing about something...

Right, and isn't that list essentially [in concept] the same thing as a 'contract' in programming?

I mean I can pick up the inverter for my laptop read "Input: 100-240V 1.7A 50-60Hz / Output: 18.5V 3.5A 65W" and tell, right there, what its promising -- which is what contracts [are supposed to] do, right?

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 2016-12-13 19:53, Shark8 wrote:
> On Tuesday, December 13, 2016 at 1:28:57 AM UTC-7, Dmitry A. Kazakov wrote:
>> On 12/12/2016 22:33, Shark8 wrote:
>>> On Monday, December 12, 2016 at 1:46:15 PM UTC-7, Dmitry A. Kazakov wrote:
>>>>
>>>> Add data-sheets to the list...
>>>
>>> Er, what list?
>>
>> The list of thing informing about something...
>
> Right, and isn't that list essentially [in concept] the same thing as a 'contract' in programming?
>
> I mean I can pick up the inverter for my laptop read "Input:
> 100-240V  1.7A 50-60Hz / Output: 18.5V 3.5A 65W" and tell, right there, what its
> promising -- which is what contracts [are supposed to] do, right?

Does it inform you or your laptop? That is the difference.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Shark8]

On Tuesday, December 13, 2016 at 2:11:50 PM UTC-7, Dmitry A. Kazakov wrote:
> On 2016-12-13 19:53, Shark8 wrote:
> > I mean I can pick up the inverter for my laptop read "Input:
> > 100-240V  1.7A 50-60Hz / Output: 18.5V 3.5A 65W" and tell, right there, what its
> > promising -- which is what contracts [are supposed to] do, right?
> 
> Does it inform you or your laptop? That is the difference.

Yes.
Next question.

(Alright, a bit more serious, the promice is made in conjunction with the laptop -- insofar as the laptop is concerned as long as the 18.5V, 3.5A, 65W power comes in it's happy... much like a implementation/body, it doesn't care so long as the interface is respected.)

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 13/12/2016 23:16, Shark8 wrote:
> On Tuesday, December 13, 2016 at 2:11:50 PM UTC-7, Dmitry A. Kazakov wrote:
>> On 2016-12-13 19:53, Shark8 wrote:
>>> I mean I can pick up the inverter for my laptop read "Input:
>>> 100-240V  1.7A 50-60Hz / Output: 18.5V 3.5A 65W" and tell, right there, what its
>>> promising -- which is what contracts [are supposed to] do, right?
>>
>> Does it inform you or your laptop? That is the difference.
>
> Yes.
> Next question.
>
> (Alright, a bit more serious, the promice is made in conjunction
> with  the laptop -- insofar as the laptop is concerned as long as the 18.5V,
> 3.5A, 65W power comes in it's happy... much like a implementation/body,
> it doesn't care so long as the interface is respected.)

See, it is your concern, not the labtop's one. You are here to enforce 
the contract on both the laptop and the power supply. It is information 
for you and a contract for laptop.

If the laptop used its camera to read power supply's inscription before 
connecting itself to it, then it would be a part of laptop functionality 
and not a contract anymore. There would be some other contract in place 
of course, like that inscription in English and tells truth etc.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Paul Rubin]

"G.B." <bauhaus@notmyhomepage.invalid> writes:
> CLU uses "requires", Eiffel uses "require" for Pre,
> perhaps preventing a misunderstanding:
> Pre only happens to be descriptive in proven programs.
> Pre is really meant for programmers unconditionally.
> Pre produces a maximally informed start for programming.

I thought Eiffel contracts could be checked at either compile time or
run time.  Dijkstra's original description of preconditions didn't
involve any type of compile time checking.  Preconditions/contracts
state assumptions of the implementation, and if you can prove them,
that's great, but I don't remember hearing this was required.  Ada
certainly allows Pre=> to be checked at runtime.  I'd be interested to
know what happens if you try to compile a SPARK program with outstanding
verification conditions (proof obligations).

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 12/12/2016 00:58, Paul Rubin wrote:
> "G.B." <bauhaus@notmyhomepage.invalid> writes:
>> CLU uses "requires", Eiffel uses "require" for Pre,
>> perhaps preventing a misunderstanding:
>> Pre only happens to be descriptive in proven programs.
>> Pre is really meant for programmers unconditionally.
>> Pre produces a maximally informed start for programming.
>
> I thought Eiffel contracts could be checked at either compile time or
> run time.  Dijkstra's original description of preconditions didn't
> involve any type of compile time checking.  Preconditions/contracts
> state assumptions of the implementation, and if you can prove them,
> that's great, but I don't remember hearing this was required.

It is not required. A program is still same if nothing about it was 
proven. That is another way to say that a precondition cannot be checked 
by the program itself = preconditions are not statements of the object 
language.

> Ada certainly allows Pre=> to be checked at runtime.

Because they are not preconditions, what in Ada is falsely called 
preconditions is a part of the subprogram body. Surely you could not 
turn it off, but you could optimize it away.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[G.B.]

On 12/12/2016 09:33, Dmitry A. Kazakov wrote:
> On 12/12/2016 00:58, Paul Rubin wrote:

>> Ada certainly allows Pre=> to be checked at runtime.
>
> Because they are not preconditions,

Right, the aspect is called Pre, not Precondition. Good Thing.
The language makers aren't usually shy about using full
names, so... The Rationale outlines their intent.

> part of the subprogram body.

Does the LRM state that Pre checks must be part
of the subprogram body? I don't think so.

> Surely you could not turn it off, but you could optimize it away.

How so, if the programmer has configured Checks?

Re: Ada 2012 Constraints (WRT an Ada IR)

[G.B.]

On 12/12/2016 16:23, G.B. wrote:
> On 12/12/2016 09:33, Dmitry A. Kazakov wrote:
>> On 12/12/2016 00:58, Paul Rubin wrote:
>
>>> Ada certainly allows Pre=> to be checked at runtime.
>>
>> Because they are not preconditions,
>
> Right, the aspect is called Pre, not Precondition. Good Thing.
> The language makers aren't usually shy about using full
> names, so... The Rationale outlines their intent.

A bit more:

function F (...) return T is
    Result : T;
begin
    if DEFENSIVE_CHECK (...) then
       ...
    else
       --  hidden assumption is true
       Result := perform_algorithm(...)
    end if;
    return Result;
end F;

The above is plain old defensive programming.
I understand you want to prevent more aggressive,
DbC like programming without DEFENSIVE_CHECK
and would favor program analysis instructing the
optimizer to optimize DEFENSIVE_CHECK away if
possible. Is that right? I.e., only the compiler
is allowed to prove that DEFENSIVE_CHECK should
not be in there?

Re: Ada 2012 Constraints (WRT an Ada IR)

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:o2b79r$1dit$1@gioia.aioe.org...
> On 07/12/2016 23:26, Randy Brukardt wrote:
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>> news:o28non$1fn8$1@gioia.aioe.org...
>>> On 07/12/2016 00:15, Randy Brukardt wrote:
>> ...
>>>> Moreover, most contracts (at least the ones I'd write) raise specific
>>>> exceptions (not Assertion_Error). Indeed, this is a far better way to
>>>> define
>>>> something that raises an exception than an English comment. (Which is 
>>>> the
>>>> only other alternative for the specification - and its the 
>>>> specification
>>>> that matters, not the body.)
>>>
>>> As I said in another post it is a bad idea. The list exceptions, their
>>> names, must tell the reader when they are to propagate. You could 
>>> specify
>>> the exact condition in a few very limited cases. In a real life scenario
>>> you cannot specify the Boolean expression guarding Disk_Error. Moreover,
>>> in most cases that would be an over-specification.
>>
>> I never meant the above to be exclusive. Sometimes, as you say, an 
>> exception
>> is raised by something external to the Ada program, and that is probably
>> besst described in English. I was just talking about exceptions that 
>> depend
>> only on the parameter values.
>
> That does not change much. In most cases you still cannot do that without 
> having the expression as complex as the body itself. Instead of one 
> implementation you have two and thus you double the opportunity for making 
> an error.

One surely hopes that you aren't repeating the preconditions in the body. 
That's madness.

>>> My point is that either you don't need the expression or else it 
>>> must/can
>>> be statically provable and thus become a proper pre-/post-condition with
>>> no exceptions involved.
>>
>> Not everything can be statically proven (think Unchecked_Conversion), and 
>> a
>> lot of stuff can only be proven in a full-program scenario, so I'm 
>> dubious
>> of the above in any case. But even if that turns out to be possible years
>> from now, I'm more interested in what I can do today -- especially if it 
>> is
>> likely to be helpful to present (i.e. Codepeer) and future provers.
>
> Right
>
>> A
>> dynamic check that can be proven (or better proven and eliminated by the
tested-------------------------^^^^^
>> compiler) helps more than specifications with no machine-processable
>> description.
>
> Wrong. The proper way to do this is elevate the check into the behavior 
> and contract an exception. Later, when proofs are mature, client could 
> prove absence of the exception. Nothing lost, everybody is happy.

That's precisely what Ada 2012 contracts do. You can't leave this sort of 
behavior hidden to clients, or mixed in with the rest of the body (unless 
you have abandoned the idea of separation of specification [what the caller 
needs to know] and body [what the caller does *not* need to know]).

                         Randy.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Alejandro R. Mosteo]

On 05/12/16 09:58, Dmitry A. Kazakov wrote:
> On 05/12/2016 09:41, Stefan.Lucks@uni-weimar.de wrote:
>> On Sun, 4 Dec 2016, Robert Eachus wrote:
>
>>> I would consider it a major bug to have a pragma Assert that could
>>> fail at run-time absent a hardware failure or some such. (Even though
>>> it would be turned off in production code.)
>>
>> I don't quite think so. A failed Assert (or a failed pre- or
>> postcondition, which are essentially a nice way to put Asserts in
>> specifications) *may* be checked even in the productin system. What is
>> important is to always shut down when upon Assert-failure -- preferably
>> after writing diagnostic information to wherever digagnostics goe.
>
> A run-time "failed" Assert is an if-statement evaluating false. There is
> nothing of failure there.
>
> Things called in Ada pre- and post-conditions if evaluated during
> run-time are merely subprogram bodies booby-trapped with unanticipated
> exceptions. Bad thing.

Jumping in here for lack of a better place. I'm a bit flabbergasted (in 
a good way, I'm learning a lot) about some positions being argued. It 
seems I'm way out of league when it comes to theory of languages.

At some points it seems to me that the discussion is almost merely about 
semantics of the terms being used (precondition, predicate, etc) but 
then at other it clearly seems not:

- Pre are not preconditions (but what's the formal definition?)
- Pre/Post (aspects in general?) should not be used, or be hidden

(Apologies if I am misremembering.)

Generally speaking, I see these additions to Ada 2012 as something that 
average programmers would welcome, so it surprises me that they should 
be characterized as that problematic. At the same time, I think that 
SPARK was one of the reasons to bring them on (to make SPARK comments 
part of the static/dynamic checks?), which again seems a movement in the 
direction of reliability that Ada strives for.

Since it seems that usually is you, Dmitry, the one coming from a more 
theoretical (mathematical? purist?) POV into the arguments, perhaps you 
could recommend to me some reference(s) where I can better understand 
the principles involved in this discussion (the part about 
preconditions/predicates, not IR)? I confess to having only a 
superficial grasping of the situation, by way of using the Ada 2012 
facilities.

Thanks,
Álex.

>
>> On one hand, there are systems that must not shut down (maybe an
>> autopilot at flight time). If that is the case, Assert-checking in
>> production executables is plain wrong.
>
> It is plain wrong regardless. If assertion is a correctness statement it
> shall never be checked at run time. If assertion is an if-statement with
> exception raised upon one of the outcomes it must *always* be evaluated
> unless the condition proven static. It is either or, never both.
>

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 13/12/2016 12:56, Alejandro R. Mosteo wrote:

> Since it seems that usually is you, Dmitry, the one coming from a more
> theoretical (mathematical? purist?) POV into the arguments, perhaps you
> could recommend to me some reference(s) where I can better understand
> the principles involved in this discussion (the part about
> preconditions/predicates, not IR)? I confess to having only a
> superficial grasping of the situation, by way of using the Ada 2012
> facilities.

"The science of programming" by David Gries changed my world.

https://www.amazon.com/Science-Programming-Monographs-Computer/dp/0387964800/ref=asap_bc?ie=UTF8

The rest is just to exercise little grey cells, as Poirot used to say.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Alejandro R. Mosteo]

On 13/12/16 16:02, Dmitry A. Kazakov wrote:
> On 13/12/2016 12:56, Alejandro R. Mosteo wrote:
>
>> Since it seems that usually is you, Dmitry, the one coming from a more
>> theoretical (mathematical? purist?) POV into the arguments, perhaps you
>> could recommend to me some reference(s) where I can better understand
>> the principles involved in this discussion (the part about
>> preconditions/predicates, not IR)? I confess to having only a
>> superficial grasping of the situation, by way of using the Ada 2012
>> facilities.
>
> "The science of programming" by David Gries changed my world.
>
> https://www.amazon.com/Science-Programming-Monographs-Computer/dp/0387964800/ref=asap_bc?ie=UTF8
>
>
> The rest is just to exercise little grey cells, as Poirot used to say.

Thanks, let's see if my little grey cells are up to the task :P

Re: Ada 2012 Constraints (WRT an Ada IR)

[Randy Brukardt]

<Stefan.Lucks@uni-weimar.de> wrote in message 
news:alpine.DEB.2.20.1612050922450.22845@debian...
...
>On the other hand, there are systems, where a malfunction is worse than no
>function (e.g., a secure router -- better no communication than allowing
>attackers to pass through the security perimeter). In such cases, it may
>be wise do perform Assert-checking even in production executables.

My opinion is that the vast majority of systems are in this category, 
especially if one considers each task (here using "task" in its English 
meaning as a block of work) separately. Every system that I've personally 
worked on has been in this category (anti-spam filter - a bug causes a 
message to be quarantined, which provides a path to reproducing the bug; web 
server - a bug causes nothing useful to be returned, better than allowing a 
security hole and returning, say, a password file; Ada compiler - a bug 
usually causes the compiler to crash rather than producing incorrect code 
that might cause problems; Claw Builder - a bug usually causes buggy 
generated code, which breaks the contract with the user).

Most such systems need an "others" handler to ensure that one failing task 
(again, English meaning) doesn't cause the entire system to fail. Such 
handlers need some sort of reporting system so they're not silently covering 
bugs.

I also tend to disagree about suppressing/ignoring checks and predicates. In 
my experience, if a check or predicate or assertion is too expensive to run 
in the production system, it's also too expensive to run in testing. Simple 
checks should never be turned off -- a visible bug is always better than an 
invisible bug. (Moreover, compilers are always getting better about 
eliminating such checks, in which case many checks aren't made at all.) 
Expensive checks, if one has to have them at all, need to be managed 
separately from assertions/constraints/predicates -- one would only want to 
turn them on if all else has failed, and that clearly needs to be separate 
from the suppress/ignore mechanism. (Most of the systems I've worked on have 
a runtime management setup for tracing/assertions, where they get managed by 
functional areas as needed for figuring out the problem at hand.)

                             Randy.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Niklas Holsti]

On 16-11-29 01:49 , Shark8 wrote:
> So, with Ada 2012 we gained some really nice possibilities
> with the way to express constraints, the downside is that
> there's now a fairly wide range of ways to express constraints on
> types. Obviously these differences must be accounted for, but
> the are functionally equivalent, for example:
>
> Subtype P0 is Natural range Natural'Succ(Natural'First)..Natural'Last;

This seems the same as Positive, to me.

> Subtype P1 is Integer range 1..Integer'Last;

And this is the standard definition of Positive.

> Subtype P2 is Integer
>     with Static_Predicate => P2 in 1..Integer'Last
>                           or else raise Constraint_Error;

Perhaps it was obvious to you, but this differs from Positive in that 
you cannot write P2'First or similar (illegal by RM 3.2.4(26/3)), but 
you can write Positive'First.

> Subtype P3 is Integer with
>   Static_Predicate  => P3 in 1..Integer'Last,
>   Predicate_Failure => raise Constraint_Error;

Same difference as for P2, I think.

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 2016-11-29 18:53, Niklas Holsti wrote:

>> Subtype P2 is Integer
>>     with Static_Predicate => P2 in 1..Integer'Last
>>                           or else raise Constraint_Error;
>
> Perhaps it was obvious to you, but this differs from Positive in that
> you cannot write P2'First or similar (illegal by RM 3.2.4(26/3)), but
> you can write Positive'First.

'First, 'Last, 'Range operations seem covariant. A constrained-only 
subtype would have all operations contravariant.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Shark8]

On Tuesday, November 29, 2016 at 10:53:59 AM UTC-7, Niklas Holsti wrote:
> On 16-11-29 01:49 , Shark8 wrote:
> > So, with Ada 2012 we gained some really nice possibilities
> > with the way to express constraints, the downside is that
> > there's now a fairly wide range of ways to express constraints on
> > types. Obviously these differences must be accounted for, but
> > the are functionally equivalent, for example:
> >
> > Subtype P0 is Natural range Natural'Succ(Natural'First)..Natural'Last;
> 
> This seems the same as Positive, to me.

It is.

> > Subtype P1 is Integer range 1..Integer'Last;
> 
> And this is the standard definition of Positive.

It is.

> > Subtype P2 is Integer
> >     with Static_Predicate => P2 in 1..Integer'Last
> >                           or else raise Constraint_Error;
> 
> Perhaps it was obvious to you, but this differs from Positive in that 
> you cannot write P2'First or similar (illegal by RM 3.2.4(26/3)), but 
> you can write Positive'First.

But insofar as a "type" (the collection of values and operations*) goes it is the same: its values have the same range, the operations* are the same, and it raises the same error when they are violated.


* Assuming we're considering attributes as something different than an 'operation' and excluding them.

> 
> > Subtype P3 is Integer with
> >   Static_Predicate  => P3 in 1..Integer'Last,
> >   Predicate_Failure => raise Constraint_Error;
> 
> Same difference as for P2, I think.
> 

So there *IS* something in common about all the above, that's what the thrust of the topic (an Ada IR) is getting at. Something like "can't use attributes like 'First" could be handled [implementation-wise] as something like:

-- Vastly oversimplified.
Type Subtype_Node( Accessible_Attributes : Boolean := True ) is record
  Name   : String_Holder;
  Parent : Type_Node;
  Values : -- value-set.
  -- or however we represent the constraints, errors, and messages.
enc;
end record;

Re: Ada 2012 Constraints (WRT an Ada IR)

[Randy Brukardt]

"Shark8" <onewingedshark@gmail.com> wrote in message 
news:f2c50fc6-18e1-48c7-8db7-aca274c74ac7@googlegroups.com...
> On Tuesday, November 29, 2016 at 10:53:59 AM UTC-7, Niklas Holsti wrote:
...
>> > Subtype P2 is Integer
>> >     with Static_Predicate => P2 in 1..Integer'Last
>> >                           or else raise Constraint_Error;
>>
>> Perhaps it was obvious to you, but this differs from Positive in that
>> you cannot write P2'First or similar (illegal by RM 3.2.4(26/3)), but
>> you can write Positive'First.
>
> But insofar as a "type" (the collection of values and operations*) goes it 
> is the same: its
> values have the same range, the operations* are the same, and it raises 
> the same error
> when they are violated.
>
> * Assuming we're considering attributes as something different than an 
> 'operation' and excluding them.

That's a pretty strange thing to do, IMHO. (And keep in mind the difference 
of operation for memberships that I noted previously -- do you want to 
exclude that, too??)

>> > Subtype P3 is Integer with
>> >   Static_Predicate  => P3 in 1..Integer'Last,
>> >   Predicate_Failure => raise Constraint_Error;
>>
>> Same difference as for P2, I think.
>>
>
> So there *IS* something in common about all the above, that's what the 
> thrust of the topic (an Ada IR) is getting at.

Perhaps we better start back that the beginning. What do you mean by "IR"? I 
had assumed that you wanted advice for chosing between these possibilities, 
but this message seems to be concentrating on implementing an Ada compiler. 
That seems irrelevant to virtually all Ada users (my advice, as always, when 
thinking about starting a new Ada implementation, is DON'T -- no one -- or 
even a small group -- has the 15 years of effort needed). I'd rather talk 
about things that are relevant.

                            Randy.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Shark8]

On Tuesday, November 29, 2016 at 5:03:07 PM UTC-7, Randy Brukardt wrote:
> "Shark8" wrote in message 
> news:f2c50fc6-18e1-48c7-8db7-aca274c74ac7...
> > On Tuesday, November 29, 2016 at 10:53:59 AM UTC-7, Niklas Holsti wrote:
> ...
> >> > Subtype P2 is Integer
> >> >     with Static_Predicate => P2 in 1..Integer'Last
> >> >                           or else raise Constraint_Error;
> >>
> >> Perhaps it was obvious to you, but this differs from Positive in that
> >> you cannot write P2'First or similar (illegal by RM 3.2.4(26/3)), but
> >> you can write Positive'First.
> >
> > But insofar as a "type" (the collection of values and operations*) goes it 
> > is the same: its
> > values have the same range, the operations* are the same, and it raises 
> > the same error
> > when they are violated.
> >
> > * Assuming we're considering attributes as something different than an 
> > 'operation' and excluding them.
> 
> That's a pretty strange thing to do, IMHO. (And keep in mind the difference 
> of operation for memberships that I noted previously -- do you want to 
> exclude that, too??)

Is it?
Are 'First and 'Last operations of the type? Objects of that type? Both? Neither? Dependent on the type of attribute and/or the type of variable?

For example, "Type K array(positive range <>) of integer" doesn't define a 'First and 'Last operation for the type... even though given "X : K;" X'First and X'Last are perfectly fine.


> 
> >> > Subtype P3 is Integer with
> >> >   Static_Predicate  => P3 in 1..Integer'Last,
> >> >   Predicate_Failure => raise Constraint_Error;
> >>
> >> Same difference as for P2, I think.
> >>
> >
> > So there *IS* something in common about all the above, that's what the 
> > thrust of the topic (an Ada IR) is getting at.
> 
> Perhaps we better start back that the beginning. What do you mean by "IR"? 

Intermediate Representation.

> I had assumed that you wanted advice for choosing between these possibilities, but this message seems to be concentrating on implementing an Ada compiler. 

It is only partially about implementing a compiler, it's partly about really understanding Ada, it's also about understanding a good way to represent the underling concepts. -- A good IR could also provide a good foundation for creating a sort of "CPAN for Ada", but amiable to consistency assurance both in the repository itself [1] and for dependencies themselves.

(1) -- I have a friend who uses Perl, in his usage of CPAN he's encountered corrupted index-files, corrupted archives, and dependency issues.

> That seems irrelevant to virtually all Ada users (my advice, as always, when 
> thinking about starting a new Ada implementation, is DON'T -- no one -- or 
> even a small group -- has the 15 years of effort needed). I'd rather talk 
> about things that are relevant.

One of the things that a lot of people have said -- survey results here: https://docs.google.com/spreadsheets/d/1ixr84Q8zif44IxX4x22o6I1UBZ_knu4pp6q4Yft5GaI/edit#gid=588264163 -- that keeps them from adopting Ada is:
(1) a lack of free and low-cost implementations [even here on comp.lang.ada we have people of much the same opinion WRT AdaCore's perceived monopoly],
(2) a [perceived] lack of tools "like lint" or CPAN [I'll admit SPARK is/has a pretty nice set of tools, and that your average Ada implementation already has huge chunks of that functionality],
(3) lack of libraries, or the ability to find them.

Re: Ada 2012 Constraints (WRT an Ada IR)

[AdaMagica]

Am Dienstag, 29. November 2016 18:53:59 UTC+1 schrieb Niklas Holsti:
> > Subtype P2 is Integer
> >     with Static_Predicate => P2 in 1..Integer'Last
> >                           or else raise Constraint_Error;
> 
> Perhaps it was obvious to you, but this differs from Positive in that 
> you cannot write P2'First or similar (illegal by RM 3.2.4(26/3)), but 
> you can write Positive'First.

'First, 'Last, 'Range are disallowed. There are 'First_Valid and 'Last_Valid instead. RM 5.5(7.2/4-7.3/4)

Re: Ada 2012 Constraints (WRT an Ada IR)

[Randy Brukardt]

"Shark8" <onewingedshark@gmail.com> wrote in message 
news:c06ee4e6-d616-4e01-ba2e-cb111a81f6f6@googlegroups.com...
>So, with Ada 2012 we gained some really nice possibilities with the way to 
>express constraints, the
>downside is that there's now a fairly wide range of ways to express 
>constraints on types. Obviously
>these differences must be accounted for, but the are functionally 
>equivalent, for example:
>
>Subtype P0 is Natural range Natural'Succ(Natural'First)..Natural'Last;
>Subtype P1 is Integer range 1..Integer'Last;
>Subtype P2 is Integer with Static_Predicate => P2 in 1..Integer'Last or 
>else raise Constraint_Error;
>Subtype P3 is Integer with
>  Static_Predicate  => P3 in 1..Integer'Last,
>  Predicate_Failure => raise Constraint_Error;
>
>Now, these should be generally the same way of writing the same thing (ie 
>"Positive") -- though
> I'm not completely certain that this is the case in terms of subtle 
> semantics (am I missing something?)

P2 is different than the others when used in a membership:

    Obj in P2

would raise Constraint_Error rather than return False (like the others) if 
Obj has the value 0. It's not recommended.

P0 and P1 are more likely to be optimized by a compiler (just because of the 
many years of history). Perhaps P3 will catch up, but I wouldn't hold my 
breath on that.

                               Randy.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Shark8]

On Tuesday, November 29, 2016 at 4:52:20 PM UTC-7, Randy Brukardt wrote:
> "Shark8" wrote in message 
> news:c06ee4e6-d616-4e01-ba2e-cb111a81f6f6@...
> >So, with Ada 2012 we gained some really nice possibilities with the way to 
> >express constraints, the
> >downside is that there's now a fairly wide range of ways to express 
> >constraints on types. Obviously
> >these differences must be accounted for, but the are functionally 
> >equivalent, for example:
> >
> >Subtype P0 is Natural range Natural'Succ(Natural'First)..Natural'Last;
> >Subtype P1 is Integer range 1..Integer'Last;
> >Subtype P2 is Integer with Static_Predicate => P2 in 1..Integer'Last or 
> >else raise Constraint_Error;
> >Subtype P3 is Integer with
> >  Static_Predicate  => P3 in 1..Integer'Last,
> >  Predicate_Failure => raise Constraint_Error;
> >
> >Now, these should be generally the same way of writing the same thing (ie 
> >"Positive") -- though
> > I'm not completely certain that this is the case in terms of subtle 
> > semantics (am I missing something?)
> 
> P2 is different than the others when used in a membership:
> 
>     Obj in P2
> 
> would raise Constraint_Error rather than return False (like the others) if 
> Obj has the value 0. It's not recommended.

Ah, I didn't realize that... I see the logic of why it does that: it fails the predicate's membership-test and then executes the raise-statement. But if that's the case whey isn't P3 the same? It is, after all, failing the membership-test and therefore failing the predicate, no?

> P0 and P1 are more likely to be optimized by a compiler (just because of the 
> many years of history). Perhaps P3 will catch up, but I wouldn't hold my 
> breath on that.

What I'm saying is that P0, P1, and P3 (and perhaps arguably P2) should be represented as the same thing... that there ought to be some way to abstract types and subtypes so that there is a common representation.

Just like a function with a single simple return-statement and an expression-function should be able to be represented as the same thing because the standard says the forms are equivalent. eg:

    Function One return Integer is
    begin
      return 1;
    end One;
and
    Function One return Integer is
      (1);

Could be represented by a parse-tree construct that looks something like this:

  Function_node
   name       : one
   parameters : ()
   return_type: Integer
   body       : Value_node
                 Type : integer
                 Value: 1
^
L__ Deliberately not Ada-syntax.

Maybe with a field for keeping track of whether or not an expression-function or long-form function are being used... or that could be discarded and let the programmer's viewer-tool take care of how it should display it.

The point is that we can have the IR capable of representing the construct "function" uniformly despite syntax-permutations -- Since types are, as noted upthread, a set of values and a set of operations on those values, there ought to be a way to represent a type in a uniform manner, right?

Re: Ada 2012 Constraints (WRT an Ada IR)

[Randy Brukardt]

"Shark8" <onewingedshark@gmail.com> wrote in message 
news:638d0618-f565-47ef-9793-dd05a4b1a662@googlegroups.com...
On Tuesday, November 29, 2016 at 4:52:20 PM UTC-7, Randy Brukardt wrote:
...
>> P2 is different than the others when used in a membership:
>>
>>     Obj in P2
>>
>> would raise Constraint_Error rather than return False (like the others) 
>> if
>> Obj has the value 0. It's not recommended.
>
>Ah, I didn't realize that... I see the logic of why it does that: it fails 
>the predicate's
> membership-test and then executes the raise-statement. But if that's the 
> case
> whey isn't P3 the same? It is, after all, failing the membership-test and 
> therefore
> failing the predicate, no?

Ah, that's why predicate_failure exists. A membership (or 'Valid, which is 
similar) doesn't "fail", it returns True or False. By definition, the 
Predicate_Failure aspect isn't used in those cases. That makes it equivalent 
to P0 and P1.

>> P0 and P1 are more likely to be optimized by a compiler (just because of 
>> the
>> many years of history). Perhaps P3 will catch up, but I wouldn't hold my
>> breath on that.
>
>What I'm saying is that P0, P1, and P3 (and perhaps arguably P2) should be
> represented as the same thing... that there ought to be some way to 
> abstract
> types and subtypes so that there is a common representation.

Very unlikely in existing implementations. And maybe not a good idea in 
general, as there is a semantic difference in terms of the set of values for 
a constraint vs. a predicate. (This is one of those cases where I don't know 
of a way to tell that semantic difference, but I'd probably take a 
conservative approach and assume that someone will find one someday -- Ada 
has many amazing ways to do things you'd not expect.)

>Just like a function with a single simple return-statement and an 
>expression-function
> should be able to be represented as the same thing because the standard 
> says the
> forms are equivalent.

That's different, in that the standard literally says that. But there is no 
need for IR of any kind for this sort of construct (Janus/Ada only has a 
symbol table and expression trees; no larger pieces of program code are ever 
in memory. That then gets turned into a virtual stack machine [instructions 
which are similar to that of a real machine] which gets optimized and 
converted into machine code.)

For the most part, there is little need for the time waste involved with 
creating a parse tree of any sort; you have to do that for expressions 
because of the way Ada resolution works, but it's unnecessary for program 
units and control flow. (That decision does effectively require implementing 
shared generics; that fact that we don't have any parse trees in our 
compiler makes a template implementation essentially impossible.)

                                       Randy.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Shark8]

On Tuesday, November 29, 2016 at 4:52:20 PM UTC-7, Randy Brukardt wrote:
> 
> P0 and P1 are more likely to be optimized by a compiler (just because of the 
> many years of history). Perhaps P3 will catch up, but I wouldn't hold my 
> breath on that.

Oh, BTW, *THIS* is exactly the motivation for having a uniform IR -- when put into a common form then all optimizations on that object/construct are applicable. This is to say that when P3 and P1 share a representation, every optimization of P1 is possible for P3. (Despite syntax differences; again, assuming they're truly equivalent in the same way that "Integer > 0" and "Integer in 1..Integer'Last" are.)

Re: Ada 2012 Constraints (WRT an Ada IR)

[Randy Brukardt]

"Shark8" <onewingedshark@gmail.com> wrote in message 
news:8b3ea401-822b-4b51-be48-133861ef2e0b@googlegroups.com...
>On Tuesday, November 29, 2016 at 4:52:20 PM UTC-7, Randy Brukardt wrote:
>>
>> P0 and P1 are more likely to be optimized by a compiler (just because of 
>> the
>> many years of history). Perhaps P3 will catch up, but I wouldn't hold my
>> breath on that.
>
>Oh, BTW, *THIS* is exactly the motivation for having a uniform IR -- when 
>put into a
>common form then all optimizations on that object/construct are applicable. 
>This is to
>say that when P3 and P1 share a representation, every optimization of P1 is 
>possible
>for P3. (Despite syntax differences; again, assuming they're truly 
>equivalent in the same
>way that "Integer > 0" and "Integer in 1..Integer'Last" are.)

We don't do any optimizations in the high-level IR (that would be expression 
trees); that's all done in the conversion to the low-level IR (the stack 
based machine) or on that IR directly. There's few Ada constructs in the 
low-level IR.

In any case, the semantic description of the two constructs is different, 
although as far as I know the effect is the same. My experience in Ada is 
that whenever you think you can collapse Ada constructs, you eventually will 
be proved wrong, either by a new ACATS test, a customer bug report, or by 
some future change in the language (either a bug fix or new revision). I 
would generally reecommend avoiding that as much as possible.

                                     Randy.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Shark8]

On Wednesday, November 30, 2016 at 3:17:51 PM UTC-7, Randy Brukardt wrote:
> "Shark8" wrote in message 
> news:8b3ea401-822b-4b51-be48-133861ef2e0b...
> >On Tuesday, November 29, 2016 at 4:52:20 PM UTC-7, Randy Brukardt wrote:
> >>
> >> P0 and P1 are more likely to be optimized by a compiler (just because of 
> >> the
> >> many years of history). Perhaps P3 will catch up, but I wouldn't hold my
> >> breath on that.
> >
> >Oh, BTW, *THIS* is exactly the motivation for having a uniform IR -- when 
> >put into a
> >common form then all optimizations on that object/construct are applicable. 
> >This is to
> >say that when P3 and P1 share a representation, every optimization of P1 is 
> >possible
> >for P3. (Despite syntax differences; again, assuming they're truly 
> >equivalent in the same
> >way that "Integer > 0" and "Integer in 1..Integer'Last" are.)
> 
> We don't do any optimizations in the high-level IR (that would be expression 
> trees); that's all done in the conversion to the low-level IR (the stack 
> based machine) or on that IR directly. There's few Ada constructs in the 
> low-level IR.

Hm, I think I see your point.

> In any case, the semantic description of the two constructs is different, 
> although as far as I know the effect is the same. My experience in Ada is 
> that whenever you think you can collapse Ada constructs, you eventually will 
> be proved wrong, either by a new ACATS test, a customer bug report, or by 
> some future change in the language (either a bug fix or new revision). I 
> would generally reecommend avoiding that as much as possible.

Then maybe this is a valid issue to put in an Ada-comment; the thinking of things in terms of sets is something that's been in Ada since its inception (eg case-coverage) -- and acknowledging that the common definition of 'type' as "a set of values and a set of operations on those values" is solid enough that codifying those constructs as the same would be useful to implementations, no?

Re: Ada 2012 Constraints (WRT an Ada IR)

[Randy Brukardt]

"Shark8" <onewingedshark@gmail.com> wrote in message 
news:5eb00dbc-d36e-47e5-bc76-0d0683281c09@googlegroups.com...
On Wednesday, November 30, 2016 at 3:17:51 PM UTC-7, Randy Brukardt wrote:
...
>> In any case, the semantic description of the two constructs is different,
>> although as far as I know the effect is the same. My experience in Ada is
>> that whenever you think you can collapse Ada constructs, you eventually 
>> will
>> be proved wrong, either by a new ACATS test, a customer bug report, or by
>> some future change in the language (either a bug fix or new revision). I
>> would generally reecommend avoiding that as much as possible.

>Then maybe this is a valid issue to put in an Ada-comment; the thinking of 
>things in
>terms of sets is something that's been in Ada since its inception (eg 
>case-coverage)
> -- and acknowledging that the common definition of 'type' as "a set of 
> values and
> a set of operations on those values" is solid enough that codifying those 
> constructs
> as the same would be useful to implementations, no?

Well, like everything it would be different and potentially incompatible. 
Proving that it is *not* incompatible or inconsistent would be difficult, 
yet there is no chance that such a non-required change would be made absent 
such a proof.

In any case, I would have preferred that Ada not have static predicates and 
rather have "set constraints", which would have made ranges and sets 
consistent semantically. I pushed that alternative repeatedly at meetings, 
but I never got any traction - I pretty much was alone in thinking that was 
a better option. Ergo, I think any proposal like the one you are suggesting 
would be a very uphill battle. (And then you have to decide which battle of 
the many possibilities is worth such an effort. If I was going to undertake 
such a battle, I'd rather focus on either allowing object overloading or 
allowing types in private parts of protected objects - both of which would 
solve long standing issues and unify the language a bit more; changing the 
description of the language is a lot of running in place.

Bob Duff likes to say that he doesn't think we should spend any time on an 
issue unless a user or implementer could get it wrong otherwise. I don't 
think such a description change could have any real effect on 
implementations, so it would be a lot of work for no real gain (and some 
risk of introducing errors on top of that).

                                   Randy.

Re: Ada 2012 Constraints (WRT an Ada IR)

[AdaMagica]

Am Mittwoch, 30. November 2016 00:52:20 UTC+1 schrieb Randy Brukardt:

> >Subtype P2 is Integer with Static_Predicate => P2 in 1..Integer'Last or 
> >else raise Constraint_Error;
> 
> P2 is different than the others when used in a membership:
> 
>     Obj in P2
> 
> would raise Constraint_Error rather than return False (like the others) if 
> Obj has the value 0. It's not recommended.

P2 is illegal, expression is not predicate static (RM 3.2.4(16-22))

subtype P2d is Integer with
  Dynamic_Predicate => P2d in 1..Integer'Last
  or else raise Constraint_Error;

Hm, GNAT GPL 2016 returns False for membership (0 in P2d); no exception.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Randy Brukardt]

[I had to break the chain of replies as the headers got so long that the 
message wouldn't post.]

"Shark8" <onewingedshark@gmail.com> wrote in message
news:8e3b18a7-1e64-40bb-8d99-66fdeba58ace@googlegroups.com...
> On Tuesday, December 6, 2016 at 4:23:55 PM UTC-7, Randy Brukardt wrote:
...
>> You seem to be assuming that it is practical to represent all kinds of
>> predicates as some sort of set. That's definitely not true; one of the
>> major
>> reasons that you can't use divide or mod in a static predicate is the
>> difficulty of representing the set. For instance, consider:
>>
>>      subtype Even is new Natural with Dynamic_Predicate => Even mod 2 =
>> 0;
>>
>> If Natural is a 64 bit type, Even is a set of 2**63 items, no two are
>> contiguous. The representation of that is going to be a problem. One
>> could
>> imagine some special case to deal with this particular case, but then
>> there
>> are many other possible predicates with this property.
>
> Just because it's represented as a set doesn't mean that the set has to be
> represented as a bit-mask. (The obvious breaking example for that
> implementation here would be a string subtype constrained to contain only
> numeric characters.)

In existing Ada implementations, sets are represented as a list of ranges.
(They come up in a number of places, including case statements and
Ada.Strings.) That's the expected implementation for any Ada set, but that
would take 2**63 items for Even.

...
>> Thus, your hypothetical IR would have to represent ranges as predicates,
>> rather than as some sort of set. But that would make it hard to do
>> operations on the IR (such as merging and check elimination).
>
> Would it though? Don't we have tools (and entire programming languages)
> built around predicate-logic?

(1) Hard /= impossible.
(2) I have no idea about tools or programming languages built around
predicate logic. Ada systems usually are built around simpler things, the
most complex being set operations. Trying to put a predicate logic prover
into a compiler optimizer sounds challenging at best. (Yes, I realize this
argument is somewhat circular.)

                               Randy.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Niklas Holsti]

On 16-12-09 23:41 , Randy Brukardt wrote:
> [I had to break the chain of replies as the headers got so long that the
> message wouldn't post.]
>
> "Shark8" <onewingedshark@gmail.com> wrote in message
> news:8e3b18a7-1e64-40bb-8d99-66fdeba58ace@googlegroups.com...
>> On Tuesday, December 6, 2016 at 4:23:55 PM UTC-7, Randy Brukardt wrote:
> ...
>>> You seem to be assuming that it is practical to represent all kinds of
>>> predicates as some sort of set. That's definitely not true; one of the
>>> major
>>> reasons that you can't use divide or mod in a static predicate is the
>>> difficulty of representing the set. For instance, consider:
>>>
>>>      subtype Even is new Natural with Dynamic_Predicate => Even mod 2 =
>>> 0;
>>>
>>> If Natural is a 64 bit type, Even is a set of 2**63 items, no two are
>>> contiguous. The representation of that is going to be a problem. One
>>> could
>>> imagine some special case to deal with this particular case, but then
>>> there
>>> are many other possible predicates with this property.
>>
>> Just because it's represented as a set doesn't mean that the set has to be
>> represented as a bit-mask. (The obvious breaking example for that
>> implementation here would be a string subtype constrained to contain only
>> numeric characters.)
>
> In existing Ada implementations, sets are represented as a list of ranges.
> (They come up in a number of places, including case statements and
> Ada.Strings.) That's the expected implementation for any Ada set, but that
> would take 2**63 items for Even.

Static program analyzers, at least those analysing machine code and 
aiming to understand address alignments and aliasing, tend to need and 
use not only ranges, but ranges with strides (congruence information). 
The set of Even numbers would be easy and compact to represent in such a 
model, with stride = 2. Of course, it is a coincidence that Even happens 
to fit this model, and your general argument is not affected.

> Trying to put a predicate logic prover into a compiler optimizer sounds
> challenging at best.

I'm a little surprised: I seem to remember that you have, earlier, said 
that you would like future compilers to prove all sorts of things about 
the program. But you were not thinking of predicate logic proofs?

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .

Re: Ada 2012 Constraints (WRT an Ada IR)

[Randy Brukardt]

"Niklas Holsti" <niklas.holsti@tidorum.invalid> wrote in message 
news:eb0po8Fgob2U1@mid.individual.net...
> On 16-12-09 23:41 , Randy Brukardt wrote:
...
>> Trying to put a predicate logic prover into a compiler optimizer sounds
>> challenging at best.
>
> I'm a little surprised: I seem to remember that you have, earlier, said 
> that you would like future compilers to prove all sorts of things about 
> the program. But you were not thinking of predicate logic proofs?

Potentially different parts of the compiler. And, no, I wasn't thinking of 
predicate logic proofs so much as simple common subexpression elimination, 
algebraic reductions, flow analysis, and other existing, common optimization 
techniques. The problem with these is more in usefully reporting the results 
to the user than with actually doing them (as they likely already exist in 
compilers, but tend to be used on lower-level code formats). In particular, 
one would want to report to the user when a precondition or postcondition 
cannot be optimized to "True", but how to do that usefully (in the back-end 
of a compiler where little source information remains),  and especially 
avoiding too much nattering, isn't obvious to me.

                                                  Randy.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Shark8]

On Monday, December 12, 2016 at 5:41:32 PM UTC-7, Randy Brukardt wrote:
> "Niklas Holsti" wrote:
> 
> > On 16-12-09 23:41 , Randy Brukardt wrote:
> ...
> >> Trying to put a predicate logic prover into a compiler optimizer sounds
> >> challenging at best.
> >
> > I'm a little surprised: I seem to remember that you have, earlier, said 
> > that you would like future compilers to prove all sorts of things about 
> > the program. But you were not thinking of predicate logic proofs?
> 
> Potentially different parts of the compiler. And, no, I wasn't thinking of 
> predicate logic proofs so much as simple common subexpression elimination, 
> algebraic reductions, flow analysis, and other existing, common optimization 
> techniques. The problem with these is more in usefully reporting the results 
> to the user than with actually doing them (as they likely already exist in 
> compilers, but tend to be used on lower-level code formats). In particular, 
> one would want to report to the user when a precondition or postcondition 
> cannot be optimized to "True", but how to do that usefully (in the back-end 
> of a compiler where little source information remains),  and especially 
> avoiding too much nattering, isn't obvious to me.
> 
>                                                   Randy.

I think I see. You're talking something more like this -- http://citeseer.ist.psu.edu/viewdoc/download;jsessionid=46530BCDD09D9D8B41C7FE958AAD0442?doi=10.1.1.53.1099&rep=rep1&type=pdf -- no?

But constraint-engines are certainly needed for (e.g.) SPARK for its SMT (satisfiability modulo theory) solver/prover... would it be a bad idea to further integrate these into the [non-restricted Ada] compiler?

Re: Ada 2012 Constraints (WRT an Ada IR)

[Randy Brukardt]

"Shark8" <onewingedshark@gmail.com> wrote in message 
news:b48d98ab-2b9b-47cd-b33e-674e07074c86@googlegroups.com...
> On Monday, December 12, 2016 at 5:41:32 PM UTC-7, Randy Brukardt wrote:
>> "Niklas Holsti" wrote:
>>
>> > On 16-12-09 23:41 , Randy Brukardt wrote:
>> ...
>> >> Trying to put a predicate logic prover into a compiler optimizer 
>> >> sounds
>> >> challenging at best.
>> >
>> > I'm a little surprised: I seem to remember that you have, earlier, said
>> > that you would like future compilers to prove all sorts of things about
>> > the program. But you were not thinking of predicate logic proofs?
>>
>> Potentially different parts of the compiler. And, no, I wasn't thinking 
>> of
>> predicate logic proofs so much as simple common subexpression 
>> elimination,
>> algebraic reductions, flow analysis, and other existing, common 
>> optimization
>> techniques. The problem with these is more in usefully reporting the 
>> results
>> to the user than with actually doing them (as they likely already exist 
>> in
>> compilers, but tend to be used on lower-level code formats). In 
>> particular,
>> one would want to report to the user when a precondition or postcondition
>> cannot be optimized to "True", but how to do that usefully (in the 
>> back-end
>> of a compiler where little source information remains),  and especially
>> avoiding too much nattering, isn't obvious to me.
>>
>
> I think I see. You're talking something more like this --  
> http://citeseer.ist.psu.edu/viewdoc/download;jsessionid=46530BCDD09D9D8B41C7FE958AAD0442?doi=10.1.1.53.1099&rep=rep1&type=pdf - 
> - no?

When I tried to open that link, my browser crashed, so I didn't look at it. 
But probably.

My primary goal here has always been to optimize Pre/Post/predicates well 
enough that it isn't necessary to ignore them. Since these are just more 
powerful constraints, and constraint checks shouldn't be suppressed unless 
all else fails, it seems to me that the same dynamic should apply to 
contract assertions.

And practically, that has to be done mainly with the existing engines in an 
Ada compiler; adding a lot more complexity to one is likely to result in an 
unmaintainable mess. (They're already close to the boundary of what's 
practical, IMHO.)

> But constraint-engines are certainly needed for (e.g.) SPARK for its SMT 
> (satisfiability modulo theory)
> solver/prover... would it be a bad idea to further integrate these into 
> the [non-restricted Ada] compiler?

Surely not a bad idea, but I think it's likely to be impractical. I suppose 
if someone started from scratch with proof in mind, they could replace a lot 
of optimization code with proof -- but is anyone really going to start a 
project like that from scratch these days? (Having a proof engine is not 
going to make Ada visibility and resolution any easier to implement.)

                                    Randy.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Shark8]

On Tuesday, December 13, 2016 at 3:35:27 PM UTC-7, Randy Brukardt wrote:
> 
> Surely not a bad idea, but I think it's likely to be impractical.

Certainly where the thrust for my original posting here was going: a unified yet general IR with respect to constraints would make things much nicer for a SPARK-like tool... and it's not unreasonable that you could get some of SPARK's advantages w/o some of its restrictions.

(Just like you point out below for optimizations.)

> I suppose if someone started from scratch with proof in mind, they could
> replace a lot of optimization code with proof -- but is anyone really
> going to start a project like that from scratch these days? (Having a
> proof engine is not going to make Ada visibility and resolution any
> easier to implement.)

Well, I've already started on Byron[1], a compiler for Ada 2012 in Ada 2012, which does aim for being provable where possible. -- And I'd always had an IR like this in mind before even starting. -- It would be nice to integrate an SMT into it, but I think implementing an SMT is beyond my current abilities. (And the reason I'm assuming that I'd have to be the one to do it is because, so far, I'm the only contributor to the project.)

I do 'cheat' a little bit with the lexer, the only phase that's complete right now... actually, I think you'd find it humorous to see how I did it. (And yes, there's some ugly code and ordering dependencies in it... the good news is that it can easily be replaced so long as the replacement emits tokens properly/consistently w/ the token packages.)

[1] -- https://github.com/OneWingedShark/Byron

Re: Ada 2012 Constraints (WRT an Ada IR)

[Niklas Holsti]

On 16-12-13 02:41 , Randy Brukardt wrote:
> "Niklas Holsti" <niklas.holsti@tidorum.invalid> wrote in message
> news:eb0po8Fgob2U1@mid.individual.net...
>> On 16-12-09 23:41 , Randy Brukardt wrote:
> ...
>>> Trying to put a predicate logic prover into a compiler optimizer sounds
>>> challenging at best.
>>
>> I'm a little surprised: I seem to remember that you have, earlier, said
>> that you would like future compilers to prove all sorts of things about
>> the program. But you were not thinking of predicate logic proofs?
>
> Potentially different parts of the compiler. And, no, I wasn't thinking of
> predicate logic proofs so much as simple common subexpression elimination,
> algebraic reductions, flow analysis, and other existing, common optimization
> techniques.

I see -- something like what CodePeer does, but integrated with the 
compiler.

> The problem with these is more in usefully reporting the results
> to the user than with actually doing them (as they likely already exist in
> compilers, but tend to be used on lower-level code formats). In particular,
> one would want to report to the user when a precondition or postcondition
> cannot be optimized to "True", but how to do that usefully (in the back-end
> of a compiler where little source information remains),  and especially
> avoiding too much nattering, isn't obvious to me.
>
>                                                   Randy.

Yes. Also the output from CodePeer can be rather voluminous and hard to 
understand, or so I have been told by my colleagues who are actively 
using it. I aim to start using it, as soon as other tasks permit :-)

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .

Re: Ada 2012 Constraints (WRT an Ada IR)

[Randy Brukardt]

"Niklas Holsti" <niklas.holsti@tidorum.invalid> wrote in message 
news:ebb502F17nuU1@mid.individual.net...
...
> Yes. Also the output from CodePeer can be rather voluminous and hard to 
> understand, or so I have been told by my colleagues who are actively using 
> it. I aim to start using it, as soon as other tasks permit :-)

Exactly. That's the problem with using optimizer technology as the basis of 
correctness checking.

In my case, I have the optimizer, and I know(*) how to use it to "prove" 
preconditions/postconditions, but how to give feedback to the programmer is 
elusive. That's especially true as one mostly wants to report the negatives: 
Pre/Post that could not be eliminated by the optimizer. For obvious reasons, 
the optimizer doesn't pay much attention to things it can't do.

(*) "Know" in the sense that I have a plan which should work based on the 
existing design of the optimizer. As with all things compiler, one doesn't 
really "know" until it's implemented and tested.

Of course, instead of working on a "fun" project like this, I'm trying to 
track down why Ada.Tags is visible in a package specification that doesn't 
"with" Ada.Tags. Ada visibility and resolution sadly take all of the fun out 
of compiler construction. :-)

                                             Randy.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Shark8]

On Tuesday, December 13, 2016 at 4:19:32 PM UTC-7, Randy Brukardt wrote:
> Ada visibility and resolution sadly take all of the fun out 
> of compiler construction. :-)

That's one of the things that I'd like the IR to do; assuming we have a DEPENDENCY node (or attribute in the root-node) then it should be possible to enforce that property so that your problem of "Tags being visible w/o Ada.Tags being WITH'ed". (This is to say, if we have the dependencies listed, say as a separate Dependency_Type then every entity in the source should have a 'handle' pointing to an item in the DEPENDENCY attribute xor to a local construct.)

You could then have a "visibility node" (USE) be a sub-tree that has its own handles into the DEPENDENCY attribute and for represents the visibility right in the tree-structure.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Randy Brukardt]

"Shark8" <onewingedshark@gmail.com> wrote in message 
news:fe2588fe-874d-4826-95a1-02cf5bc4c1e2@googlegroups.com...
On Tuesday, December 13, 2016 at 4:19:32 PM UTC-7, Randy Brukardt wrote:
>> Ada visibility and resolution sadly take all of the fun out
>> of compiler construction. :-)
>
>That's one of the things that I'd like the IR to do; assuming we have
>a DEPENDENCY node (or attribute in the root-node) then it should
>be possible to enforce that property so that your problem of "Tags
>being visible w/o Ada.Tags being WITH'ed". (This is to say, if we
>have the dependencies listed, say as a separate Dependency_Type
>then every entity in the source should have a 'handle' pointing to an
>item in the DEPENDENCY attribute xor to a local construct.)
>
>You could then have a "visibility node" (USE) be a sub-tree that has
> its own handles into the DEPENDENCY attribute and for represents
> the visibility right in the tree-structure.

It's never really about implementing something that gets 95% of 
visibility/resolution right. It's about implementing something that gets 
100% of visibility/resolution right. And that last 5% is always a beast, no 
matter how or where you start. (There are just too many details for anyone 
to get the initial version right.)

The great thing about the ACATS is that it provides a large number of vetted 
tests for Ada, so the expectations are well-defined. Getting a compiler to 
handle all of those tests, however, turns into a slog. Typically, fixing one 
issue in a test or tests just exposes another issue in the tests. It's this 
error fixing slog (plus, of course, customers sending new issues in) that 
takes a lot of the fun out of compiler construction.

                                      Randy.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Randy Brukardt]

[Too many replies again, had to break the thread to post - RLB]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
news:o2po6a$1hnq$1@gioia.aioe.org...
...
>> Right, Pre aspects are *not* body!
>
> They are being executed at run time.

So are constraint checks. So what?

The specification of a subprogram needs to contain whatever it is that the
caller needs to know. That's why traditionally one puts comments in a
specification. Pre is just one formalization of what the caller needs to
know. (Caller here means both the execution-time caller - that is the
program, and the programmer caller - that is the human that writes the
program.)

The body of a subprogram contains the remainder - the part the caller does
not need to know.

The separation has nothing to do with execution or compile-time, it's just a
need-to-know. You insist on thinking that execution can somehow be separated
from compile-time, but it's something with no firm boundary. It's all just
semantics in the end (think of a just-in-time compiler for an extreme
example).

                             Randy.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Randy Brukardt]

[Yet again had to break the thread because the thread has gotten too long to 
reply to - RLB]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
news:o2s8l1$1fef$1@gioia.aioe.org...
> On 2016-12-14 20:23, Shark8 wrote:
...
>> You are observably wrong.
>> If you supply a negative number, the body of X never executes.
>
> Of course it does. Semantically any effect of a call to X is due to X's
> body. There is nothing else there.

This is clearly false. The definition of the execution of a subprogram call
(RM 6.4(10/2)) specifically says that the parameter associations are
evaluated before the subprogram body is executed. 6.4.1 says that evaluation
of the parameter associations include the conversion to the formal subtype -
that conversion does the check that raises Constraint_Error.

One of the reasons that we get into these extended arguments is that you
insist on inventing a model of semantics which is different than Ada's. So
most of us discuss things as they are, and you are discussing something
totally different but using the same terminology. No wonder most of us are
confused by what you say.

                                                   Randy.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 14/12/2016 23:40, Randy Brukardt wrote:
> [Yet again had to break the thread because the thread has gotten too long to
> reply to - RLB]
>
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
> news:o2s8l1$1fef$1@gioia.aioe.org...
>> On 2016-12-14 20:23, Shark8 wrote:
> ...
>>> You are observably wrong.
>>> If you supply a negative number, the body of X never executes.
>>
>> Of course it does. Semantically any effect of a call to X is due to X's
>> body. There is nothing else there.
>
> This is clearly false. The definition of the execution of a subprogram call
> (RM 6.4(10/2)) specifically says that the parameter associations are
> evaluated before the subprogram body is executed. 6.4.1 says that evaluation
> of the parameter associations include the conversion to the formal subtype -
> that conversion does the check that raises Constraint_Error.

And semantically all this is a part of the body.

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:o2tlcd$1aro$2@gioia.aioe.org...
> On 14/12/2016 23:40, Randy Brukardt wrote:
>> [Yet again had to break the thread because the thread has gotten too long 
>> to
>> reply to - RLB]
>>
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>> news:o2s8l1$1fef$1@gioia.aioe.org...
>>> On 2016-12-14 20:23, Shark8 wrote:
>> ...
>>>> You are observably wrong.
>>>> If you supply a negative number, the body of X never executes.
>>>
>>> Of course it does. Semantically any effect of a call to X is due to X's
>>> body. There is nothing else there.
>>
>> This is clearly false. The definition of the execution of a subprogram 
>> call
>> (RM 6.4(10/2)) specifically says that the parameter associations are
>> evaluated before the subprogram body is executed. 6.4.1 says that 
>> evaluation
>> of the parameter associations include the conversion to the formal 
>> subtype -
>> that conversion does the check that raises Constraint_Error.
>
> And semantically all this is a part of the body.

I just quoted the rules in the RM that say specifically that it is not part 
of the body. You STILL deny that's true?? If you're redefining the meaning 
of "semantics" or "body" to suit your own world view, then it is essentially 
impossible to talk with you about Ada (one never knows when you're using a 
term in some sense other than its RM definition).

                                             Randy.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 15/12/2016 23:24, Randy Brukardt wrote:
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
> news:o2tlcd$1aro$2@gioia.aioe.org...
>> On 14/12/2016 23:40, Randy Brukardt wrote:
>>> [Yet again had to break the thread because the thread has gotten too long
>>> to
>>> reply to - RLB]
>>>
>>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>>> news:o2s8l1$1fef$1@gioia.aioe.org...
>>>> On 2016-12-14 20:23, Shark8 wrote:
>>> ...
>>>>> You are observably wrong.
>>>>> If you supply a negative number, the body of X never executes.
>>>>
>>>> Of course it does. Semantically any effect of a call to X is due to X's
>>>> body. There is nothing else there.
>>>
>>> This is clearly false. The definition of the execution of a subprogram call
>>> (RM 6.4(10/2)) specifically says that the parameter associations are
>>> evaluated before the subprogram body is executed. 6.4.1 says that evaluation
>>> of the parameter associations include the conversion to the formal subtype -
>>> that conversion does the check that raises Constraint_Error.
>>
>> And semantically all this is a part of the body.
>
> I just quoted the rules in the RM that say specifically that it is not part
> of the body.

What the problem? There is time to fix the RM wording. Call it "user 
specified body" as opposed to the "body in effect".

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:o309ac$1f4q$2@gioia.aioe.org...
> On 15/12/2016 23:24, Randy Brukardt wrote:
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>> news:o2tlcd$1aro$2@gioia.aioe.org...
>>> On 14/12/2016 23:40, Randy Brukardt wrote:
>>>> [Yet again had to break the thread because the thread has gotten too 
>>>> long
>>>> to
>>>> reply to - RLB]
>>>>
>>>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>>>> news:o2s8l1$1fef$1@gioia.aioe.org...
>>>>> On 2016-12-14 20:23, Shark8 wrote:
>>>> ...
>>>>>> You are observably wrong.
>>>>>> If you supply a negative number, the body of X never executes.
>>>>>
>>>>> Of course it does. Semantically any effect of a call to X is due to 
>>>>> X's
>>>>> body. There is nothing else there.
>>>>
>>>> This is clearly false. The definition of the execution of a subprogram 
>>>> call
>>>> (RM 6.4(10/2)) specifically says that the parameter associations are
>>>> evaluated before the subprogram body is executed. 6.4.1 says that 
>>>> evaluation
>>>> of the parameter associations include the conversion to the formal 
>>>> subtype -
>>>> that conversion does the check that raises Constraint_Error.
>>>
>>> And semantically all this is a part of the body.
>>
>> I just quoted the rules in the RM that say specifically that it is not 
>> part
>> of the body.
>
> What the problem? There is time to fix the RM wording. Call it "user 
> specified body" as opposed to the "body in effect".

What possible good would it do? If such a change subtly changed the effect 
of Ada programs, that would be very bad, and if it didn't, it would just be 
churn for no reason. (The rule of thumb being that a change that doesn't 
change the behavior of any user or implementer is an unnecessary change.)

The semantics of Ada are what the RM defines them to be, not what you or I 
or anyone else wishes they were. That's the whole point of having the 
semantics of the language defined by a Standard.

                                    Randy.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 2016-12-16 20:46, Randy Brukardt wrote:
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
> news:o309ac$1f4q$2@gioia.aioe.org...
>> On 15/12/2016 23:24, Randy Brukardt wrote:
>>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>>> news:o2tlcd$1aro$2@gioia.aioe.org...
>>>> On 14/12/2016 23:40, Randy Brukardt wrote:
>>>>> [Yet again had to break the thread because the thread has gotten too
>>>>> long
>>>>> to
>>>>> reply to - RLB]
>>>>>
>>>>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>>>>> news:o2s8l1$1fef$1@gioia.aioe.org...
>>>>>> On 2016-12-14 20:23, Shark8 wrote:
>>>>> ...
>>>>>>> You are observably wrong.
>>>>>>> If you supply a negative number, the body of X never executes.
>>>>>>
>>>>>> Of course it does. Semantically any effect of a call to X is due to
>>>>>> X's body. There is nothing else there.
>>>>>
>>>>> This is clearly false. The definition of the execution of a subprogram call
>>>>> (RM 6.4(10/2)) specifically says that the parameter associations are
>>>>> evaluated before the subprogram body is executed. 6.4.1 says that
>>>>> evaluation of the parameter associations include the conversion to the formal
>>>>> subtype - that conversion does the check that raises Constraint_Error.
>>>>
>>>> And semantically all this is a part of the body.
>>>
>>> I just quoted the rules in the RM that say specifically that it is not
>>> part of the body.
>>
>> What the problem? There is time to fix the RM wording. Call it "user
>> specified body" as opposed to the "body in effect".
>
> What possible good would it do?

It would fix wrong wording and eliminate misunderstanding about the 
semantics of parameter checks and other prologues (and epilogues!) the 
compiler uses to decorate the user body.

This is especially important for correctness proofs. A proof must take 
into account *all* body. The user body part is not enough.

And with extensible bodies (as required by initialization, finalization 
and aggregates) and the gluing code between them I don't know how are 
you going to maintain this silly concept further...

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:o31hvm$1p4s$1@gioia.aioe.org...
> On 2016-12-16 20:46, Randy Brukardt wrote:
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
...
>>>> I just quoted the rules in the RM that say specifically that it is not
>>>> part of the body.
>>>
>>> What the problem? There is time to fix the RM wording. Call it "user
>>> specified body" as opposed to the "body in effect".
>>
>> What possible good would it do?
>
> It would fix wrong wording and eliminate misunderstanding about the 
> semantics of parameter checks and other prologues (and epilogues!) the 
> compiler uses to decorate the user body.

"Wrong wording"? You'd have to find some observable case of incorrect 
behavior to make such a claim. So far as I can tell, only you have a 
"misunderstanding about the semantics", since there is no such thing as 
"decorating the user body". Some stuff happens at the call site before the 
user body is invoked. Clearly some dynamic stuff has to be done there 
(evaluation of actuals can't happen in the body for obvious reasons), and 
where one draws the line is a matter of taste.

> This is especially important for correctness proofs. A proof must take 
> into account *all* body. The user body part is not enough.

A body proof surely has to take into account the body's specification. Can't 
see how it would be otherwise. The proof of a call, OTOH, need only take 
into account whatever is in the specification of the called routine. 
Otherwise, one has given up on separation of implementation for the purposes 
of proof (and proof can only then be done on completed programs, too late in 
the development cycle to be practical).

But so far as I can tell, it doesn't matter much what is in the 
specification and what is in the body, just so that there is a good 
definition of which belongs to each.

> And with extensible bodies (as required by initialization, finalization 
> and aggregates) and the gluing code between them I don't know how are you 
> going to maintain this silly concept further...

I don't follow this at all. There's nothing different about the built-in 
extensions (mostly streams) from any other subprogram. Certainly not in 
terms of proof. (And initialization, finalization, and aggregates are not 
extensible in Ada, at least not in any significant way. Anything that might 
cause trouble has to be written explicitly, and then we're just back to the 
normal case.)

                     Randy.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 2016-12-19 23:52, Randy Brukardt wrote:
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
> news:o31hvm$1p4s$1@gioia.aioe.org...
>> On 2016-12-16 20:46, Randy Brukardt wrote:
>>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
> ...
>>>>> I just quoted the rules in the RM that say specifically that it is not
>>>>> part of the body.
>>>>
>>>> What the problem? There is time to fix the RM wording. Call it "user
>>>> specified body" as opposed to the "body in effect".
>>>
>>> What possible good would it do?
>>
>> It would fix wrong wording and eliminate misunderstanding about the
>> semantics of parameter checks and other prologues (and epilogues!) the
>> compiler uses to decorate the user body.
>
> "Wrong wording"? You'd have to find some observable case of incorrect
> behavior to make such a claim.

You already did it. According to the wording there exist implementations 
that do not raise Constraint_Error but being called still do (due to 
"out-of-body experience" range check). This is a trivial contradiction.

> So far as I can tell, only you have a
> "misunderstanding about the semantics", since there is no such thing as
> "decorating the user body". Some stuff happens at the call site before the
> user body is invoked. Clearly some dynamic stuff has to be done there
> (evaluation of actuals can't happen in the body for obvious reasons), and
> where one draws the line is a matter of taste.

Exactly this mess!

>> This is especially important for correctness proofs. A proof must take
>> into account *all* body. The user body part is not enough.
>
> A body proof surely has to take into account the body's specification.

A specification that does not correspond to the implementation! 
According to the wording, the specification tells it raises, and the 
"body" does not.

> Can't see how it would be otherwise.

Elementary, the specification and the body must correspond each other.

>> And with extensible bodies (as required by initialization, finalization
>> and aggregates) and the gluing code between them I don't know how are you
>> going to maintain this silly concept further...
>
> I don't follow this at all. There's nothing different about the built-in
> extensions (mostly streams) from any other subprogram.

Certainly checks decorating user-defined bodies of stream attributes for 
some components may raise something. According to the nonsense you are 
defending, these would not be the result of the body, being propagated 
right from the middle of its execution...

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:o3b2va$153k$1@gioia.aioe.org...
> On 2016-12-19 23:52, Randy Brukardt wrote:
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>> news:o31hvm$1p4s$1@gioia.aioe.org...
>>> On 2016-12-16 20:46, Randy Brukardt wrote:
>>>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>> ...
>>>>>> I just quoted the rules in the RM that say specifically that it is 
>>>>>> not
>>>>>> part of the body.
>>>>>
>>>>> What the problem? There is time to fix the RM wording. Call it "user
>>>>> specified body" as opposed to the "body in effect".
>>>>
>>>> What possible good would it do?
>>>
>>> It would fix wrong wording and eliminate misunderstanding about the
>>> semantics of parameter checks and other prologues (and epilogues!) the
>>> compiler uses to decorate the user body.
>>
>> "Wrong wording"? You'd have to find some observable case of incorrect
>> behavior to make such a claim.
>
> You already did it. According to the wording there exist implementations 
> that do not raise Constraint_Error but being called still do (due to 
> "out-of-body experience" range check). This is a trivial contradiction.

I don't understand "but being called still do". In any case, a body is not 
called if evaluating the parameters raise an exception; a call (like 
everything else) is a multi-part process.

In any case, some part of the execution of a subprogram call has to be 
evaluated at the call site, since the details of the actual parameters 
cannot be part of the body (they'll be different for every call). And those 
evaluations can raise exceptions. So the only question is precisely where 
the line is drawn, and that is only important in that it is precisely 
defined - the exact definition doesn't matter.

To take an example. The rule is that all parameter expressions are 
implicitly converted to the type/subtype of the parameter in a call.

     X : constant Integer := 0;
    procedure Foo (P : Positive);

   Foo (10 / X); -- Clearly, the evaluation of the call raises 
Contraint_Error (for a divide-by-zero). The body never executes.

   Foo (Positive(X)); -- Clearly, the evalation of the call raises 
Constraint_Error (for a conversion failure). The body never executes.

   Foo (X); -- Raises Constraint_Error because the implicit conversion is 
the same as the explicit onew given above. Again, the body never executes.

My understanding is that the designers of Ada 83 wanted the semantics of the 
last two calls to be exactly the same, as the former is just the explicit 
version of the implicit conversion of the second call. It would be unusual 
if they executed differently at all. (On top of which, the rules for 
derivation include similar implicit conversions, and those conversions need 
to work the same as similar code written explicitly.) None of that has ever 
been changed since Ada 83.

...
>> So far as I can tell, only you have a
>> "misunderstanding about the semantics", since there is no such thing as
>> "decorating the user body". Some stuff happens at the call site before 
>> the
>> user body is invoked. Clearly some dynamic stuff has to be done there
>> (evaluation of actuals can't happen in the body for obvious reasons), and
>> where one draws the line is a matter of taste.
>
> Exactly this mess!

It has to be true, there is no alternative. You just want to move the line a 
bit, but there is no advantage to doing that. But it necessarily would 
produce worse code (an Ada compiler is not allowed to look into bodies 
outside of Inline), and it also would make implicit and explicit conversions 
work differently.

>>> This is especially important for correctness proofs. A proof must take
>>> into account *all* body. The user body part is not enough.
>>
>> A body proof surely has to take into account the body's specification.
>
> A specification that does not correspond to the implementation! According 
> to the wording, the specification tells it raises, and the "body" does 
> not.
>
>> Can't see how it would be otherwise.
>
> Elementary, the specification and the body must correspond each other.

And of course they do. Ada has rules that require them to be exactly the 
same. So what? Some rules are checked before the actual call is made, and 
some after. All that is important is that which are checked where are 
well-defined. It's impossible to check all rules at one place or the other.

>>> And with extensible bodies (as required by initialization, finalization
>>> and aggregates) and the gluing code between them I don't know how are 
>>> you
>>> going to maintain this silly concept further...
>>
>> I don't follow this at all. There's nothing different about the built-in
>> extensions (mostly streams) from any other subprogram.
>
> Certainly checks decorating user-defined bodies of stream attributes for 
> some components may raise something. According to the nonsense you are 
> defending, these would not be the result of the body, being propagated 
> right from the middle of its execution...

The result of *which* body? In this case, (as in all cases involving 
implicit things) there are implicit calls of the original bodies. There's no 
actual combining of routines (that would be problematic both semantically 
and implementationally). And of course implicit calls follow the rules of 
other calls.

                               Randy.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Dmitry A. Kazakov]

On 2016-12-21 01:50, Randy Brukardt wrote:

> In any case, some part of the execution of a subprogram call has to be
> evaluated at the call site, since the details of the actual parameters
> cannot be part of the body (they'll be different for every call). And those
> evaluations can raise exceptions.

This is all OK.

> So the only question is precisely where
> the line is drawn, and that is only important in that it is precisely
> defined - the exact definition doesn't matter.

The line is drawn at the [sub]type border. Once the parameter is of the 
nominal [sub]type it is the body-in-effect. Once the out parameter or 
result changes the [sub]type it is out of the body-in-effect.

> To take an example. The rule is that all parameter expressions are
> implicitly converted to the type/subtype of the parameter in a call.
>
>      X : constant Integer := 0;
>     procedure Foo (P : Positive);
>
>    Foo (10 / X); -- Clearly, the evaluation of the call raises
> Contraint_Error (for a divide-by-zero). The body never executes.
>
>    Foo (Positive(X)); -- Clearly, the evalation of the call raises
> Constraint_Error (for a conversion failure). The body never executes.
>
>    Foo (X); -- Raises Constraint_Error because the implicit conversion is
> the same as the explicit onew given above. Again, the body never executes.
>
> My understanding is that the designers of Ada 83 wanted the semantics of the
> last two calls to be exactly the same, as the former is just the explicit
> version of the implicit conversion of the second call. It would be unusual
> if they executed differently at all. (On top of which, the rules for
> derivation include similar implicit conversions, and those conversions need
> to work the same as similar code written explicitly.) None of that has ever
> been changed since Ada 83.

The effect of two last calls maybe same, the attributed semantics is 
not. From the POV of a typed system the last call must be to an Integer 
operation composed from the original Foo and a type conversion 
Integer->Positive.

A composition of two operations is exactly calling one and then another. 
No difference.

Theoretically we should be able to pass Integer Foo as a parameter to 
another subprogram or generic expecting procedure (X : Integer). This is 
rightfully prevented for Positive Foo by subtype conformance. That would 
be a case where semantic difference would play a role.

> It has to be true, there is no alternative. You just want to move the line a
> bit, but there is no advantage to doing that. But it necessarily would
> produce worse code (an Ada compiler is not allowed to look into bodies
> outside of Inline), and it also would make implicit and explicit conversions
> work differently.

I don't see why they should. Nothing requires the body-in-effect be one 
chunk of code. The compiler is free to inline any of its parts.

>>> I don't follow this at all. There's nothing different about the built-in
>>> extensions (mostly streams) from any other subprogram.
>>
>> Certainly checks decorating user-defined bodies of stream attributes for
>> some components may raise something. According to the nonsense you are
>> defending, these would not be the result of the body, being propagated
>> right from the middle of its execution...
>
> The result of *which* body? In this case, (as in all cases involving
> implicit things) there are implicit calls of the original bodies. There's no
> actual combining of routines (that would be problematic both semantically
> and implementationally). And of course implicit calls follow the rules of
> other calls.

No body no implementation, what is being called?

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

Re: Ada 2012 Constraints (WRT an Ada IR)

[Randy Brukardt]

[Breaking the thread yet again because of too many replies. Sorry.]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
news:o3e8nc$593$1@gioia.aioe.org...
> On 2016-12-21 01:59, Randy Brukardt wrote:
...
>> One certainly can reason about it.
>
> You can tell nothing about such subsets, they are general case subsets.

I suspect that most mathematicians would be surprised to hear that. :-)

> They are worse than that, if the constraint is allowed to use non-local
> dynamic Boolean functions. That would produce non-sets.

As I clearly said before, static_prediates require very restricted
expressions that correspond to a compile-time known set. No dynamic anything
is allowed (nor are any function calls), which should be obvious from the
name alone.

                                   Randy.

Re: Ada 2012 Constraints (WRT an Ada IR)

[Shark8]

On Wednesday, December 21, 2016 at 3:03:30 PM UTC-7, Randy Brukardt wrote:
> [Breaking the thread yet again because of too many replies. Sorry.]
> 
> "Dmitry A. Kazakov" wrote in message
> > On 2016-12-21 01:59, Randy Brukardt wrote:
> ...
> >> One certainly can reason about it.
> >
> > You can tell nothing about such subsets, they are general case subsets.
> 
> I suspect that most mathematicians would be surprised to hear that. :-)

I certainly am.
In fact it seems so foundational; that 'absurd' seems to fit well.

> 
> > They are worse than that, if the constraint is allowed to use non-local
> > dynamic Boolean functions. That would produce non-sets.
> 
> As I clearly said before, static_prediates require very restricted
> expressions that correspond to a compile-time known set. No dynamic anything
> is allowed (nor are any function calls), which should be obvious from the
> name alone.

Well, we obviously can't rely on the LRM's definitions, as exemplified upthread... what makes us think we could rely on mathematics?

;)

Re: Ada 2012 Constraints (WRT an Ada IR)

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
news:o3erdj$169p$1@gioia.aioe.org...
...
> When predicate is not a complete function of the argument, e.g.
>
>    P (x) = (Integer (Clock - Epoch) mod 2) = 1

Complete straw man -- this isn't legal for a static predicate, which is the
case in question.

It's legal for a dynamic predicate, but that's just an assertion, no more,
no less, and not the topic of this thread in any case.

Static and dynamic predicates are completely different things, especially in
terms of the reasoning that you can apply to them. I think it's evil that
GNAT allows confusing them by just calling the thing a "predicate", on top
of which that it is not portable.

                              Randy.