#9 VC Enumeration

[Juan Pablo Galeotti]

Given a Java code, different verification conditions emerge:

For instance:

/**
* @ensures \result>0
*/
int m(C o) {
if (o.f > 0)
...
}

Generates two different VC:

1. Is o.f safe?
2. Assuming o.f is safe, is postcondition ensured?

These VC's allows two different translations and anlysis.