Adapting software to multiple usage patterns

[Nick Keighley]

Well they try by using english with a specialised vocabulary. Though
the number of arguments in clc indicates how successful this is...

If you mean you're using a term in a way that almost no
one else uses it, I agree with you.

oh I don't know there a plenty of people who use the term "formal"
when they mean "partially formal" or "nearly formal". Hence my "little
bit pregnant" comment.

 

[Keith Thompson]

It is of course possible to write a formal semantics
for C, or any other programming languge. My comment
was about C's official specification in the ISO standard
documents.

The allegedly laughable comment (from Richard Heathfield) was:

Permaybehaps. I think if you focus only on the subset of C that
always exhibits well-defined behaviour (i.e. ignore all programs
that invoke UB or USB or IDB), it's not unreasonable to call that
subset a formal system.

I'd argue that whether something qualifies as a formal system is
independent of whether and where a formal semantics for it has been
written down.

 

[jacob navia]

Tim Rentsch a écrit :

It is of course possible to write a formal semantics
for C, or any other programming languge. My comment
was about C's official specification in the ISO standard
documents.

The document is VERY interesting. It shows the limits of those approaches.

The author has entered the C grammar into a theorem prover. Obviously not
the WHOLE grammar but a fairly large subset of it.

Then, he tries to prove

void strcpy(char *s, char *t) { while (*s++ = *t++) ; }

This is too much for the theorem prover, so he has to
rearrange the loop into:

while (*t) {*s = *t;s++;t++;}
*s = *t;
s++;
t++;

And then he successfully proves that...

The next program (a 400 line piece of C program) was impossible to
prove.

Imagine the complexity of proving a normal piece of software in
the 10 000 lines range.

Another problem is that the formal system is dependent on...
another system called HOL, the theorem prover!

It is not proven that HOL has no bugs, and it is not proven that
the author did not any mistake when writing the HOL grammar the
is used as the basis of the approach.

In any case it is a very interesting piece of work.

 

[lawrence.jones]

It is of course possible to write a formal semantics
for C, or any other programming languge. My comment
was about C's official specification in the ISO standard
documents.

Yes, the committee thought it more valuable to have an informal
specification that most people could read and understand rather than a
formal one that hardly anyone could.

 

[Tim Rentsch]

Well they try by using english with a specialised vocabulary. Though
the number of arguments in clc indicates how successful this is...

Yes, the standard is written in formal English. Actually
I think it does a pretty good job of defining things
unambiguously, although obviously there are some exceptions.

oh I don't know there a plenty of people who use the term "formal"
when they mean "partially formal" or "nearly formal". Hence my "little
bit pregnant" comment.

My comment was made about "formal system", not just the "formal"
part. Certainly the standard is written in formal English.
That's different from being a formal system, and I think it's
important to distinguish the two.

 

[Phil Carmody]

Ah, but the C library, as defined by the language standard, does not
use camel case, and this would almost certainly be what Seebs was
referring to.

_Bool isn't exactly the prettiest thing in the world, though.

Phil

 

[Seebs]

I feel obliged to point out that the Standard itself makes the same
distinction that Jacob does here. Section 6 is Language. Section 7
is Library.

Yes. But they are both part of the standard for the C Language.

The language contains both language and library.

As someone recently pointed out, it's not exactly a rigorous formal model.

-s

 

[Seebs]

C doesn't /use/ any case. It copes with camel case precisely
as well as it copes with lower case.

Standard usage, though, has rigorously avoided camel case, and I think
that even just fixing that and using more C-like names would improve the
chances of people being convinced to use the container library.

-s

 

[Tim Rentsch]

The allegedly laughable comment (from Richard Heathfield) was:

Permaybehaps. I think if you focus only on the subset of C that
always exhibits well-defined behaviour (i.e. ignore all programs
that invoke UB or USB or IDB), it's not unreasonable to call that
subset a formal system.

I'd argue that whether something qualifies as a formal system is
independent of whether and where a formal semantics for it has been
written down.

