A Behavioral Specification of Imperative Programming Languages

Masaki NAKAMURA  Masahiro WATANABE  Kokichi FUTATSUGI  

Publication
IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences   Vol.E89-A   No.6   pp.1558-1565
Publication Date: 2006/06/01
Online ISSN: 1745-1337
DOI: 10.1093/ietfec/e89-a.6.1558
Print ISSN: 0916-8508
Type of Manuscript: Special Section PAPER (Special Section on Papers Selected from 2005 International Technical Conference on Circuits/Systems, Computers and Communications (ITC-CSCC2005))
Category: 
Keyword: 
semantics of imperative programs,  behavioral specification,  CafeOBJ,  

Full Text: PDF(196.7KB)>>
Buy this Article




Summary: 
In this paper, we give a denotational semantics of imperative programming languages as a CafeOBJ behavioral specification. Since CafeOBJ is an executable algebraic specification language, not only execution of programs but also semi-automatic verification of programs properties can be done. We first describe an imperative programming language with integer and Boolean types, called IPL. Next we discuss about how to extend IPL, that is, IPL with user-defined types. We give a notion of equivalent programs, which is defined by using the notion of the behavioral equivalence of behavioral specifications. We show a sufficient condition for the equivalence relation of programs, which reduces the task to prove programs to be equivalent.