ESSLLI 2016 Course: Algebraic Specification and Verification with CafeOBJ
During this year’s ESSLLI (European Summer School in Logic, Language and Information) I was teaching a course on Algebraic Specification and Verification with CafeOBJ. Now that the course is over I can relax a bit and enjoy the beauty of the surrounding North Tyrol.
For those who couldn’t attend the ESSLLI or the course, here are the course materials:
- Day 1 – Introduction, with two short programming challenges: esslli-cafeobj-day1.pdf
- Day 2 – Advanced topics: esslli-cafeobj-day2.pdf
- Day 3 – Advanced topics II and CloudSync: esslli-cafeobj-day3.pdf
- Day 4 – Exploiting AC and Hidden Algebras: esslli-cafeobj-day4.pdf
- Day 5 – Proving with CafeOBJ – CITP: esslli-cafeobj-day5.pdf
- Code for all the lectures and exercises: cafe.zip
Thanks to the participants for the interesting questions and participation.
What follows is the original description of the course.
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.
