Abstract:
We propose a minimal extension to the UNITY formalism to express
mobility. Basically, we assign an explicit location to variables. This
approach implies to define a semantic notion of mapping correctness. In
this first proposal, we only use mobile variables and replicated code. This
approach aims at providing a helpful expression of algorithms to refine and
prove them more easily. To illustrate it, we develop a mobility-based mutual
exclusion algorithm and prove its safety.
Michel Charpentier <
>
Last modified: Thu Feb 10 13:36:55 EST 2000