research-article

K-Java: A Complete Semantics of Java

Authors:

Denis Bogdanas,

Grigore RoşuAuthors Info & Claims

POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Pages 445 - 456

https://doi.org/10.1145/2676726.2676982

Published: 14 January 2015 Publication History

Abstract

This paper presents K-Java, a complete executable formal semantics of Java 1.4. K-Java was extensively tested with a test suite developed alongside the project, following the Test Driven Development methodology. In order to maintain clarity while handling the great size of Java, the semantics was split into two separate definitions -- a static semantics and a dynamic semantics. The output of the static semantics is a preprocessed Java program, which is passed as input to the dynamic semantics for execution. The preprocessed program is a valid Java program, which uses a subset of the features of Java. The semantics is applied to model-check multi-threaded programs. Both the test suite and the static semantics are generic and ready to be used in other Java-related projects.

Supplementary Material

ZIP File (popl097.zip)

K-Java: Runtime Semantics for Method Invocation and Object Instantiation

Download
229.86 KB

MPG File (p445-sidebyside.mpg)

Download
1822.64 MB

References

[1]

K-Java repository. URL https://github.com/kframework/java-semantics/tree/popl-artifact-evaluation.

[2]

Gaining access to the JCK. URL http://openjdk.java.net/groups/conformance/JckAccess/.

[3]

Using Java 5 features in earlier JDKs. URL http://www.ibm.com/developerworks/java/library/j-jtp02277/index.html.

[4]

Translation of lambda expressions. URL http://cr.openjdk.java.net/~briangoetz/lambda/lambda-translation.html.

[5]

MatchC project. URL http://fsl.cs.illinois.edu/index.php/Special:MatchCOnline.

[6]

Mauve. URL https://sourceware.org/mauve/.

[7]

Openjdk project. URL http://openjdk.java.net/.

[8]

A simple scenario using wait() and notify() in Java. URL http://stackoverflow.com/questions/2536692/a-simple-scenario-using-wait-and-notify-in-java.

[9]

L. Bettini, F. Damiani, I. Schaefer, and F. Strocco. Traitrecordj: A programming language with traits and records. Sci. Comput. Program., 78(5):521--541, May 2013.

Digital Library

[10]

M. Bodin, A. Chargueraud, D. Filaretti, P. Gardner, S. Maffeis, D. Naudziuniene, A. Schmitt, and G. Smith. A trusted mechanised JavaScript specification. In POPL'14, pages 87--100. ACM, 2014.

Digital Library

[11]

D. Bogdănaş. Label-based programming language semantics in K framework with SDF. In SYNASC '12, pages 160--167. IEEE, 2012.

Digital Library

[12]

D. Bogdănaş. K-Java: runtime semantics for method invocation and object instantiation. Technical report, University of Illinois, 2014. URL http://hdl.handle.net/2142/55512.

[13]

E. Börger, N. G. Fruja, V. Gervasi, and R. F. Stärk. A high-level modular definition of the semantics of C#. Theor. Comput. Sci., 336 (2--3):235--284, May 2005.

Digital Library

[14]

G. Bracha, M. Odersky, D. Stoutamire, and P. Wadler. Making the future safe for the past: Adding genericity to the java programming language. In OOPSLA '98, pages 183--200. ACM, 1998.

Digital Library

[15]

M. Bravenboer, R. Vermaas, R. de Groot, and E. Dolstra. Java Front. URL http://strategoxt.org/Stratego/JavaFront.

[16]

M. Clavel, F. Durn, S. Eker, P. Lincoln, N. Martoliet, J. Meseguer, and C. Talcott. Maude manual (version 2.6), 2011. URL http://maude.cs.uiuc.edu/maude2-manual/.

[17]

A. ştefănescu, c. Ciobâcă, R. Mereuţă, B. M. Moore, T. F. Şerbănuţă, and G. Roşu. All-path reachability logic. In RTA-TLCA'14, LNCS. Springer, 2014.

[18]

S. Eker, J. Meseguer, and A. Sridharanarayanan. The Maude LTL model checker and its implementation. In SPIN'03, pages 230--234. Springer-Verlag, 2003.

Digital Library

[19]

C. Ellison. A Formal Semantics of C with Applications. PhD thesis, University of Illinois, July 2012.

