Subject: Re: Liveness or fairness
Date: Mon, 22 May 2000 17:30:25 -0700
From: lamport@pa.dec.com
To: mcristia@fceia.unr.edu.ar
CC: abadi@research.bell-labs.com


Dear Professor Cristia,

> Reading your comments about the paper of Dederichs and Weber a question
> arose to me. In that paer you said:
>   
> "While machine-closure/feasibility is necessary for a practical
> programing language, it is not clear that it is necessary or even
> desirable for an abstract specification."
>   
> while in all of your papers about TLA you emphasize that
>   
>      a)TLA is usefull for system/program specification
>      b)one should express liveness as fairness in order to obtain
> "machine-closure" specifications
>   
> So, what should I tell to my students regarded the form of a
> specification? That they should specify as you do with TLA in order to
> obtain "closed-machines"? That they shouldn't worry about writing
> liveness as fairness because isn't so important to describe a
> "closed-machine" at the specification level? What would you tell them?

Any specification that is supposed to describe an implementation
should be machine closed.  For example, specifications of algorithms
should be machine closed.

Abstract (high-level) specifications can sometimes be expressed most
conveniently with a non-machine-closed specifications.  However, when
writing such a specification, one should be aware that it is not
machine closed.  One should never write a non-machine-closed
specification by mistake.  An advantage of TLA is that it allows you
to express liveness with fairness formulas in such a way that you are
assured that you have not accidentally written a non-machine-closed
specification.

Leslie Lamport