<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p><br>
</p>
<div class="moz-cite-prefix">On 13/07/2020 14:31, Peter Bernard
Ladkin wrote:<br>
</div>
<blockquote type="cite"
cite="mid:0fa341fb-ba1c-ae02-0f7d-c8485a81145f@causalis.com"><br>
<pre class="moz-quote-pre" wrap="">As I use the term, source code SC is developed CbyC, it means
* there is a Requirements Specification RS which allows one practically to determine whether certain
program behaviours fulfil it or not
* there is a means Chk of determining whether program behaviours will satisfy RS through analysis of
the source code SC of the program and the meaning of SC. (This statement assumes Chk is sound.)
* Chk is incremental, that is, it may be applied soundly to source code as it is being written, and
relatively comprehensive, that is, it can be applied to most programs SC
* SC is indeed developed with incremental use of Chk
</pre>
</blockquote>
<p>Plus what PBL has here omitted - and without which any attempt at
CbyC can rapidly fall apart:</p>
<p><br>
</p>
<p>1. Draconian configuration management of all tools used within
the process and artefacts produced by it. <br>
</p>
<p>2. Validated compilers and, for some languages, draconian
language subsets.</p>
<p>3. A suitably capable Chk element supporting *automated*
program proof. SPARK tools are pretty good but C tools vary. Homo
sapiens is useless.<br>
</p>
<p>4. In-process review procedures that are fit-for-purpose and
strictly followed.<br>
</p>
<p>6. A critical mass of suitably trained and supportive staff.<br>
</p>
<p>7. Supportive, technically-aware management that understands
what CbyC does - and does not - do for them.</p>
<p>8. Users/clients who are prepared to participate in early
life-cycle CbyC activities, e.g. walk-throughs of formal
specifications in Z.</p>
<p>9. The right kind of application to deploy it on.<br>
</p>
<p>... etc. ...</p>
<p><br>
</p>
<p>SPARKies please shoot me down if I'm spouting BS,<br>
</p>
<p>Olwen</p>
<p> <br>
</p>
<p><br>
</p>
<p><br>
</p>
<p><br>
</p>
<p><br>
</p>
<p><br>
</p>
<blockquote type="cite"
cite="mid:0fa341fb-ba1c-ae02-0f7d-c8485a81145f@causalis.com">
<pre class="moz-quote-pre" wrap="">
PBL
Prof. Peter Bernard Ladkin, Bielefeld, Germany
Styelfy Bleibgsnd
Tel+msg +49 (0)521 880 7319 <a class="moz-txt-link-abbreviated" href="http://www.rvs-bi.de">www.rvs-bi.de</a>
</pre>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
The System Safety Mailing List
<a class="moz-txt-link-abbreviated" href="mailto:systemsafety@TechFak.Uni-Bielefeld.DE">systemsafety@TechFak.Uni-Bielefeld.DE</a>
Manage your subscription: <a class="moz-txt-link-freetext" href="https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety">https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety</a></pre>
</blockquote>
</body>
</html>