[20]

C. Ellison and G. Roşu. An executable formal semantics of C with applications. In POPL '12, pages 533--544. ACM, 2012.

Digital Library

[21]

A. Farzan, F. Chen, J. Meseguer, and G. Roşu. Formal analysis of Java programs in JavaFAN. In CAV'04, volume 3114 of LNCS, pages 501--505, 2004.

[22]

D. Filaretti and S. Maffeis. An executable formal semantics of PHP. In ECOOP'14, pages 567--592, 2014.

Digital Library

[23]

M. Flatt, S. Krishnamurthi, and M. Felleisen. A programmer's reduction semantics for classes and mixins. In Formal Syntax and Semantics of Java, pages 241--269. Springer-Verlag, 1999.

Digital Library

[24]

FSF. C language testsuites: "C-torture" version 4.4.2, 2010. URL http://gcc.gnu.org/onlinedocs/gccint/C-Tests.html.

[25]

J. Gosling, B. Joy, G. Steele, and G. Bracha. Java Language Specification, Second Edition. Addison-Wesley, 2nd edition, 2000.

Digital Library

[26]

D. Guth. A formal semantics of Python 3.3. Master's thesis, University of Illinois at Urbana-Champaign, July 2013.

[27]

C. Haack, E. Poll, J. Schfer, and A. Schubert. Immutable objects for a java-like language. In ESOP'07, volume 4421 of LNCS, pages 347--362. Springer Berlin Heidelberg, 2007.

Digital Library

[28]

J. Heering, P. R. H. Hendriks, P. Klint, and J. Rekers. The syntax definition formalism SDF "reference manual" .SIGPLAN Not., 24 (11):43--75, Nov. 1989.

Digital Library

[29]

K. Kreft and A. Langer. Understanding the closures debate, 2008. URL http://www.javaworld.com/article/2077869/scripting-jvm-languages/understanding-the-closures-debate.html.

[30]

J. G. Politz, A. Martinez, M. Milano, S. Warren, D. Patterson, J. Li, A. Chitipothu, and S. Krishnamurthi. Python: The full monty. In OOPSLA '13, pages 217--232. ACM, 2013.

Digital Library

[31]

G. Roşu and A. Ştefănescu. Checking reachability using matching logic. In OOPSLA'12, pages 555--574. ACM, 2012.

Digital Library

[32]

G. Roşu, A. Ştefănescu, c. Ciobâcă, and B. M. Moore. One-path reachability logic. In LICS'13, pages 358--367. IEEE, June 2013.

Digital Library

[33]

G. Roşu and T. F. Şerbănuţă. An overview of the K semantic frame-work. JLAP, 79(6):397--434, 2010.

[34]

P. Sestoft. Java Precisely. MIT Press, 2002.

Digital Library

[35]

R. F. Stärk, E. Börger, and J. Schmid. Java and the Java Virtual Machine: Definition, Verification, Validation. Springer-Verlag, 2001.

Digital Library

Cited By

de Boer FJohnsen EPun VTapia Tarifa S(2024)Proving Correctness of Parallel Implementations of Transition System ModelsACM Transactions on Programming Languages and Systems10.1145/366063046:3(1-50)Online publication date: 20-Apr-2024
https://dl.acm.org/doi/10.1145/3660630
Gauthier LPrevosto VSignoles JFuria CLopes APlat NGnesi S(2024)A Semantics of Structures, Unions, and Underspecified Terms for Formal SpecificationProceedings of the 2024 IEEE/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE)10.1145/3644033.3644380(100-110)Online publication date: 14-Apr-2024
https://dl.acm.org/doi/10.1145/3644033.3644380
Kan SChen ZSanán DLiu Y(2024)Formally understanding Rust’s ownership and borrowing system at the memory levelFormal Methods in System Design10.1007/s10703-024-00460-3Online publication date: 9-Jul-2024
https://doi.org/10.1007/s10703-024-00460-3
Show More Cited By

Index Terms

K-Java: A Complete Semantics of Java
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
      1. Semantics
2. Theory of computation
  1. Semantics and reasoning
    1. Program semantics

Recommendations

KJS: a complete formal semantics of JavaScript
PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation

