Certifying a java type resolution function using program transformation, annotation, and reflection

Victor Winter, Carl Reinke, Jonathan Guerrero

Research output: Contribution to journalArticle

Abstract

In Java, type resolution is a function that takes a reference to a type occurring in a given context as input and returns the canonical name of that type. This information is fundamental to static analysis—a “must have” function underlying virtually all forms of semantic-based analysis. In the case of Java, this function is also complex and it is quite common to encounter tools where it is implemented incorrectly. This paper presents a novel approach for certifying the correctness of a given type resolution function with respect to an arbitrary Java source code base. The approach uses program transformation to instrument a subject code base in such a way that reflection can then be used to certify the correctness of the type resolution function against the function used by the Java compiler. In this form of certification, the type resolution function of the Java compiler serves as the test oracle.

Original languageEnglish (US)
Pages (from-to)115-135
Number of pages21
JournalSoftware Quality Journal
Volume24
Issue number1
DOIs
StatePublished - Mar 1 2016

Fingerprint

Semantics

Keywords

  • Annotation
  • Java
  • Program transformation
  • Reflection
  • Source code analysis
  • Type resolution

ASJC Scopus subject areas

  • Software
  • Safety, Risk, Reliability and Quality

Cite this

Certifying a java type resolution function using program transformation, annotation, and reflection. / Winter, Victor; Reinke, Carl; Guerrero, Jonathan.

In: Software Quality Journal, Vol. 24, No. 1, 01.03.2016, p. 115-135.

Research output: Contribution to journalArticle

Winter, Victor ; Reinke, Carl ; Guerrero, Jonathan. / Certifying a java type resolution function using program transformation, annotation, and reflection. In: Software Quality Journal. 2016 ; Vol. 24, No. 1. pp. 115-135.
@article{af982058d35546a2acd112813c7ef752,
title = "Certifying a java type resolution function using program transformation, annotation, and reflection",
abstract = "In Java, type resolution is a function that takes a reference to a type occurring in a given context as input and returns the canonical name of that type. This information is fundamental to static analysis—a “must have” function underlying virtually all forms of semantic-based analysis. In the case of Java, this function is also complex and it is quite common to encounter tools where it is implemented incorrectly. This paper presents a novel approach for certifying the correctness of a given type resolution function with respect to an arbitrary Java source code base. The approach uses program transformation to instrument a subject code base in such a way that reflection can then be used to certify the correctness of the type resolution function against the function used by the Java compiler. In this form of certification, the type resolution function of the Java compiler serves as the test oracle.",
keywords = "Annotation, Java, Program transformation, Reflection, Source code analysis, Type resolution",
author = "Victor Winter and Carl Reinke and Jonathan Guerrero",
year = "2016",
month = "3",
day = "1",
doi = "10.1007/s11219-014-9262-2",
language = "English (US)",
volume = "24",
pages = "115--135",
journal = "Software Quality Journal",
issn = "0963-9314",
publisher = "Springer New York",
number = "1",

}

TY - JOUR

T1 - Certifying a java type resolution function using program transformation, annotation, and reflection

AU - Winter, Victor

AU - Reinke, Carl

AU - Guerrero, Jonathan

PY - 2016/3/1

Y1 - 2016/3/1

N2 - In Java, type resolution is a function that takes a reference to a type occurring in a given context as input and returns the canonical name of that type. This information is fundamental to static analysis—a “must have” function underlying virtually all forms of semantic-based analysis. In the case of Java, this function is also complex and it is quite common to encounter tools where it is implemented incorrectly. This paper presents a novel approach for certifying the correctness of a given type resolution function with respect to an arbitrary Java source code base. The approach uses program transformation to instrument a subject code base in such a way that reflection can then be used to certify the correctness of the type resolution function against the function used by the Java compiler. In this form of certification, the type resolution function of the Java compiler serves as the test oracle.

AB - In Java, type resolution is a function that takes a reference to a type occurring in a given context as input and returns the canonical name of that type. This information is fundamental to static analysis—a “must have” function underlying virtually all forms of semantic-based analysis. In the case of Java, this function is also complex and it is quite common to encounter tools where it is implemented incorrectly. This paper presents a novel approach for certifying the correctness of a given type resolution function with respect to an arbitrary Java source code base. The approach uses program transformation to instrument a subject code base in such a way that reflection can then be used to certify the correctness of the type resolution function against the function used by the Java compiler. In this form of certification, the type resolution function of the Java compiler serves as the test oracle.

KW - Annotation

KW - Java

KW - Program transformation

KW - Reflection

KW - Source code analysis

KW - Type resolution

UR - http://www.scopus.com/inward/record.url?scp=84956661831&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84956661831&partnerID=8YFLogxK

U2 - 10.1007/s11219-014-9262-2

DO - 10.1007/s11219-014-9262-2

M3 - Article

AN - SCOPUS:84956661831

VL - 24

SP - 115

EP - 135

JO - Software Quality Journal

JF - Software Quality Journal

SN - 0963-9314

IS - 1

ER -