HOME - ABOUT JOT - LETTERS - CONTACT US - INFORMATION FOR AUTHORS
Book Reviews
Product Reviews
Earlier Issues


SEARCH


Subscribe to
JOT's newsletter

O-O NEWS &
EVENTS











 

CONTENTS

PDF


Editorial


PDF

Write a letter to the editor

 
REFEREED ARTICLES


Inspector Methods for State Abstraction
By Bart Jacobs and Frank Piessens



PDF

This paper proposes an approach, based on the Boogie methodology, to the verification of programs that use inspector methods in method contracts and object invariants, to support state abstraction in specifications. However, performing state abstraction in a programming language that allows aliasing through object references poses a framing problem, which is solved thanks to a novel logical encoding of the heap, without breaking information hiding.

Modelling a JVM for polymorphic bytecode
By Giovanni Lagorio

PDF

The paper analyzes how polymorphic bytecode can be dynamically linked by presenting a deterministic model of a Java Virtual Machine which interleaves loading and linking steps with execution. In this model, loading and execution phases are basically standard, whereas verification handles also type constraints, which are part of polymorphic bytecode, and resolution blends in verification.

A Parameterized Type System for Simple Loose Ownership Domains
By Jan Schaefer and Arnd Poetzsch-Heffter

PDF

This paper develops so-called loose domains which abstract over several precise domains in order to overcome the limitations of expressiveness of ownership domains. Furthermore, ownership domains are simplified by reducing the number of domains per object to two and hard-wiring the access permissions between domains. The resulting type system is formalized for anOO core language and proofs of type soundness and of a fundamental accessibility property are provided.

OUTLOOK


A brief outlook to the next issue



PDF


 

Editor-in-Chief: Richard Wiener rsw@runbox.com
  ISSN 1660-1769

JOT is published by
the Chair of Software Engineering

the ETH Zürich