LARA

This is an old revision of the document!


Semantics of Field Reads and Writes

How to model $x.f$ ?

How to model field assignment $x.f=y$ ?

What about null pointer checks?

Examples:

y = x.next.next
x.next.next.prev = y
(x = null | x.next == y)

Statement simplification.

Short-circuit evaluation.

Type and definition sketch of a recursive (Scala) function that simplifies expressions and statements.