The idea of using a rational number to express permissions to access a
reference dates back to the type system of fractional
permissions by Boyland [1]}. His work used
fractional permissions to verify race freedom of a concurrent program
without a may-alias analysis. Later,
Terauchi [2]} proposed a type-inference
algorithm that reduces typing constraints to a set of linear
inequalities over rational numbers. Boyland's idea also inspired a
variant of separation logic for a concurrent programming
language [3]} to express sharing of read
permissions among several threads. Our previous
work [4]}, [5]}, inspired by that
in [2]}, [3]}, proposed methods for type-based
verification of resource-leak freedom, in which a rational number
expresses an obligation to deallocate certain resource, not
just a permission.
