Computer Engineering | Open Access Articles | Digital Commons Network™

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.

Go to article

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

Departmental Technical Reports (CS)

Unlike Hoare-style program verification, functional program verification supports forward reasoning by viewing a program as a mathematical function from one program state to another and proving its correctness by essentially comparing two mathematical functions, the function computed by the program and its specification. Since it requires a minimal mathematical background and reflects the way that programmers reason about the correctness of a program informally, it can be taught and practiced effectively. However, there is no formal notation supporting the functional program verification. In this article, we describe a formal notation for writing functional program specifications for Java programs. The notation, …

Go to article

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

Departmental Technical Reports (CS)

In a Cleanroom-style functional program verification, a program is viewed as a mathematical function from one program state to another, and a verification is done by comparing two functions, the implemented and the expected behaviors of a program. The technique requires a minimal mathematical background and supports forward reasoning, but it doesn't support assertions such as class invariants. However, assertions such as class invariants are not only a practical programming tool but also play a key role in the correctness proof of a program by specifying conditions and constraints that an object has to satisfy and thus defining valid states …

Go to article

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

Departmental Technical Reports (CS)

Unlike a Hoare-style program verification, a functional program verification supports forward reasoning by viewing a program as a mathematical function from one program state to another and proving its correctness by essentially comparing two mathematical functions, the function computed by the program and its specification. Since it requires a minimal mathematical background and reflects the way programmers reason about the correctness of a program informally, it can be taught and practiced effectively. However, there is no formal notation supporting the functional program verification. In this paper, we propose a formal notation for writing functional program specifications for Java programs. The …

Go to article

Computer Engineering Commons^™

Full-Text Articles in Computer Engineering

A Catalog Of While Loop Specification Patterns, Aditi Barua, Yoonsik Cheon

Departmental Technical Reports (CS)

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

Departmental Technical Reports (CS)

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

Departmental Technical Reports (CS)