An input/output semantics for distributed program equivalence reasoning

Miquel Bertran, Francesc Xavier Babot, August Climent

Producció científica: Article en revista indexadaArticle de conferènciaAvaluat per experts

7 Cites (Scopus)


A new notion of input/output equivalence of distributed imperative programs, with synchronous communications, is introduced. It preserves the input/output relation, encompassing both, initial/final state and communication channel values. For its mathematical justification, the semantic framework of Manna and Pnueli, based on finite transition systems and reduced behaviors, is extended with the notion of input/output behavior. A set of laws for the equivalence is overviewed. A deduction rule for the substitution of references to input/output equivalent procedures is defined and justified in the new semantics. The rule is applied to decompose distributed program simplification proofs, introduced in a prior work, which use the laws to establish the equivalence between a sequential and a parallel communicating program. They include communication elimination as one of their steps. An outline of one of such proofs, for a pipelined processor model, is included.

Idioma originalAnglès
Pàgines (de-a)25-46
Nombre de pàgines22
RevistaElectronic Notes in Theoretical Computer Science
Estat de la publicacióPublicada - 20 de jul. 2005
EsdevenimentProceedings of the Fourth Spanish Conference on programming and Computer Languages (PROLE 2004) -
Durada: 10 de gen. 200412 de nov. 2004


Navegar pels temes de recerca de 'An input/output semantics for distributed program equivalence reasoning'. Junts formen un fingerprint únic.

Com citar-ho