[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: New Book: CONCURRENCY
On Tue, 20 Apr 1999, Oyvind Teig wrote:
> Ian Robert East wrote:
> > Somewhere (don't press me for reference) I have seen
> > published surveys that support the claim of little tangible benefit.
> Does OO Sync with How We Think?
> Les Hatton, IEEE Software May/June 1998
> Judith Bishop wrote:
> > This year we used the analyser and animator tool, LTSA from day
> > one, and Wow, what a difference.
> In that context, I'm a student as well, after 24 years in the
> business. Occam, written with a folding editor is semi-graphical!
> The LTSA analyzer is what I've been waiting for for 8 1/2 years!
> (Not any high-end expensive tool.) Or at least what this community
> have been telling me I should wait for.. But why did I have to
> input FSP to it? What's wrong with occam? (WHILE loops? Variables?)
> Someone in this community was working an an occam->SMV compiler,
> I think. How did it go?
It's me. The occam->SMV depends on the flattening in occam->PIC which is
> WHY CAN'T I INPUT IN OCCAM?
> It MUST be better to model check and code in the same language, eh?
That's not uncontroversial. I think so, but others would have you design,
prove and (maybe) check in an unexecutable specification language and
then refine (with automated checking of the refinement) into an
Denis A Nicole WWW: http://www.hpcc.ecs.soton.ac.uk/~dan
High Performance Computing Centre Email: dan@xxxxxxxxxxxxxxx
University of Southampton Phone: +44 1703 592703
UK. Fax: +44 1703 593903