A note on Coinduction and Weak Bisimilarity for While Programs
P.O. Box 94079, 1090 GB Amsterdam, The Netherlands;
email@example.com. URL: www.cwi.nl/~janr
Revised: 26 April 1999
An illustration of coinduction in terms of a notion of weak bisimilarity is presented. First, an operational semantics for while programs is defined in terms of a final automaton. It identifies any two programs that are weakly bisimilar, and induces in a canonical manner a compositional model . Next is proved by coinduction.
Mathematics Subject Classification: 68Q10 / 68Q55
Key words: Coalgebra / automaton / weak bisimulation / coinduction / while program.
© EDP Sciences, 1999