<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<div class="moz-cite-prefix">Dear Mr Jones,</div>
<div class="moz-cite-prefix"><br>
</div>
<div class="moz-cite-prefix">Le 09/12/2019 à 15:38, Derek M Jones a
écrit :<br>
</div>
<blockquote type="cite"
cite="mid:9ae682de-ac35-c88d-e3fa-eee71ec4ad67@knosof.co.uk">
<blockquote type="cite" style="color: #000000;">"The second
contribution is a <b class="moz-txt-star"><span
class="moz-txt-tag">*</span>soundness proof<span
class="moz-txt-tag">*</span></b> for this algorithm,
<br>
mechanized using
<br>
the Coq proof assistant, guaranteeing with the highest
confidence that
<br>
if the
<br>
validation of an automaton A against a grammar G succeeds, then
the automa-
<br>
ton A and the interpreter that executes it form a <b
class="moz-txt-star"><span class="moz-txt-tag">*</span>correct<span
class="moz-txt-tag">*</span></b> parser for
<br>
G." (p. 2 of the paper, bold is mine)
<br>
</blockquote>
<br>
There is no proof that the grammar G has any connection to C, or
<br>
any other language.</blockquote>
<p>Of course. The grammar G is the specification, we go back to
other discussion thread, where I said the specification should be
checked through other means.</p>
<p>In the case of CompCert certification for Airbus, an interpreter
was built using the grammar and its associated formal semantics,
and this interpreter was thoroughly tested. If I remember
correctly discussion with one researcher behind CompCert, 4 bugs
were found. All in the dark corners of the C language semantics.</p>
<p>By the way, how do you know that the grammar of C used in gcc,
Clang, diab or any other C compiler is the correct one?<br>
</p>
<p>Best regards,<br>
D. Mentré</p>
<p><br>
</p>
</body>
</html>