Algebraic Specification and Verification – an Introduction to CafeOBJ

Norbert Preining

  • Area: LoCo
  • Level: I
  • Week: 2
  • Time: 09:00 – 10:30
  • Room: C3.06 A5.18

Abstract

Ensuring correctness of complex systems like computer programs or communication protocols is gaining ever increasing importance. For correctness it does not suffice to consider the finished system, but correctness already on the level of specification is necessary, that is, before the actual implementation starts. To this aim, algebraic specification and verification languages have been conceived. They are aiming at a mathematically correct description of the properties and behavior of the systems under discussion, and in addition often allow to prove (verify) correctness within the same system.

This course will give an introduction to algebraic specification, its history, logic roots, and actuality with respect to current developments. Paired with the theoretical background we give an introduction to CafeOBJ, a programming language that allows both specification and verification to be carried out together. The course should enable students to understand the theoretical background of algebraic specification, as well as enable them to read and write basic specifications in CafeOBJ.

Description

CafeOBJ is a specification language based on three-way extensions to many-sorted equational logic: the underlying logic is order-sorted, not just many-sorted; it admits unidirectional transitions, as well as equations; it also accommodates hidden sorts, on top of ordinary, visible sorts. A subset of CafeOBJ is executable, where the operational semantics is given by a conditional order-sorted term rewriting system.

The language system CafeOBJ has been under constant development at the institute of the lecturers since the late 80ies. It is closely related to other algebraic specification languages in the OBJ family, including Maude. The CafeOBJ language and the range of verification methods and tools it supports – including its support for inductive theorem proving, verification of behavioral specifications, deductive invariant proof, and reachability analysis of concurrent systems – has played a key role in both extending and bringing algebraic specification techniques into contact with many software engineering applications.

The following topics will be discussed:

  • algebraic foundations: many-sorted algebras, order-sorted algebras, behavioral specification
  • computational foundations: rewriting
  • programming with CafeOBJ: language elements, modules, simple programs
  • CloudSync: presentation of an example cloud synchronization protocol and its verification

To make the lectures not too `heavy’, we will structure each lecture into two parts: A first part providing an introduction of some theoretical concept, or framework, and a second part dealing with actual programming and implementation. Especially for the second part of each lecture students are encouraged to use their laptops to try out code and experiment.

In addition, if time permits, we are willing to provide out-of-lecture lab-style meeting where we help students to get CafeOBJ installed and running, as well as making the first steps.

Code

Code used during the lessons and solutions to the exercises

  • Day 1 and Day 2: cafe.zip
  • Emacs initialization file: dot.emacs – save as .emacs in your home directory
  • Updated cloudsync file for current CafeOBJ interpreter: cloudsync-20160824.cafe (rename the file to cloudsync-20160824.cafe)
  • Day 4: cafe4.zip

Slides

Additional References