scholarly journals Inter-Deriving Semantic Artifacts for Object-Oriented Programming

2008 ◽  
Vol 15 (5) ◽  
Author(s):  
Olivier Danvy ◽  
Jacob Johannsen
Keyword(s):  
Operational Semantics ◽  
Object Oriented ◽  
Object Oriented Programming ◽  
Small Step ◽  
Abstract Machine ◽  
Abstract Machines ◽  
Explicit Substitutions

We present a new abstract machine for Abadi and Cardelli's untyped calculus of objects. What is special about this semantic artifact (i.e., man-made construct) is that is mechanically corresponds to both the reduction semantics (i.e., small-step operational semantics) and the natural semantics (i.e., big-step operational semantics) specified in Abadi and Cardelli's monograph. This abstract machine therefore embodies the soundness of Abadi and Cardelli's reduction semantics and natural semantics relative to each other. <br /> <br />To move closer to actual implementations, which use environments rather than actual substitutions, we then represent object methods as closures and in the same inter-derivational spirit, we present three new semantic artifacts: a reduction semantics for a version of Abadi and Cardelli's untyped calculus of objects with explicit substitutions, an environment-based abstract machine, and a natural semantics (i.e., an interpreter) with environments. These three new semantic artifacts mechanically correspond to each other, and furthermore, they are coherent with the previous ones since as we show, the two abstract machines are bisimilar. Overall, though, the significance of these artifacts lies in them not having been designed from scratch and then proved correct: instead, they were mechanically inter-derived.

scholarly journals Compilation and equivalence of imperative objects

1999 ◽  
Vol 9 (4) ◽  
pp. 373-426 ◽  
Author(s):  
ANDREW D. GORDON ◽  
PAUL D. HANKIN ◽  
SØREN B. LASSEN
Keyword(s):  
Operational Semantics ◽  
Direct Proof ◽  
Object Oriented ◽  
Small Step ◽  
Abstract Machine ◽  
Program Equivalence ◽  
Contextual Equivalence ◽  
Object Oriented Languages

We adopt the untyped imperative object calculus of Abadi and Cardelli as a minimal setting in which to study problems of compilation and program equivalence that arise when compiling object-oriented languages. We present both a big-step and a small-step substitution-based operational semantics for the calculus. Our first two results are theorems asserting the equivalence of our substitution-based semantics with a closure-based semantics like that given by Abadi and Cardelli. Our third result is a direct proof of the correctness of compilation to a stack-based abstract machine via a small-step decompilation algorithm. Our fourth result is that contextual equivalence of objects coincides with a form of Mason and Talcott's CIU equivalence; the latter provides a tractable means of establishing operational equivalences. Finally, we prove correct an algorithm, used in our prototype compiler, for statically resolving method offsets. This is the first study of correctness of an object-oriented abstract machine, and of operational equivalence for the imperative object calculus.

scholarly journals An Investigation of Abadi and Cardelli's Untyped Calculus of Objects

2008 ◽  
Vol 15 (6) ◽  
Author(s):  
Jacob Johannsen
Keyword(s):  
Program Transformations ◽  
Small Step ◽  
Abstract Machine ◽  
Abstract Machines ◽  
Explicit Substitutions ◽  
The Relationship ◽  
Two Machines

We study the relationship between the natural (big-step) semantics and the reduction (small-step) semantics of Abadi and Cardelli's untyped calculus of objects. By applying Danvy et al.'s functional correspondence to the natural semantics, we derive an abstract machine for this calculus, and by applying Danvy et al.'s syntactic correspondence to the reduction semantics, we also derive an abstract machines for this calculus. These two abstract machines are identical. The fact that the machines are identical, and the fact that they have been derived using meaning-preserving program transformations, entail that the derivation constitutes a proof of equivalence between natural semantics and the reduction semantics. The derivational nature of our proof contrasts with Abadi and Cardelli's soundness proof, which was carried out by pen and paper. We also note that the abstract machine is new.<br /> <br />To move closer to actual language implementations, we reformulate the calculus to use explicit substitutions. The reformulated calculus is new. By applying the functional and syntactic correspondences to natural and reduction semantics of this new calculus, we again obtain two abstract machines. These two machines are also identical, and as such, they establish the equivalence of the natural semantics and the reduction semantics of the new calculus.<br /> <br />Finally, we prove that the two abstract machines are strongly bisimilar. Therefore, the two calculi are computationally equivalent.

