Re: [sc] Dependable/"safe" subsets

Re: [sc] Dependable/"safe" subsets

From: Derek M Jones <derek_at_xxxxxx>
Date: Thu, 26 Oct 2006 11:35:05 +0100
Message-ID: <45408F59.8000906@xxxxxx>

>>>> I don't see the point about "current technology". We are talking about
>>>> stuff which is over a century, respectively nearly half a century, old.
>> The theory might be, but the practice is very resource intensive.
> Perhaps, but the MoD funded effort for an FD of SPARK was quite a bit
> of what would be needed.

Perhaps Rod can tell us what properties the FD of SPARK has been proved
to have.

> Also, if your 'model implementation' of C had been derived from a formal 
> definition,
> if could act as a check in the way I am advocating!

The C Model Implementation was originally written in Pascal and
then converted to C.

Given the availability of tools for C it was possible to check
a lot more of its properties than if it had been written in some
formal definition language (we are talking early 1990's here).

However, whatever it had been written it, it would still be too big to
check for internal consistency even today.

Derek M. Jones                              tel: +44 (0) 1252 520 667
Knowledge Software Ltd                      mailto:derek@xxxxxx
Applications Standards Conformance Testing
Received on Thu 26 Oct 2006 - 11:35:40 BST