cs6110, Project Proposal1:
Verifying a Java Program with JML Specification
using HOL-4

Seungkeol Choe
skchoe@cs.utah.edu

Abstract

In this proposal, we present a plan of a project which is about verification of Java program annotated by Java modeling language(JML) using theorem proving system HOL-4. Specifically we noticed that there's a preconducted research which has used Coq theorem prover with same environment. By using the multi-output property of WHY tool, and WHY-HOL interface that takes output of WHY into HOL-4, we expect to verify the Java program using HOL-4.

Contents

1  Project Summary
2  Project Description
    2.1  JML: Java Modeling Language
    2.2  Supporting Tools
        2.2.1  Krakatoa
        2.2.2  Why
3  Work Plan
    3.1  Concerete Goal Description
    3.2  Milestones and Justifications
4  Extensions/Fallback

1  Project Summary

In class cs6110 'Formal method in system design', we dealt with the theorem proving system HOL-4 which is based on functional programming language sml(Standard Meta Language). By the ability for sml to represent non functional programming language, which is called imperative language, we want to expand the capability of HOL-4 to that kinds of progamming language in specification and verification. One of the way for this is to verify the imperative programming language using HOL-4.
In this project, we noticed there's been pretty much efforts to verify imperative programming languages. We chose Java Modeling Language(JML) for a specification of imperative language to verify. The JML can be used to specify the detailed design of Java classes and interfaces by adding annotations to Java source files. The aim of JML is to provide a specification language that is easy to use for Java programmers and that is supported by a wide range of tools for specification type-checking, runtime debugging, static analysis, and verification.
The main flow for verifying the program can be divided by two phases: One is for processing specification and semantics of imperative programming language which is a java program with annotation observing the JML specification. The tools that we'll going to apply will change the specification and imperative features of the language into ML-like minimal language, with very limited imperative features which will be transformed to a proof obligations including calculus of weakest preconditions for programs written in its own language especially designed for program certification.
The next phase of this project is to import the output of the first phase into HOL-4 using WHY-HOL interface. There is already an attempt that corresponds to this phase. The tool Coq which is an interactive theorem proving tool, has used to process the output of the first phase. The main feature of this project is to conduct verification of specification of the input program and compare the process with that is done already by Coq.

2  Project Description

The programming language for verification of their specification is Java language with specification annotated. Throughout the project, it will be required to use supporting tools to process annotated specification, imperativeness of the original input program to be right form of input of HOL-4 the theorem prover. By the previous research, we presume that we'll need to use 2 major tools and 1 interface for HOL. In this section, we explain the way how to accomplish the goal by going over the object to be verified and each tools that allow this.

2.1  JML: Java Modeling Language

Before addressing JML specifically, we need to go over the imperative programming language which JML is one of the representative of it in our project. The imperative programming, in a word, is a program structure which manages states. Classical data structure of a program such as hash table contains a module updating arrays and pointers. A quick overview of comparision of this property with functional programming is describe concisely in [3].
So the main issue in imperative programming is how to deal with its own characteristics in functional way. This allows us to define programs which may be subjected to analysis much more easily. Using a functional language we can make assertions about programs and prove these assertions to be correct. It is possible to do the same for traditional, imperative programs - just much harder.
As mentioned briefly in project summary, JML is for specifying behavioral interface specification language that can be used for Java modules. The example introduced in [2] is showing the main feature of JML specification. The main core of the annotated part of Java program is its representation for precondition, invariants, and postcondition. JML extends the Java syntax with several keywords, it also extends Java's expression syntax with serveral operators. Insides of 3 core parts of annotation, all boolean expression is showing the specification of the program. The reference manual [4] explains these in detail.

2.2  Supporting Tools

In this section, I briefly review the papers which describe each JML specification supporting tools. These tools allow to transform JML annotated program to the right format of theorem prover HOL-4. That is to say, it takes imperative property and JML specification and functional program which HOL-4 can recognize. The extended capability of Standard ML make this possible and the tools are implemented based on this property.

2.2.1  Krakatoa

Krakatoa is a powerful tool which takes JML annotated java program and generate a WHY file for each method we want to verify. The output file contains an annotated WHY program translated from its JML specification and JAVA code automatically.
The paper[5] is showing how Krakatoa is working in the environment of proving JML annotated Java program by Coq theorem prover. It explains 5 steps in detail which specifically comments how to transform each annotated pre/postconditions and invariants and other JML constructs, how to generate WHY specification files for the program. It deals with declarations of global variables, method of WHY external function, WHY predicate for each pure method. In case of using Coq as theorem prover, it generates Coq files containing definitions of predicates and functions corresponding to pure methods and class invariants.
The Krakatoa implementation has an limitation in supporting JML constructs. Constructs which are taken into account are: class invariants, requires, assignable, ensures and signals clauses for each method as well as loop invariants and decreases clauses for each while-loop or for-loop. Regarding the decreases clauses, that means we prove the termination of the loops. For recursive methods Krakatoa do not handle the measured_by clauses, and prove only partial correctness.[5] The assertions also partially supported.
The goal about this project is to use Krakatoa in using HOL-4 instead of Coq theorem prover. As done in the paper [5], we are able to apply the tools used in the procedure of the paper to process the Java program. Also already built HOL-4 interface allow us to take HOL-4 to be primary theorem prover of the Java program.

