Open Access. Powered by Scholars. Published by Universities.®
Articles 1 - 8 of 8
Full-Text Articles in Entire DC Network
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 …
A Catalog Of While Loop Specification Patterns, Aditi Barua, Yoonsik Cheon
A Catalog Of While Loop Specification Patterns, Aditi Barua, Yoonsik Cheon
Departmental Technical Reports (CS)
This document provides a catalog of while loop patterns along with their skeletal specifications. The specifications are written in a functional form known as intended functions. The catalog can be used to derive specifications of while loops by first matching the loops to the cataloged patterns and then instantiating the skeletal specifications of the matched patterns. Once their specifications are formulated and written, the correctness of while loops can be proved rigorously or formally using the functional program verification technique in which a program is viewed as a mathematical function from one program state to another.
Finding Specifications Of While Statements Using Patterns, Aditi Barua, Yoonsik Cheon
Finding Specifications Of While Statements Using Patterns, Aditi Barua, Yoonsik Cheon
Departmental Technical Reports (CS)
A formal correctness proof of code containing loops such as while statements typically uses the technique of proof-by-induction, and often the most difficult part of carrying out an inductive proof is formulating a correct induction hypothesis, a specification for a loop statement. An incorrect induction hypothesis will surely lead to a proof failure. In this paper we propose a systematic way for identifying specifications of while statements. The key idea of our approach is to categorize and document common patterns of while statements along with their specifications. This is based on our observation that similarly-structured while statements frequently have similarly-structured …
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 …
The Cleanjava Language For Functional Program Verification, Yoonsik Cheon, Cesar Yeep, Melisa Vela
The Cleanjava Language For Functional Program Verification, Yoonsik Cheon, Cesar Yeep, Melisa Vela
Departmental Technical Reports (CS)
Functional Verification Of Class Invariants In Cleanjava, Carmen Avila, Yoonsik Cheon
Functional Verification Of Class Invariants In Cleanjava, Carmen Avila, Yoonsik Cheon
Departmental Technical Reports (CS)
Cleanjava: A Formal Notation For Functional Program Verification, Yoonsik Cheon, Cesar Yeep, Melisa Vela
Cleanjava: A Formal Notation For Functional Program Verification, Yoonsik Cheon, Cesar Yeep, Melisa Vela
Departmental Technical Reports (CS)