scholarly journals Compilation and Equivalence of Imperative Objects (Revised Report)

1998 ◽  
Vol 5 (55) ◽  
Author(s):  
Andrew D. Gordon ◽  
Paul D. Hankin ◽  
Søren B. Lassen
Keyword(s):  
Operational Semantics ◽  
Direct Proof ◽  
Object Oriented ◽  
Small Step ◽  
Abstract Machine ◽  
Program Equivalence ◽  
Contextual Equivalence

We adopt the untyped imperative object calculus of Abadi and<br />Cardelli as a minimal setting in which to study problems of compilation<br />and program equivalence that arise when compiling object oriented<br />languages. We present both a big-step and a small-step<br />substitution-based operational semantics for the calculus. Our first<br />two results are theorems asserting the equivalence of our substitution based semantics with a closure-based semantics like that given by Abadi and Cardelli. Our third result is a direct proof of the correctness of compilation to a stack-based abstract machine via a small-step decompilation algorithm. Our fourth result is that contextual equivalence of objects coincides with a form of Mason and Talcott's CIU<br />equivalence; the latter provides a tractable means of establishing operational equivalences. Finally, we prove correct an algorithm, used in<br />our prototype compiler, for statically resolving method offsets. This is<br />the first study of correctness of an object-oriented abstract machine,<br />and of operational equivalence for the imperative object calculus.

scholarly journals Compilation and Equivalence of Imperative Objects

1997 ◽  
Vol 4 (19) ◽  
Author(s):  
Andrew D. Gordon ◽  
Paul D. Hankin ◽  
Søren B. Lassen
Keyword(s):  
Operational Semantics ◽  
Direct Proof ◽  
Object Oriented ◽  
Small Step ◽  
Abstract Machine ◽  
Program Equivalence ◽  
Contextual Equivalence ◽  
Object Oriented Languages

We adopt the untyped imperative object calculus of Abadi and Cardelli as a minimal setting in which to study problems of compilation and program equivalence that arise when compiling object-oriented languages. We present both a big-step and a small-step substitution-based operational semantics for the calculus and prove them equivalent to the closure-based operational semantics given by Abadi and Cardelli. Our first result is a direct proof of the correctness of compilation to a stack-based abstract machine via a small-step decompilation algorithm. Our second result is that contextual equivalence of objects coincides with a form of Mason and Talcott's CIU equivalence; the latter provides a tractable means of establishing operational equivalences. Finally, we prove correct an algorithm, used in our prototype compiler, for statically resolving method offsets. This is the first study of correctness of an object-oriented abstract machine, and of operational equivalence for the imperative object calculus.<br /><br />This report is superseded by BRICS-RS-98-55.

A specification logic for concurrent object-oriented programming

1999 ◽  
Vol 9 (3) ◽  
pp. 253-286 ◽  
Author(s):  
G. DELZANNO ◽  
D. GALMICHE ◽  
M. MARTELLI
Keyword(s):  
Logic Programming ◽  
Programming Languages ◽  
Linear Logic ◽  
Operational Semantics ◽  
Object Oriented ◽  
Object Oriented Programming ◽  
Higher Order Logic ◽  
Specification Logic ◽  
Theoretic Characterization

This paper focuses on the use of linear logic as a specification language for the operational semantics of advanced concepts of programming such as concurrency and object-orientation. Our approach is based on a refinement of linear logic sequent calculi based on the proof-theoretic characterization of logic programming. A well-founded combination of higher-order logic programming and linear logic will be used to give an accurate encoding of the traditional features of concurrent object-oriented programming languages, whose corner-stone is the notion of encapsulation.

scholarly journals Baby Modula-3 and a theory of objects

1994 ◽  
Vol 4 (2) ◽  
pp. 249-283 ◽  
Author(s):  
Martin Abadi
Keyword(s):  
Programming Language ◽  
Formal Semantics ◽  
Operational Semantics ◽  
Object Oriented ◽  
Denotational Semantics ◽  
Object Oriented Programming ◽  
The Core ◽  
Functional Object ◽  
Oriented Programming Language

AbstractBaby Modula-3 is a small, functional, object-oriented programming language. It is intended as a vehicle for explaining the core of Modula-3 from a biased perspective: Baby Modula-3 includes the main features of Modula-3 related to objects, but not much else. To the theoretician, Baby Modula-3 provides a tractable, concrete example of an object-oriented language, and we use it to study the formal semantics of objects. Baby Modula-3 is defined with a structured operational semantics and with a set of static type rules. A denotational semantics guarantees the soundness of this definition.

