Open Access. Powered by Scholars. Published by Universities.®
Programming Languages and Compilers
University of Texas at El Paso
- Keyword
-
- Functional program verification (4)
- Intended function (3)
- Android (2)
- Application framework (2)
- CleanJava (2)
-
- Java (2)
- Object Constraint Language (2)
- Program specification (2)
- Specification pattern (2)
- While statement (2)
- Annotation (1)
- Annotation processor (1)
- Assertions (1)
- Class invariant (1)
- Cleanjava (1)
- Control flow (1)
- Correctness proof (1)
- Domain specific language (1)
- Event-based programming (1)
- Explicit invocation (1)
- Formal annotation language (1)
- Formal proof (1)
- Formal specification (1)
- Formal specifications (1)
- Functional programming (1)
- Implicit invocation (1)
- Intended functions (1)
- JML (1)
- JastAddJ (1)
- Java; JUnit (1)
Articles 1 - 10 of 10
Full-Text Articles in Entire DC Network
Sudoku App: Model-Driven Development Of Android Apps Using Ocl?, Yoonsik Cheon, Aditi Barua
Sudoku App: Model-Driven Development Of Android Apps Using Ocl?, Yoonsik Cheon, Aditi Barua
Departmental Technical Reports (CS)
Model driven development (MDD) shifts the focus of software development from writing code to building models by developing an application as a series of transformations on models including eventual code generation. Can the key ideas of MDD be applied to the development of Android apps, one of the most popular mobile platforms of today? To answer this question, we perform a small case study of developing an Android app for playing Sudoku puzzles. We use the Object Constraint Language (OCL) as the notation for creating precise models and translate OCL constraints to Android Java code. Our findings are mixed in …
Writing Jml Specifications Using Java 8 Streams, Yoonsik Cheon, Zejing Cao, Khandoker Rahad
Writing Jml Specifications Using Java 8 Streams, Yoonsik Cheon, Zejing Cao, Khandoker Rahad
Departmental Technical Reports (CS)
JML is a formal behavioral interface specification language for Java to document Java program modules such as classes and interfaces. When composing JML specifications, one frequently writes assertions involving a collection of values. In this paper we propose to use Java 8 streams for writing more concise and cleaner assertions on a collection. The use of streams in JML can be minimal and non-invasive in the conventional style of writing assertions. It can also be holistic to write all assertions in the abstract state defined by streams. We perform a small case study to illustrate our approach and show its …
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 …
Toward Unification Of Explicit And Implicit Invocation-Style Programming, Yoonsik Cheon
Toward Unification Of Explicit And Implicit Invocation-Style Programming, Yoonsik Cheon
Departmental Technical Reports (CS)
Subprograms like procedures and methods can be invoked explicitly or implicitly; in implicit invocation, an event implicitly causes the invocation of subprograms that are registered an interest in the event. Mixing these two styles is common in programming and often unavoidable in developing such software as GUI applications and event-based control systems. However, it isn't also uncommon for the mixed use to complicate programming logic and thus produce unclean code, code that is hard to read and understand. We show, through a small but realistic example, that the problem is not much on mixing two different styles itself but more …
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.
Writing Self-Testing Java Classes With Selftest, Yoonsik Cheon
Writing Self-Testing Java Classes With Selftest, Yoonsik Cheon
Departmental Technical Reports (CS)
This document provides a tutorial introduction to Java annotations called SelfTest. The SelfTest annotations allow one to annotate Java classes with test data, and the SelfTest annotation processor generates executable JUnit test classes from annotated Java classes by translating test cases to executable JUnit tests. The SelfTest annotations not only automate unit testing of Java classes significantly but also provides a step toward writing self-testing Java classes by embedding test data in source code for both compile and runtime processing.
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 …
Cjc: An Extensible Checker For The Cleanjava Annotation Language, Cesar Yeep
Cjc: An Extensible Checker For The Cleanjava Annotation Language, Cesar Yeep
Departmental Technical Reports (CS)
CleanJava is a formal annotation language for the Java programming language to support a Cleanroom-style functional program verification technique that views programs as mathematical functions. It needs a suite of support tools including a checker that can parse annotations and check them for syntactic and static semantic correctness. The two key requirements of the checker are flexibility and extensibility. Since the language is still under development and refinement, it should be flexible to facilitate language experimentation and accommodate language changes. It should be also extensible to provide base code for developing more advanced support tools like an automated theorem prover. …
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 …
Extending Java For Android Programming, Yoonsik Cheon
Extending Java For Android Programming, Yoonsik Cheon
Departmental Technical Reports (CS)
Android is one of the most popular platforms for developing mobile applications. However, its framework relies on programming conventions and styles to implement framework-specific concepts like activities and intents, causing problems such as reliability, readability, understandability, and maintainability. We propose to extend Java to support Android framework concepts explicitly as built-in language features. Our extension called Android Java will allow Android programmers to express these concepts in a more reliable, natural, and succinct way.