Conditional Circular Coinductive Rewriting with Case Analysis

  • Joseph A. Goguen
  • Kai Lin
  • Grigore Roşu
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2755)


We argue for an algorithmic approach to behavioral proofs, review the hidden algebra approach, develop circular coinductive rewriting for conditional goals, extend it with case analysis, and give some examples.


Case Analysis Inference Rule Behavioral Theory Data Context Condition Elimination 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Bernot, G., Bidoit, M., Knapik, T.: Observational specifications and the indistinguishability assumption. Theoretical Computer Science 139, 275–314 (1995)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Berregeb, N., Bouhoula, A., Rusinowitch, M.: Observational proofs with critical contexts. In: Astesiano, E. (ed.) ETAPS 1998 and FASE 1998. LNCS, vol. 1382, pp. 38–53. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  3. 3.
    Bidoit, M., Hennicker, R.: Behavioral theories and the proof of behavioral properties. Theoretical Computer Science 165(1), 3–55 (1996)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Bidoit, M., Hennicker, R.: Observer complete definitions are behaviourally coherent. In: Futatsugi, K., Goguen, J., Meseguer, J. (eds.) OBJ/CafeOBJ/Maude at Formal Methods 1999, Theta, pp. 83–94 (1999)Google Scholar
  5. 5.
    Buss, S., Roşu, G.: Incompleteness of behavioral logics. In: Reichel, H. (ed.) Proceedings of Coalgebraic Methods in Computer Science. Electronic Notes in Theoretical Computer Science, vol. 33, pp. 61–79. Elsevier Science, Amsterdam (2000)Google Scholar
  6. 6.
    Diaconescu, R., Futatsugi, K.: CafeOBJ Report: The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification. AMAST Series in Computing, vol. 6. World Scientific, Singapore (1998)zbMATHGoogle Scholar
  7. 7.
    Diaconescu, R., Futatsugi, K.: Behavioral coherence in object-oriented algebraic specification. Journal of Universal Computer Science 6(1), 74–96 (2000)MathSciNetzbMATHGoogle Scholar
  8. 8.
    Futatsugi, K., Ogata, K.: Rewriting can verify distributed real-time systems – how to verify in CafeOBJ. In: Toyama, Y. (ed.) Proc. Int. Workshop on Rewriting in Proof and Computation, pp. 60–79. Tohoku University (2001)Google Scholar
  9. 9.
    Goguen, J.: Types as theories. In: Reed, G.M., Roscoe, A.W., Wachter, R.F. (eds.) Topology and Category Theory in Computer Science, Oxford, pp. 357–390 (1991)Google Scholar
  10. 10.
    Goguen, J., Lin, K., Roşu, G.: Circular coinductive rewriting. In: Proceedings, Automated Software Engineering, pp. 123–131. IEEE, Los Alamitos (2000)Google Scholar
  11. 11.
    Goguen, J., Malcolm, G.: A hidden agenda. Theoretical Computer Science 245(1), 55–101 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Goguen, J., Roşu, G.: Hiding more of hidden algebra. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol. 1709, pp. 1704–1719. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  13. 13.
    Hennicker, R.: Context induction: a proof principle for behavioral abstractions. Formal Aspects of Computing 3(4), 326–345 (1991)CrossRefzbMATHGoogle Scholar
  14. 14.
    Hennicker, R., Bidoit, M.: Observational logic. In: Haeberer, A.M. (ed.) AMAST 1998. LNCS, vol. 1548, pp. 263–277. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  15. 15.
    Jacobs, B.: Mongruences and cofree coalgebras. In: Alagar, V.S., Nivat, M. (eds.) AMAST 1995. LNCS, vol. 936, pp. 245–260. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  16. 16.
    Jacobs, B., Rutten, J.: A tutorial on (co)algebras and (co)induction. Bulletin of European Association for Theoretical Computer Science 62, 222–259 (1997)zbMATHGoogle Scholar
  17. 17.
    Padawitz, P.: Towards the one-tiered design of data types and transition systems. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 365–380. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  18. 18.
    Roşu, G.: Behavioral coinductive rewriting. In: Futatsugi, K., Goguen, J., Meseguer, J. (eds.) OBJ/CafeOBJ/Maude at Formal Methods 1999, Theta, pp. 179–196 (1999)Google Scholar
  19. 19.
    Roşu, G.: Hidden Logic. PhD thesis, University of California, San Diego (2000)Google Scholar
  20. 20.
    Roşu, G., Goguen, J.: Hidden congruent deduction. In: Caferra, R., Salzer, G. (eds.) FTP 1998. LNCS (LNAI), vol. 1761, pp. 252–267. Springer, Heidelberg (2000)Google Scholar
  21. 21.
    Roşu, G., Goguen, J.: Circular coinduction. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083. Springer, Heidelberg (2001)Google Scholar
  22. 22.
    Rutten, J.: Universal coalgebra: a theory of systems. Theoretical Computer Science 249, 3–80 (2000)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Joseph A. Goguen
    • 1
  • Kai Lin
    • 1
  • Grigore Roşu
    • 2
  1. 1.Department of Computer Science & EngineeringUniversity of California at San DiegoUSA
  2. 2.Department of Computer ScienceUniversity of Illinois at Urbana-ChampaignUSA

Personalised recommendations