scholarly journals Object Cloning for Ownership Systems

2021 ◽  
Author(s):  
◽  
Paley Guangping Li
Keyword(s):  
Comparative Analysis ◽  
Programming Languages ◽  
Formal Model ◽  
Operational Semantics ◽  
Type System ◽  
Object Oriented ◽  
Object Oriented Programming ◽  
Constraint System ◽  
Existential Quantification ◽  
Ownership Types

<p>Modern object-oriented programming languages frequently need the ability to clone, duplicate, and copy objects. The usual approaches taken by languages are rudimentary, primarily because these approaches operate with little understanding of the object being cloned. Deep cloning naively copies every object that has a reachable reference path from the object being cloned, even if the objects being copied have no innate relationship with that object. For more sophisticated cloning operations, languages usually only provide the capacity for programmers to define their own cloning operations for specific objects, and with no help from the type system.  Sheep cloning is an automated operation that clones objects by leveraging information about those objects’ structures, which the programmer imparts into their programs with ownership types. Ownership types are a language mechanism that defines an owner for every object in the program. Ownership types create a hierarchical structure for the heap.  In this thesis, we construct an extensible formal model for an object-oriented language with ownership types (Core), and use it to explore different formalisms of sheep cloning. We formalise three distinct operational semantics of sheep cloning, and for each approach we include proofs or proof outlines where appropriate, and provide a comparative analysis of each model’s benefits. Our main contribution is the descripSC formal model of sheep cloning and its proof of type soundness.  The second contribution of this thesis is the formalism of Mojo-jojo, a multiple ownership system that includes existential quantification over types and context parameters, along with a constraint system for context parameters. We prove type soundness for Mojo-jojo. Multiple ownership is a mechanism which allows objects to have more than one owner. Context parameters in Mojo-jojo can use binary operators such as: intersection, union, and disjointness.</p>

scholarly journals An Operational Foundation for Delimited Continuations in the CPS Hierarchy

2004 ◽  
Vol 11 (29) ◽  
Author(s):  
Malgorzata Biernacka ◽  
Dariusz Biernacki ◽  
Olivier Danvy
Keyword(s):  
Operational Semantics ◽  
Lambda Calculus ◽  
Explicit Representation ◽  
Small Step ◽  
Abstract Machine ◽  
Delimited Continuations ◽  
New Applications ◽  
Control Operators

We present an abstract machine and a reduction semantics for the lambda-calculus extended with control operators that give access to delimited continuations in the CPS hierarchy. The abstract machine is derived from an evaluator in continuation-passing style (CPS); the reduction semantics (i.e., a small-step operational semantics with an explicit representation of evaluation contexts) is constructed from the abstract machine; and the control operators are the shift and reset family. At level n of the CPS hierarchy, programs can use the control operators shift_i and reset_i for 1 <= i <= n, the evaluator has n + 1 layers of continuations, the abstract machine has n + 1 layers of control stacks, and the reduction semantics has n + 1 layers of evaluation contexts.<br /> <br /> We also present new applications of delimited continuations in the CPS hierarchy: finding list prefixes and normalization by evaluation for a hierarchical language of units and products.

scholarly journals Formal Semantics for Java-like Languages and Research Opportunities

2018 ◽  
Vol 25 (3) ◽  
pp. 62
Author(s):  
Samuel Da Silva Feitosa ◽  
Rodrigo Geraldo Ribeiro ◽  
Andre Rauber Du Bois
Keyword(s):  
Formal Specification ◽  
Formal Semantics ◽  
Operational Semantics ◽  
Object Oriented ◽  
The State ◽  
Small Step ◽  
Research Opportunities ◽  
Type Safety ◽  
State Of Art ◽  
Object Oriented Languages

The objective of this paper is twofold: first, we discuss the state of art on Java-like semantics, focusing on those that provide formal specification using operational semantics (big-step or small-step), studying in detail the most cited projects and presenting some derivative works that extend the originals aggregating useful features. Also, we filter our research for those that provide some insights in type-safety proofs. Furthermore, we provide a comparison between the most used projects in order to show which functionalities are covered in such projects. Second, our effort is focused towards the research opportunities in this area, showing some important works that can be applied to the previously presented projects to study features of object-oriented languages, and pointing for some possibilities to explore in future researches.

Sign in / Sign up

Export Citation Format

Share Document