MJ (Middleweight Java) - MJ: an imperative core calculus for Java and Java with effects. In order to study rigorously object-oriented languages such as Java or C#, a common practice is to define lightweight fragments, or calculi, which are sufficiently small to facilitate formal proofs of key properties. However many of the current proposals for calculi lack important language features. In this paper we propose Middleweight Java, MJ, as a contender for a minimal imperative core calculus for Java. Whilst compact, MJ models features such as object identity, field assignment, constructor methods and block structure. We define the syntax, type system and operational semantics of MJ, and give a proof of type safety. In order to demonstrate the usefulness of MJ to reason about operational features, we consider a recent proposal of Greenhouse and Boyland to extend Java with an effects system. This effects system is intended to delimit the scope of computational effects within a Java program. We define an extension of MJ with a similar effects system and instrument the operational semantics. We then prove the correctness of the effects system; a question left open by Greenhouse and Boyland. We also consider the question of effect inference for our extended calculus, detail an algorithm for inferring effects information and give a proof of correctness.
Keywords for this software
References in zbMATH (referenced in 12 articles )
Showing results 1 to 12 of 12.
- Haller, Philipp; Miller, Heather: A reduction semantics for direct-style asynchronous observables (2019)
- Sisto, Riccardo; Bettassa Copet, Piergiuseppe; Avalle, Matteo; Pironti, Alfredo: Formally sound implementations of security protocols with JavaSPI (2018)
- Iranmanesh, Zeinab; Fallah, Mehran S.: Specification and static enforcement of scheduler-independent noninterference in a middleweight Java (2016)
- Avalle, Matteo; Pironti, Alfredo; Sisto, Riccardo: Formal verification of security protocol implementations: a survey (2014) ioport
- Bettini, Lorenzo; Damiani, Ferruccio; Schaefer, Ina; Strocco, Fabio: \textscTraitRecordJ: a programming language with traits and records (2013) ioport
- Reza, Juan Rolando: Java supervenience (2012) ioport
- Bergel, Alexandre: Reconciling method overloading and dynamically typed scripting languages (2011)
- Smans, Jan; Jacobs, Bart; Piessens, Frank; Schulte, Wolfram: Automatic verification of Java programs with dynamic frames (2010)
- Dezani-Ciancaglini, Mariangiola; Drossopoulou, Sophia; Mostrous, Dimitris; Yoshida, Nobuko: Objects and session types (2009)
- Ahern, Alexander; Yoshida, Nobuko: Formalising Java RMI with explicit code mobility (2007)
- Coppo, Mario; Dezani-Ciancaglini, Mariangiola; Yoshida, Nobuko: Asynchronous session types and progress for object oriented languages (2007)
- Yoshida, Nobuko: Type-based security for mobile computing integrity, secrecy and liveness (2006)