ECOOP

Coinductive abstract compilation is a novel technique, which has been recently introduced, for defining precise type systems for object-oriented languages. In this approach, type inference consists in translating the program to be analyzed into a Horn ...

Wildcard types enrich the types expressible in Java, and extend the set of typeable Java programs. Syntactic models and proofs of soundness for type systems related to Java wildcards have been suggested in the past, however, the semantics of wildcards ...

"Exception-safety strong guarantee: The operation has either completed successfully or thrown an exception, leaving the program state exactly as it was before the operation started." David Abrahams [1] The above definition of strong exception-safety ...

We present a separation logic specification and verification of linked lists with views, a data structure from the C5 collection library for C#. A view is a generalization of the well-known concept of an iterator. Linked lists with views form an ...

This paper describes a novel technique for fully automated procedure-modular verification of Java programs equipped with method-local and global assertions that specify safety properties of sequences of method invocations. Modularity of verification is ...

In this paper we present prototype tool-support for the runtime assertion checking of the Java Modeling Language (JML) extended with communication histories specified by attribute grammars. Our tool suite integrates Rascal, a meta programming language ...

Tracking the state of an object (in the sense of how a File can be in an Open or Closed state) is difficult not just because of the problem of managing state transitions but also due to the complexity introduced by aliasing. Unchecked duplication of ...

Refactoring transformations are important for productivity and quality in software evolution. Modular reasoning about semantics preserving transformations is difficult even in typed class-based languages because transformations can change the internal ...

Engineers in many disciplines use state machines to reason about system changes, and many object-oriented libraries require their clients to follow state machine protocols. No existing language, however, has native support for state machines, and ...