Re: language for (abstract) semantic specification

vali.irimia@ntlworld.com (Vali) writes:
|>
|> I've been searching the web for a kind of semantic specification
|> language (for C code) that is really used in practice somewhere. I've
|> found that PC-Lint has something for function semantics (-sem option)
|> but I'm looking for something more complex/flexible and maybe already
|> in use in some real applications.


I have looked at this a few times, and the situation is dire.


The program-proving diehards tend to go in for arcane notations, often
to cover up the fact that there isn't a hell of a lot of substance
behind the woffle. Now, there IS some good work but, to make sense of
it, you have to climb an immense cliff. Being mostly modern-style
computer scientists, few of the practitioners regard it as being even
respectable to make their work relevant to the real world (e.g. usable
by real programmers), though they often criticise practical
programmers for not using the methods.


I wish that I were joking :-(


One of the few notations that has been used for real work is Z, which
was used to design the new version of IBM CICS and other things.
There are probably others. Most have the serious defects that they
use non-ASCII notations, and the specifications can be handled only by
special programs. This is claimed to be necessary, but I have seen no
evidence for it, and the fact that even standard mathematical concepts
have been obscured by new terminology and notation leaves me very
suspicious.


If you find anything useful, PLEASE let me know. I have some interest
in such specification languages, for real use - but the problem is
that even my more elementary requirements push the program-proving
notations to their limits and beyond! For example, I want to be able
to specify aliasing constraints, and functional programmers 'solve'
those by defining them out of existence.


Regards,
Nick Maclaren.

Return to the comp.compilers page.
Search the comp.compilers archives again.