Title :
Circular coinductive rewriting
Author :
J. Goguen;K. Lin;C. Rosu
Author_Institution :
Dept. of Comput. Sci. & Eng., California Univ., San Diego, La Jolla, CA, USA
fDate :
6/22/1905 12:00:00 AM
Abstract :
Circular coinductive rewriting is a new method for proving behavioral properties, that combines behavioral rewriting with circular coinduction. This method is implemented in our new BOBJ (Behavioral OBJects) behavioral specification and computation system, which is used in examples throughout this paper. These examples demonstrate the surprising power of circular coinductive rewriting. The paper also sketches the underlying hidden algebraic theory and briefly describes BOBJ and some of its algorithms.
Keywords :
"Equations","Algebra","Computer science","Power engineering computing","Logic functions","Mathematics","Induction generators"
Conference_Titel :
Automated Software Engineering, 2000. Proceedings ASE 2000. The Fifteenth IEEE International Conference on
Print_ISBN :
0-7695-0710-7
DOI :
10.1109/ASE.2000.873657