Object Cloning for Ownership Systems

<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>

Object Cloning for Ownership Systems

<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>

Encapsulation Enforcement with Dynamic Ownership

<p>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.</p>

Encapsulation Enforcement with Dynamic Ownership

<p>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.</p>

Dynamic Behaviors of a Two-Degree-of-Freedom Impact Oscillator with Two-Sided Constraints

The dynamic model of a vibroimpact system subjected to harmonic excitation with symmetric elastic constraints is investigated with analytical and numerical methods. The codimension-one bifurcation diagrams with respect to frequency of the excitation are obtained by means of the continuation technique, and the different types of bifurcations are detected, such as grazing bifurcation, saddle-node bifurcation, and period-doubling bifurcation, which predicts the complexity of the system considered. Based on the grazing phenomenon obtained, the zero-time-discontinuity mapping is extended from the single constraint system presented in the literature to the two-sided elastic constraint system discussed in this paper. The Poincare mapping of double grazing periodic motion is derived, and this compound mapping is applied to obtain the existence conditions of codimension-two grazing bifurcation point of the system. According to the deduced theoretical result, the grazing curve and the codimension-two grazing bifurcation points are validated by numerical simulation. Finally, various types of periodic-impact motions near the codimension-two grazing bifurcation point are illustrated through the unfolding diagram and phase diagrams.

ATLAS: Automated Amortised Complexity Analysis of Self-adjusting Data Structures

Being able to argue about the performance of self-adjusting data structures such as splay trees has been a main objective, when Sleator and Tarjan introduced the notion of amortised complexity.Analysing these data structures requires sophisticated potential functions, which typically contain logarithmic expressions. Possibly for these reasons, and despite the recent progress in automated resource analysis, they have so far eluded automation. In this paper, we report on the first fully-automated amortised complexity analysis of self-adjusting data structures. Following earlier work, our analysis is based on potential function templates with unknown coefficients.We make the following contributions: 1) We encode the search for concrete potential function coefficients as an optimisation problem over a suitable constraint system. Our target function steers the search towards coefficients that minimise the inferred amortised complexity. 2) Automation is achieved by using a linear constraint system in conjunction with suitable lemmata schemes that encapsulate the required non-linear facts about the logarithm. We discuss our choices that achieve a scalable analysis. 3) We present our tool $$\mathsf {ATLAS}$$ ATLAS and report on experimental results for splay trees, splay heaps and pairing heaps. We completely automatically infer complexity estimates that match previous results (obtained by sophisticated pen-and-paper proofs), and in some cases even infer better complexity estimates than previously published.

Global Rigidity of 2D Linearly Constrained Frameworks

A linearly constrained framework in $\mathbb{R}^d$ is a point configuration together with a system of constraints that fixes the distances between some pairs of points and additionally restricts some of the points to lie in given affine subspaces. It is globally rigid if the configuration is uniquely defined by the constraint system. We show that a generic linearly constrained framework in $\mathbb{R}^2$ is globally rigid if and only if it is redundantly rigid and “balanced”. For unbalanced generic frameworks, we determine the precise number of solutions to the constraint system whenever the rigidity matroid of the framework is connected. We obtain a stress matrix sufficient condition and a Hendrickson type necessary condition for a generic linearly constrained framework to be globally rigid in $\mathbb{R}^d$.

Approximate Membership Function Shapes of Solutions to Intuitionistic Fuzzy Transportation Problems

In this paper, proposing a mathematical model with disjunctive constraint system, and providing approximate membership function shapes to the optimal values of the decision variables, we improve the solution approach to transportation problems with trapezoidal fuzzy parameters. We further extend the approach to solving transportation problems with intuitionistic fuzzy parameters; and compare the membership function shapes of the fuzzy solutions obtained by our approach to the fuzzy solutions to full fuzzy transportation problems yielded by approaches found in the literature.