ABSTRACT: After introductory explanations of the CafeOBJ algebraic specificationlanguage 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 the 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 semantics/specifications in CafeOBJ and write proof scores for verifying properties about the semantics/specifications.

BIOGRAPHY: Kokichi Futatsugi has been a professor of JAIST since 1993. Before getting a full professorship at JAIST, he worked at ETL (Electrotechnical Laboratory), MITI (Ministry of International Trade and Industry), Japanese Government and was appointed the Chief Researcher of ETL in 1992.  He worked also at SRI International (Stanford Research Institute), California for 1983-1984 as a visiting researcher. His research interests include formal specification languages, formal methods, systems verifications, software requirements/specifications, and his current research activities are centered around formal specification and verification based on CafeOBJ (an executable formal specification language). He got a Fellow Award of Japan Society for Software Science and Technology in 2008, and is now adviser/editor of international journals like IJSI ( <link www.ijsi.org _blank>www.ijsi.org</link> ), JAL ( <link www.elsevier.com/locate/jal _blank>www.elsevier.com/locate/jal</link> ), and JHOSC ( <link www.springerlink.com/content/102420/ _blank>www.springerlink.com/content/102420/</link> ). ( <link http//www.jaist.ac.jp/~kokichi/ _blank>http://www.jaist.ac.jp/~kokichi/</link> )


SCHEDULE:

• July 18 (Wed)
  Lecture/Exercise 1: Basics of CafeOBJ and Peano Style Natural Numbers
  Lecture:   10:00-11:30
  Exercise:  14:00-15:30
  
  
• July 25 (Wed)
  Lecture/Exercise 2: Parametrized Modules and Generic List Structure
  Lecture:   10:00-11:30
  Exercise:  14:00-15:30
  
  
• August 1 (Wed)
  Lecture/Exercise 3: Definition of the Minila Programming Language and its Interpreter and Virtual Machine
  Lecture:   10:00-11:30
  Exercises: 14:00-15:30
  
  
• August 8 (Wed)
  Lecture/Exercise 4: Compiler of Minila and its Verification with Proof Scores
  Lecture:   10:00-11:30
  Exercise:  14:00-15:30

All lectures and tutorials take place in: Library E185.1, Argentinierstr. 8