Context
We are working on a static verifier for Scala programs (early work described in this Master's thesis), and the current focus lies on verifying Scala features that involve lazy evaluation. We are mainly interested in the semantics (behaviour) of the features, not in other (nevertheless important) aspects such as comprehensibility or conciseness.
To simplify things, we - for the time being - ignore special roles that singleton objects could have. For example, that some are companion objects (which is probably orthogonal w.r.t. to their lazy nature), or that some are package objects.
Properties of lazy vals and singleton objects
Lazy vals
Assume a lazy val
lazy val v = I
where I is the initialiser block, i.e., the code that determines the value of the lazy val. The initialiser block I is executed when the lazy val v is dereferenced for the first time.
Singleton objects
Assume a singleton object
object Foo {
C1
val v1 = I1
var v2 = I2
lazy val v3 = I3
def m() {C2}
}
where C1 is the code making up the constructor of object Foo, where I1 to I3 are again initialiser blocks, and where C2 is the body of method m. When the object Foo is first used (dereferenced, or assigned to a variable/field), then C1, I1 and I2 are executed. I3 is only executed when Foo.v3 is dereferenced (since v3 is a lazy val) and C2 is executed whenever m is called.
Question
Consider this version of Foo, where the singleton object has been encoded by a lazy val and an anonymous class:
// Should probably sit in a package object
lazy val Foo = new {
C1
val v1 = I1
var v2 = I2
lazy val v3 = I3
def m() {C2}
}
Can anybody think of a reason for why the encoding of the singleton object Foo as a lazy val would show a different behaviour than the original singleton object? That is, are there (corner) cases where the encoded version would have a different semantics than the original code?