Inhaling and exhaling

Permissions can be added to the verification state by inhaling, and removed by exhaling. This can be useful for debugging but should not be needed for normal verification purposes.

Removing permissions with exhale

The statement exhale ASSERTION

  1. checks that all value constraints in ASSERTION hold, otherwise an error is reported.
  2. checks that all permissions mentioned by ASSERTION are held, otherwise an error is reported.
  3. removes all permissions mentioned by ASSERTION

Exhale is similar to assert, with the difference that assert does not remove any permissions:

requires acc(x, 1)
func breatheOut(x *int) {
	assert acc(x, 1)
	exhale acc(x, 1/4)
	assert acc(x, 3/4)
	assert acc(x, 3/4) // no permission removed
	exhale acc(x, 1) // error
}

ERROR Exhale might fail. 
Permission to x might not suffice.

The last exhale failed since at this point only a permission amount of 3/4 is held.

Adding permissions with inhale

The statement inhale ASSERTION

  1. adds all permissions mentioned by ASSERTION
  2. assumes all value constraints in ASSERTION hold
Inhaling can result in an inconsistent state. Do not use it without a good reason, except for debugging and learning. 
requires acc(x, 1/2)
func breatheIn(x *int) {
	assert acc(x, 1/2)
	inhale acc(x, 1/2)
	assert acc(x, 1/1)
}

By inhaling a permission amount of 1 for the pointer x while already holding acc(x, 1/2), we reach an inconsistent state, and false can be asserted:

requires acc(x, 1/2)
func breatheMore(x *int) {
	inhale acc(x, 1)
	assert acc(x, 3/2)
	assert false
}