This paper presents KJS, the most complete and throughly tested formal semantics of JavaScript to date. Being executable, KJS has been tested against the ECMAScript 5.1 conformance test suite, and passes all 2,782 core language tests. Among the ...
KJS: a complete formal semantics of JavaScript
PLDI '15

This paper presents KJS, the most complete and throughly tested formal semantics of JavaScript to date. Being executable, KJS has been tested against the ECMAScript 5.1 conformance test suite, and passes all 2,782 core language tests. Among the ...
Evaluating the Java Native Interface JNI: Leveraging Existing Native Code, Libraries and Threads to a Running Java Virtual Machine

This article aims to explore JNI features and to discover fundamental operations of the Java programming language, such as arrays, objects, classes, threads and exception handling, and to illustrate these by using various algorithms and code samples. ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 2015

716 pages

ISBN:9781450333009

DOI:10.1145/2676726

General Chair:
Sriram Rajamani
Microsoft Research, India
,
Program Chair:
David Walker
Princeton University, USA

ACM SIGPLAN Notices Volume 50, Issue 1
POPL '15
January 2015
682 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2775051
Editor:
Andy Gill
University of Kansas, Lawrence, KS
Issue’s Table of Contents

Copyright © 2015 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 January 2015

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

POPL '15

Sponsor:

SIGPLAN

POPL '15: The 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 15 - 17, 2015

Mumbai, India

Acceptance Rates

POPL '15 Paper Acceptance Rate 52 of 227 submissions, 23%;

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

99
Total Citations
View Citations
835
Total Downloads

Downloads (Last 12 months)61
Downloads (Last 6 weeks)4

Reflects downloads up to 24 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

de Boer FJohnsen EPun VTapia Tarifa S(2024)Proving Correctness of Parallel Implementations of Transition System ModelsACM Transactions on Programming Languages and Systems10.1145/366063046:3(1-50)Online publication date: 20-Apr-2024
https://dl.acm.org/doi/10.1145/3660630
Gauthier LPrevosto VSignoles JFuria CLopes APlat NGnesi S(2024)A Semantics of Structures, Unions, and Underspecified Terms for Formal SpecificationProceedings of the 2024 IEEE/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE)10.1145/3644033.3644380(100-110)Online publication date: 14-Apr-2024
https://dl.acm.org/doi/10.1145/3644033.3644380
Kan SChen ZSanán DLiu Y(2024)Formally understanding Rust’s ownership and borrowing system at the memory levelFormal Methods in System Design10.1007/s10703-024-00460-3Online publication date: 9-Jul-2024
https://doi.org/10.1007/s10703-024-00460-3
Lee JBae K(2024)Formal Semantics and Analysis of Multitask PLC ST Programs with PreemptionFormal Methods10.1007/978-3-031-71162-6_22(425-442)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-71162-6_22
Keidel SHelm DRoth TMezini M(2024)A Modular Soundness Theory for the Blackboard Analysis ArchitectureProgramming Languages and Systems10.1007/978-3-031-57267-8_14(361-390)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57267-8_14
Yu GChae SBae KMoon S(2024)Formal Specification of Trusted Execution Environment APIsFundamental Approaches to Software Engineering10.1007/978-3-031-57259-3_5(101-121)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57259-3_5
Jensen TRébiscoul VSchmitt A(2023)Deriving Abstract Interpreters from Skeletal SemanticsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.387.8387(97-113)Online publication date: 14-Sep-2023
https://doi.org/10.4204/EPTCS.387.8
Park JYoun DLee KRyu S(2023)Feature-Sensitive Coverage for Conformance Testing of Programming Language ImplementationsProceedings of the ACM on Programming Languages10.1145/35912407:PLDI(493-515)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591240
Watt CTrela MLammich PMärkl F(2023)WasmRef-Isabelle: A Verified Monadic Interpreter and Industrial Fuzzing Oracle for WebAssemblyProceedings of the ACM on Programming Languages10.1145/35912247:PLDI(100-123)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591224
Wang KWang JPoskitt CChen XSun JCheng P(2023)K-ST: A Formal Executable Semantics of the Structured Text Language for PLCsIEEE Transactions on Software Engineering10.1109/TSE.2023.331529249:10(4796-4813)Online publication date: 1-Oct-2023
https://doi.org/10.1109/TSE.2023.3315292
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents