Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.lang.c > #401210

Re: Constants and undefined behavior

Show key headers only | View raw

antispam@fricas.org (Waldek Hebisch) writes:

> Tim Rentsch <tr.17687@z991.linuxsc.com> wrote:
>
>> antispam@fricas.org (Waldek Hebisch) writes:
>>
>> [...]
>>
>>> I think that lawyerish style of current C standard is mostly
>>> inertia,
>>
>> I wouldn't use a term like lawyerish to describe the text in the
>> ISO C standard.  Can you explain what quality you mean to ascribe
>> to "lawyerish" writing in the C standard without using any term
>> related to lawyering or legal documents?
>
> Sorry no, I can not.  My point is that you need to treat
> C standard almost like legal document and I can not explain
> this without using proper terminology.
>
>>> and making standard more mathematical would improve it.
>>
>> Could you elaborate on that statement?  In what ways would giving
>> a more mathematical treatment of C semantics improve the quality
>> of the ISO C document?  How would doing that advance the stated
>> purposes or goals of the C standard?
>
> There are many aspect of mathematical treatment.  One is care
> about terminology, namely that terms are either reasonably
> clearly marked as "primitve" (and assumed to be understood
> by readers) or are precisely defined.  Related is that
> words can be taken as written, without needing to look at
> intent or similar legal style arguments.  You may think that
> C standard already posseses such properties, but recent
> example, that is definition of expression nicely illustrates
> current problems.  With mathematical treatment expression
> would be part of C program derived from corresponding
> grammar rule and that would resolve the problem.  In the
> past in this group there were several discussions about
> various parts of C standard, and there were cases were
> standard wording looked genuinly confusing.  I am not
> prepared to dig into those discussions, but my impression
> was that in some cases mathematical treatment would make
> things clearer.
>
>>> But giving formal semantic in the standard would mean
>>> significantly bigger change.
>>
>> Due to the nature of C, I believe it is effectively impossible to
>> give a formal mathematical definition of the semantics of C.  Do
>> you think such a thing is feasible or practicable?  If so can you
>> explain the reasoning behind your thinking?
>
> I think that this is possible given dedicated team of qualified
> people doing the work.  I do not know if it is practically
> possible to assemble needed team.  I already mentioned axiomatic
> semantics.  There is C grammar and we need to assign semantics
> to various production rules.  We do this assigning precondtions
> and postcondtions to the rules.  In much simpler cases this
> was done.  C is bigger language and rules are more complicated,
> but that for me looks like quantitive problem, that is there is
> more work and result will be bigger.  Clearly, this would
> require buy-in from the standard body.  Namely, formalization
> is likely to uncover many unclear places in C standard and
> ensuring that formalization matches the standard would require
> resolution by the standard body.  It is quite possible that
> standard body would refuse to cooperate.  To explain this more,
> let me mention past discussion about Extended Pascal in a
> different forum.  I was looking at types of constants, but in
> specific case rules looked contradictory, so I asked a
> question.  One response was from former commitee member (this
> was several years after Pascal standard was ratified), he
> basicaly said that type of constants does not matter.  Which
> was mostly true, but my reason for asking the question was
> that validity of programs depended on types of constants.
> Something similar may happen during formalization:
> formalization may discover unclear places in C standard
> which C commitee considers irrelevant in practice and
> refuses to clarify.
>
> BTW:  Authors of some tools already need and have formal
> semantics for language rather close to C.  Namely,
> Comp-Cert compiler is matching conditions in source
> code with machine code and for that it needs reasonably
> good aproximation to formal semantics of language implemented
> by C compiler (more precisely gcc).  Microsoft developed
> formal checking tools and that too needs formal semantics.
> But since goals are different neither give semantics of
> standard C.

A disappointing response.  You can't explain what you mean.
The properties ascribed to a mathematical writing might
just as well be met by more clearly written English.  About
defining a formal semantics, all you really say is you think
it is possible, under some not very well defined conditions.
All in all not too compelling.

Back to comp.lang.c | Previous | Next — Previous in thread | Find similar | Unroll thread

Thread

Re: Constants and undefined behavior Tim Rentsch <tr.17687@z991.linuxsc.com> - 2026-06-21 15:26 -0700
  Re: Constants and undefined behavior antispam@fricas.org (Waldek Hebisch) - 2026-06-22 03:40 +0000
    Re: Constants and undefined behavior Tim Rentsch <tr.17687@z991.linuxsc.com> - 2026-08-15 07:50 -0700

csiph-web