Re: Ada 2012 Constraints (WRT an Ada IR)

[Shark8 <onewingedshark@gmail.com>]

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.