Object Cloning for Ownership Systems

10.26686/wgtn.17012642.v1 ◽

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

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.

Download Full-text

A specification logic for concurrent object-oriented programming

Mathematical Structures in Computer Science ◽

10.1017/s0960129599002789 ◽

1999 ◽

Vol 9 (3) ◽

pp. 253-286 ◽

Cited By ~ 4

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.

Download Full-text

Generic Ownership: a Practical Approach to Ownership and Confinement in Object-Oriented Programming Languages

10.26686/wgtn.16934452 ◽

2021 ◽

Author(s):

◽

Alex Potanin

Keyword(s):

Programming Languages ◽

Object Oriented ◽

Object Oriented Programming ◽

Minimal Extension ◽

Language Implementation ◽

The Core ◽

Simple Formalism ◽

Functional Setting ◽

Type Information ◽

Ownership Types

Modern object-oriented programming languages support many techniques that simplify the work of a programmer. Among them is generic types: the ability to create generic descriptions of algorithms and object structures that will be automatically specialised by supplying the type information when they are used. At the same time, object-oriented technologies still suffer from aliasing: the case of many objects in a program's memory referring to the same object via different references. Ownership types enforce encapsulation in object-oriented programs by ensuring that objects cannot be referred to from the outside of the object(s) that own them. Existing ownership programming languages either do not support generic types or attempt to add them on top of ownership restrictions. The goal of this work is to bring object ownership into mainstream object-oriented programming languages. This thesis presents Generic Ownership which provides perobject ownership on top of a generic imperative language. Surprisingly, the resulting system not only provides ownership guarantees comparable to the established systems, but also requires few additional language mechanisms to achieve them due to full reuse of generic types. In this thesis I formalise the core of Generic Ownership, highlighting that the restriction of this calls, owner preservation over subtyping, and appropriate owner nesting are the only necessary requirements for ownership. I describe two formalisms: (1) a simple formalism, capturing confinement in a functional setting, and (2) a complete formalism, providing a way for Generic Ownership to support both deep and shallow variations of ownership types. I support the formal work by describing how the Ownership Generic Java (OGJ) language is implemented as a minimal extension to Java 5. OGJ is the first publicly available language implementation that supports ownership, confinement, and generic types at the same time. I demonstrate OGJ in practice: show how to use OGJ to write programs and provide insights into the implementations of Generic Ownership.

Download Full-text

A paradigmatic object-oriented programming language: Design, static typing and semantics

Journal of Functional Programming ◽

10.1017/s0956796800001039 ◽

1994 ◽

Vol 4 (2) ◽

pp. 127-206 ◽

Cited By ~ 68

Author(s):

Kim B. Bruce

Keyword(s):

Fixed Points ◽

Programming Languages ◽

Programming Language ◽

Type System ◽

Object Oriented ◽

Object Oriented Programming ◽

Language Design ◽

Type Checking ◽

Basic Features ◽

Oriented Programming Language

AbstractTo illuminate the fundamental concepts involved in object-oriented programming languages, we describe the design of TOOPL, a paradigmatic, statically-typed, functional, object-oriented programming language which supports classes, objects, methods, hidden instance variables, subtypes and inheritance.It has proven to be quite difficult to design such a language which has a secure type system. A particular problem with statically type checking object-oriented languages is designing typechecking rules which ensure that methods provided in a superclass will continue to be type correct when inherited in a subclass. The type-checking rules for TOOPL have this feature, enabling library suppliers to provide only the interfaces of classes with actual executable code, while still allowing users to safely create subclasses. To achieve greater expressibility while retaining type-safety, we choose to separate the inheritance and subtyping hierarchy in the language.The design of TOOPL has been guided by an analysis of the semantics of the language, which is given in terms of a model of the F-bounded second-order lambda calculus with fixed points at both the element and type level. This semantics supports the language design by providing a means to prove that the type-checking rules are sound, thus guaranteeing that the language is type-safe.While the semantics of our language is rather complex, involving fixed points at both the element and type level, we believe that this reflects the inherent complexity of the basic features of object-oriented programming languages. Particularly complex features include the implicit recursion inherent in the use of the keyword, self, to refer to the current object, and its corresponding type, MyType. The notions of subclass and inheritance introduce the greatest semantic complexities, whereas the notion of subtype is more straightforward to deal with. Our semantic investigations lead us to recommend caution in the use of inheritance, since small changes to method definitions in subclasses can result in major changes to the meanings of the other methods of the class.

Download Full-text

Encapsulation Enforcement with Dynamic Ownership

10.26686/wgtn.16946002.v1 ◽

2021 ◽

Author(s):

◽

Donald James Gordon

Keyword(s):

Programming Languages ◽

Control Systems ◽

Object Oriented ◽

Object Oriented Programming ◽

Constraint System ◽

Dynamic Languages

