Note on Coinduction and Weak Bisimilarity for While Programs

摘要

An illustration of coinduction in terms of a notion of weak bisimilarity is211u001epresented. First, an operational semantic O for while programs is defined in 211u001eterms of a final automation. It identifies any two programs that are weakly 211u001ebisimilar, and induces in a canonical manner a compositional model D. next O=D is 211u001eproved by coinduction.