Quantified variables are not treated as bound (cannot be reused in same scope) about silver HOT 4 CLOSED

Bitbucket user Korbinian Breu commented on 2014-01-18 13:46

I just created a pull request that solves this issue - however, there may be more work to do, because apparently scopes are not built to be nested?

The following gives no error:

#!scala
method k(S:Seq[Ref]) {
    while(true) {
        var bla:Int
    }

    assume bla == 5
}

from silver.

@alexanderjsummers commented on 2014-01-20 13:11

Thanks for the fix - that's great!

We don't really have block scopes in SIL; the program that you wrote above is treated analogously to

#!scala

method k(S:Seq[Ref]) {
    var bla:Int
    while(true) {

    }

    assume bla == 5
}

In particular, if one "declares" a local variable with the same name in the two branches of an if-conditional (or in nested blocks), then an error is expected. This is a bit confusing, but we didn't want scopes built-in, and forcing all declarations to be at the start of the method body can be a bit annoying if the method gets large...

from silver.

@alexanderjsummers commented on 2014-01-22 13:16

Fixed in commit c206a59

from silver.

@alexanderjsummers on 2014-01-22 13:16:

• changed state from new to resolved

from silver.