Open Access. Powered by Scholars. Published by Universities.®

Computer Engineering Commons

Open Access. Powered by Scholars. Published by Universities.®

University of Texas at El Paso

Intended function

Publication Year

Articles 1 - 5 of 5

Full-Text Articles in Computer Engineering

The Cleanjava Language For Functional Program Verification, Yoonsik Cheon, Cesar Yeep, Melisa Vela Aug 2011

Functional Verification Of Class Invariants In Cleanjava, Carmen Avila, Yoonsik Cheon May 2011

Cleanjava: A Formal Notation For Functional Program Verification, Yoonsik Cheon, Cesar Yeep, Melisa Vela Nov 2010

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

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

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 ...