Luca Aceto, Arnar Birgisson, Anna Ingolfsdottir, MohammadReza Mousavi and Michel Reniers,, Proceedings of the 3rd International Conference on Fundamentals of Software Engineering (FSEN'09), Kish Island, Iran, Lecture Notes in Computer Science, Springer-Verlag, April 2009.
Determinism is a semantic property of (a fragment of) a language that specifies that a program cannot evolve operationally in several different ways. Idempotency is a property of binary composition operators requiring that the composition of two identical specifications or programs will result in a piece of specification or program that is equivalent to the original components. In this paper, we propose two (related) meta-theorems for guaranteeing determinism and idempotency of binary operators. These meta-theorems are formulated in terms of syntactic templates for operational semantics, called rule formats. We show the applicability of our formats by applying them to various operational semantics from the literature.
(Paper in .ps format in .pdf format) (A presentation in .pdf format)
@InProceedings{MousaviFSEN09,
author = "Aceto, Luca and Birgisson, Arnar and Ingolfsdottir, Anna and Mousavi, MohammadReza and Reniers, Michel A.",
title = "Rule Formats for Determinism and Idempotency",
booktitle = "Proceedings of the 3rd International Conference on Fundamentals of Software Engineering ({FSEN}'09)",
series = "Lecture Notes in Computer Science",
address = "Kish Island, Iran",
publisher = "Springer-Verlag, Berlin, Germany",
year = "2009"
}