Saying something is a formal system normally means it is expressed
using a precise mathematical characterization. The C standard is
written in formal English, but certainly it is not a precise
mathematical characterization. C is defined by the various ISO
documents; what C is may be /formalizable/, but that doesn't make
it a formal system.

Note that, for any implemented programming language, it's always
possible to formalize (one version of) the programming language,
simply by giving the program that implements it as the formal
definition. Presumably the comments above were about C as
it is defined by the ISO documents; in talking about whether
C is a formal system, it's important to talk about that
definition, because a different definition may very well
(and the case of C probably will) define a different language.

Probably it would have been better if I'd written this more
complete explanation in place of my original short statement.
Occasionally I too succumb to the temptation of posting
sound bites. (And please, no jokes about "sound bytes".

 

[Seebs]

_Bool isn't exactly the prettiest thing in the world, though.

Certainly not. Basically a namespace issue.

-s

 

[Tim Rentsch]

Yes. But they are both part of the standard for the C Language.

The language contains both language and library.

As someone recently pointed out, it's not exactly a rigorous formal model.

OMG! Hoist with my own petard...

 

[Tim Rentsch]

Yes, the committee thought it more valuable to have an informal
specification that most people could read and understand rather than a
formal one that hardly anyone could.

Right. Definitely the better choice in this case IMO.

 

[Keith Thompson]

_Bool isn't exactly the prettiest thing in the world, though.

Agreed, but that's not camel case.

When inventing a new keyword, the committee needed to choose an
identifier reserved for all purposes. It had to be something
starting either with two underscores, or with an underscore and an
uppercase letter. I think _Bool is better than __bool. I suppose
they could have used __BOOL, but that looks like a macro name rather
than a keyword. And for normal use, it's hidden behind the "bool"
macro in <stdbool.h>. Same for _Complex and _Imaginary.

Of course just using "bool" (as C++ did) would have been ideal if not
for the fact that it would have broken existing code.

 

[Keith Thompson]

Saying something is a formal system normally means it is expressed
using a precise mathematical characterization. The C standard is
written in formal English, but certainly it is not a precise
mathematical characterization. C is defined by the various ISO
documents; what C is may be /formalizable/, but that doesn't make
it a formal system.

[...]

Hmm. We're definitely getting into angels-on-pinheads territory
here, but ...

Suppose you have a language that *is* defined by a formal semantics;
that language is a formal system. You then write an equivalent
informal description of the same language, comparable to the current
C standard, and burn the only copy of the document defining the
formal semantics. Does the language stop being a formal system?

(Personally, I find the question more interesting than any likely
answer.)

 

[Tech07]

One of the main arguments being advanced by the people that oppose
the standardization of a container library in C is the fact that
there are many different usage patterns for such a library, and it
would be impossible to satisfy them all.

The solution proposed overcomes this problem in an elegant way
by using a function table.

That's silly.

For example, let's see how that would work in lists, one of the
simplest containers.

As it stands now, the list header structure, with free list, pointer
to first, last, a size_t for the count of the items, and several
other fields could be "top heavy", and bring too much overhead if
the list is very small. For instance, if you know in advance
that you will never store more than 5 items at a time in the
list, such a "top heavy" overhead would be too much.

The solution is to write a specialization of the list
software for very small lists, where (for instance)
you just allocate all the 5 items at once when creating the
list, you eliminate the free list and the heap manager.

You're on the right track (sort of). But developing a theory of container
design based on one requirement is, well, lame. Of course, your "track" is:
How to shoehorn containers into C. To which I "reply": why bother? It would
seem that there are people that would like C to remain stagnant and you're
trying to clean up the water(?) Been there, done that: better to move to a
better location. OK, been there, done that too. So, better to build your own
house/country/whatever, the way you like it (or the way you think others
will like it, if that's your goal).

Jacob, when you keep trying to meld your concepts onto C, to me you seem
light-years behind. Put all that know-how into a new language, and you're
way ahead. I don't have compiler technology in my workshop, for example
(yet?). (.02).

 

[Tech07]

One of the main arguments being advanced by the people that oppose
the standardization of a container library in C is the fact that
there are many different usage patterns for such a library, and it
would be impossible to satisfy them all.

Or maybe they are wrong or lying or maybe you're trying to exploit that. ? I
dunno, are you "that smart"?

 

[Phil Carmody]

Agreed, but that's not camel case.

It does have a bit of a bump, though. And for perversity, there's
also some anti-camel usage: PRIiLEAST32! Pretence that cosmetic
optimality has been achieved will be laughed at.

When inventing a new keyword, the committee needed to choose an
identifier reserved for all purposes. It had to be something
starting either with two underscores, or with an underscore and an
uppercase letter. I think _Bool is better than __bool. I suppose
they could have used __BOOL, but that looks like a macro name rather
than a keyword.

Booleans are such a restricted type, having only two values, that I
think they should have just used 'restrict' for its name.

Phil

 

[Tim Rentsch]

Saying something is a formal system normally means it is expressed
using a precise mathematical characterization. The C standard is
written in formal English, but certainly it is not a precise
mathematical characterization. C is defined by the various ISO
documents; what C is may be /formalizable/, but that doesn't make
it a formal system.

[...]

Hmm. We're definitely getting into angels-on-pinheads territory
here, but ...

Suppose you have a language that *is* defined by a formal semantics;
that language is a formal system. You then write an equivalent
informal description of the same language, comparable to the current
C standard, and burn the only copy of the document defining the
formal semantics. Does the language stop being a formal system?

There's an assumption in there that the two documents define the
same language. Do they? We know from experience that different
people form different opinions about what ISO C is; moreover this
happens despite ISO C being defined in carefully written, formal
English. The only way we can be sure that the two descriptions
define the same language is if the second description is just as
technically precise as the first. In other words, if the two
documents really define the same language, the second document
must also be precise enough to serve as a statement of formal
semantics.

Note that if we _can't_ be sure whether two language documents
define the same language then the two languages are necessarily
different, because at least one of them will be ambiguous about
what language is being defined.

 

[jacob navia]

Tim Rentsch a écrit :

There's an assumption in there that the two documents define the
same language. Do they? We know from experience that different
people form different opinions about what ISO C is; moreover this
happens despite ISO C being defined in carefully written, formal
English. The only way we can be sure that the two descriptions
define the same language is if the second description is just as
technically precise as the first. In other words, if the two
documents really define the same language, the second document
must also be precise enough to serve as a statement of formal
semantics.

Note that if we _can't_ be sure whether two language documents
define the same language then the two languages are necessarily
different, because at least one of them will be ambiguous about
what language is being defined.

How many times in this group we are left with interpreting the
obscure wordings of the C standard?

Not to speak about the buffer overflow error in the C standard
in the code of the asctime() function. Not to speak about functions
described in the library that will never be able to have correct
behavior unless they are lucky: YES gets() is in the C standard.

The C standard is an important document, but it is nowhere
near what we could call a coherent formal system, and I do not
think that that was the intent anyway.

 

[Stefan Ram]

There's an assumption in there that the two documents define
the same language. Do they?

A very valid question!

In fact, it can not be answered, because to answer it, a
formal meta-system (meta-calculus) would be required that
contains both the »non-formal« specification and the
formal specification and then defines the rules for when
they are deemed to »define the same language«.

But, first, we do not have such a meta-system, and, second,
even if we had such a meta system, it would be subject
to discussions of its correctness itself.

Thus, every formal specification derived from a less formal
specification must be deemed to be an /interpretation/ of
the less formal specification; and such an interpretation
never is unique, because, if it would be unique, then the
less formal specification already would be unique, that is,
formal.

(ISO/IEC 9899:1999 (E) already uses a formal notation for
the syntax, so this discussion only is about semantics.
If the set of programs would be finite, one might compare
the semantics for each possible program. But a derivation
of semantics for an individual program from the non-formal
specification, again, is an /interpretation/.)

The best one can say about such a formal specification
therefore is, that - so far - there is no known
contradiction to the less formal specification that is being
interpreted by the formal specification.