2.2.2  Why

Why is a verification tool which takes annotated programs as input and produces verification conditions as output. But it is not a proof tool but it gives out conditions for existing proof tools. The paper [7] is officially mentioning that the proof tools are Coq, PVS, Mizar, and HOL-Light. The HOL-4 is not in the list yet but we believe WHY-HOL will work for this as an interface to HOL-4.
For input language, it can takes ML, C, and output of Krakatoa which takes JML-annotated Java language. This input is translated into WHY internal language which is a small ML-like language with imperative features, such as references and arrays, exceptions and annotations. It looks like ML in the sense that the internal language merges expressions, statements, local variables, and functions into a single syntactic class. This makes symbolic manipulaions be easy and limits the number of cases to consider when computing weakest preconditions or verification conditions.
The return, break, or continue which are abrupt termination in imperative language are dealt as exceptions without special constructs for them. The rules for exceptions are giving the excepted verification conditions. The internal language is a form which is close to a subset of Objective Caml.

3  Work Plan

3.1  Concerete Goal Description

One of goal of this project is to apply theorem prover HOL-4 to imperative programs. With Java program there were previous attempt to use theorem prover Coq. So the most typical example problems to solve is those chosen by Why-Coq prover and apply HOL-4 to the problems. Heres the list of programs written on Krakatoa documents[5][8].
These are proved examples by Karkatoa and Coq theorem prover. In this project I plan to prove them using HOL-4. Still the amount or difficulty of the proofs are not known to us, this will cause the change of project work plan.
One thing needed to look into is the right JML-annotation of each examples. They were found as a input format of WHY tools. Also it is not clear that the examples are under Krakatoa's support. In the paper of Krakatoa using Coq, there're example proofs by Coq. In this project I plan to reproduce JML annotated Java program and use HOL-4 to prove the following:
  1. Dijkstra's Dutch national flag
  2. Levenshtein distance (code by Claude Marché)
  3. Binary search
As an extended example for proof, I will prove the following sorting algorithms.
  1. Maximum sort
  2. Selection sort
  3. Quicksort

3.2  Milestones and Justifications

4  Extensions/Fallback

The schedule of this project requires quite a few variation because it needs to learning 4 specification and tools. Also there's no way to figure out how complicate are the algorithms to be proved.
As an extension and fallback, it might be useful if we can make progress further so that we can design our own Java program with modeling of JML spec. Selecting a realworld problem, adding annontation for formal specification, and proving it using HOL-4 can be fruitful result of this project. On the other hand, if some of algorithm required something which is not possible to be used by tools we had, and we needed to update and build additional module, it will cause a diminishing the scope of algorithm to be proved.

References

[1]
Lawrence C. Paulson, ML for the Working Programmer, 2nd Ed., Cambridge Univ Press, 1996.
[2]
Lilian Burdy, Yoonsik Cheon, David Cok, Michael Ernst, Joe Kiniry, Gary T. Leavens, K. Rustan M. Leino, and Erik Poll. An overview of JML tools and applications, To appear in International Journal on Software Tools for Technology Transfer
[3]
Introdcution to Functional Programming, course description about how it is different from imperative programming, http://www.dcs.napier.ac.uk/course-notes/sml/introfp.htm
[4]
Gary T. Leavens, Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David Cok, and Joseph Kiniry. JML Reference Manual (DRAFT), July 2004.
http://www.cs.iastate.edu/ ~ leavens/JML/jmlrefman/jmlrefman_toc.html
[5]
C.Marche, C. Paulin-Mohring and X. Urbain. The Krakatoa Tool for the Certification of JAVA/JAVACARD Programs annotated in JML, Preprint submitted to Elsevier Science.
http://krakatoa.lri.fr/papers/KrakatoaJLAPearly.ps
[6]
J.-C.Filliatre, C. Marche, C. Paulin-Mohring, X. Urbain Modeling of Java programs in Coq, Sep. 23th, 2002.
http://krakatoa.lri.fr/verisafe-abstract.ps
[7]
Jean-Christophe Filliatre Why: a multi-language multi-prover verification condition generator
http://www.lri.fr/ ~ filliatr/ftp/publis/why-tool.ps.gz
[8]
A Gallery of Certified Programs by WHY
http://why.lri.fr/examples/

Footnotes:

1This proposal is composed of 2 parts: one is about brief description of JML and tools, the other is about the plan to conduct project which contains example algorithms for me to plan to prove using HOL-4

File translated from TEX by TTH, version 3.67.
On 24 Feb 2005, 22:05.