Open Access. Powered by Scholars. Published by Universities.^{®}

Articles **1** - **5** of ** 5**

## Full-Text Articles in Computer Engineering

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)*

A Tutorial On Functional Program Verification, Yoonsik Cheon, Melisa Vela

#### A Tutorial On Functional Program Verification, Yoonsik Cheon, Melisa Vela

*Departmental Technical Reports (CS)*

Functional Specification And Verification Of Object-Oriented Programs, Yoonsik Cheon

#### Functional Specification And Verification Of Object-Oriented Programs, Yoonsik Cheon

*Departmental Technical Reports (CS)*

One weakness of Hoare-style verification techniques based on first-order predicate logic is that reasoning is backward from postconditions to preconditions. A natural, forward reasoning is possible by viewing a program as a mathematical function that maps one program state to another. This functional program verification technique requires a minimal mathematical background as it uses equational reasoning based on sets and functions. Thus, it can be easily taught and used in practice. In this paper, we formalize a functional program specification and verification technique and extend it for object-oriented programs. Our approach allows one to formally specify and verify the behavior ...