Web Page for Lectures on
Introduction to Specification and Verification in CafeOBJ
at
Vienna University of Technology, Vienna, July+August 2012
by FUTATSUGI,Kokichi
(JAIST)
Abstract
After introductory explanations of CafeOBJ
algebraic specification language system, the lectures gradually
develop executable algebraic semantics (or specifications) of a simple
imperative programming language called Minila. The
semantics/specifications are composed of that of an interpreter of
Minila , an abstract machine, and a compiler from Minila to machine
codes of the abstract machine. A verification of a part of the
compiler is also given.
The lectures are prepared for the beginners
for CafeOBJ and only fundamental knowledge of algorithms and data
structures, automata and languages, elementary mathematical logic are
assumed. The lectures are also designed to be combined with
interactive exercises with CafeOBJ language system, and all attendees
are expected to bring in their personal computers to class room.
After attending the lectures, the attendees are expected to be able to
construct elementary formal specifications in CafeOBJ and
write proof scores for verifying properties about the
specifications.
Schedule
18 July 2012 (Wednesday)
10:00 - 11:30 Lecture 1
14:00 - 15:30 Exercise 1
25 July 2012 (Wednesday)
10:00 - 11:30 Lecture 2
14:00 - 15:30 Exercise 2
1 August 2012 (Wednesday)
10:00 - 11:30 Lecture/Exercise 3
14:00 - 15:30 Lecture/Exercise 4
8 August 2012 (Wednesday)
10:00 - 11:30 Lecture/Exercise 5
14:00 - 15:30 Lecture/Exercise 6
Lectures/Exercise Materials
(Please notice that contents of the following meterials
may be revised.)
Preparation:
-
Every attendee is supposed to install CafeOBJ system to her/his personal computer
from the following web page before attending the lectures
(be sure to install the version 1.4.8, for the version 1.4.9 can not
read some examples)
:
-
Every attendee is recommended to look into the following materials
before attending the lectures.
Lecture/Exercise 1: Basics of CafeOBJ and Peano Style Natural Numbers
Lecture/Exercise 2: Parametrized Modules and Generic List Structure
Lecture/Exercise 3: Definition of Minila Programming Language
Lecture/Exercise 4: Interpreter and Virtual Machine of Minila
Lecture/Exercise 5: Compiler of Minila
Lecture/Exercise 6: Verification with Proof Score of Arithmetic Expression Compiler
Full CafeOBJ codes of the processors of Minila:
(used in lectures 3, 4, and 5)
Related Web Pages
http://www.jaist.ac.jp/~kokichi/class/TUW1207+08/ (this web page)
last update: 2012.08.07