[e-lang] Comments requested on paper: functional purity in Joe-E

[Toby Murray]

On Wed, 2008-06-04 at 14:19 +0100, Toby Murray wrote:
> That's a seriously interesting paper. It never occurred to me how useful
> the Joe-E overlay type system could be for program verification until
> now. 

> (Am yet to read past Section 6 but might pester with more comments about
> later sections as I read them.)

Have now finished the paper; comments for remaining sections below.

Section 7.2.2

"The last received serial number was stored as a static field inside the
BallotMessage ..." -- linebreak required before "BallotMessage".

"After refactoring, the method was changed to use a ByteArray instead of
byte[]." Wouldn't the method also need to be changed to return a Ballot
object rather than a boolean and to throw an exception upon error rather
than (presumably) returning false ? 

Section 7.3.4

More linebreak failures due to \tt{} fonts on "IsEqualFilter"

"In particular, there cannot be any cycles in immutable data
structures." I don't get this.. What about

public class Bar implements Immutable{
   private Foo _foo;
   public Bar(Foo foo){
      _foo = foo;
   }
}
public class Foo implements Immutable{
   private Bar _bar;
   public Foo(){
      _bar = new Bar(this);
   }
}

Would Foo not be considered Immutable?


Overfull second-to-last line in Section 7.3.4



Again, very cool stuff. Cheers for the good read.

Toby


> On Tue, 2008-06-03 at 23:00 -0700, Adrian Mettler wrote:
> > Resending with URL instead of attachment, as it appears moderator 
> > approval isn't happening:
> > http://www.cs.berkeley.edu/~amettler/purecomp.pdf
> > 
> > -
> > 
> > David Wagner and I have recently submitted our first paper relating to
> > our work on Joe-E, an object-capability subset of Java.  It focuses on a
> > simple pattern that ensures that a method is side-effect free and
> > behaves as a deterministic function of its arguments (i.e. invocations
> > with equivalent arguments will yield equivalent return values) and how
> > this property can be used to verify security properties.  We would be
> > interested in comments from more people in order to improve the paper.
> > There's a fair amount of time before any camera ready would be due (it's
> > still a while before committee decision comes back).
> > 
> > Thanks,
> > Adrian
> > 
> > 
> > 
> > _______________________________________________
> > e-lang mailing list
> > e-lang at mail.eros-os.org
> > http://www.eros-os.org/mailman/listinfo/e-lang
> _______________________________________________
> e-lang mailing list
> e-lang at mail.eros-os.org
> http://www.eros-os.org/mailman/listinfo/e-lang