Author name cluster

Ran Rinat

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

2 papers

1 author row

I&C Journal 2002 Journal Article

Type-Safe Covariant Specialization with Generalized Matching

Ran Rinat

Matching is a relation between object types originally designed to support type-safe subclassing with binary methods. In this paper we generalize it to deal with general covariance by allowing field and method parameter types to change covariantly in matching types. In addition, object types may explicitly contain virtual types which can also change covariantly. The result is a significant increase in the flexibility of subclassing. The new definition is accompanied by appropriate machinery, allowing the loss of subsumption to be compensated by match-bounded parameterization and hash types. We define a language LGM supporting generalized matching, its typing rules, and its operational semantics and establish a subject reduction theorem showing the soundness of the system.

Details DOI

I&C Journal 1988 Journal Article

Infinite trees, markings, and well-foundedness

Ran Rinat
Nissim Francez
Orna Grumberg

A necessary and sufficient condition for a given marked tree to have no infinite paths satisfying a given formula is presented. The formulas are taken from a language introduced by Harel, covering a wide scale of properties of infinite paths, including most of the known notions of fairness. This condition underlies a proof rule for proving that a nondeterministic program has no infinite computations satisfying a given formula, interpreted over state sequences. We also show two different forms of seemingly more natural necessary and sufficient conditions to be inadequate.

Details DOI