[Pl-seminar] PL seminar schedule

[Aaron Turon]

NEU Programming Languages Seminar presents

Derek Rayside
MIT

Wednesday, December 9, 2009
11:45-1:30
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Title:  Satisfying the Object Contract with Declarative Abstraction Functions

Abstract:

We use declarative specifications of abstraction functions to
synthesize object equality and hashing methods.  These methods are
required to satisfy the Object Contract.  It is well known that
programmers using conventional techniques have difficulty satisfying
this contract.  Our empirical results show that using our declarative
technique leads to shorter programs that are correct by construction,
while still retaining acceptable performance.

Our abstraction functions are written in a variant of the Alloy
specification language.  We have developed three strategies for
evaluating these abstraction functions at runtime, at different points
on the trade-off curve between generality and speed.  The strategy
with the shortest execution times involves a static analysis of the
abstraction function to derive desired data structure invariants; a
model-checker is used to verify that these desired invariants are true
of the program; this knowledge is used to synthesize more efficient
code.