What about a Static_Assertion?

What about a Static_Assertion?

[Yannick Duchêne (Hibou57)]

Hi Ada novelists,


Don't you believe it would be great to have static assertion just like we  
have static predicates?

Would play the role of a package Static_Predicate when at package level  
and of an implementation Static_Predicate when at a sub‑program level.

Assertions are great, but I can't avoid the feeling more distinction  
between the very different kinds (very different in the implications) of  
assertions would be profitable.

To be more precise, I see at least three kinds:

  * The assertion uses a static expression
  * The assertion uses a constant expression (may not be static!)
  * The assertion uses a variable expression

All three are not the same, and it would be nice to be allowed to  
explicitly state the kind of assertion we are making. The compiler could  
check what is said to be a constant assertion does not unfortunately  
depends on a variable entity, and this would help to trust and better  
understand the consequence of what you read.

I believe this would not be too much a nightmare to be added to any Ada  
202X, this would just requires a check on the kind of the expression used  
for the assertion, and failure of a static assertion, could be said to  
make the compilation to necessary fails.

So what about to have `pragma Static_Assertion (…)`, `pragma  
Constant_Assertion (…)` and `pragma Assert (…)` (the classic one, for  
variable assertions)?

-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

Re: What about a Static_Assertion?

[Dmitry A. Kazakov]

On Tue, 23 Jul 2013 20:07:54 +0200, Yannick Duchêne (Hibou57) wrote:

> Don't you believe it would be great to have static assertion just like we  
> have static predicates?

What is the difference between assertion and precondition or invariant?
 
-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: What about a Static_Assertion?

[Yannick Duchêne (Hibou57)]

Le Tue, 23 Jul 2013 20:43:19 +0200, Dmitry A. Kazakov  
<mailbox@dmitry-kazakov.de> a écrit:

> On Tue, 23 Jul 2013 20:07:54 +0200, Yannick Duchêne (Hibou57) wrote:
>
>> Don't you believe it would be great to have static assertion just like  
>> we
>> have static predicates?
>
> What is the difference between assertion and precondition or invariant?
>

An assertion may applies to multiple things at a time. I like to see an  
assertion as hypothesis (and I prefer the hypothesis to be statically  
checkable :-P ), and it is an hypothesis I may refer to from multiple  
place in a package (although I may like to duplicate it in multiple case),  
not from a single sub‑program.

Also, there is no distinction between private and public predicates, while  
a can put an assertions in a package body, which I will refer to, to  
“prove” the implementation is correct (at least free of runtime errors), I  
can't do the same with a predicate. For hypothesis used in the  
implementation only, public sub‑program predicates are not suitable.

By the way, I don't believe assertions are seen as a deprecated feature,  
and that suggest from many one's eyes, it is indeed different and can't be  
replaced by the actual predicates.

-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

Re: What about a Static_Assertion?

[Dmitry A. Kazakov]

On Tue, 23 Jul 2013 20:57:05 +0200, Yannick Duchêne (Hibou57) wrote:

> Le Tue, 23 Jul 2013 20:43:19 +0200, Dmitry A. Kazakov  
> <mailbox@dmitry-kazakov.de> a écrit:
> 
>> On Tue, 23 Jul 2013 20:07:54 +0200, Yannick Duchêne (Hibou57) wrote:
>>
>>> Don't you believe it would be great to have static assertion just like  
>>> we have static predicates?
>>
>> What is the difference between assertion and precondition or invariant?
> 
> An assertion may applies to multiple things at a time. I like to see an  
> assertion as hypothesis (and I prefer the hypothesis to be statically  
> checkable :-P ), and it is an hypothesis I may refer to from multiple  
> place in a package (although I may like to duplicate it in multiple case),  
> not from a single sub‑program.

This does not make any sense. Provided we are talking about static things,
they by definition hold to the program as a whole.
 
> By the way, I don't believe assertions are seen as a deprecated feature,  
> and that suggest from many one's eyes, it is indeed different and can't be  
> replaced by the actual predicates.

Predicate by definition is a Boolean expression.

http://en.wikipedia.org/wiki/Predicate_%28mathematical_logic%29

Assertion, precondition, postcondition, invariant are all predicates. What
Ada 2012 calls "static predicate" is also a predicate.

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

Re: What about a Static_Assertion?

[Georg Bauhaus]

On 23.07.13 20:07, Yannick Duchêne (Hibou57) wrote:
>
> I believe this would not be too much a nightmare to be added to any Ada 202X, this would just requires a check on the kind of the expression used for the assertion, and failure of a static assertion, could be said to make the compilation to necessary fails.

It should take no more than a little syntax, I think, and
no other changes to compilers are needed, insofar as compilers
have calculated static Boolean expressions for a long time.
The following two static tests builds on discrete_choice_lists
covering all values in type Boolean:

package Static_Assertion is

    Test: constant Boolean := ((not True) or False);
    -- see below

private

    type Check1 (Dummy : Boolean) is
       record
          case Dummy is
             when Test => null;
             when False => null;
          end case;
       end record;

    type Nix is access constant Boolean;
    for Nix'Storage_Size use 0;

    Check2 : constant array (Boolean) of Nix :=
      (Test => null,
       False => null);

end Static_Assertion;

Check2 declares an object, while Check1 does not.