Re: Compiler quality (was: Extending discriminant types)

[anon@anon.org (anon)]

Your not understanding the concept finite for programs. And this explanation 
does not the finite concept of hardware.

The Ada RM states in 2.2 (15) that the implementation must support at least 
200 character in a line length and lexical elements. But the RM allows the 
implementation to set the default maximum size.

So, by definition a identifier (a lexical elements) is define as:

RM 2.3 (2)   identifier ::=   identifier_letter {[underline] letter_or_digit}
RM 2.3 (3)   letter_or_digit ::= identifier_letter | digit


RM 2.1 (7)   identifier_letter
                upper_case_identifier_letter | lower_case_identifier_letter

RM 2.1 (8)   upper_case_identifier_letter
                Any character of Row 00 of ISO 10646 BMP whose name begins
                ``Latin Capital Letter''.

RM 2.1 (9)   lower_case_identifier_letter
                Any character of Row 00 of ISO 10646 BMP whose name begins
                ``Latin Small Letter''.

RM 2.1 (10)  digit =>   One of the characters 0, 1, 2, 3, 4, 5, 6, 7, 8, or 9.



So, identifier has only a finite number of characters that may be use, with the 
length set by the vendor there exist only a finite number of identifiers that the 
vendor's compiler can use. That number may be large by the RM definition but 
it is still finite value.

Which means there is NO infinite number of identifier, so your are in error 
about infinite.

So anyone can create a program that can create a single to multi set of 
programs to test every identifier that a vendors's compiler can use.

And every statement type is defined in the RM and because the vendor also set 
limits, there exist only a finite number of statements.

Also, for testing identifier in GNAT you can use the "-gnatMxx" where xx is a 
smaller number such as 10 to 15 another finite number. That way, the number 
of identifier is more manageable.


The problem is, do you need to generate every statement to prove there is no 
syntax BUGs in a computer. 
The answer is no! 

An example is like using the following statement

                   X := Sin ( A ) + Cos ( W ) ;

do use need to also create the statement

                   X := Cos ( W ) + Sin ( A ) ;

to prove that a simple mathematical statement is BUG free.  The answer is no! 
So a vendor may use one not both to perform the test, to say the statement 
checking is BUG free.  

And using every statement that can be created is just overkill, but it can be 
done. There are places in a compiler that are tested to the point of being 
BUG free and that number of testing is finite. 


In <9cb27caa-8e9f-4123-ad36-4980c3032722@20g2000yqt.googlegroups.com>, Ludovic Brenta <ludovic@ludovic-brenta.org> writes:
>On Nov 25, 12:33 am, a...@anon.org (anon) wrote:
>> You also forget that Adacore has 100s may be even 1,000,000s of simple
>> files they use for syntax checking for each Ada specifications.  That can
>> trap all syntax type of errors. And that group of files grows yearly, if not
>> daily.
>
>Apparently you also forgot to read what I wrote earlier:
>
>> Even an infinite amount of testing cannot prove a program to be bug-
>> free; it can only uncover an infinite amount of bugs. If you want to
>> prove a program correct, you must use formal methods, not testing.
>
>The rest of your rantings are only a consequence of this basic
>misunderstanding of yours.
>
>--
>Ludovic Brenta.