Unrestricted aliasing is a problem endemic to object oriented programming. It allows notions of encapsulation fundamental to object oriented programming to be violated. This thesis describes ConstrainedJava, an implementation of a language that provides alias control via a much stronger encapsulation guarantees than traditional object-oriented programming languages, integrated with a constraint system. Unlike most existing aliasing control systems, this encapsulation system integrates well with untyped dynamic languages such as ConstrainedJava. This stronger form of encapsulation has been enhanced to make it easier to write practical programs while still providing useful encapsulation guarantees.

Download Full-text

Inheritance in Programming Languages

Encyclopedia of Information Science and Technology, Second Edition ◽

10.4018/978-1-60566-026-4.ch321 ◽

2011 ◽

pp. 2042-2047

Author(s):

Krishnaprasad Thirunarayan

Keyword(s):

Programming Languages ◽

Common Sense ◽

Effective Means ◽

Type System ◽

Object Oriented ◽

Object Oriented Programming ◽

Multiple Inheritance ◽

Contrast Method ◽

Compare And Contrast ◽

Object Oriented Databases

Inheritance is a powerful concept employed in computer science, especially in artificial intelligence (AI), object-oriented programming (OOP), and object-oriented databases (OODB). In the field of AI, inheritance has been primarily used as a concise and effective means of representing and reasoning with common-sense knowledge (Thirunarayan, 1995). In programming languages and databases, inheritance has been used for the purpose of sharing data and methods, and for enabling modularity of software (re)use and maintenance (Lakshmanan & Thirunarayan, 1998). In this chapter, we present various design choices for incorporating inheritance into programming languages from an application programmer’s perspective. In contrast with the language of mathematics, which is mature and well-understood, the embodiment of object-oriented concepts and constructs in a concrete programming language is neither fixed nor universally accepted. We exhibit programs with similar syntax in different languages that have very different semantics, and different looking programs that are equivalent. We compare and contrast method inheritance, interaction of type system with method binding, constructs for method redefinition, and their implementation in widely used languages such as C++ (Stroustrup, 1997), Java (Arnold, Gosling, & Holmes, 2005), and C# (Hejlsberg, Wiltamuth, & Golde, 2006), to illustrate subtle issues of interest to programmers. Finally, we discuss multiple inheritance briefly.

Download Full-text

Generic Ownership: a Practical Approach to Ownership and Confinement in Object-Oriented Programming Languages

10.26686/wgtn.16934452.v1 ◽

2021 ◽

Author(s):

◽

Alex Potanin

Keyword(s):

Programming Languages ◽

Object Oriented ◽

Object Oriented Programming ◽

Minimal Extension ◽

Language Implementation ◽

The Core ◽

Simple Formalism ◽

Functional Setting ◽

Type Information ◽

Ownership Types

Modern object-oriented programming languages support many techniques that simplify the work of a programmer. Among them is generic types: the ability to create generic descriptions of algorithms and object structures that will be automatically specialised by supplying the type information when they are used. At the same time, object-oriented technologies still suffer from aliasing: the case of many objects in a program's memory referring to the same object via different references. Ownership types enforce encapsulation in object-oriented programs by ensuring that objects cannot be referred to from the outside of the object(s) that own them. Existing ownership programming languages either do not support generic types or attempt to add them on top of ownership restrictions. The goal of this work is to bring object ownership into mainstream object-oriented programming languages. This thesis presents Generic Ownership which provides perobject ownership on top of a generic imperative language. Surprisingly, the resulting system not only provides ownership guarantees comparable to the established systems, but also requires few additional language mechanisms to achieve them due to full reuse of generic types. In this thesis I formalise the core of Generic Ownership, highlighting that the restriction of this calls, owner preservation over subtyping, and appropriate owner nesting are the only necessary requirements for ownership. I describe two formalisms: (1) a simple formalism, capturing confinement in a functional setting, and (2) a complete formalism, providing a way for Generic Ownership to support both deep and shallow variations of ownership types. I support the formal work by describing how the Ownership Generic Java (OGJ) language is implemented as a minimal extension to Java 5. OGJ is the first publicly available language implementation that supports ownership, confinement, and generic types at the same time. I demonstrate OGJ in practice: show how to use OGJ to write programs and provide insights into the implementations of Generic Ownership.

Download Full-text

Encapsulation Enforcement with Dynamic Ownership

10.26686/wgtn.16946002 ◽

2021 ◽

Author(s):

◽

Donald James Gordon

Keyword(s):

Programming Languages ◽

Control Systems ◽

Object Oriented ◽

Object Oriented Programming ◽

Constraint System ◽

Dynamic Languages

Unrestricted aliasing is a problem endemic to object oriented programming. It allows notions of encapsulation fundamental to object oriented programming to be violated. This thesis describes ConstrainedJava, an implementation of a language that provides alias control via a much stronger encapsulation guarantees than traditional object-oriented programming languages, integrated with a constraint system. Unlike most existing aliasing control systems, this encapsulation system integrates well with untyped dynamic languages such as ConstrainedJava. This stronger form of encapsulation has been enhanced to make it easier to write practical programs while still providing useful encapsulation guarantees.

Download Full-text