Translations to Support Loop Invariant Generation in JML
Saved in:
| Title: | Translations to Support Loop Invariant Generation in JML |
|---|---|
| Authors: | Koja, Kohei |
| Committee Members: | Leavens, Gary |
| Summary: | Software is used in many critical systems in the real world such as autonomous cars and medical devices. Such software must be reliable to protect the general public. One standard way to make reliable software is to use Hoare-style verification techniques. However, for Hoare-style verification of loop correctness, loop invariants are necessary but are difficult for people to write themselves. Since Java is one of the most popular programming languages in the world, it is useful to have a tool to generate loop invariants for Java programs. OpenJML is a widely used program verification tool for Java. However, it does not provide automatic loop invariant generation. Therefore, the problem that this thesis addresses is to automatically generate loop invariants in OpenJML. The plan is to use a third-party tool to achieve this goal. Since this external tool does not support Java, a package is necessary to translate from Java/JML to the syntax of the loop invariant tool. However, there are a few conditions that the package has to meet. Since the programming language that the third- party tool supports has a limited grammar, we have to work around unsupported syntax. The resulting package is successful because it can integrate a loop invariant generation tool with OpenJML. Therefore, this package may help developers produce more reliable Java programs. |
| URL: | https://stars.library.ucf.edu/etd2020/1235 |
| Database: | OpenDissertations |
| Abstract: | Software is used in many critical systems in the real world such as autonomous cars and medical devices. Such software must be reliable to protect the general public. One standard way to make reliable software is to use Hoare-style verification techniques. However, for Hoare-style verification of loop correctness, loop invariants are necessary but are difficult for people to write themselves. Since Java is one of the most popular programming languages in the world, it is useful to have a tool to generate loop invariants for Java programs. OpenJML is a widely used program verification tool for Java. However, it does not provide automatic loop invariant generation. Therefore, the problem that this thesis addresses is to automatically generate loop invariants in OpenJML. The plan is to use a third-party tool to achieve this goal. Since this external tool does not support Java, a package is necessary to translate from Java/JML to the syntax of the loop invariant tool. However, there are a few conditions that the package has to meet. Since the programming language that the third- party tool supports has a limited grammar, we have to work around unsupported syntax. The resulting package is successful because it can integrate a loop invariant generation tool with OpenJML. Therefore, this package may help developers produce more reliable Java programs. |
|---|
