[cs63201] QUESTION

[Mikhail Nesterenko]

> 
>    I don't quit understand definition of  "Correct computation" in the last
> lecture, what kind of feature could make a computation "correct"?.
> 

A property is an (arbitrary) set of computations. A problem
(specification), e.g. the Mutual Exclusion Problem that we studied, is
a collection of properties.

Computation is correct (with respect to a single property) if it
belongs to the property. In wich case we say that the computation
satisfies this property.  A computation is correct with respect to the
problem specification if it satisfies its every property.

A program is correct if its every compuation satisfies every property
of the problem specification.


>   And i found some definition on "Safety" and "Liveness" from the textbook
> from page 50 to 52.
> 
> "
> A safety   require-ment imposes that a certain property must hold for each
> execution of the system in every configuration reached in that execution.
> A liveness require-ment imposes that a certain property must hold for each
> execution of the system in  some configuration reached in that execution.
> 
> A safety   property of an algorithm is a property of the form  "Assertion P
>  is true in each configuration of each exeCution of the algorithm
> A liveness property of an algorithm is a property of the form  "Assertion P
>  is true in some configuration of each execution of the algorithm"

do not use book definitions. Instead, get the paper I emailed and read it.

> Is the terms below equal to the terms in the lecture on the right side? And
> Is the meaning of  "Safety" and "Liveness" consistent with that in the
> lecture?
> 
>    execution        = computation
>    configuration    = state
>    Assertion         = guarded cmd
> 

No, these terms are not equivalent. I am considering providing a
translation of terms that Gerard Tel is using and I am
using. Meanwhile, to get the definitions, read the papers the
references to which I emailed

Thanks,
--
Mikhail