• DocumentCode
    3783059
  • 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
  • fYear
    2000
  • fDate
    6/22/1905 12:00:00 AM
  • Firstpage
    123
  • Lastpage
    131
  • 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"
  • Publisher
    ieee
  • Conference_Titel
    Automated Software Engineering, 2000. Proceedings ASE 2000. The Fifteenth IEEE International Conference on
  • ISSN
    1938-4300
  • Print_ISBN
    0-7695-0710-7
  • Type

    conf

  • DOI
    10.1109/ASE.2000.873657
  • Filename
    873657