/// #invariant {:msg "the variable x is 0"} x == 0;
// Good, x holds in the beginning
function example_observability() {
// x is still 0 if x was zero
// x is still zero if x was zero, great!
function example_violation() {
// x is not zero anymore 😢
// now the invariant is violated
function example_nonviolation() {
// Now x is non zero, but that doesn't matter. We're not "observable".
// We immediately return x back to what it was
// x is back to zero again (if it was zero before)!
function example_external(address externalContract) {
// Now x is non zero. Which violates the invariant.
// externalContract might call back into us, assuming that the invariant holds
// If externalContract calls this.example_observability(), expecting all invariants to hold.
// Unfortunately, x is not 0. example_observability()'s assumption is violated.