Information Technology Reference
In-Depth Information
A Graph-Based Implementation for Mechanized
Refinement Calculus of OO Programs
Zhiming Liu
1
, Charles Morisset
2
, and Shuling Wang
1
,
3
1
UNU-IIST, P.O. Box 3058, Macau S.A.R., China
2
Royal Holloway, University of London
Information Security Group
Egham, Surrey TW20 0EX, U.K.
3
State Key Lab. of Computer Science
Institute of Software, Chinese Academy of Sciences
Abstract.
This paper extends the mechanization of the refinement cal-
culus done by von Wright in HOL, representing the state of a program
as a graph instead of a tuple, in order to deal with object-orientation.
The state graph structure is implemented in Isabelle, together with def-
initions and lemmas, to help the manipulation of states. We then show
how proof obligations are automatically generated from the rCOS tool
and can be loaded in Isabelle to be proved. We illustrate our approach by
generating the proof obligations for a simple example, including object
access and method invocation.
Keywords:
Isabelle, Proof obligations, rCOS, Theorem proving.
1
Introduction
Software verification is about demonstrating that an
implementation
(executable
code) of the software meets its
specification
(formal description of the behavior)
and several techniques are available in order to achieve this goal. Testing and
model checking usually aim to verify if a property holds on a subset of instances
of a program, or on a model of the program, respectively, while theorem proving
aims to build the proof of correctness, that is, the semantics of the implementa-
tion logically implies the specification. For all these techniques, there are several
challenges to address:
i
) An increasing number of software is written using the
approach, and
therefore the execution states of a program are complex, due to the complex
relations among objects, aliasing, dynamic binding, and polymorphism. This
makes it hard to understand and reason about the behavior of the program.
ii
) When a tool is provided to help the development of software, it should
offer an environment where the user can specify, analyze, implement and verify
a program. Therefore, the different verification techniques need to be integrated
within the tool.
iii
) In general, it is not possible to automatically verify if an implementation
satisfies a specification, therefore the tool is required to guide the user through
the different steps of the verification process.
oo
Search WWH ::
Custom Search