Thanks to Takahiro Seino there is now an introduction to CafeOBJ targeting beginners. This introduction is available in both English and Japanese. I have added links to the Introduction on the Documentation Page and in the Documentation menu. Thanks to Seino-san for his contribution.
This second in a series of tutorials will introduce you to functional programming the CafeOBJ way, in particular will we discuss lists and various ways to implement, use, and abuse the. We expect a running CafeOBJ interpreter being available. For a first steps tutorial, please consult this post.
This tutorial will guide you through starting the CafeOBJ interpreter, and some simple calculations. We will also give a very short introduction to the logic background of CafeOBJ, and the basic structure of the language.
QLOCK, a variant of Dijkstra’s binary semaphore, is a well known protocol of mutual exclusion, and many implementation and verifications in CafeOBJ are available. I have extended the current proofs of mutual exclusion to cover also fairness, i.e., any agent will eventually enter the queue and eventually go into critical […]
Specification and verification of a simplified cloud synchronization protocol. Arbitrary many PCs can connect to a central cloud, fetch the value from the cloud, compare it with their own value, and update the cloud or their own value depending on which is larger. A detailed explanation can be found in […]
