Re: N*log(N) doesn't exist (Re: [RFC] Vector (string?) growth...)

[Gabriel Dos Reis <gdr at integrable-solutions dot net>]

Paolo Carlini <pcarlini@suse.de> writes:

| Gabriel Dos Reis wrote:
| 
| > | Still, this is the first time that I notice that a requirement in the
| > | standard cannot strictly speaking be assessed. So to speak, there are
| > | areas where it's "undecidable" ;) if a library, running on a finite
| > | system, is conforming or not.
| >
| > The standard is not written with all mathematical rigour, so I don't
| > know how you define "strctly speaking assessed".
| 
| Eh, right, but this is a slippery slope... I'm definitely not Bourbaki-an
| in math (I'm not a mathematician at all ;) but in other areas things seem
| simpler. For instance, talking of strings or vectors, requiring a given
| behavior for push_back, I don't know, perhaps we could even formalize it
| couldn't we? 

It could be done.  You "just" need to formalize the underlying
abstract machine (for example you might not want to include the
infamous "volatile" that imply that an alpha ray fired up from Alpha
Centuri may have an effect unknown to the compiler.  I suspect that
you may probably use "Hoare logic". 

| Well, all over the world, real mathematicians prove theorems
| about strings of zeros and ones as abstract dynamical systems..

Yep.  There is a huge amount of research there; but one of the most
important thing is your specific case is to come up with a good
axiomatic description of the C++ abstract machine.

-- Gaby