🚀 go-pugleaf

In article <RNMAX3C@xds13.ferranti.com> peter@ficc.ferranti.com (Peter da Silva) writes:
>In article <50097@nigel.ee.udel.edu> new@ee.udel.edu (Darren New) writes:
>> You can also write programs which could not possibly be implemented in
>> C, even by Dan Bernstein :-).  What more proof do you need?

>This is as insane a claim as any of Dan's. If it's implementable in
>principle it's implementable in C. It might take building another
>language on top of C to make it convenient, but it's implementable.

If you look closely at the complete post, you will notice that I never
claimed that all LOTOS programs are implementable.  For example, LOTOS
very easily allows you to use integers and queues and such, and you
must go out of your way to use integers mod 2^32 or bounded queues or
whatever.  Of course, programs which you write based on a LOTOS
specification will not necessarily implement the full specification,
but it is possible to determine where there will be problems.  In
practice, people write things like "every time you get a connection,
either pick a new port or return an error."  The specification says
that it is possible to always pick a new port or always return an
error.  For different and hopefully obvious reasons, neither is
practical.  But the point of LOTOS is not the automatic implementation
from the specification (use Estelle for that :-) but the concise and
formal description of complex reactive behavior.

>> How do you know Ada's validation suite tests all the semantics of Ada?
>> Do you want to build SDI based on "I think so"?

>Is there an alternative? How do you specify hardware and human actions
>based on a formal language specification?

I understand a CPU called "viper" has in some way been formally validated.
Check out ACM architecture-oriented journals.  Also, law-goverend systems
can formally specify the ways in which people are allowed to interact
with the system, including the ways in which they are allowed to change
the code and the laws themselves. (The laws are enforced, so it really
is formal.) LGS's are described in various Rutgers University tech reports.

In any case, a formal semantics for Ada would allow you to know that
the validation suite tested all parts of the compiler.  These tests
would not necessarily assure you that the compiler is correct, of course.
Kind of like testing the implementation of a protocol by making sure
that all transitions in the state machine fire at least once and wind
up in the correct final state; without that, you don't even know if
all the code is linked in, let alone correct.

              --                 --                --

BTW, in reference to the FORTH-based NOVA chip:
I can't find the reference, but that isn't suprising since most of
my journals are in boxes in another state.  I suspect I read about
it in one of the ACM publications, probably ASPLOS.  Definitely sometime
around 1987 or 1988.                        -- Darren


-- 
--- Darren New --- Grad Student --- CIS --- Univ. of Delaware ---
----- Network Protocols, Graphics, Programming Languages, FDTs -----
+=+=+ My time is very valuable, but unfortunately only to me +=+=+
+=+=+ When you drive screws with a hammer, nails look better +=+=+