Using program transformation, annotation, and reflection to certify a java type resolution function

Victor L. Winter, Carl Reinke, Jonathan Guerrero

Research output: Contribution to conferencePaper

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 form 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)
Pages137-145
Number of pages9
DOIs
StatePublished - Jan 1 2014
Event2014 IEEE 15th International Symposium on High-Assurance Systems Engineering, HASE 2014 - Miami, FL, United States
Duration: Jan 9 2014Jan 11 2014

Conference

Conference2014 IEEE 15th International Symposium on High-Assurance Systems Engineering, HASE 2014
CountryUnited States
CityMiami, FL
Period1/9/141/11/14

Fingerprint

Static analysis
Semantics

Keywords

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

ASJC Scopus subject areas

  • Software

Cite this

Winter, V. L., Reinke, C., & Guerrero, J. (2014). Using program transformation, annotation, and reflection to certify a java type resolution function. 137-145. Paper presented at 2014 IEEE 15th International Symposium on High-Assurance Systems Engineering, HASE 2014, Miami, FL, United States. https://doi.org/10.1109/HASE.2014.27

Using program transformation, annotation, and reflection to certify a java type resolution function. / Winter, Victor L.; Reinke, Carl; Guerrero, Jonathan.

2014. 137-145 Paper presented at 2014 IEEE 15th International Symposium on High-Assurance Systems Engineering, HASE 2014, Miami, FL, United States.

Research output: Contribution to conferencePaper

Winter, VL, Reinke, C & Guerrero, J 2014, 'Using program transformation, annotation, and reflection to certify a java type resolution function', Paper presented at 2014 IEEE 15th International Symposium on High-Assurance Systems Engineering, HASE 2014, Miami, FL, United States, 1/9/14 - 1/11/14 pp. 137-145. https://doi.org/10.1109/HASE.2014.27
Winter VL, Reinke C, Guerrero J. Using program transformation, annotation, and reflection to certify a java type resolution function. 2014. Paper presented at 2014 IEEE 15th International Symposium on High-Assurance Systems Engineering, HASE 2014, Miami, FL, United States. https://doi.org/10.1109/HASE.2014.27
Winter, Victor L. ; Reinke, Carl ; Guerrero, Jonathan. / Using program transformation, annotation, and reflection to certify a java type resolution function. Paper presented at 2014 IEEE 15th International Symposium on High-Assurance Systems Engineering, HASE 2014, Miami, FL, United States.9 p.
@conference{7b6e3dcee96140a1b13a5e2823b529cc,
title = "Using program transformation, annotation, and reflection to certify a java type resolution function",
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 form 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 = "Winter, {Victor L.} and Carl Reinke and Jonathan Guerrero",
year = "2014",
month = "1",
day = "1",
doi = "10.1109/HASE.2014.27",
language = "English (US)",
pages = "137--145",
note = "2014 IEEE 15th International Symposium on High-Assurance Systems Engineering, HASE 2014 ; Conference date: 09-01-2014 Through 11-01-2014",

}

TY - CONF

T1 - Using program transformation, annotation, and reflection to certify a java type resolution function

AU - Winter, Victor L.

AU - Reinke, Carl

AU - Guerrero, Jonathan

PY - 2014/1/1

Y1 - 2014/1/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 form 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 form 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=84898659531&partnerID=8YFLogxK

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

U2 - 10.1109/HASE.2014.27

DO - 10.1109/HASE.2014.27

M3 - Paper

AN - SCOPUS:84898659531

SP - 137

EP - 145

ER -