Skip to main content
SpringerLink
Log in

Fostering Proof Scores in CafeOBJ 

  • Conference paper
Formal Methods and Software Engineering (ICFEM 2010)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 6447))

Included in the following conference series:

Abstract

Proof scores are instructions to a proof engine such that when executed, if everything evaluates as expected, then a desired theorem is proved. Proof scores hide the detailed calculations done by machines, while revealing the proof plan created by humans. Although proof scores are executalbe by machines, they are also for human beings to read for proving (or verifying) desired properties on a system of interest. The technique of proof scores was brought up by the OBJ/CafeOBJ community, and substantial developments were done after a reliable implementation of CafeOBJ language system was available. This paper give an overview of evolution of proof scores which have been done under the efforts of verifying vearious kinds of formal specifications in CafeOBJ .

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development – Coq’Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004)

    Book  MATH  Google Scholar 

  2. Bidoit, M., Hennicker, R.: Behavioural theories and the proof of behavioural properties. Theoretical Computer Science 165(1), 3–55 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  3. Burstall, R.M., Goguen, J.A.: Putting theories together to make specifications. In: IJCAI, pp. 1045–1058 (1977)

    Google Scholar 

  4. CafeOBJ: Web page (2010), http://www.ldl.jaist.ac.jp/cafeobj/

  5. Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley, Reading (1988)

    MATH  Google Scholar 

  6. Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)

    Google Scholar 

  7. 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)

    MATH  Google Scholar 

  8. Diaconescu, R., Futatsugi, K.: Behavioural coherence in object-oriented algebraic specification. Journal of Universal Computer Science 6(1), 74–96 (2000)

    MathSciNet  MATH  Google Scholar 

  9. Diaconescu, R., Futatsugi, K.: Logical foundations of CafeOBJ. Theor. Comput. Sci. 285(2), 289–318 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  10. Diaconescu, R., Futatsugi, K., Iida, S.: Component-based algebraic specification and verification in CafeOBJ. In: Wing et al. [65], pp. 1644–1663

    Google Scholar 

  11. FSSV 2010: Web page (March 2010), http://www.ldl.jaist.ac.jp/jaist-fssv2010/lectureMaterials/

  12. Futatsugi, K.: An overview of OBJ2. In: Fuchi, K., Nivat, M. (eds.) Programming of Future Generation Computers, pp. 139–160. North-Holland, Amsterdam (1986); Proc. of Franco-Japanese Symp. on Programming of Future Generation Computers, Tokyo (October 1986)

    Google Scholar 

  13. Futatsugi, K.: Trends in formal specification methods based on algebraic specification techniques – from abstract data types to software processes: A personal perspective. In: Proceedings of the International Conference of Information Technology to Commemorating the 30th Anniversary of the Information Processing Society of Japan (InfoJapan 1990), pp. 59–66. Information Processing Society of Japan (1990) (invited talk)

    Google Scholar 

  14. Futatsugi, K.: Formal methods in CafeOBJ. In: Hu, Z., Rodríguez-Artalejo, M. (eds.) FLOPS 2002. LNCS, vol. 2441, pp. 1–20. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  15. Futatsugi, K.: Verifying specifications with proof scores in CafeOBJ. In: Proc. of 21st IEEE/ACM International Conference on Automated Software Engineering (ASE 2006), pp. 3–10. IEEE Computer Society, Los Alamitos (2006)

    Chapter  Google Scholar 

  16. Futatsugi, K., Goguen, J., Meseguer, J. (eds.): OBJ/CafeOBJ/Maude at Formal Methods 1999. The Theta Foundation, Bucharest (1999) ISBN 973-99097-1-X

    Google Scholar 

  17. Futatsugi, K., Goguen, J.A., Jouannaud, J.P., Meseguer, J.: Principles of OBJ2. In: Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages (POPL 1985), New Orleans, Louisiana, pp. 52–66. ACM, New York (1985)

    Google Scholar 

  18. Futatsugi, K., Goguen, J.A., Meseguer, J., Okada, K.: Parameterized programming in OBJ2. In: ICSE, pp. 51–60 (1987)

    Google Scholar 

  19. Futatsugi, K., Goguen, J.A., Ogata, K.: Verifying design with proof scores. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol. 4171, Springer, Heidelberg (2008)

    Google Scholar 

  20. Futatsugi, K., Jouannaud, J.P., Meseguer, J. (eds.): Algebra, Meaning, and Computation. LNCS, vol. 4060. Springer, Heidelberg (2006)

    MATH  Google Scholar 

  21. Futatsugi, K., Nakagawa, A.: An overview of CAFE specification environment - an algebraic approach for creating, verifying, and maintaining formal specifications over networks. In: Proc. of 1st International Conference on Formal Engineering Methods (ICFEM 1997), Hiroshima, Japan, November 12-14, pp. 170–182. IEEE, Los Alamitos (1997)

    Chapter  Google Scholar 

  22. Futatsugi, K., Nakagawa, A., Tamai, T. (eds.): CAFE: An Industrial-Strength Algebraic Formal Method. Elsevier Science B.V., Amsterdam (2000) ISBN 0-444-50556-3

    Google Scholar 

  23. Futatsugi, K., Ogata, K.: Rewriting can verify distributed real-time systems. In: Proc. of International Symposium on Rewriting, Proof, and Computation (PRC 2001), pp. 60–79. Tohoku Univ. (2001)

    Google Scholar 

  24. Futatsugi, K., Okada, K.: Specification writing as construction of hierarchically structured clusters of operators. In: IFIP Congress, pp. 287–292 (1980)

    Google Scholar 

  25. Gâinâ, D., Futatsugi, K., Ogata, K.: Constructor-based institutions. In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol. 5728, pp. 398–412. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  26. Goguen, J.: Hidden algebraic engineering. In: Nehaniv, C., Ito, M. (eds.) Algebraic Engineering. pp. 17–36. World Scientific, Singapore (1998), papers from a conference at the University of Aizu, Japan, 24–26 March 1997; also UCSD Technical Report CS97–569 (December 1997)

    Google Scholar 

  27. Goguen, J.: Theorem Proving and Algebra. [Unpublished Book] (now being planned to be up on the web for the free use)

    Google Scholar 

  28. Goguen, J., Malcolm, G.: A hidden agenda. Theoretical Computer Science 245(1), 55–101 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  29. Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.P.: Introducing OBJ. In: Goguen, J., Malcolm, G. (eds.) Software Engineering with OBJ: Algebraic Specification in Action, pp. 3–167. Kluwer, Dordrecht (2000)

    Chapter  Google Scholar 

  30. Goguen, J.A., Burstall, R.M.: Institutions: Abstract model theory for specification and programming. J. ACM 39(1), 95–146 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  31. Goguen, J.A., Diaconescu, R.: An oxford survey of order sorted algebra. Mathematical Structures in Computer Science 4(3), 363–392 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  32. Goguen, J.A., Lin, K., Mori, A., Rosu, G., Sato, A.: Distributed cooperative formal methods tools. In: Proc. of 1997 International Conference on Automated Software Engineering (ASE 1997), Lake Tahoe, CA, November 02-05, pp. 55–62. IEEE, Los Alamitos (1997)

    Google Scholar 

  33. Goguen, J.A., Malcolm, G.: Algebraic Semantics of Imperative Programs. MIT Press, Cambridge (1996)

    MATH  Google Scholar 

  34. Goguen, J.A., Meseguer, J.: Eqlog: Equality, types, and generic modules for logic programming. In: DeGroot, D., Lindstrom, G. (eds.) Logic Programming: Functions, Relations, and Equations, pp. 295–363. Prentice-Hall, Englewood Cliffs (1986)

    Google Scholar 

  35. Goguen, J.A., Meseguer, J.: Unifying functional, object-oriented and relational programming with logical semantics. In: Shriver, B., Wegner, P. (eds.) Research Directions in Object-Oriented Programming, pp. 417–478. MIT Press, Cambridge (1987)

    Google Scholar 

  36. Goguen, J.A., Meseguer, J.: Order-sorted algebra I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theor. Comput. Sci. 105(2), 217–273 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  37. Guttag, J.V., Horning, J.J., Garland, S.J., Jones, K.D., Modet, A., Wing, J.M.: Larch: Languages and Tools for Formal Specification. Springer, Heidelberg (1993)

    Book  Google Scholar 

  38. Hennicker, R., Bidoit, M.: Observational logic. In: Haeberer, A.M. (ed.) AMAST 1998. LNCS, vol. 1548, pp. 263–277. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  39. Jacobs, B., Rutten, J.: A tutorial on (co)algebras and (co)induction. Bulletin of the European Association for Theoretical Computer Science 62, 222–259 (1997)

    MATH  Google Scholar 

  40. Kong, W., Ogata, K., Futatsugi, K.: Algebraic approaches to formal analysis of the mondex electronic purse system. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 393–412. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  41. Kong, W., Ogata, K., Futatsugi, K.: Specification and verification of workflows with Rbac mechanism and Sod constraints. International Journal of Software Engineering and Knowledge Engineering 17(1), 3–32 (2007)

    Article  Google Scholar 

  42. Maude: Web page (2010), http://maude.cs.uiuc.edu/

  43. Meseguer, J.: A logical theory of concurrent objects. In: OOPSLA/ECOOP, pp. 101–115 (1990)

    Google Scholar 

  44. Meseguer, J.: Conditioned rewriting logic as a united model of concurrency. Theor. Comput. Sci. 96(1), 73–155 (1992)

    Article  MATH  Google Scholar 

  45. Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18–61. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  46. Meseguer, J.: From OBJ to Maude and beyond. In: Futatsugi et al. [20], pp. 252–280

    Google Scholar 

  47. Mori, A., Futatsugi, K.: Verifying behavioural specifications in CafeOBJ environment. In: Wing et al. [65], pp. 1625–1643

    Google Scholar 

  48. Mori, A., Futatsugi, K.: CafeOBJ as a tool for behavioral system verification. In: Okada, M., Pierce, B.C., Scedrov, A., Tokuda, H., Yonezawa, A. (eds.) ISSS 2002. LNCS, vol. 2609, pp. 461–470. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  49. Nakano, M., Ogata, K., Nakamura, M., Futatsugi, K.: Crème: an automatic invariant prover of behavioral specifications. International Journal of Software Engineering and Knowledge Engineering 17(6), 783–804 (2007)

    Article  Google Scholar 

  50. Nipkow, T., Paulson, L.C., Wenzel, M.T. (eds.): Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  51. Ogata, K., Futatsugi, K.: Specification and verification of some classical mutual exclusion algorithms with CafeOBJ. In: Futatsugi et al. [16], pp. 159–177 ISBN 973-99097-1-X

    Google Scholar 

  52. Ogata, K., Futatsugi, K.: Modeling and verification of distributed real-time systems based on CafeOBJ. In: Proceedings of the 16th International Conference on Automated Software Engineering (16th ASE), pp. 185–192. IEEE Computer Society Press, Los Alamitos (2001)

    Chapter  Google Scholar 

  53. Ogata, K., Futatsugi, K.: Specifying and verifying a railroad crossing with CafeOBJ. In: Proceedings of the 6th International Workshop on Formal Methods for Parallel Programming: Theory and Applications (6th FMPPTA); Part of Proceedings of the 15th IPDPS, p. 150. IEEE Computer Society Press, Los Alamitos (2001)

    Google Scholar 

  54. Ogata, K., Futatsugi, K.: Rewriting-based verification of authentication protocols. In: 4th WRLA. ENTCS, vol. 71, pp. 189–203. Elsevier, Amsterdam (2002)

    Google Scholar 

  55. Ogata, K., Futatsugi, K.: Flaw and modification of the iKP electronic payment protocols. Information Processing Letters 86(2), 57–62 (2003)

    Article  MathSciNet  Google Scholar 

  56. Ogata, K., Futatsugi, K.: Formal analysis of the iKP electronic payment protocols. In: Okada, M., Pierce, B.C., Scedrov, A., Tokuda, H., Yonezawa, A. (eds.) ISSS 2002. LNCS, vol. 2609, pp. 441–460. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  57. Ogata, K., Futatsugi, K.: Formal verification of the Horn-Preneel micropayment protocol. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 238–252. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  58. Ogata, K., Futatsugi, K.: Proof scores in the OTS/CafeOBJ method. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp. 170–184. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  59. Ogata, K., Futatsugi, K.: Equational approach to formal verification of SET. In: Proceedings of the 4th International Conference on Quality Software (4th QSIC), pp. 50–59. IEEE Computer Society Press, Los Alamitos (2004)

    Google Scholar 

  60. Ogata, K., Futatsugi, K.: Equational approach to formal analysis of TLS. In: 25th ICDCS, pp. 795–804. IEEE CS Press, Los Alamitos (2005)

    Google Scholar 

  61. Ogata, K., Futatsugi, K.: Some tips on writing proof scores in the OTS/CafeOBJ method. In: Futatsugi et al. [20], pp. 596–615

    Google Scholar 

  62. Ogata, K., Futatsugi, K.: Simulation-based verification for invariant properties in the ots/cafeobj ethod. Electr. Notes Theor. Comput. Sci. 201, 127–154 (2008)

    Article  Google Scholar 

  63. Ogata, K., Futatsugi, K.: A combination of forward & backward reachability analysis method. In: Proc. of 12th International Conference on Formal Engineering Methods (ICFEM 2010), Shanghai, China, November 16-19. Springer, Heidelberg (2010) (to appear)

    Google Scholar 

  64. Sawada, T., Kishida, K., Futatsugi, K.: Past, present, and future of SRA implementation of CafeOBJ: Annex. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 7–17. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  65. Wing, J.M., Woodcock, J., Davies, J. (eds.): FM 1999. LNCS, vol. 1709. Springer, Heidelberg (1999)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Graduate School of Information Science & Research Center for Software Verification, Japan Advanced Institute of Science and Technology (JAIST), 1-1 Asahidai, Nomi, Ishikawa, 923-1292, Japan

    Kokichi Futatsugi

Authors
  1. Kokichi Futatsugi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computing, Computer Science Dept, National University of Singapore, 13 Computing Drive, 117417, Singapore, Singapore

    Jin Song Dong

  2. Software Engineering Institute, East China Normal University, 3663 Zhongshan Road (North), 200062, Shanghai, China

    Huibiao Zhu

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Futatsugi, K. (2010). Fostering Proof Scores in CafeOBJ . In: Dong, J.S., Zhu, H. (eds) Formal Methods and Software Engineering. ICFEM 2010. Lecture Notes in Computer Science, vol 6447. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16901-4_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-16901-4_1

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-16900-7

  • Online ISBN: 978-3-642-16901-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation