Thanks, yes this will all be true of my heap invar...

2010-04-16T10:23:22.204-04:00

Thanks, yes this will all be true of my heap invariant, since at it's core my language is Java-like. But my heap invariant will preserve additional properties as well (e.g., the locks that are currently held, the abstract state an object is in) because of the additional properties our type system enforces.

Thanks!

If you define a heap as a mapping from addresses t...

2010-04-14T01:24:11.739-04:00

If you define a heap as a mapping from addresses to expressions (or values), then a well-typed heap is a heap that is associated with a mapping from addresses to types, where each value at an address has the corresponding type in the "heap typing".

Your preservation proof should state that the resulting heap after the step has the same "heap tying" or has a "heap typing" that is an extension of the previous one.

Comments on Blogface.org: Proof of Soundness for a Typestate Checker with Lo...

Thanks, yes this will all be true of my heap invar...

If you define a heap as a mapping from addresses t...