Journal ArticleOPEN ACCESS

Proof scores in the OTS/CafeOBJ method

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (2003) 2884 170-184
DOI: 10.1007/978-3-540-39958-2_12
114Citations
Citations of this article
5Readers
Mendeley users who have this article in their library.

This article is free to access.

Abstract

A way to write proof scores showing that distributed systems have invariant properties in algebraic specification languages is described, which has been devised through several case studies. The way makes it possible to divide a formula stating an invariant property under discussion into reasonably small ones, each of which is proved by writing proof scores individually. This relieves the load to reduce logical formulas and can decrease the number of subcases into which the case is split in case analysis. © IFIP International Federation for Information Processing 2003.

Author supplied keywords

Cite

CITATION STYLE

APA

Ogata, K., & Futatsugi, K. (2003). Proof scores in the OTS/CafeOBJ method. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2884, 170–184. https://doi.org/10.1007/978-3-540-39958-2_12

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free