Open Access. Powered by Scholars. Published by Universities.®
Physical Sciences and Mathematics Commons™
Open Access. Powered by Scholars. Published by Universities.®
- Discipline
Articles 1 - 3 of 3
Full-Text Articles in Physical Sciences and Mathematics
A Systematic Derivation Of Loop Specifications Using Patterns, Aditi Barua, Yoonsik Cheon
A Systematic Derivation Of Loop Specifications Using Patterns, Aditi Barua, Yoonsik Cheon
Departmental Technical Reports (CS)
Any non-trivial program contains loop control structures such as while, for and do statements. A formal correctness proof of code containing loop control structures is typically performed using an induction-based technique, and oftentimes the most challenging step of an inductive proof is formulating a correct induction hypothesis. An incorrectly-formulated induction hypothesis will surely lead to a failure of the proof. In this paper we propose a systematic approach for formulating and driving specifications of loop control structures for formal analysis and verification of programs. We explain our approach using while loops and a functional program verification technique in which a …
Enhancing The Expressiveness Of The Cleanjava Language, Melisa Vela, Yoonsik Cheon
Enhancing The Expressiveness Of The Cleanjava Language, Melisa Vela, Yoonsik Cheon
Departmental Technical Reports (CS)
The CleanJava language is a formal annotation language for Java to support Cleanroom-style functional program verification that views a program as a mathematical function from one program state to another. The CleanJava notation is based on the Java expression syntax with a few extensions, and thus its vocabulary is somewhat limited to that of Java. This often makes it difficult to specify the rich semantics of a Java program in a succinct and natural way that is easy to manipulate for formal correctness reasoning. In this paper we propose to make the CleanJava language more expressive by supporting user-defined mathematical …
Constructing Verifiably Correct Java Programs Using Ocl And Cleanjava, Yoonsik Cheon, Carmen Avila
Constructing Verifiably Correct Java Programs Using Ocl And Cleanjava, Yoonsik Cheon, Carmen Avila
Departmental Technical Reports (CS)
A recent trend in software development is building a precise model that can be used as a basis for the software development. Such a model may enable an automatic generation of working code, and more importantly it provides a foundation for correctness reasoning of code. In this paper we propose a practical approach for constructing a verifiably correct program from such a model. The key idea of our approach is (a) to systematically translate formally-specified design constraints such as class invariants and operation pre and postconditions to code-level annotations and (b) to use the annotations for the correctness proof of …